Asking a question of the machine

The bridge between DescriptiveComplexity.GameProg – the machine's two hooks into the source structure – and the phases that use them. Everything before this file is parametric in concOk and isTarget; here they are the ones a program supplies, and the round becomes a statement about a sentence:

DescriptiveComplexity.GameProg.altWin_ask: if the question holds of the two assignments the tape carries, the machine wins from the entry of its prefix.

The three things the bridge has to say

• A claim vector is a claim vector. The phase carries Fin M → Bool and the question Fin (natoms q) → Bool; DescriptiveComplexity.GameProg.claimsOf extends one to the other and claimsOf_apply reads it back. Nothing is padded – the extension is junk above natoms q, which no rule looks at.
• A correct claim is a hit. The cell a challenge addresses is cellPt a₀ rr i ā with i the atom's relation variable, ā its arguments read at the valuation, and rr the region the atom's copy names – the current position sitting in region r and the candidate in the other, which is DescriptiveComplexity.GameProg.cond_copy. Its symbol carries the bit the tape gives it, and the claim being right says that bit is the claim.
• The residue is the guard. concOk at the concluding phase is literally (data q).sub b realized at the valuation the tuple carries, which is what DescriptiveComplexity.QuestionData.MatrixHolds supplies.

The claim vector

def DescriptiveComplexity.GameProg.claimsOf {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) (q : GameQuestion) (b : Fin (prog.data q).natoms → Bool) : Fin M → Bool

The claim vector a phase carries, from the question's own: junk above the question's atoms, which no rule ever looks at.

Equations

• prog.claimsOf q b k = if h : ↑k < (prog.data q).natoms then b ⟨↑k, h⟩ else false

theorem DescriptiveComplexity.GameProg.claimsOf_apply {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} (prog : GameProg K B V M) (q : GameQuestion) (b : Fin (prog.data q).natoms → Bool) (j : Fin (prog.data q).natoms) : prog.claimsOf q b (Fin.castLE ⋯ j) = b j

The region a copy names

theorem DescriptiveComplexity.GameProg.cond_copy {B : SOBlock} {A : Type} (r copy : Bool) (ρ σ : B.Assignment A) : (bif copy then bif !r then σ else ρ else bif r then σ else ρ) = bif if copy = true then !r else r then σ else ρ

The current position sits in region r and the candidate in the other one, so the copy an atom reads picks the region if copy then !r else r – which is exactly the region DescriptiveComplexity.GameProg.isTarget looks in.

A correct claim is a hit

theorem DescriptiveComplexity.GameProg.seekHit_of_claim {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [LinearOrder A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (q : GameQuestion) (r par : Bool) {b : Fin (prog.data q).natoms → Bool} {vv : Fin (gameDim B V) → A} (hb : ∀ (j : Fin (prog.data q).natoms), b j = true ↔ ((prog.data q).atoms j).Holds (bif r then σ else ρ) (bif !r then σ else ρ) (prog.valOf q vv)) (k : Fin (M + 1)) (hk : ↑k < prog.natoms q) : ∃ (pos : GamePt B V M A), machPosn pos ∧ machDom (ctrlArity prog.vars) pos ∧ SeekHit a₀ prog.isTarget (MachPh.seekPh q r (prog.claimsOf q b) k par) vv (tapeOfAssign a₀ hdim ρ σ) pos

The cell a challenge addresses carries the bit that was claimed, when the claim is right – so the seek finds it and the challenge is answered.

The residue is the guard

theorem DescriptiveComplexity.GameProg.concOk_of_sub {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] (q : GameQuestion) (r par : Bool) {b : Fin (prog.data q).natoms → Bool} {vv : Fin (gameDim B V) → A} (hsub : ((prog.data q).sub b).Realize default (prog.valOf q vv)) : prog.concOk (MachPh.concPh q r (prog.claimsOf q b) par) vv

The concluding transition's guard is the residual formula, read at the valuation the tuple carries.

The round, and the question

theorem DescriptiveComplexity.GameProg.altWin_matrix {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (q : GameQuestion) {r par : Bool} {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hmat : (prog.data q).MatrixHolds (bif r then σ else ρ) (bif !r then σ else ρ) (prog.valOf q vv)) (h : CtrlCfg a₀ hdim prog.vars ρ σ (MachPh.claimPh q r par) vv c) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c

The claim phase wins when the matrix holds. The existential player claims the vector the matrix supplies; each challenge is answered because the claim is right, and the concluding transition is guarded by the residue.

theorem DescriptiveComplexity.GameProg.altWin_ask {K : FirstOrder.Language} {B : SOBlock} {V M : ℕ} {prog : GameProg K B V M} {A : Type} [K.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound B ≤ gameDim B V} {ρ σ : B.Assignment A} (h₀ : IsBot a₀) (q : GameQuestion) {φ : ((K.sum B.lang).sum B.lang).Sentence} (hplays : (prog.data q).Plays φ) {r par : Bool} {jj : Fin (V + 1)} (hjj : ↑jj = 0) {vv : Fin (gameDim B V) → A} {c : Config (GamePt B V M A)} (hφ : A ⊨ φ) (h : CtrlCfg a₀ hdim prog.vars ρ σ (MachPh.prePh q r jj par) vv c) : (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c

The machine wins from the entry of a question's prefix when the question holds. This is the whole of the second normal form on the machine side: the prefix is played as moves, the matrix is claimed and challenged, and no evaluator appears anywhere.