An Implicit Characterization of PSPACE

We present a type system for an extension of lambda calculus with a conditional construction, named STA B , that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont’s Soft Linear Logic and characterizing the PTIME class....

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2012-04, Vol.13 (2), p.1-36
Main Authors: Gaboardi, Marco, Marion, Jean-Yves, Ronchi Della Rocca, Simona
Format: Article
Language:English
Subjects:
Additives
Computer Science
Logic in Computer Science
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a type system for an extension of lambda calculus with a conditional construction, named STA B , that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont’s Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for Booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STA B is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.
ISSN:1529-3785
1557-945X
DOI:10.1145/2159531.2159540