The operator pinned: PSPACE = NL.exp

The check on DescriptiveComplexity.ComplexityClass.exp at the one level where this library independently knows the answer, in both directions. DescriptiveComplexity.PSPACE_subset_NL_exp is the easy half: an DescriptiveComplexity.SOTCSpec is the graph REACH reads on the expansion whose points are its states. This file closes the converse, so that the operator is pinned rather than merely bounded.

The route

Nondeterministic logarithmic space read over an expanded universe is machine space, and the machine is the one the library already captures (DescriptiveComplexity.tcDefinable_iff_automaton): a finite control with k two-way heads, each holding one point of the expansion. Three steps:

1. the walk witnessing Q ∈ NL is carried to the trivialized expansion (DescriptiveComplexity.ExpExpansion.relSpec), where every tagged assignment is a point and the old universe survives as a mark – so that a head's succ is the plain binary increment and never has to skip anything;
2. that walk is compiled into a two-way multi-head automaton (DescriptiveComplexity.accepts_drvP), whose tests are quantifier-free by fiat;
3. the automaton is simulated by a walk over the base (DescriptiveComplexity.ExpExpansion.autoSpec), a configuration being one assignment of one block.

Nothing in the chain evaluates a quantifier ranging over the expanded universe, which is exactly the obstruction the translation lemma names.

What is and is not a corollary

LOGSPACE.exp ⊆ PSPACE follows by monotonicity. The reverse inclusion does not: DescriptiveComplexity.SOTCDefinable.expDefinable draws the graph of a walk and then asks REACH of it, and REACH is not known to this library to be in DescriptiveComplexity.LOGSPACE. LOGSPACE.exp = PSPACE would need the walk of the expansion to be functional – a deterministic reachability argument, i.e., Savitch read one exponential up – and is not claimed here.

theorem DescriptiveComplexity.NL_exp_subset_PSPACE : NL.exp ⊆ PSPACE

NL.exp ⊆ PSPACE: a problem that nondeterministic logarithmic space decides over an exponentially larger definable universe is decided by a polynomial-space walk over the base. The machine of the expansion holds k of its points, a point is an assignment of a block, so a configuration of that machine is one assignment of one block – a state of an DescriptiveComplexity.SOTCSpec.

theorem DescriptiveComplexity.PSPACE_eq_NL_exp : PSPACE = NL.exp

PSPACE = NL.exp: polynomial space is nondeterministic logarithmic space read one exponential up. Both inclusions are theorems – the easy one is DescriptiveComplexity.PSPACE_subset_NL_exp – so the exponential operator is pinned at this level, not merely bounded.

theorem DescriptiveComplexity.LOGSPACE_exp_subset_PSPACE : LOGSPACE.exp ⊆ PSPACE

LOGSPACE.exp ⊆ PSPACE, by monotonicity. The reverse inclusion is not claimed; see the module docstring.

theorem DescriptiveComplexity.NL_exp_eq_PSPACE : NL.exp = PSPACE

NL.exp ⊆ EXPTIME sharpened: read through the gate, the inclusion DescriptiveComplexity.NL_exp_subset_EXPTIME is just PSPACE ⊆ EXPTIME.