LINEAR LOGIC AS A LOGIC OF COMPUTATIONS

The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the linear implication -., the tensor product X, and the modal storage operator !. We give a complete computational interpretation for the !-Horn fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known 'or'-like connective +, and, for the sake of the computational duality, we introduce a new 'and'-like connective @. For!-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the (!, +)-Horn fragment of Linear Logic, which uses only positive literals, the linear implication -., ''the tensor product X, the modal storage operator!, and the additive 'disjunction' +, we prove that standard Minsky machines [21] can be directly encoded in this (!, +)-Horn fragment. Standard Minsky machines can be directly encoded in the corresponding 'dual' (!, @)-Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable.