A type system for PSPACE derived from light linear logic

Lucien Capdevielle
(ENS de Lyon)

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial space: dual light affine logic with booleans (DLALB).

To build DLALB we start from DLAL (which has a simple type language with a linear and an intuitionistic type arrow, as well as one modality) which characterizes FPTIME functions. In order to extend its expressiveness we add two boolean constants and a conditional constructor in the same way as with the system STAB.

We show that the value of a well-typed term can be computed by an alternating machine in polynomial time, thus such a term represents a program of PSPACE (given that PSPACE = APTIME).

We also prove that all polynomial space decision functions can be represented in DLALB.

Therefore DLALB characterizes PSPACE predicates.

In Jean-Yves Marion: Proceedings Second Workshop on Developments in Implicit Computational Complexity (DICE 2011), Saarbrücken, Germany, April 2nd and 3rd, 2011, Electronic Proceedings in Theoretical Computer Science 75, pp. 33–46.
Published: 1st January 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.75.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org