The ladder, written with the relations a second-order block guesses

A second-order block cannot guess a function A → Config A; it guesses the three relations of DescriptiveComplexity.tmGuessBlock – Q t q, “the state at time t is q”, H t p, “the head is on p”, and T t p a, “the cell p holds a”. DescriptiveComplexity.Problems.Machine.Walk already relates the two forms existentially (DescriptiveComplexity.TMData.exists_relWalk_iff_exists_walk); the ladder needs more, because its rounds alternate: a universal round quantifies over all assignments and must be able to assume that the one it is given is functional.

So this file is the pointwise dictionary. DescriptiveComplexity.Graphs ρ w says the assignment ρ is the graph of the walk w; every assignment that is functional is a graph (DescriptiveComplexity.exists_graphs) and every walk has one (DescriptiveComplexity.graphOf), and each condition the game puts on a walk gets a relational twin that agrees with it along the dictionary. The transfer of a whole quantifier is DescriptiveComplexity.bareQ_transfer, and the result is DescriptiveComplexity.ATMData.altLadder_iff_runAltLadder.

One condition is not a transcription: “the walk stands still because it is stuck” quantifies over the successor configurations, which a first-order formula cannot do. It does not have to: DescriptiveComplexity.TMData.exists_step_iff_appTr says a successor exists exactly when an applicable transition does – the successor configuration can be assembled from the transition's own data – and that is a first-order condition on the transition table.

Applicable transitions

def DescriptiveComplexity.TMData.AppTr {A : Type} (M : TMData A) (c : Config A) : Prop

A transition applies to the configuration c: it fires on the state and the symbol under the head, it has a target state and a symbol to write, and the head has somewhere to move. Unlike “c has a successor” this quantifies only over elements of the universe.

Equations

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

theorem DescriptiveComplexity.TMData.exists_step_iff_appTr {A : Type} {M : TMData A} {c : Config A} : (∃ (c' : Config A), M.Step c c') ↔ M.AppTr c

Having a successor is having an applicable transition: the successor configuration is assembled from the transition, writing under the head and leaving every other cell alone.

A guessed run, and the walk it is the graph of

def DescriptiveComplexity.runQ {A : Type} (ρ : tmGuessBlock.Assignment A) (t q : A) : Prop

The state relation of a guessed run: at time t the state is q.

Equations

• DescriptiveComplexity.runQ ρ t q = ρ DescriptiveComplexity.TMIdx.state ![t, q]

def DescriptiveComplexity.runH {A : Type} (ρ : tmGuessBlock.Assignment A) (t p : A) : Prop

The head relation of a guessed run: at time t the head is on p.

Equations

• DescriptiveComplexity.runH ρ t p = ρ DescriptiveComplexity.TMIdx.head ![t, p]

def DescriptiveComplexity.runT {A : Type} (ρ : tmGuessBlock.Assignment A) (t p a : A) : Prop

The tape relation of a guessed run: at time t the cell p holds a.

Equations

• DescriptiveComplexity.runT ρ t p a = ρ DescriptiveComplexity.TMIdx.tape ![t, p, a]

def DescriptiveComplexity.RunFun {A : Type} (ρ : tmGuessBlock.Assignment A) : Prop

The guess is functional, the six clauses that make it read as one configuration per time.

Equations

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

def DescriptiveComplexity.Graphs {A : Type} (ρ : tmGuessBlock.Assignment A) (w : A → Config A) : Prop

The guess is the graph of the walk w.

Equations

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

def DescriptiveComplexity.graphOf {A : Type} (w : A → Config A) : tmGuessBlock.Assignment A

The graph of a walk, as an assignment of the guessing block.

Equations

• DescriptiveComplexity.graphOf w DescriptiveComplexity.TMIdx.state = fun (v : Fin 2 → A) => v 1 = (w (v 0)).state
• DescriptiveComplexity.graphOf w DescriptiveComplexity.TMIdx.head = fun (v : Fin 2 → A) => v 1 = (w (v 0)).head
• DescriptiveComplexity.graphOf w DescriptiveComplexity.TMIdx.tape = fun (v : Fin 3 → A) => v 2 = (w (v 0)).tape (v 1)

@[simp]

theorem DescriptiveComplexity.graphs_graphOf {A : Type} (w : A → Config A) : Graphs (graphOf w) w

theorem DescriptiveComplexity.eq_of_iff_eq {α : Type} {x y : α} (h : ∀ (a : α), a = x ↔ a = y) : x = y

Two values with the same graph are equal.

theorem DescriptiveComplexity.RunFun.of_graphs {A : Type} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) : RunFun ρ

A graph is functional.

theorem DescriptiveComplexity.exists_graphs {A : Type} {ρ : tmGuessBlock.Assignment A} (h : RunFun ρ) : ∃ (w : A → Config A), Graphs ρ w

A functional guess is a graph: the configuration at each time is the one its three relations single out.

Transferring a quantifier

theorem DescriptiveComplexity.bareQ_transfer {A : Type} (pol : Bool) {Cw Pw : (A → Config A) → Prop} {Cρ Pρ : tmGuessBlock.Assignment A → Prop} (hC : ∀ (ρ : tmGuessBlock.Assignment A) (w : A → Config A), Graphs ρ w → (Cρ ρ ↔ Cw w)) (hP : ∀ (ρ : tmGuessBlock.Assignment A) (w : A → Config A), Graphs ρ w → (Pρ ρ ↔ Pw w)) : bareQ pol Cw Pw ↔ bareQ pol (fun (ρ : tmGuessBlock.Assignment A) => RunFun ρ ∧ Cρ ρ) Pρ

A quantifier over walks is a quantifier over functional guesses. The guard picks up the functionality clauses; everything else is read through the dictionary.

The conditions of the game, relationally

def DescriptiveComplexity.ATMData.RunAcc {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (t : A) : Prop

The state at time t is accepting.

Equations

• M.RunAcc ρ t = ∀ (q : A), DescriptiveComplexity.runQ ρ t q → M.Acc q

def DescriptiveComplexity.ATMData.RunBlk {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (j : ℕ) (t : A) : Prop

The state at time t is in block j.

Equations

• M.RunBlk ρ j t = ∀ (q : A), DescriptiveComplexity.runQ ρ t q → M.Blk j q

def DescriptiveComplexity.ATMData.RunBlkLt {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (i : ℕ) (t : A) : Prop

The state at time t is in a block below i.

Equations

• M.RunBlkLt ρ i t = ∀ (q : A), DescriptiveComplexity.runQ ρ t q → M.BlkLt i q

def DescriptiveComplexity.ATMData.RunInit {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (t : A) : Prop

The configuration at time t is initial.

Equations

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

def DescriptiveComplexity.ATMData.RunAppTr {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (t : A) : Prop

Some transition applies to the configuration at time t.

Equations

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

def DescriptiveComplexity.ATMData.RunSame {A : Type} (ρ ρ' : tmGuessBlock.Assignment A) (t t' : A) : Prop

The configuration at time t' of ρ' is the one at time t of ρ.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ATMData.RunStep {A : Type} (M : ATMData A) {ρ : tmGuessBlock.Assignment A} (t t' : A) : Prop

The step clause, relationally, is DescriptiveComplexity.TMData.RelStep of the three relations.

Equations

• M.RunStep t t' = M.RelStep (DescriptiveComplexity.runQ ρ) (DescriptiveComplexity.runH ρ) (DescriptiveComplexity.runT ρ) t t'

def DescriptiveComplexity.ATMData.RunBlkMono {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) : Prop

The blocks of a guessed run never decrease.

Equations

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

def DescriptiveComplexity.ATMData.RunLegalBelow {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) (i : ℕ) : Prop

A guessed run legal below block i.

Equations

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

def DescriptiveComplexity.ATMData.RunAccAt {A : Type} (M : ATMData A) (ρ : tmGuessBlock.Assignment A) : Prop

The guessed run accepts: its state at the highest time is accepting.

Equations

• M.RunAccAt ρ = ∀ (p : A), DescriptiveComplexity.MaxPos M.Le M.Posn p → M.RunAcc ρ p

def DescriptiveComplexity.ATMData.RunAgreeBelow {A : Type} (M : ATMData A) (ρ ρ' : tmGuessBlock.Assignment A) (i : ℕ) : Prop

The guessed run ρ' reproduces what ρ committed below block i.

Equations

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

def DescriptiveComplexity.ATMData.RunRoundCond {A : Type} (M : ATMData A) (ρ ρ' : tmGuessBlock.Assignment A) (i : ℕ) : Prop

The condition round i puts on its guess.

Equations

• M.RunRoundCond ρ ρ' i = (M.RunLegalBelow ρ' (i + 1) ∧ M.RunAgreeBelow ρ ρ' i)

The dictionary

theorem DescriptiveComplexity.ATMData.runAcc_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (t : A) : M.RunAcc ρ t ↔ M.Acc (w t).state

theorem DescriptiveComplexity.ATMData.runBlk_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (j : ℕ) (t : A) : M.RunBlk ρ j t ↔ M.Blk j (w t).state

theorem DescriptiveComplexity.ATMData.runBlkLt_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (i : ℕ) (t : A) : M.RunBlkLt ρ i t ↔ M.BlkLt i (w t).state

theorem DescriptiveComplexity.ATMData.runInit_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (t : A) : M.RunInit ρ t ↔ M.IsInit (w t)

theorem DescriptiveComplexity.ATMData.runSame_iff {A : Type} {ρ ρ' : tmGuessBlock.Assignment A} {w w' : A → Config A} (hg : Graphs ρ w) (hg' : Graphs ρ' w') (t t' : A) : RunSame ρ ρ' t t' ↔ w' t' = w t

theorem DescriptiveComplexity.ATMData.runAppTr_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (t : A) : M.RunAppTr ρ t ↔ M.AppTr (w t)

theorem DescriptiveComplexity.ATMData.runStuck_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (t : A) : ¬M.RunAppTr ρ t ↔ M.Stuck (w t)

theorem DescriptiveComplexity.ATMData.runStep_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (t t' : A) : M.RunStep t t' ↔ M.Step (w t) (w t')

theorem DescriptiveComplexity.ATMData.runBlkMono_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) : M.RunBlkMono ρ ↔ M.BlkMono w

theorem DescriptiveComplexity.ATMData.runLegalBelow_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) (i : ℕ) : M.RunLegalBelow ρ i ↔ M.LegalBelow i w

theorem DescriptiveComplexity.ATMData.runAccAt_iff {A : Type} {M : ATMData A} {ρ : tmGuessBlock.Assignment A} {w : A → Config A} (h : Graphs ρ w) : M.RunAccAt ρ ↔ M.AccAt w

theorem DescriptiveComplexity.ATMData.runAgreeBelow_iff {A : Type} {M : ATMData A} {ρ ρ' : tmGuessBlock.Assignment A} {w w' : A → Config A} (hg : Graphs ρ w) (hg' : Graphs ρ' w') (i : ℕ) : M.RunAgreeBelow ρ ρ' i ↔ M.AgreeBelow i w' w

theorem DescriptiveComplexity.ATMData.runRoundCond_iff {A : Type} {M : ATMData A} {ρ ρ' : tmGuessBlock.Assignment A} {w w' : A → Config A} (hg : Graphs ρ w) (hg' : Graphs ρ' w') (i : ℕ) : M.RunRoundCond ρ ρ' i ↔ M.RoundCond i w w'

The ladder over guesses

def DescriptiveComplexity.ATMData.runLadder {A : Type} (M : ATMData A) (start : Bool) (i : ℕ) : ℕ → tmGuessBlock.Assignment A → Prop

The ladder from round i on, over guessed runs.

Equations

• One or more equations did not get rendered due to their size.
• M.runLadder start i 0 x✝ = M.RunAccAt x✝

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

The whole ladder, over guessed runs: the sentence's semantics.

Equations

• One or more equations did not get rendered due to their size.
• M.RunAltLadder start 0 = False

theorem DescriptiveComplexity.ATMData.gameLadder_iff_runLadder {A : Type} (M : ATMData A) (start : Bool) (m i : ℕ) (ρprev : tmGuessBlock.Assignment A) (prev : A → Config A) : Graphs ρprev prev → (M.gameLadder start i m prev ↔ M.runLadder start i m ρprev)

The ladder over walks is the ladder over guesses, from round i on.

theorem DescriptiveComplexity.ATMData.altLadder_iff_runAltLadder {A : Type} (M : ATMData A) (start : Bool) (n : ℕ) : M.AltLadder start n ↔ M.RunAltLadder start n

The whole ladder over walks is the whole ladder over guesses.