Alternating machine acceptance in bounded space, as a decision problem

EXPTIME's complete problem: an alternating Turing machine is data in an instance, and

does this machine accept its input, with the tape indexed by the positions and no bound whatever on the length of a play?

is DescriptiveComplexity.ATMAcceptSpace, an ordinary iso-invariant problem of the catalog. It stands to DescriptiveComplexity.ATMAccept exactly as DescriptiveComplexity.DTMAcceptSpace stands to DescriptiveComplexity.DTMAccept: the step bound is dropped and the space stays bounded by construction.

Two differences from the polynomial-hierarchy problem, both of them relaxations:

• the vocabulary is FirstOrder.Language.turingAlt 2 – two marks, one per player – and the promise folded into the yes-instances is only that they split the states (DescriptiveComplexity.ATMData.BlocksSplit), not DescriptiveComplexity.ATMData.BlocksWellFormed, whose ordering clause is what bounds the number of alternations. Here the alternation is unbounded, which is the whole point;
• acceptance is DescriptiveComplexity.ATMData.AltAcceptsSpace, the least fixed point of the game operator rather than a budgeted recursion.

Isomorphism-invariance is proved from the two agreements an isomorphism supplies – one per direction – so that only the forward transport lemmas of DescriptiveComplexity.MachinesAltSpace are needed and no finiteness is assumed.

The problem

def DescriptiveComplexity.ATMAcceptSpace : DecisionProblem (FirstOrder.Language.turingAlt 2)

Alternating acceptance in bounded space: the machine is well formed, its two marks split the states, and the existential player wins the game on the configuration graph from some initial configuration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.atmAcceptSpace_holds_iff (A : Type) [(FirstOrder.Language.turingAlt 2).Structure A] : ATMAcceptSpace.Holds A ↔ (atmData 2 A).WellFormed ∧ (atmData 2 A).BlocksSplit ∧ (atmData 2 A).AltAcceptsSpace true