Alternating machines in bounded space

The fourth acceptance notion of DescriptiveComplexity.TMData, and the one that reaches EXPTIME: an alternating machine whose tape is indexed by the positions, with no bound on the length of a play and no bound on the number of alternations. It stands to DescriptiveComplexity.ATMData.AltAccepts exactly as DescriptiveComplexity.TMData.AcceptsSpace stands to DescriptiveComplexity.TMData.Accepts: the step budget is dropped, the space stays bounded by construction, and what changes is that a play no longer fits inside the structure.

Winning, as an inductive predicate

DescriptiveComplexity.ATMData.AltAcc recurses on a budget, which is what makes it a Lean-level recursion rather than a fixed point. With the budget gone the right presentation is the least fixed point of the game operator, and in Lean that is an inductive predicate (DescriptiveComplexity.ATMData.AltWin): an accepting state wins; an existential configuration wins when some successor does; a universal one when it has a successor and every successor wins. Looping therefore loses, which is the standard convention and the one that agrees with the budgeted definition (DescriptiveComplexity.ATMData.altWin_iff_exists_altAcc).

Being an inductive rather than a ∃ n also makes the correspondence with the AND/OR game of alternating reachability a matter of matching constructors, which is what the EXPTIME membership proof consumes.

Unbounded alternation, at no cost

DescriptiveComplexity.ATMData.BlocksWellFormed is what bounds the number of alternations, by forbidding a transition from lowering the block index; it is not imposed here. What is imposed instead is only that the marks partition the states in two (DescriptiveComplexity.ATMData.BlocksSplit), so that block 0 is the existential player and block 1 the universal one (DescriptiveComplexity.ATMData.isUniv_true_iff_blk_one). No second machine record is needed and no lemma of DescriptiveComplexity.MachinesAlt has to be restated: the vocabulary is FirstOrder.Language.turingAlt 2 unchanged.

def DescriptiveComplexity.Config.equivProd (A : Type) : Config A ≃ A × A × (A → A)

A configuration is a state, a head position and a tape, and nothing else.

Equations

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

instance DescriptiveComplexity.Config.instFinite {A : Type} [Finite A] : Finite (Config A)

Winning the game on the configuration graph

inductive DescriptiveComplexity.ATMData.AltWin {A : Type} (M : ATMData A) (start : Bool) : Config A → Prop

Winning the alternating game, with no bound on the length of a play: an accepting state wins; an existential configuration wins when some successor does; a universal one wins when it has a successor and every successor wins.

Being a least fixed point, this makes an infinite play a loss for the existential player – the standard convention, and the one the budgeted DescriptiveComplexity.ATMData.AltAcc already has.

• acc {A : Type} {M : ATMData A} {start : Bool} {c : Config A} : M.Acc c.state → M.AltWin start c

  An accepting state wins outright.

• ex {A : Type} {M : ATMData A} {start : Bool} {c c' : Config A} : ¬M.IsUniv start c.state → M.Step c c' → M.AltWin start c' → M.AltWin start c

  An existential configuration wins when some successor does.

• all {A : Type} {M : ATMData A} {start : Bool} {c : Config A} : M.IsUniv start c.state → (∃ (c' : Config A), M.Step c c') → (∀ (c' : Config A), M.Step c c' → M.AltWin start c') → M.AltWin start c

  A universal configuration wins when it has a successor and every successor wins.

def DescriptiveComplexity.ATMData.AltAcceptsSpace {A : Type} (M : ATMData A) (start : Bool) : Prop

Acceptance in bounded space: an initial configuration wins, the choice of that configuration belonging to the player who moves first – exactly as in DescriptiveComplexity.ATMData.AltAccepts, and for the same reason.

Equations

• M.AltAcceptsSpace start = DescriptiveComplexity.guardQ start (fun (c₀ : DescriptiveComplexity.Config A) => M.IsInit c₀) fun (c₀ : DescriptiveComplexity.Config A) => M.AltWin start c₀

The budgeted definition, unbounded

theorem DescriptiveComplexity.ATMData.altWin_iff_exists_altAcc {A : Type} {M : ATMData A} [Finite A] {start : Bool} {c : Config A} : M.AltWin start c ↔ ∃ (n : ℕ), M.AltAcc start n c

The two presentations agree: winning is accepting within some budget. Over a finite configuration space the budgeted recursion of DescriptiveComplexity.ATMData.AltAcc computes the least fixed point, one stage at a time.

With no universal state the model is the nondeterministic one

theorem DescriptiveComplexity.ATMData.altAcceptsSpace_true_iff_acceptsSpace {A : Type} {M : ATMData A} (hex : ∀ (q : A), ¬M.IsUniv true q) : M.AltAcceptsSpace true ↔ M.AcceptsSpace

Acceptance in bounded space, without a universal state, is acceptance in bounded space of the underlying machine.

Two blocks are a bipartition of the states

def DescriptiveComplexity.ATMData.BlocksSplit {A : Type} (M : ATMData A) : Prop

The marks split the states in two. This is all the block discipline an unbounded alternation needs: no state carries a mark above 1, and every state carries exactly one of the two. DescriptiveComplexity.ATMData.BlocksWellFormed is deliberately not required – its ordering clause is what bounds the number of alternations.

Equations

• M.BlocksSplit = ∀ (q : A), ∃ j < 2, M.Blk j q ∧ ∀ (j' : ℕ), M.Blk j' q → j' = j

theorem DescriptiveComplexity.ATMData.isUniv_true_iff_blk_one {A : Type} {M : ATMData A} (hsplit : M.BlocksSplit) (q : A) : M.IsUniv true q ↔ M.Blk 1 q

Block 1 is the universal player. With the marks split in two, the polarity bookkeeping of DescriptiveComplexity.blockPol collapses to a single mark, so the model reads as an ordinary alternating machine with an existential and a universal set of states.

Transport along an equivalence of universes

theorem DescriptiveComplexity.ATMData.AltAgree.altAcceptsSpace_mp {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (start : Bool) : N.AltAcceptsSpace start → M.AltAcceptsSpace start

Acceptance in bounded space transports along an equivalence.

theorem DescriptiveComplexity.ATMData.AltAgree.blocksSplit_mp {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) : N.BlocksSplit → M.BlocksSplit

The two-block split transports along an equivalence.