2004/10/15 by Satoshi Matsuoka, Matsuoka, Satoshi
Computer Science · #Computability, Logic, AI Algorithms #Logic, programming, and type systems #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.cs/0410034
arxiv created 2004/10/18 · arxiv updated 2009/12/01
In CSL'99 Roversi pointed out that the Turing machine encoding of Girard's seminal paper "Light Linear Logic" has a flaw. Moreover he presented a working version of the encoding in Light Affine Logic, but not in Light Linear Logic. In this paper we present a working version of the encoding in Light Linear Logic. The idea of the encoding is based on a remark of Girard's tutorial paper on Linear Logic. The encoding is also an example which shows usefulness of additive connectives. Moreover we also consider a nondeterministic extension of Light Linear Logic. We show that the extended system is NP-complete in the same meaning as P-completeness of Light Linear Logic.