A type system for PSPACE derived from light linear logic

Details A type system for PSPACE derived from light linear logic A type system for PSPACE derived from light linear logic

2012-01-05

arxiv.org/abs/1201.1122v1

EPTCS 75, 2012, pp. 33-46

Computer Science

Computational Complexity

In Proceedings DICE 2011, arXiv:1201.0345

Scientific paper

10.4204/EPTCS.75.4

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.

Affiliated with

Also associated with

No associations

Rating

A type system for PSPACE derived from light linear logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A type system for PSPACE derived from light linear logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A type system for PSPACE derived from light linear logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-609581