PostMachineThue

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

inductive Undecidability.PostMachine.Direction : Type

The two head movements of a binary single-tape machine.

• left : Direction
• right : Direction

structure Undecidability.PostMachine.Command (Q : Type u_1) : Type u_1

One binary-machine transition writes a bit, moves once, and enters a new state. This is the machine model used in Post's 1947 construction and in the Coq Library of Undecidability's SBTM-to-rewriting reduction.

• next : Q

  The state entered after executing the Post-machine command.

• write : Bool

  The Boolean symbol written by the Post-machine command.

• move : Direction

  The tape direction taken by the Post-machine command.

@[reducible, inline]

abbrev Undecidability.PostMachine.Machine (Q : Type u_1) : Type u_1

A deterministic Post-machine transition function, with none representing halting.

Equations

• Undecidability.PostMachine.Machine Q = (Q → Bool → Option (Undecidability.PostMachine.Command Q))

structure Undecidability.PostMachine.Config (Q : Type u_1) : Type u_1

The left and right lists are stored nearest-to-the-head first.

• state : Q

  The current control state of a Post-machine configuration.

• left : List Bool

  The symbols to the left of the head, ordered from nearest to farthest.

• head : Bool

  The Boolean symbol currently under the tape head.

• right : List Bool

  The symbols to the right of the head, ordered from nearest to farthest.

def Undecidability.PostMachine.step {Q : Type u_1} (M : Machine Q) (c : Config Q) : Option (Config Q)

Blank cells contain false.

Equations

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

inductive Undecidability.PostMachine.Symbol (Q : Type u_1) : Type u_1

Alphabet of Post's rewriting simulation. Constructor separation makes the marker and unique-state-symbol invariants explicit.

• leftMarker {Q : Type u_1} : Symbol Q
• rightMarker {Q : Type u_1} : Symbol Q
• tape {Q : Type u_1} (b : Bool) : Symbol Q
• state {Q : Type u_1} (q : Q) : Symbol Q

instance Undecidability.PostMachine.instFiniteSymbol {Q : Type u_1} [Finite Q] : Finite (Symbol Q)

def Undecidability.PostMachine.encodeTape {Q : Type u_1} (w : List Bool) : List (Symbol Q)

The word of tape-symbol letters encoding a Boolean tape segment.

Equations

• Undecidability.PostMachine.encodeTape w = List.map Undecidability.PostMachine.Symbol.tape w

def Undecidability.PostMachine.encode {Q : Type u_1} (c : Config Q) : List (Symbol Q)

A configuration is written L (reverse left) head state right R.

Equations

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

def Undecidability.PostMachine.target {Q : Type u_1} : List (Symbol Q)

The two-marker target word reached by the halting simulation.

Equations

• Undecidability.PostMachine.target = [Undecidability.PostMachine.Symbol.rightMarker, Undecidability.PostMachine.Symbol.leftMarker]

inductive Undecidability.PostMachine.Rule {Q : Type u_1} (M : Machine Q) : List (Symbol Q) → List (Symbol Q) → Prop

Post's rules. The first three constructors clean a halted configuration; the remaining four simulate one boundary case and one interior case for each head direction.

• halt {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} (h : M q a = none) : Rule M [Symbol.leftMarker, Symbol.tape a, Symbol.state q, Symbol.rightMarker] [Symbol.rightMarker, Symbol.leftMarker]
• eraseLeft {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} (h : M q a = none) (b : Bool) : Rule M [Symbol.tape b, Symbol.tape a, Symbol.state q] [Symbol.tape a, Symbol.state q]
• eraseRight {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} (h : M q a = none) (b : Bool) : Rule M [Symbol.tape a, Symbol.state q, Symbol.tape b] [Symbol.tape a, Symbol.state q]
• moveLeftBoundary {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} {q' : Q} {a' : Bool} (h : M q a = some { next := q', write := a', move := Direction.left }) : Rule M [Symbol.leftMarker, Symbol.tape a, Symbol.state q] [Symbol.leftMarker, Symbol.tape false, Symbol.state q', Symbol.tape a']
• moveLeft {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} {q' : Q} {a' : Bool} (h : M q a = some { next := q', write := a', move := Direction.left }) (b : Bool) : Rule M [Symbol.tape b, Symbol.tape a, Symbol.state q] [Symbol.tape b, Symbol.state q', Symbol.tape a']
• moveRightBoundary {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} {q' : Q} {a' : Bool} (h : M q a = some { next := q', write := a', move := Direction.right }) : Rule M [Symbol.tape a, Symbol.state q, Symbol.rightMarker] [Symbol.tape a', Symbol.tape false, Symbol.state q', Symbol.rightMarker]
• moveRight {Q : Type u_1} {M : Machine Q} {q : Q} {a : Bool} {q' : Q} {a' : Bool} (h : M q a = some { next := q', write := a', move := Direction.right }) (b : Bool) : Rule M [Symbol.tape a, Symbol.state q, Symbol.tape b] [Symbol.tape a', Symbol.tape b, Symbol.state q']

def Undecidability.PostMachine.system {Q : Type u_1} (M : Machine Q) : ThueSystem (Symbol Q)

The Thue system comprising the Post-machine transition and halting rules.

Equations

• Undecidability.PostMachine.system M = {p : List (Undecidability.PostMachine.Symbol Q) × List (Undecidability.PostMachine.Symbol Q) | Undecidability.PostMachine.Rule M p.1 p.2}

def Undecidability.PostMachine.haltPair {Q : Type u_1} (i : Q × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule replacing a halting state and scanned symbol by the target markers.

Equations

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

def Undecidability.PostMachine.eraseLeftPair {Q : Type u_1} (i : Q × Bool × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule erasing a tape symbol on the left during the halting cleanup.

Equations

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

def Undecidability.PostMachine.eraseRightPair {Q : Type u_1} (i : Q × Bool × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule erasing a tape symbol on the right during the halting cleanup.

Equations

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

def Undecidability.PostMachine.moveLeftBoundaryPair {Q : Type u_1} (i : Q × Bool × Q × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule simulating a left move at the encoded tape boundary.

Equations

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

def Undecidability.PostMachine.moveLeftPair {Q : Type u_1} (i : Q × Bool × Q × Bool × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule simulating a left move across an existing neighboring tape symbol.

Equations

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

def Undecidability.PostMachine.moveRightBoundaryPair {Q : Type u_1} (i : Q × Bool × Q × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule simulating a right move at the encoded tape boundary.

Equations

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

def Undecidability.PostMachine.moveRightPair {Q : Type u_1} (i : Q × Bool × Q × Bool × Bool) : List (Symbol Q) × List (Symbol Q)

The rewriting rule simulating a right move across an existing neighboring tape symbol.

Equations

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

theorem Undecidability.PostMachine.system_finite {Q : Type u_1} [Finite Q] (M : Machine Q) : Set.Finite (system M)

A machine with finitely many states produces a finite Thue system. The proof bounds the actual rules by seven finite families, without requiring the transition function itself to carry any computability data.

theorem Undecidability.PostMachine.rule_step {Q : Type u_1} {M : Machine Q} {x y : List (Symbol Q)} (hxy : Rule M x y) (l r : List (Symbol Q)) : ThueStep (system M) (l ++ x ++ r) (l ++ y ++ r)

theorem Undecidability.PostMachine.simulation_step {Q : Type u_1} {M : Machine Q} {c d : Config Q} (hcd : step M c = some d) : ThueStep (system M) (encode c) (encode d)

Every nonhalting machine step is one application of a Post rule.

theorem Undecidability.PostMachine.simulation_halt {Q : Type u_1} {M : Machine Q} {c : Config Q} (hc : step M c = none) : ThueEq (system M) (encode c) target

Once the machine halts, deletion rules remove both finite tape fragments and the final rule produces the fixed target.

theorem Undecidability.PostMachine.target_ne_encode {Q : Type u_1} (c : Config Q) : target ≠ encode c

def Undecidability.PostMachine.isState {Q : Type u_1} : Symbol Q → Bool

The Boolean predicate recognizing control-state letters in the encoded alphabet.

Equations

• Undecidability.PostMachine.isState (Undecidability.PostMachine.Symbol.state q) = true
• Undecidability.PostMachine.isState x✝ = false

def Undecidability.PostMachine.stateCount {Q : Type u_1} (w : List (Symbol Q)) : ℕ

The number of control-state letters in an encoded word.

Equations

• Undecidability.PostMachine.stateCount w = List.countP Undecidability.PostMachine.isState w

def Undecidability.PostMachine.marker {Q : Type u_1} : Symbol Q → List Bool

The Boolean marker encoding of a boundary letter, empty for other letters.

Equations

• Undecidability.PostMachine.marker Undecidability.PostMachine.Symbol.leftMarker = [false]
• Undecidability.PostMachine.marker Undecidability.PostMachine.Symbol.rightMarker = [true]
• Undecidability.PostMachine.marker x✝ = []

def Undecidability.PostMachine.markers {Q : Type u_1} (w : List (Symbol Q)) : List Bool

The boundary-marker sequence extracted from an encoded word.

Equations

• Undecidability.PostMachine.markers w = List.flatMap Undecidability.PostMachine.marker w

theorem Undecidability.PostMachine.classify_step {Q : Type u_1} {M : Machine Q} {c d : Config Q} (hstep : step M c = some d) {w : List (Symbol Q)} (hrew : ThueStep (system M) (encode c) w) : w = encode d ∨ ∃ (p : Config Q), w = encode p ∧ step M p = some c

Post's inverse-simulation invariant for one symmetric rewrite out of a live encoded configuration.

def Undecidability.PostMachine.coding {Q : Type u_1} (M : Machine Q) : MachineThue.Coding (Config Q) (Symbol Q)

The complete machine-to-fixed-target symmetric-Thue coding.

Equations

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

theorem Undecidability.PostMachine.terminates_iff {Q : Type u_1} (M : Machine Q) (c : Config Q) : MachineThue.Terminates (step M) c ↔ ThueEq (system M) (encode c) target

A binary machine terminates exactly when its Post word is equivalent to the fixed word R L.