The machine, written in first-order logic

DescriptiveComplexity.Exponential.GameMachine builds the machine of a specification as an DescriptiveComplexity.ATMData on tagged tuples; this file writes it down, as an DescriptiveComplexity.FOInterpretation of the alternating-machine vocabulary in the ordered source vocabulary.

Why the reduction is not relativized

One might expect the unused coordinates of a tagged tuple to be pinned by a domain formula. The machine as built does not need that: its Posn is machPosn ∧ machDom, so the junk tuples are already excluded by a relation rather than by the universe, and every promise – the order is linear, the input is functional, there is one blank – was proved on the whole tagged-tuple type. So the interpretation is an ordinary one, and DescriptiveComplexity.OrderedFOReduction.toRel widens it at the very end.

What is static and what is not

A defining formula receives the tags of its arguments, so anything decided by a tag is decided when the formula is built: that is posn, acc, right, blank, start, the block marks, and the family of every transition rule. What is left is small:

• the order, which is DescriptiveComplexity.lexLeF;
• Canon and Agree on the coordinates, which are DescriptiveComplexity.canonF and DescriptiveComplexity.agreeF;
• an address read off a transition's tuple, which is DescriptiveComplexity.padTupF;
• and the two hooks into the source structure, concOk and isTarget.

Side conditions decided by the tags

noncomputable def DescriptiveComplexity.GameProg.sideF {L : FirstOrder.Language} (γ : Type) (p : Prop) : (L.sum FirstOrder.Language.order).Formula γ

A condition decided when the formula is built.

Equations

• DescriptiveComplexity.GameProg.sideF γ p = if p then ⊤ else ⊥

@[simp]

theorem DescriptiveComplexity.GameProg.realize_sideF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {p : Prop} : (sideF γ p).Realize v ↔ p

The formulas

@[reducible, inline]

abbrev DescriptiveComplexity.GameProg.argVar {B : SOBlock} {V : ℕ} (n : ℕ) (i : Fin n) : Fin (gameDim B V) → Fin n × Fin (gameDim B V)

The coordinates of the i-th argument.

Equations

• DescriptiveComplexity.GameProg.argVar n i j = (i, j)

noncomputable def DescriptiveComplexity.GameProg.posnF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Being a position: a tape tag whose coordinates beyond its own arity are pinned.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.accF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Being an accepting state: decided by the tag.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.rightF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Moving the head right: decided by the tag.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.blankF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Being the blank: the left mark, at the constant tuple.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.startF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Being the start state: the initial sweep, at the constant tuple.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.blkF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (i : Fin 2) (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

The i-th block mark: which player owns a state is a function of its tag.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.tsrcF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (t t' : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (gameDim B V))

The state a transition applies in: the tags name it, and the tuple must agree with the transition's below the arity the phase declares.

Equations

• One or more equations did not get rendered due to their size.
• prog.tsrcF t t' = ⊥

noncomputable def DescriptiveComplexity.GameProg.tdstF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (t t' : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (gameDim B V))

The state a transition moves to, the same with dst.

Equations

• One or more equations did not get rendered due to their size.
• prog.tdstF t t' = ⊥

noncomputable def DescriptiveComplexity.GameProg.addrIx {B : SOBlock} {V : ℕ} (i : B.ι) : Fin (B.arity i) → Fin (gameDim B V)

The coordinates of a transition's tuple that hold the address of a cell of the relation variable i.

Equations

• DescriptiveComplexity.GameProg.addrIx i l = ⟨V + ↑l, ⋯⟩

noncomputable def DescriptiveComplexity.GameProg.cellIx {B : SOBlock} {V : ℕ} (i : B.ι) : Fin (B.arity i) → Fin (gameDim B V)

The coordinates of a cell's own tuple that hold its address.

Equations

• DescriptiveComplexity.GameProg.cellIx i = Fin.castLE ⋯

noncomputable def DescriptiveComplexity.GameProg.treadF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t t' : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (gameDim B V))

The symbol a transition reads: a mark, or a cell's symbol at the address the transition's own tuple carries.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.GameProg.treadF t t' = ⊥

noncomputable def DescriptiveComplexity.GameProg.twriteF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t t' : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (gameDim B V))

The symbol a transition writes, the same with wr.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.GameProg.twriteF t t' = ⊥

noncomputable def DescriptiveComplexity.GameProg.inpF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (t t' : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (gameDim B V))

The initial contents of a cell: every cell starts empty, carrying its own address, and the sentinels carry their marks.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.GameProg.inpF t t' = ⊥

def DescriptiveComplexity.GameProg.eqIxF {L : FirstOrder.Language} {B : SOBlock} {V : ℕ} {γ : Type} {m : ℕ} (f g : Fin m → Fin (gameDim B V)) (u : Fin (gameDim B V) → γ) : (L.sum FirstOrder.Language.order).Formula γ

Two families of coordinates of the same argument are equal, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.concOkF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (p : MachPh V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

The guard of a concluding transition: the residual formula of the question, relabeled onto the coordinates the phase declares. This is the one place a defining formula reads the source structure.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.isTargetF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (p : MachPh V M) (s : SymTag B) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

The test a seek makes: the symbol is the one the challenged atom addresses, and the address is the atom's arguments at the valuation.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.ruleF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (tr : TrTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

The nine rule families, written down: seven of them are decided by the transition's tag, and the two hooks into the source structure are the guard of a concluding transition and the seek's test.

Equations

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

noncomputable def DescriptiveComplexity.GameProg.trF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) (t : GameTag B V M) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (gameDim B V))

Being a transition: a transition tag whose rule fires.

Equations

• prog.trF (Sum.inr (Sum.inr tr)) = prog.ruleF tr
• prog.trF t = ⊥

Their realization

@[simp]

theorem DescriptiveComplexity.GameProg.realize_posnF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) B V M} {A : Type} [L.Structure A] [LinearOrder A] {t : GameTag B V M} {v : Fin 1 × Fin (gameDim B V) → A} : (prog.posnF t).Realize v ↔ machPosn (t, fun (j : Fin (gameDim B V)) => v (0, j)) ∧ machDom (ctrlArity prog.vars) (t, fun (j : Fin (gameDim B V)) => v (0, j))

@[simp]

theorem DescriptiveComplexity.GameProg.realize_accF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {t : GameTag B V M} {v : Fin 1 × Fin (gameDim B V) → A} : (accF t).Realize v ↔ ∃ (ph : MachPh V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inl ph) ∧ ph.kind = PhKind.acc

@[simp]

theorem DescriptiveComplexity.GameProg.realize_rightF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {t : GameTag B V M} {v : Fin 1 × Fin (gameDim B V) → A} : (rightF t).Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ tr.right = true

@[simp]

theorem DescriptiveComplexity.GameProg.realize_blkF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) B V M} {A : Type} [L.Structure A] [LinearOrder A] {i : Fin 2} {t : GameTag B V M} {v : Fin 1 × Fin (gameDim B V) → A} : (prog.blkF i t).Realize v ↔ ↑i = 1 ∧ isUnivPt prog.pol (t, fun (j : Fin (gameDim B V)) => v (0, j)) ∨ ↑i = 0 ∧ ¬isUnivPt prog.pol (t, fun (j : Fin (gameDim B V)) => v (0, j))

@[simp]

theorem DescriptiveComplexity.GameProg.realize_tsrcF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) B V M} {A : Type} [L.Structure A] [LinearOrder A] {t t' : GameTag B V M} {v : Fin 2 × Fin (gameDim B V) → A} : (prog.tsrcF t t').Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ (t', fun (j : Fin (gameDim B V)) => v (1, j)).1 = Sum.inr (Sum.inl tr.src) ∧ (Canon (MachPh.arity prog.vars tr.src) fun (j : Fin (gameDim B V)) => v (1, j)) ∧ Agree (MachPh.arity prog.vars tr.src) (fun (j : Fin (gameDim B V)) => v (0, j)) fun (j : Fin (gameDim B V)) => v (1, j)

@[simp]

theorem DescriptiveComplexity.GameProg.realize_tdstF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) B V M} {A : Type} [L.Structure A] [LinearOrder A] {t t' : GameTag B V M} {v : Fin 2 × Fin (gameDim B V) → A} : (prog.tdstF t t').Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ (t', fun (j : Fin (gameDim B V)) => v (1, j)).1 = Sum.inr (Sum.inl tr.dst) ∧ (Canon (MachPh.arity prog.vars tr.dst) fun (j : Fin (gameDim B V)) => v (1, j)) ∧ Agree (MachPh.arity prog.vars tr.dst) (fun (j : Fin (gameDim B V)) => v (0, j)) fun (j : Fin (gameDim B V)) => v (1, j)

@[simp]

theorem DescriptiveComplexity.GameProg.realize_treadF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {t t' : GameTag B V M} {v : Fin 2 × Fin (gameDim B V) → A} (h₀ : IsBot a₀) : (treadF t t').Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ (t', fun (j : Fin (gameDim B V)) => v (1, j)) = gameSymPt a₀ tr.rd (addrOf fun (j : Fin (gameDim B V)) => v (0, j))

@[simp]

theorem DescriptiveComplexity.GameProg.realize_twriteF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {t t' : GameTag B V M} {v : Fin 2 × Fin (gameDim B V) → A} (h₀ : IsBot a₀) : (twriteF t t').Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ (t', fun (j : Fin (gameDim B V)) => v (1, j)) = gameSymPt a₀ tr.wr (addrOf fun (j : Fin (gameDim B V)) => v (0, j))

@[simp]

theorem DescriptiveComplexity.GameProg.realize_inpF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {a₀ : A} {t t' : GameTag B V M} {v : Fin 2 × Fin (gameDim B V) → A} (h₀ : IsBot a₀) (hdim : blockArityBound B ≤ gameDim B V) : (inpF t t').Realize v ↔ machInp a₀ hdim (t, fun (j : Fin (gameDim B V)) => v (0, j)) (t', fun (j : Fin (gameDim B V)) => v (1, j))

@[simp]

theorem DescriptiveComplexity.GameProg.realize_trF {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) B V M} {A : Type} [L.Structure A] [LinearOrder A] {t : GameTag B V M} {v : Fin 1 × Fin (gameDim B V) → A} : (prog.trF t).Realize v ↔ ∃ (tr : TrTag B V M), (t, fun (j : Fin (gameDim B V)) => v (0, j)).1 = Sum.inr (Sum.inr tr) ∧ gameRule prog.vars prog.natoms prog.concOk prog.isTarget tr fun (j : Fin (gameDim B V)) => v (0, j)

The interpretation, and the machines agree

noncomputable def DescriptiveComplexity.GameProg.gameInterp {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) : FOInterpretation (L.sum FirstOrder.Language.order) (FirstOrder.Language.turingAlt 2) (GameTag B V M) (gameDim B V)

The machine of a program, written down: an interpretation of the alternating-machine vocabulary in the ordered source vocabulary, tagged by the machine's own tags.

Equations

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

def DescriptiveComplexity.GameProg.gameMapEquiv {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) {A : Type} : GamePt B V M A ≃ prog.gameInterp.Map A

The interpreted universe is the machine's own, with nothing added.

Equations

• prog.gameMapEquiv = Equiv.refl (DescriptiveComplexity.GamePt B V M A)

@[simp]

theorem DescriptiveComplexity.GameProg.gameMapEquiv_apply {L : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) B V M) {A : Type} (p : GamePt B V M A) : prog.gameMapEquiv p = p

The machines agree

The instance, and the reduction

theorem DescriptiveComplexity.GameProg.atmAcceptSpace_map_iff {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ATMAcceptSpace.Holds (prog.gameInterp.Map A) ↔ spec.Accepts A

The interpreted structure is a yes-instance exactly when the game is won. The machine is well formed and its marks split its states by construction, so the only content is the simulation DescriptiveComplexity.altAcceptsSpace_iff_accepts, carried across the identity by DescriptiveComplexity.ATMData.AltAgree. The bottom element the machine is built over is the structure's own minimum, which exists because the universe is finite and nonempty.

noncomputable def DescriptiveComplexity.GameProg.soGame_ordered_fo_reduction_atmAcceptSpace {L : FirstOrder.Language} [L.IsRelational] {spec : SOGameSpec L} {V M : ℕ} (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) {P : DecisionProblem L} (hspec : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ spec.Accepts A) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) : OrderedFOReduction P ATMAcceptSpace

A second-order alternating game reduces to alternating acceptance in bounded space: the machine of the program, written down.

Equations

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

EXPTIME-hardness

theorem DescriptiveComplexity.SOGameDefinable.ordered_fo_reduction_atmAcceptSpace {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SOGameDefinable P) : Nonempty (OrderedFOReduction P ATMAcceptSpace)

Every SO-GAME definable problem reduces to alternating acceptance in bounded space.

theorem DescriptiveComplexity.atmAcceptSpace_EXPTIME_hard : EXPTIME.Hard ATMAcceptSpace

Alternating acceptance in bounded space is EXPTIME-hard. Every SO(≤, LFP) definable problem is a second-order alternating game (DescriptiveComplexity.SOLFPDefinable.soGameDefinable), every such game has a program (DescriptiveComplexity.exists_gameProg), and the machine of that program is first-order definable in the instance.

theorem DescriptiveComplexity.atmAcceptSpace_EXPTIME_complete : EXPTIME.Complete ATMAcceptSpace

Alternating acceptance in bounded space is EXPTIME-complete, which is Chandra, Kozen and Stockmeyer's APSPACE = EXPTIME: an alternating machine that may use as much space as its input has positions decides exactly the problems of deterministic exponential time. Registered in the Lax archive as Lax480241.APSPACEIsEXPTIME.atmAcceptSpace_EXPTIME_complete.