CSG → LBA (Kuroda): soundness

This file proves the soundness half: every accepting run of kMachine g₀ on w exhibits a derivation [S] ⇒* w (kMachine_sound).

It is a forward invariant SoundClaim over configurations reachable from the initial one (sound_invariant, by induction on the run), with one phase per machine state. The simulator reduces the decoded form toward [S] by reverse rule applications, so the current form always forward-derives to the target w·terminal; the applyRule phase carries the loop invariant of a backward pass, and the accept-check phase (check_sound, gotoLeft_check_sound) certifies the final form is exactly [S].

Soundness: a reachable accepting run exhibits a derivation

def KurodaConstruction.decodeCell {T : Type} (g₀ : grammar T) : KCell g₀ → KWork g₀

Decode one tape cell to the sentential-form symbol it represents: a raw input cell some (inl t) decodes to terminal t (so the decoded form is unchanged during the init sweep), a work cell decodes to its work symbol, a blank to nothing.

Equations

• KurodaConstruction.decodeCell g₀ none = none
• KurodaConstruction.decodeCell g₀ (some (Sum.inl t)) = some (symbol.terminal t)
• KurodaConstruction.decodeCell g₀ (some (Sum.inr (fst, fst_1, ws))) = ws

def KurodaConstruction.decodeForm {T : Type} (g₀ : grammar T) {n : ℕ} (c : Fin (n + 1) → KCell g₀) : List (symbol T g₀.nt)

The sentential form represented by a whole tape (the non-blank decoded cells, in order).

Equations

• KurodaConstruction.decodeForm g₀ c = List.filterMap id (List.ofFn fun (k : Fin (n + 1)) => KurodaConstruction.decodeCell g₀ (c k))

@[simp]

theorem KurodaConstruction.decodeCell_mkCell {T : Type} (g₀ : grammar T) {n : ℕ} (k : Fin (n + 1)) (ws : KWork g₀) : decodeCell g₀ (mkCell g₀ k ws) = ws

theorem KurodaConstruction.decodeForm_mkCell {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) : (decodeForm g₀ fun (k : Fin (n + 1)) => mkCell g₀ k (W k)) = formW g₀ W

The decoded form of a canonical work tape is its formW.

@[simp]

theorem KurodaConstruction.decodeCell_inl {T : Type} (g₀ : grammar T) (t : T) : decodeCell g₀ (some (Sum.inl t)) = some (symbol.terminal t)

theorem KurodaConstruction.decodeForm_cAt {T : Type} (g₀ : grammar T) {n : ℕ} (input : Fin (n + 1) → T) (i : ℕ) : decodeForm g₀ (cAt g₀ input i) = List.ofFn fun (k : Fin (n + 1)) => symbol.terminal (input k)

During the init sweep the decoded form is constant: every raw or converted cell of cAt input i decodes to terminal (input k).

theorem KurodaConstruction.take_succ_filterMap {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (head : Fin (n + 1)) : List.filterMap id (List.take (↑head + 1) (List.ofFn W)) = List.filterMap id (List.take (↑head) (List.ofFn W)) ++ List.filterMap id [W head]

take (i+1) peels the i-th cell off the decoded prefix.

theorem KurodaConstruction.decodeForm_split_head {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (head : Fin (n + 1)) (pre : List (symbol T g₀.nt)) (hp : List.filterMap id (List.take (↑head) (List.ofFn W)) = pre) : formW g₀ W = pre ++ List.filterMap id [W head] ++ List.filterMap id (List.drop (↑head + 1) (List.ofFn W))

The decoded form splits at the head into prefix, head cell, and suffix.

theorem KurodaConstruction.echo_moveHead_right {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (head : Fin (n + 1)) (a : KCell g₀) (ha : a = (fun (k : Fin (n + 1)) => mkCell g₀ k (W k)) head) (hlt : ↑head < n) : ({ contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := head }.write a).moveHead DLBA.Dir.right = { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := ⟨↑head + 1, ⋯⟩ }

The head-moved tape after an echo write at head (cell value re-written) with head.val < n is the same canonical tape with the head advanced one cell.

theorem KurodaConstruction.check_sound {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {cfgacc : DLBA.Cfg (KCell g₀) (KState g₀) n} (hacc : cfgacc.state = KState.accept) (W : Fin (n + 1) → KWork g₀) (d : ℕ) (seen : Bool) (head : Fin (n + 1)) : n - ↑head = d → LBA.Reaches (kMachine g₀) { state := KState.check seen, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := head } } cfgacc → (List.filterMap id (List.take (↑head) (List.ofFn W)) = if seen = true then [symbol.nonterminal g₀.initial] else []) → formW g₀ W = [symbol.nonterminal g₀.initial]

Soundness of the accept check (reverse of check_sweep): if a check sweep whose verified prefix spells [S] iff seen reaches an accepting configuration, the whole track spells [S].

theorem KurodaConstruction.gotoLeft_check_sound {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {cfgacc : DLBA.Cfg (KCell g₀) (KState g₀) n} (hacc : cfgacc.state = KState.accept) (W : Fin (n + 1) → KWork g₀) (m : ℕ) (head : Fin (n + 1)) : ↑head = m → LBA.Reaches (kMachine g₀) { state := KState.gotoLeft, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := head } } cfgacc → formW g₀ W = [symbol.nonterminal g₀.initial]

Soundness of the gotoLeft + accept-check phase. If gotoLeft (from any head) reaches an accepting configuration, the work track spells [S].

def KurodaConstruction.SoundClaim {T : Type} {n : ℕ} (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] (input : Fin (n + 1) → T) (cfg : DLBA.Cfg (KCell g₀) (KState g₀) n) : Prop

The phase-indexed soundness invariant maintained FORWARD along a run from the initial configuration. The simulator reduces the working form toward [S] by reverse rule applications, so at every reachable configuration the current form derives (forward) to the target w·terminal. The structure (cAt/mkCell) flows forward from init, which is why the induction is forward.

Equations

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

theorem KurodaConstruction.sound_invariant {T : Type} [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] {n : ℕ} (hnc : grammar_noncontracting g₀) (input : Fin (n + 1) → T) (cfg : DLBA.Cfg (KCell g₀) (KState g₀) n) (hreach : LBA.Reaches (kMachine g₀) { state := KState.init0, tape := { contents := cAt g₀ input 0, head := ⟨0, ⋯⟩ } } cfg) : SoundClaim g₀ input cfg

Forward soundness invariant. Every configuration reachable from the initial one satisfies SoundClaim.

theorem KurodaConstruction.kMachine_sound {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] (hnc : grammar_noncontracting g₀) (w : List T) : LBA.LanguageViaEmbed (kMachine g₀) (fun (t : T) => some (Sum.inl t)) w → grammar_language g₀ w

Soundness of the simulator. If the backward simulator accepts w, then the working track passed through a valid (reverse) derivation, so g₀ derives w from its start symbol.