A type system for PSPACE derived from light linear logic

TL;DR

This paper introduces DLALB, a polymorphic type system for lambda calculus that characterizes PSPACE by extending light linear logic with booleans and conditionals, ensuring programs run in polynomial space.

Contribution

It extends dual light affine logic with booleans and conditionals to characterize PSPACE, bridging the gap between FPTIME and PSPACE in type systems.

Findings

Well-typed programs in DLALB run in polynomial space.

DLALB can represent all PSPACE decision functions.

DLALB characterizes PSPACE predicates.

Abstract

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.