Alternating Turing machines over a universe, without a vocabulary

The semantics half of the machine bridge for the polynomial hierarchy: what it means for an alternating Turing machine, presented as relations on a universe, to accept. As in DescriptiveComplexity.Machines no vocabulary appears, so the reductions – which build machines rather than read them – can reason about acceptance without unfolding any RelMap.

The model

DescriptiveComplexity.ATMData is DescriptiveComplexity.TMData together with one further family of marks, Blk j q: the state q belongs to the j-th quantifier block. Two conventions fix the game the marks describe.

• Which player owns a state. Block j is existential when DescriptiveComplexity.blockPol start j is true, that is, when j is even and start is true or j is odd and start is false: the polarities alternate outwards-in from start, exactly as DescriptiveComplexity.altQuant alternates the quantifiers of a quantified Boolean formula. A state marked by a block of the other polarity is universal (DescriptiveComplexity.ATMData.IsUniv).
• Blocks mark states, not times. A variant marking the time – the phases of the run scheduled in advance – makes the round structure independent of the run, and is rejected for exactly that: it clocks the alternation, which is half of what the model is supposed to say.
• A stuck universal state rejects. A universal configuration accepts when every successor accepts and there is one (DescriptiveComplexity.ATMData.AltAcc). The other convention – vacuous universal quantification, so that a stuck universal configuration accepts – is equally standard, and this one is chosen because it makes “the machine stops without accepting” mean reject in every block, which is what a reduction needs: a checking phase that fails may then simply run out of transitions, whatever the polarity of the block it runs in.

With one block the model is the nondeterministic one: AltAcc start n c unfolds to “some run of at most n steps from c reaches an accepting state”, so DescriptiveComplexity.ATMData.AltAccepts at k = 1 is DescriptiveComplexity.TMData.Accepts.

The alternation bound

Nothing above bounds the number of alternations; the bound is DescriptiveComplexity.ATMData.BlocksWellFormed, folded into the yes-instances of the decision problem exactly as linearity of the order is: every state carries exactly one of the k marks, a transition raises the block index by 0 or 1, and a start state is in block 0. All three are first-order for a fixed k – the second because it is a condition on a single transition, which is what makes “at most k - 1 alternations” checkable by the kernel of a Σₖ definition rather than by an inspection of runs. The last two together make a run pass through the blocks in succession, starting at the first, which is what lets it be read as k rounds of a game with the right player in each.

Transport

DescriptiveComplexity.ATMData.AltAgree records that two alternating machines over different universes correspond along an equivalence, and the lemmas below transport acceptance along it – all the isomorphism-invariance proof of the decision problem needs.

structure DescriptiveComplexity.ATMData (A : Type) extends DescriptiveComplexity.TMData A : Type

An alternating Turing machine presented as relations on a universe: a machine in the sense of DescriptiveComplexity.TMData, together with marks splitting its states into quantifier blocks.

• Posn : A → Prop
• Le : A → A → Prop
• Tr : A → Prop
• Start : A → Prop
• Acc : A → Prop
• Blank : A → Prop
• Right : A → Prop
• Src : A → A → Prop
• Read : A → A → Prop
• Dst : A → A → Prop
• Write : A → A → Prop
• Inp : A → A → Prop
• Blk : ℕ → A → Prop

  Blk j q: the state q belongs to the j-th quantifier block.

def DescriptiveComplexity.blockPol (start : Bool) (j : ℕ) : Bool

The polarity of the j-th quantifier block of a prefix starting with polarity start: true for an existential block, false for a universal one. The polarities alternate, so the parity of j decides.

Equations

• DescriptiveComplexity.blockPol start j = if j % 2 = 0 then start else !start

@[simp]

theorem DescriptiveComplexity.blockPol_zero (start : Bool) : blockPol start 0 = start

theorem DescriptiveComplexity.blockPol_succ (start : Bool) (j : ℕ) : blockPol start (j + 1) = !blockPol start j

The polarities of consecutive blocks are opposite.

def DescriptiveComplexity.guardQ (pol : Bool) {α : Type} (C P : α → Prop) : Prop

Quantification with a polarity, guarded. Existentially, the guard is conjoined; universally it is assumed – and, in the same breath, required to be satisfiable by something. That extra clause is the “a stuck universal state rejects” convention of the module docstring, at the level of quantifiers: a universal player with no legal move loses rather than winning vacuously.

Equations

• DescriptiveComplexity.guardQ true C P = ∃ (a : α), C a ∧ P a
• DescriptiveComplexity.guardQ false C P = ((∃ (a : α), C a) ∧ ∀ (a : α), C a → P a)

theorem DescriptiveComplexity.guardQ_true {α : Type} (C P : α → Prop) : guardQ true C P ↔ ∃ (a : α), C a ∧ P a

theorem DescriptiveComplexity.guardQ_false {α : Type} (C P : α → Prop) : guardQ false C P ↔ (∃ (a : α), C a) ∧ ∀ (a : α), C a → P a

theorem DescriptiveComplexity.guardQ_congr (pol : Bool) {α : Type} {C C' P P' : α → Prop} (hC : ∀ (a : α), C a ↔ C' a) (hP : ∀ (a : α), C a → (P a ↔ P' a)) : guardQ pol C P ↔ guardQ pol C' P'

Guarded quantification only depends on its two predicates up to pointwise equivalence.

The players

def DescriptiveComplexity.ATMData.BlkLt {A : Type} (M : ATMData A) (i : ℕ) (q : A) : Prop

The state q belongs to a block below i.

Equations

• M.BlkLt i q = ∃ j < i, M.Blk j q

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

The state q is universal: it carries the mark of a block whose polarity is universal, so the moves out of it belong to the universal player.

Equations

• M.IsUniv start q = ∃ (j : ℕ), M.Blk j q ∧ DescriptiveComplexity.blockPol start j = false

def DescriptiveComplexity.ATMData.Stuck {A : Type} (M : ATMData A) (c : Config A) : Prop

No step is available from the configuration c: the machine stops there. Whether that is an acceptance depends only on the state, never on the block – see the module docstring.

Equations

• M.Stuck c = ∀ (c' : DescriptiveComplexity.Config A), ¬M.Step c c'

Alternating acceptance

def DescriptiveComplexity.ATMData.AltAcc {A : Type} (M : ATMData A) (start : Bool) : ℕ → Config A → Prop

Alternating acceptance within a budget. M.AltAcc start n c says the configuration c accepts with n steps to spare: an accepting state accepts outright, an existential configuration accepts when some successor does, and a universal one when it has a successor and every successor accepts.

The budget recurses, so the definition is a Lean-level recursion rather than a fixed point, and DescriptiveComplexity.ATMData.AltAccepts cashes it in at the number of positions – the same unary bound as DescriptiveComplexity.TMData.Accepts.

Equations

• One or more equations did not get rendered due to their size.
• M.AltAcc start 0 x✝ = M.Acc x✝.state

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

Alternating acceptance: an initial configuration accepts within as many steps as there are positions – chosen by the player of block 0, which is what DescriptiveComplexity.guardQ at the polarity start says.

The residual freedom in the initial configuration (a machine may have several start states, and its input may leave cells to the blank) belongs to the same player as the first move, since it is the first move; at start = true this is the ∃ c₀ of DescriptiveComplexity.TMData.Accepts, which the problem therefore specializes to when every state lies in an existential block.

Equations

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

def DescriptiveComplexity.ATMData.BlocksWellFormed {A : Type} (M : ATMData A) (k : ℕ) : Prop

The block structure is well formed, in the style of DescriptiveComplexity.TMData.WellFormed: every state carries exactly one of the k block marks, and every transition either stays in its block or moves to the next one. The second clause is what bounds the number of alternations by k - 1, and it is a condition on a single transition, hence first-order.

The blocks are entered in order – a transition may not skip one, and the run starts in block 0 – so that the phases of a run are the blocks in succession. Skipping would be harmless for the number of alternations but not for the reading of the run as k rounds of a game: the round of a player would no longer be the block whose moves it makes, and a run starting above block 0 would hand the choice of its initial configuration to the wrong player. Padding a machine that skips is a matter of inserting one state per skipped block.

Equations

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

Elementary properties

theorem DescriptiveComplexity.ATMData.stuck_iff_not_exists_step {A : Type} {M : ATMData A} {c : Config A} : M.Stuck c ↔ ¬∃ (c' : Config A), M.Step c c'

Being stuck is the negation of having a successor.

theorem DescriptiveComplexity.ATMData.altAcc_succ {A : Type} {M : ATMData A} {start : Bool} (n : ℕ) {c : Config A} : M.AltAcc start n c → M.AltAcc start (n + 1) c

Spare budget is never harmful: one more step to spare cannot turn an accepting configuration into a rejecting one.

theorem DescriptiveComplexity.ATMData.altAcc_mono {A : Type} {M : ATMData A} {start : Bool} {m n : ℕ} : n ≤ m → ∀ {c : Config A}, M.AltAcc start n c → M.AltAcc start m c

Acceptance is monotone in the budget.

theorem DescriptiveComplexity.ATMData.altAcc_of_acc {A : Type} {M : ATMData A} {start : Bool} {n : ℕ} {c : Config A} (h : M.Acc c.state) : M.AltAcc start n c

An accepting state accepts, whatever the budget.

theorem DescriptiveComplexity.ATMData.altAcc_succ_iff {A : Type} {M : ATMData A} {start : Bool} {n : ℕ} {c : Config A} : M.AltAcc start (n + 1) c ↔ M.Acc c.state ∨ (M.IsUniv start c.state ∧ (∃ (c' : Config A), M.Step c c') ∧ ∀ (c' : Config A), M.Step c c' → M.AltAcc start n c') ∨ ¬M.IsUniv start c.state ∧ ∃ (c' : Config A), M.Step c c' ∧ M.AltAcc start n c'

Unfolding one step, in the form the proofs use: with a positive budget an accepting configuration either is accepting outright, or hands the choice to the player owning its state.

theorem DescriptiveComplexity.ATMData.altAcc_iff_stepsIn {A : Type} {M : ATMData A} {start : Bool} (hex : ∀ (q : A), ¬M.IsUniv start q) (n : ℕ) (c : Config A) : M.AltAcc start n c ↔ ∃ m ≤ n, ∃ (d : Config A), M.StepsIn m c d ∧ M.Acc d.state

With no universal state the model is the nondeterministic one: the recursion unfolds to “some run of at most n steps reaches an accepting state”. This is what makes the one-block problem the machine problem of DescriptiveComplexity.Machines again, and it is why the alternating model is a conservative extension rather than a new one.

theorem DescriptiveComplexity.ATMData.altAccepts_true_iff_accepts {A : Type} {M : ATMData A} [Finite A] (hex : ∀ (q : A), ¬M.IsUniv true q) (hne : ∃ (p : A), M.Posn p) : M.AltAccepts true ↔ M.Accepts

The one-block model accepts exactly when the underlying machine does. Stated at an existential outermost polarity, where the initial configuration is chosen existentially, as DescriptiveComplexity.TMData.Accepts chooses it.

Transport along an equivalence of universes

structure DescriptiveComplexity.ATMData.AltAgree {A B : Type} (u : B ≃ A) (N : ATMData B) (M : ATMData A) : Prop

Two alternating machines over different universes agree along an equivalence when their underlying machines do and their block marks correspond.

• base : TMData.Agree u N.toTMData M.toTMData

  The underlying machines agree.

• blk (j : ℕ) (b : B) : N.Blk j b ↔ M.Blk j (u b)

  The block marks correspond.

theorem DescriptiveComplexity.ATMData.AltAgree.isUniv {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (start : Bool) (b : B) : N.IsUniv start b ↔ M.IsUniv start (u b)

Universality of a state transports along an equivalence.

theorem DescriptiveComplexity.ATMData.AltAgree.stuck {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (c : Config B) : N.Stuck c ↔ M.Stuck (Config.map u c)

Being stuck transports along an equivalence.

theorem DescriptiveComplexity.ATMData.AltAgree.altAcc {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (start : Bool) (n : ℕ) (c : Config B) : N.AltAcc start n c ↔ M.AltAcc start n (Config.map u c)

Alternating acceptance within a budget transports along an equivalence.

theorem DescriptiveComplexity.ATMData.AltAgree.altAccepts {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (start : Bool) : N.AltAccepts start ↔ M.AltAccepts start

Alternating acceptance transports along an equivalence.

theorem DescriptiveComplexity.ATMData.AltAgree.blocksWellFormed {A : Type} {M : ATMData A} {B : Type} {u : B ≃ A} {N : ATMData B} (h : AltAgree u N M) (k : ℕ) : N.BlocksWellFormed k ↔ M.BlocksWellFormed k

Well-formedness of the block structure transports along an equivalence.