Langlib

Langlib.Automata.LinearBounded.Equivalence.EndmarkerTape

Simulating the bounded-tape model on `⊢ w ⊣` (the `ε`-carrying half of `CS = LBA`) #

The canonical model for the context-sensitive languages is the endmarker LBA (is_LBA, Automata/LinearBounded/Definition.lean), which decides the empty word with the machine itself (running on ⊢⊣). This file builds the simMachine that runs a bounded-tape machine M (Automata/LinearBounded/Positive.lean) on ⊢ w ⊣, together with language_simMachine_eq; this is the tool used in Equivalence/EndmarkerToFlag.lean to assemble CS ⊆ LBA (and the whole CS = LBA).

Strategy #

simMachine M b runs M on the interior cells 1 … |w|; when a simulated move would step onto an endmarker it bounces back, exactly reproducing M's boundary clamping. The empty word is decided on ⊢⊣ directly by the bit b (always instantiated to decide (ε ∈ L)), so no flag lives on the machine. The result is language_simMachine_eq: LanguageEnd (simMachine M b) = (b ∧ ·=[]) ∨ LanguageViaEmbed M (some ∘ inl).

inductive LBA.SimState (Λ : Type u_4) :

Type u_4

States of the endmarker machine simulating a marker-free flag LBA M: start/entry walk past the left marker and split off the empty-word case, run q simulates M in state q on the interior cells (bouncing off the markers to mimic M's clamping), and acc/rej are the empty-word sinks.

start {Λ : Type u_4} : SimState Λ
entry {Λ : Type u_4} : SimState Λ
run {Λ : Type u_4} (q : Λ) : SimState Λ
acc {Λ : Type u_4} : SimState Λ
rej {Λ : Type u_4} : SimState Λ

Instances For

instance LBA.instDecidableEqSimState {Λ✝ : Type u_4} [DecidableEq Λ✝] :

DecidableEq (SimState Λ✝)

Equations

LBA.instDecidableEqSimState = LBA.instDecidableEqSimState.decEq

def LBA.instDecidableEqSimState.decEq {Λ✝ : Type u_4} [DecidableEq Λ✝] (x✝ x✝¹ : SimState Λ✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

noncomputable instance LBA.instFintypeSimState {Λ : Type u_3} [Fintype Λ] :

Fintype (SimState Λ)

Equations

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

def LBA.simTransition {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

SimState Λ → EndAlpha T Γ → Set (SimState Λ × EndAlpha T Γ × DLBA.Dir)

Transition of the endmarker machine simulating the marker-free flag LBA M (flag b): walk past ⊢; on ⊣ immediately at entry decide ε by the flag; otherwise simulate M's transitions on the interior, bouncing off either marker to reproduce M's boundary clamping.

Equations

LBA.simTransition M b LBA.SimState.start (Sum.inr false) = {(LBA.SimState.entry , LBA.leftMark , DLBA.Dir.right )}
LBA.simTransition M b LBA.SimState.entry (Sum.inr true) = if b = true then {(LBA.SimState.acc , LBA.rightMark , DLBA.Dir.stay )} else {(LBA.SimState.rej , LBA.rightMark , DLBA.Dir.stay )}
LBA.simTransition M b LBA.SimState.entry (Sum.inl c) = {(LBA.SimState.run M.initial, Sum.inl c, DLBA.Dir.stay )}
LBA.simTransition M b (LBA.SimState.run q) (Sum.inl c) = {x : LBA.SimState Λ × LBA.EndAlpha T Γ × DLBA.Dir | ∃ p ∈ M.transition q c, x = (LBA.SimState.run p.1, Sum.inl p.2.1, p.2.2)}
LBA.simTransition M b (LBA.SimState.run q) (Sum.inr false) = {(LBA.SimState.run q, LBA.leftMark , DLBA.Dir.right )}
LBA.simTransition M b (LBA.SimState.run q) (Sum.inr true) = {(LBA.SimState.run q, LBA.rightMark , DLBA.Dir.left )}
LBA.simTransition M b s a = ∅

Instances For

def LBA.simMachine {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

Machine (EndAlpha T Γ) (SimState Λ)

The endmarker machine simulating the marker-free flag LBA M with empty-word flag b.

Equations

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

Instances For

Encoding a marker-free configuration as an endmarker configuration #

The simulator runs M on the interior cells 1 … n+1 of an (n+3)-cell endmarker tape, with ⊢ at cell 0 and ⊣ at cell n+2. enc brackets an (n+1)-cell marker-free tape, encHead shifts a head position into the interior, and φ packages an M-configuration as the corresponding run-phase simulator configuration.

def LBA.enc {T : Type u_1} {Γ : Type u_2} {n : ℕ} (c : Fin (n + 1) → Option (T ⊕ Γ)) :

Fin (n + 3) → EndAlpha T Γ

Bracket an (n+1)-cell marker-free tape into the interior of an (n+3)-cell endmarker tape: ⊢ at cell 0, ⊣ at cell n+2, and the original contents shifted into cells 1 … n+1.

Equations

LBA.enc c k = if h0 : ↑k = 0 then LBA.leftMark else if h2 : ↑k = n + 2 then LBA.rightMark else Sum.inl (c ⟨↑k - 1, ⋯⟩)

Instances For

def LBA.encHead {n : ℕ} (h : Fin (n + 1)) :

Fin (n + 3)

Shift a marker-free head position h into the endmarker interior (cell h + 1).

Equations

LBA.encHead h = ⟨↑h + 1, ⋯⟩

Instances For

def LBA.φ {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg (Option (T ⊕ Γ)) Λ n) :

DLBA.Cfg (EndAlpha T Γ) (SimState Λ) (n + 2)

Package an M-configuration as the corresponding run-phase simulator configuration.

Equations

LBA.φ cfg = { state := LBA.SimState.run cfg.state, tape := { contents := LBA.enc cfg.tape.contents, head := LBA.encHead cfg.tape.head } }

Instances For

@[simp]

theorem LBA.enc_zero {T : Type u_1} {Γ : Type u_2} {n : ℕ} (c : Fin (n + 1) → Option (T ⊕ Γ)) (h : 0 < n + 3) :

enc c ⟨0, h⟩ = leftMark

@[simp]

theorem LBA.enc_last {T : Type u_1} {Γ : Type u_2} {n : ℕ} (c : Fin (n + 1) → Option (T ⊕ Γ)) (h : n + 2 < n + 3) :

enc c ⟨n + 2, h⟩ = rightMark

@[simp]

theorem LBA.enc_interior {T : Type u_1} {Γ : Type u_2} {n : ℕ} (c : Fin (n + 1) → Option (T ⊕ Γ)) (h : Fin (n + 1)) :

enc c (encHead h) = Sum.inl (c h)

theorem LBA.enc_update {T : Type u_1} {Γ : Type u_2} {n : ℕ} (c : Fin (n + 1) → Option (T ⊕ Γ)) (h : Fin (n + 1)) (a : Option (T ⊕ Γ)) :

Function.update (enc c) (encHead h) (Sum.inl a) = enc (Function.update c h a)

Writing Sum.inl a at an interior cell of enc c is the same as writing a in c.

Transition equation lemmas (definitional). #

theorem LBA.simTransition_run_inl {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (q : Λ) (c : Option (T ⊕ Γ)) :

simTransition M b (SimState.run q) (Sum.inl c) = {x : SimState Λ × (Option (T ⊕ Γ) ⊕ Bool) × DLBA.Dir | ∃ p ∈ M.transition q c, x = (SimState.run p.1, Sum.inl p.2.1, p.2.2)}

theorem LBA.simTransition_run_left {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (q : Λ) :

simTransition M b (SimState.run q) leftMark = {(SimState.run q, leftMark , DLBA.Dir.right )}

theorem LBA.simTransition_run_right {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (q : Λ) :

simTransition M b (SimState.run q) rightMark = {(SimState.run q, rightMark , DLBA.Dir.left )}

theorem LBA.simTransition_start {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

simTransition M b SimState.start leftMark = {(SimState.entry , leftMark , DLBA.Dir.right )}

theorem LBA.simTransition_entry_inl {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (c : Option (T ⊕ Γ)) :

simTransition M b SimState.entry (Sum.inl c) = {(SimState.run M.initial, Sum.inl c, DLBA.Dir.stay )}

theorem LBA.simTransition_entry_right {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

simTransition M b SimState.entry rightMark = if b = true then {(SimState.acc , rightMark , DLBA.Dir.stay )} else {(SimState.rej , rightMark , DLBA.Dir.stay )}

@[simp]

theorem LBA.simMachine_accept_run {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (q : Λ) :

(simMachine M b).accept (SimState.run q) = M.accept q

theorem LBA.read_φ {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} {n : ℕ} (cfg : DLBA.Cfg (Option (T ⊕ Γ)) Λ n) :

(φ cfg).tape.read = Sum.inl cfg.tape.read

Reading the head of φ cfg returns the (tagged) symbol M reads.

theorem LBA.cfg_ext {Γ' : Type u_4} {Λ' : Type u_5} {N : ℕ} {X Y : DLBA.Cfg Γ' Λ' N} (hs : X.state = Y.state) (hc : X.tape.contents = Y.tape.contents) (hh : X.tape.head = Y.tape.head) :

X = Y

Configurations are equal when their state, tape contents and head agree.

Forward simulation: each `M`-step is matched by one or two simulator steps. #

theorem LBA.forward_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {n : ℕ} {cfg cfg' : DLBA.Cfg (Option (T ⊕ Γ)) Λ n} (hstep : Step M cfg cfg') :

Reaches (simMachine M b) (φ cfg) (φ cfg')

A single M-step is simulated by one or two simulator steps (two when M's head clamps at a boundary, where the simulator bounces off the corresponding endmarker).

theorem LBA.forward_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {n : ℕ} {cfg cfg' : DLBA.Cfg (Option (T ⊕ Γ)) Λ n} (h : Reaches M cfg cfg') :

Reaches (simMachine M b) (φ cfg) (φ cfg')

The forward simulation extends to whole computations.

Backward simulation: a single decoding invariant. #

Good c₀ s says the simulator configuration s, reached from the start on ⊢ c₀ ⊣, decodes to a genuine M-configuration reachable from M's start on c₀. The three branches are the two pre-run setup states and the run phase; in the run phase the head is either on the encoded interior cell or sitting on a marker mid-bounce (recording where M's head clamped).

def LBA.Good {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) (s : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) (m + 2)) :

Equations

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

Instances For

theorem LBA.good_init {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) :

Good M c₀ { state := SimState.start, tape := { contents := enc c₀, head := ⟨0, ⋯⟩ } }

The simulator start configuration on ⊢ c₀ ⊣ satisfies the invariant.

theorem LBA.good_accepts {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) {s : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) (m + 2)} (hg : Good M c₀ s) (hacc : (simMachine M b).accept s.state = true) :

Accepts M { state := M.initial, tape := { contents := c₀, head := ⟨0, ⋯⟩ } }

From the invariant, an accepting simulator state yields an accepting M-run.

theorem LBA.good_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) {s s' : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) (m + 2)} (hg : Good M c₀ s) (hstep : Step (simMachine M b) s s') :

Good M c₀ s'

The decoding invariant is preserved by a simulator step.

theorem LBA.good_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) {s : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) (m + 2)} (h : Reaches (simMachine M b) { state := SimState.start, tape := { contents := enc c₀, head := ⟨0, ⋯⟩ } } s) :

Good M c₀ s

Every simulator configuration reachable from the start on ⊢ c₀ ⊣ satisfies the invariant.

theorem LBA.setup_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) :

Reaches (simMachine M b) { state := SimState.start, tape := { contents := enc c₀, head := ⟨0, ⋯⟩ } } (φ { state := M.initial, tape := { contents := c₀, head := ⟨0, ⋯⟩ } })

The two setup steps: from ⊢ c₀ ⊣ the simulator walks onto the interior and enters the run phase at M.initial, reaching the encoding of M's start configuration.

theorem LBA.sim_accepts_iff {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {m : ℕ} (c₀ : Fin (m + 1) → Option (T ⊕ Γ)) :

Accepts (simMachine M b) { state := SimState.start, tape := { contents := enc c₀, head := ⟨0, ⋯⟩ } } ↔ Accepts M { state := M.initial, tape := { contents := c₀, head := ⟨0, ⋯⟩ } }

Key bisimulation. On the bracketed tape ⊢ c₀ ⊣, the endmarker simulator accepts iff the underlying flag machine M accepts on c₀ — dimension-clean, no empty-word subtlety.

The empty word: decided by the machine itself on the two-cell tape `⊢⊣`. #

theorem LBA.simTransition_acc {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (x : EndAlpha T Γ) :

simTransition M b SimState.acc x = ∅

theorem LBA.simTransition_rej {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (x : EndAlpha T Γ) :

simTransition M b SimState.rej x = ∅

def LBA.εGood {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (b : Bool) (cfg : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) 1) :

Invariant for the empty-word run on ⊢⊣: contents stay ⊢⊣, and the state/head track the fixed two-step protocol, ending in acc exactly when the flag b is set.

Equations

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

Instances For

theorem LBA.εc0 {T : Type u_1} {Γ : Type u_2} :

(loadEnd []).contents ⟨0, εc0._proof_2 ⟩ = leftMark

theorem LBA.εc1 {T : Type u_1} {Γ : Type u_2} :

(loadEnd []).contents ⟨1, εc1._proof_2 ⟩ = rightMark

theorem LBA.εGood_init {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (b : Bool) :

εGood b { state := SimState.start, tape := loadEnd [] }

theorem LBA.εGood_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {cfg cfg' : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) 1} (hg : εGood b cfg) (hstep : Step (simMachine M b) cfg cfg') :

εGood b cfg'

theorem LBA.εGood_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) {cfg : DLBA.Cfg (EndAlpha T Γ) (SimState Λ) 1} (h : Reaches (simMachine M b) { state := SimState.start, tape := loadEnd [] } cfg) :

εGood b cfg

theorem LBA.accepts_empty {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

Accepts (simMachine M b) (initCfgEnd (simMachine M b) []) ↔ b = true

The simulator decides the empty word by itself on ⊢⊣, accepting iff the flag b is set.

Assembling the language equivalence. #

Connecting the dimension-clean sim_accepts_iff to the canonical loadEnd/initCfgList configurations requires one transport across (w.map embed).length = w.length (List.length_map), handled here once via HEq.

theorem LBA.accepts_heq {Γ' : Type u_4} {Λ' : Type u_5} {n n' : ℕ} (Mx : Machine Γ' Λ') {cfg : DLBA.Cfg Γ' Λ' n} {cfg' : DLBA.Cfg Γ' Λ' n'} (hn : n = n') (hcfg : cfg ≍ cfg') :

Accepts Mx cfg ↔ Accepts Mx cfg'

Accepts transports across a dimension equality and a heterogeneous configuration equality.

theorem LBA.boundedtape_heq {Γ' : Type u_4} {n n' : ℕ} (hn : n = n') {t : DLBA.BoundedTape Γ' n} {t' : DLBA.BoundedTape Γ' n'} (hc : t.contents ≍ t'.contents) (hh : ↑t.head = ↑t'.head) :

t ≍ t'

Heterogeneous tape equality from a dimension equality, heterogeneous contents and equal head.

theorem LBA.cfg_heq {Γ' : Type u_4} {Λ' : Type u_5} {n n' : ℕ} (hn : n = n') {c : DLBA.Cfg Γ' Λ' n} {c' : DLBA.Cfg Γ' Λ' n'} (hs : c.state = c'.state) (ht : c.tape ≍ c'.tape) :

c ≍ c'

Heterogeneous configuration equality from a dimension equality, equal state and tape HEq.

theorem LBA.sim_accepts_input {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) (w : List T) (hv : List.map (fun (t : T) => some (Sum.inl t)) w ≠ []) :

Accepts (simMachine M b) { state := SimState.start, tape := loadEnd w } ↔ Accepts M (initCfgList M (List.map (fun (t : T) => some (Sum.inl t)) w) hv)

On a non-empty input, the endmarker simulator on ⊢ w ⊣ accepts iff the flag machine M accepts on the canonically loaded w — connecting sim_accepts_iff to the canonical tapes.

theorem LBA.language_simMachine_eq {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M : Machine (Option (T ⊕ Γ)) Λ) (b : Bool) :

LanguageEnd (simMachine M b) = LanguageRecognized M (fun (t : T) => some (Sum.inl t)) b