Choiceless Polynomial Space

TL;DR

This work defines Choiceless Polynomial Space ($CPS$) as the PSPACE analogue of Choiceless Polynomial Time (CPT) using deterministic PSPACE-bounded ASMs. It develops a partial fixed-point characterization over the Stärk/Nanchen logic for deterministic ASMs and leverages a transitive-structure construction together with a weakened Support Theorem to relate computations to $FO[PFP]$ on active objects. The main result is that $CPS$ cannot capture $PSPACE$ (in particular, parity is not separable by $CPS$), though $CPS$ does subsume CPT and can capture PSPACE on ordered structures via a simple deterministic simulation of nondeterminism. These findings clarify the expressive limits of choiceless logics for space-bounded computation and highlight directions for future work, including potential counting extensions and separations under arbitrary input signatures.

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ärk/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.

Theorems & Definitions (13)

• theorem 1: Fixed-Point Theorem
• proof
• theorem 2: Support Theorem
• lemma 1
• proof
• lemma 2
• lemma 3
• lemma 4
• lemma 5
• lemma 6