Choiceless Polynomial Space

TL;DR

This paper introduces deterministic PSPACE-bounded Abstract State Machines and proves they cannot capture the entire PSPACE complexity class, extending previous work on PTIME-bounded ASMs and choiceless computation.

Contribution

It extends the characterization of choiceless computation from PTIME to PSPACE by defining and analyzing deterministic PSPACE-bounded ASMs.

Findings

Deterministic PSPACE-bounded ASMs do not capture PSPACE.

Characterization via partial fixed-point formulae over the Stark/Nanchen logic.

Construction of transitive structures demonstrating the limitations.

Abstract

Abstract State Machines (ASMs) provide a model of computations on structures rather than strings. Blass, Gurevich and Shelah showed that deterministic PTIME-bounded ASMs define the choiceless fragment of PTIME, but cannot capture PTIME. In this article deterministic PSPACE-bounded ASMs are introduced, and it is proven that they cannot capture PSPACE. The key for the proof is a characterisation by partial fixed-point formulae over the St\"ark/Nanchen logic for deterministic ASMs and a construction of transitive structures, in which such formulae must hold. This construction exploits that the decisive support theorem for choiceless polynomial time holds under slightly weaker assumptions.