Linear logic as a logic of computations (Q1326780): Difference between revisions

The author gives a complete computational interpretation of several initial fragments of linear logic and, based on this interpretation, establishes precisely the complexity level of these fragments. He begins with the !-Horn fragment of linear logic, which uses only positive literals, the linear implication, the tensor product \(\otimes\) and the modal storage operator !. He gives a complete computational interpretation for the !-Horn fragment of linear logic and for some natural generalizations of it formed by introducing additive connectives. He considers the `or'-like connective \(\oplus\), and, for the sake of computational duality, he introduces a new `and'-like connective \(\@\). The complete computational characterization is used to establish exactly the complexity level of all these initial fragments of linear logic in question. As known from the literature, linear logic provides us with a natural encoding of Petri net problems. The author demonstrates that the derivability problem for the !-Horn fragment of linear logic is exactly equivalent to the reachability problem for Petri nets. Next, the author shows that the expressive power of the \((!,\@)\)-Horn fragment of linear logic is of the highest possible order, by encoding standard many-counter machines into this fragment. The same encoding provides direct simulation of standard Minsky machines in the \((!,\oplus)\)-Horn fragment of linear logic, as well. As a corollary, both the \((!,\oplus)\)-Horn and \((!,\@)\)-Horn fragments of linear logic are proved to be undecidable. In his concluding remarks, the author notes that the storage operator ! turns out to be an extremely powerful tool even in the simplest case, the Horn one: (1) The storage operator ! (together with the multiplicatives) is already sufficient for describing dynamic behaviour of such complicated systems as Petri nets; (2) while combining the storage operator ! with the additives allows direct simulation of arbitrary computations of many-counter Minsky machines.