ThueBridge

Part of the dependency closure of the small undecidable group constructions.

def Undecidability.MachineThue.iterate {C : Type u_1} (step : C → Option C) : ℕ → C → Option C

Iteration of a deterministic partial transition function. The zeroth iterate is the initial configuration; a missing transition at any later stage records termination.

Equations

• Undecidability.MachineThue.iterate step 0 x✝ = some x✝
• Undecidability.MachineThue.iterate step n.succ x✝ = (step x✝).bind (Undecidability.MachineThue.iterate step n)

def Undecidability.MachineThue.Terminates {C : Type u_1} (step : C → Option C) (c : C) : Prop

A configuration terminates when some finite iterate encounters a missing transition.

Equations

• Undecidability.MachineThue.Terminates step c = ∃ (n : ℕ), Undecidability.MachineThue.iterate step n c = none

theorem Undecidability.MachineThue.terminates_of_halted {C : Type u_1} {step : C → Option C} {c : C} (h : step c = none) : Terminates step c

theorem Undecidability.MachineThue.terminates_of_step {C : Type u_1} {step : C → Option C} {c d : C} (hcd : step c = some d) (hd : Terminates step d) : Terminates step c

theorem Undecidability.MachineThue.terminates_after_step {C : Type u_1} {step : C → Option C} {c d : C} (hcd : step c = some d) (hc : Terminates step c) : Terminates step d

theorem Undecidability.MachineThue.terminates_iff_reaches_halt {C : Type u_1} {step : C → Option C} {c : C} : Terminates step c ↔ ∃ (h : C), StateTransition.Reaches step c h ∧ step h = none

theorem Undecidability.MachineThue.terminates_iff_eval_dom {C : Type u_1} {step : C → Option C} {c : C} : Terminates step c ↔ (StateTransition.eval step c).Dom

Terminates agrees with Mathlib's domain predicate for the standard state-transition evaluator.

structure Undecidability.MachineThue.Coding (C : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

The exact local obligations needed to turn a deterministic partial machine into a symmetric Thue system with a fixed target.

classify is Post's key inverse-simulation lemma. At a nonterminal encoded configuration, a symmetric rewrite either performs the unique forward machine step or reaches an encoded predecessor. The latter alternative is harmless: determinism lets us cancel that backwards excursion from any terminating run.

• step : C → Option C

  The partial transition function of the machine being simulated.

• system : ThueSystem α

  The Thue system simulating the partial transition function.

• encode : C → List α

  The word encoding a machine configuration in the simulating Thue system.

• target : List α

  The target word representing halting in the simulating Thue system.

• target_ne_encode (c : C) : self.target ≠ self.encode c
• simulate_step {c d : C} : self.step c = some d → ThueStep self.system (self.encode c) (self.encode d)
• simulate_halt {c : C} : self.step c = none → ThueEq self.system (self.encode c) self.target
• classify {c d : C} {w : List α} : self.step c = some d → ThueStep self.system (self.encode c) w → w = self.encode d ∨ ∃ (p : C), w = self.encode p ∧ self.step p = some c

theorem Undecidability.MachineThue.Coding.simulation {C : Type u_1} {α : Type u_2} (K : Coding C α) {c : C} : Terminates K.step c → ThueEq K.system (K.encode c) K.target

theorem Undecidability.MachineThue.Coding.inverse_simulation {C : Type u_1} {α : Type u_2} (K : Coding C α) {c : C} : ThueEq K.system (K.encode c) K.target → Terminates K.step c

theorem Undecidability.MachineThue.Coding.terminates_iff {C : Type u_1} {α : Type u_2} (K : Coding C α) {c : C} : Terminates K.step c ↔ ThueEq K.system (K.encode c) K.target

A deterministic machine terminates exactly when its encoding is Thue-equivalent to the fixed target.