P-time Completeness of Light Linear Logic and its Nondeterministic Extension

TL;DR

This paper corrects and completes the encoding of Turing machines in Light Linear Logic, demonstrates its usefulness, and extends the logic to a nondeterministic version that remains NP-complete.

Contribution

It provides a working encoding in Light Linear Logic and introduces a nondeterministic extension with NP-completeness results.

Findings

Corrected encoding of Turing machines in Light Linear Logic

Demonstrated the usefulness of additive connectives

Extended Light Linear Logic to a nondeterministic system with NP-completeness

Abstract

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.