Splicing a play into a walk

The direction DescriptiveComplexity.Problems.Machine.AltRank does not cover: turning a play of block i into the walk a round of the game has to produce. DescriptiveComplexity.ATMData.splice follows the previous round's walk up to the entry time t, replays the given play from there, and then stands still.

Standing still is legitimate because DescriptiveComplexity.ATMData.LegalBelow asks a round's walk for nothing once it has handed over: if the play ends in block i + 1 there is no obligation at all, and if it ends inside block i then it ended by accepting or by getting stuck, and stuttering there is exactly what a walk is allowed to do. That is the hypothesis hend of DescriptiveComplexity.ATMData.roundCond_splice, and it is the only thing the construction needs to know about how the play stopped.

The proof is three cases, cut by comparing the rank of a position with the rank of t: strictly below it the walk is the previous one, at it the play starts, above it the play runs and then repeats. Nothing else about the order is involved, which is why the file is short.

noncomputable def DescriptiveComplexity.ATMData.splice {A : Type} (M : ATMData A) (prev : A → Config A) (t : A) (ℓ : ℕ) (f : ℕ → Config A) : A → Config A

The walk following prev up to t and the play f after it, standing still once the play is over.

Equations

• M.splice prev t ℓ f x = if M.Posn x ∧ ¬M.Le x t then f (min (DescriptiveComplexity.bitRank M.Le M.Posn x - DescriptiveComplexity.bitRank M.Le M.Posn t) ℓ) else prev x

theorem DescriptiveComplexity.ATMData.splice_of_le {A : Type} {M : ATMData A} {prev : A → Config A} {t : A} {ℓ : ℕ} {f : ℕ → Config A} {x : A} (h : ¬(M.Posn x ∧ ¬M.Le x t)) : M.splice prev t ℓ f x = prev x

Below the entry time the spliced walk is the previous one.

theorem DescriptiveComplexity.ATMData.splice_of_lt {A : Type} {M : ATMData A} (hlin : IsLinOrd M.Le) {prev : A → Config A} {t : A} {ℓ : ℕ} {f : ℕ → Config A} {x : A} (hx : M.Posn x) (ht : M.Posn t) (hle : M.Le t x) (h0 : prev t = f 0) : M.splice prev t ℓ f x = f (min (bitRank M.Le M.Posn x - bitRank M.Le M.Posn t) ℓ)

Above the entry time the spliced walk replays the play.

theorem DescriptiveComplexity.ATMData.splice_posSeq {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {prev : A → Config A} {t : A} {ℓ : ℕ} {f : ℕ → Config A} {p₁ : A} (ht : M.Posn t) (hmax : MaxPos M.Le M.Posn p₁) (h0 : prev t = f 0) {j : ℕ} (hj : j ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) : M.splice prev t ℓ f (M.posSeq t j) = f (min j ℓ)

The spliced walk at the j-th position after t.

The spliced walk is an admissible move

theorem DescriptiveComplexity.ATMData.roundCond_splice {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {i : ℕ} {prev : A → Config A} (hprev : M.LegalBelow i prev) {t p₁ : A} (ht : M.Posn t) (hmax : MaxPos M.Le M.Posn p₁) (hti : M.Blk i (prev t).state) (hpast : ∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (prev s).state) {ℓ : ℕ} {f : ℕ → Config A} (hℓ : ℓ ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) (hplay : M.BlockPlay i (prev t) ℓ f) (hend : ℓ < bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t → M.BlkLt (i + 1) (f ℓ).state → M.Acc (f ℓ).state ∨ M.Stuck (f ℓ)) : M.RoundCond i prev (M.splice prev t ℓ f)

Splicing a play into the previous round's walk produces an admissible move for round i. The hypotheses say that t is the entry into block i (everything strictly below it is in a lower block, and prev is legal there), that f is a play of block i from the entry configuration, and that if the play stopped early inside its own block it stopped by accepting or by getting stuck.

Every initial configuration extends to a walk

A round cannot be asked for a move it cannot make, and the universal rounds of the game are guarded by an existence clause (DescriptiveComplexity.guardQ); so the game needs to know that a legal walk exists at all. It does: step while a step is available, and stand still otherwise, which is legal because standing still in a stuck configuration is allowed.

noncomputable def DescriptiveComplexity.ATMData.greedy {A : Type} (M : ATMData A) (c₀ : Config A) : ℕ → Config A

The greedy continuation of a configuration: step while a step is available, and stand still once stuck.

Equations

• M.greedy c₀ 0 = c₀
• M.greedy c₀ j.succ = if M.Acc (M.greedy c₀ j).state then M.greedy c₀ j else if h : ∃ (d : DescriptiveComplexity.Config A), M.Step (M.greedy c₀ j) d then h.choose else M.greedy c₀ j

theorem DescriptiveComplexity.ATMData.greedy_step {A : Type} (M : ATMData A) (c₀ : Config A) (j : ℕ) : M.Step (M.greedy c₀ j) (M.greedy c₀ (j + 1)) ∧ ¬M.Acc (M.greedy c₀ j).state ∨ M.greedy c₀ (j + 1) = M.greedy c₀ j ∧ (M.Acc (M.greedy c₀ j).state ∨ M.Stuck (M.greedy c₀ j))

One greedy move is a step, or standing still in a stuck configuration.

noncomputable def DescriptiveComplexity.ATMData.greedyWalk {A : Type} (M : ATMData A) (c₀ : Config A) : A → Config A

The walk that runs the greedy continuation along the positions.

Equations

• M.greedyWalk c₀ x = M.greedy c₀ (DescriptiveComplexity.bitRank M.Le M.Posn x)

theorem DescriptiveComplexity.ATMData.legalBelow_greedyWalk {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {c₀ : Config A} (hinit : M.IsInit c₀) (i : ℕ) : M.LegalBelow i (M.greedyWalk c₀) ∧ ∀ (p : A), MinPos M.Le M.Posn p → M.greedyWalk c₀ p = c₀

Every initial configuration extends to a walk legal below any block.