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_of_altAcc {A : Type} {M : ATMData A} {start : Bool} (n : ℕ) {c : Config A} : M.AltAcc start n c → M.AltWin start c

A budgeted win is a win.

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

A win is a budgeted win, the budget being the depth of the winning strategy. The universal case takes the greatest budget its successors need, which is where the finiteness of the configuration space is used.

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.altWin_iff_reach {A : Type} {M : ATMData A} {start : Bool} (hex : ∀ (q : A), ¬M.IsUniv start q) (c : Config A) : M.AltWin start c ↔ ∃ (d : Config A), Relation.ReflTransGen M.Step c d ∧ M.Acc d.state

Without a universal state, winning is reaching an accepting state. The alternating model is a conservative extension of the space-bounded nondeterministic one, exactly as DescriptiveComplexity.ATMData.altAcc_iff_stepsIn says of the budgeted model.

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.altWin_mp {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (start : Bool) {c : Config B} : N.AltWin start c → M.AltWin start (Config.map u c)

Winning transports along an equivalence of universes. Stated as an implication rather than an equivalence, and proved without any finiteness: the converse comes from the agreement in the other direction, which the isomorphism-invariance of a decision problem has anyway.

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.