Codes for single-tape Turing machines
Halting within a number of steps
DefinitionBounded halting of a single-tape machine#✓fully proved
A single-tape Turing machine \(M\) halts within \(T\) steps on a word \(l\) when, started in its initial state with \(l\) on the tape and the head on the first letter of \(l\) (on a blank if \(l\) is empty), it reaches after some \(j \le T\) steps a configuration that has no successor.
TheoremHalting within a bound is monotone in the bound#✓fully proved
For a single-tape Turing machine \(M\), a list \(l\) of symbols and numbers \(T \le T'\), if \(M\) started on \(l\) halts within \(T\) steps, then \(M\) started on \(l\) halts within \(T'\) steps.
theorem HaltsWithin.mono {M : TM0.Machine Γ Λ} {l : List Γ} {T T' : ℕ} (h : HaltsWithin M l T)
(hT : T ≤ T') : HaltsWithin M l T'def HaltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) (T : ℕ) : Prop :=
∃ j ≤ T, ∃ d, (flip bind (TM0.step M))^[j] (some (TM0.init l)) = some d ∧ TM0.step M d = noneCSLibExt/Computability/Machines/Turing/Universal/Code.lean:83
Uses 1
TheoremHalting is halting within some number of steps#✓fully proved
For a single-tape Turing machine \(M\) and an input word \(l\), the evaluation of \(M\) on \(l\) is defined (that is, \(M\) halts on \(l\)) if and only if there is \(T \in \mathbb{N}\) such that \(M\) halts on \(l\) within \(T\) steps.
theorem dom_eval_iff_exists_haltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) :
(TM0.eval M l).Dom ↔ ∃ T, HaltsWithin M l Tdef HaltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) (T : ℕ) : Prop :=
∃ j ≤ T, ∃ d, (flip bind (TM0.step M))^[j] (some (TM0.init l)) = some d ∧ TM0.step M d = noneCSLibExt/Computability/Machines/Turing/Universal/Code.lean:83
Uses 2 · Used by 1
Codes
StructureCodes for single-tape machines#✓fully proved
A code is a transition table: a finite list of rows, row \(q\) belonging to the state \(q \in \mathbb{N}\), each a finite list of entries, entry \(a\) of a row belonging to the symbol \(a \in \mathbb{N}\). The entry in row \(q\) and column \(a\) is either empty, meaning that the machine halts, or a pair \((q', s)\) of natural numbers, meaning that the machine enters the state \(q'\) and does the action coded by \(s\): \(0\) moves left, \(1\) moves right and \(b + 2\) writes \(b\). A state or symbol outside the table halts the machine.
structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqUsed by 69
DefinitionDecoding an action#✓fully proved
A natural number codes a statement of a single-tape Turing machine with symbols in \(\mathbb{N}\): \(0\) moves the head left, \(1\) moves the head right, and \(a + 2\) writes the symbol \(a\).
def decodeStmt : ℕ → TM0.Stmt ℕ
| 0 => .move .left
| 1 => .move .right
| a + 2 => .write aDefinitionSymbol of an input bit#✓fully proved
The tape symbol of a bit \(b\) is \(1\) if \(b\) is false and \(2\) if \(b\) is true; the symbol \(0\) is the blank.
Used by 23
DefinitionInput word of a list of bits#✓fully proved
The input word of a list of bits \(x\) is the list of natural numbers obtained from \(x\) by replacing each bit by its symbol: \(1\) for false and \(2\) for true.
def input (x : List Bool) : List ℕ := x.map bitSymdef bitSym (b : Bool) : ℕ := cond b 2 1CSLibExt/Computability/Machines/Turing/Universal/Code.lean:117
Uses 1 · Used by 18
DefinitionSingle-tape codes as tables#✓fully proved
Codes for single-tape machines correspond bijectively to transition tables, that is, to lists of rows, each a list of entries that are either empty or a pair of natural numbers: a code corresponds to its table.
def equivTable : Code ≃ List (List (Option (ℕ × ℕ))) where
toFun := table
invFun := mk
left_inv _ := rfl
right_inv _ := rflstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:107
Uses 1 · Used by 1
DefinitionTable lookup of a code#✓fully proved
For a code \(c\) and numbers \(q\) and \(a\), the lookup of \(c\) at state \(q\) and symbol \(a\) is the entry in row \(q\), column \(a\) of the table of \(c\): either a pair \((q', s)\) of a next state and an action code, or no entry (halt). It is no entry when the table has no row \(q\) or that row has no column \(a\).
def lookup (c : Code) (q a : ℕ) : Option (ℕ × ℕ) := (c.table[q]?.bind fun row ↦ row[a]?).joinstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 1 · Used by 15
DefinitionThe machine of a single-tape code#✓fully proved
The machine of a code \(c\) is the single-tape Turing machine with states and symbols in \(\mathbb{N}\) that, in state \(q\) reading symbol \(a\), halts if the table lookup of \(c\) at state \(q\) and symbol \(a\) has no entry, and otherwise, if the entry is \((q', s)\), enters state \(q'\) and does the action coded by \(s\): \(0\) moves left, \(1\) moves right and \(a' + 2\) writes \(a'\).
def machine (c : Code) : TM0.Machine ℕ ℕ := fun q a ↦
(c.lookup q a).map fun e ↦ (e.1, decodeStmt e.2)structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def decodeStmt : ℕ → TM0.Stmt ℕ
| 0 => .move .left
| 1 => .move .right
| a + 2 => .write aCSLibExt/Computability/Machines/Turing/Universal/Code.lean:111
Uses 3 · Used by 8
DefinitionStates of a single-tape code#✓fully proved
The set of states of a code \(c\) is the finite set of natural numbers consisting of the initial state \(0\) and every state \(q'\) such that some entry of the table of \(c\) is a pair \((q', s)\).
def states (c : Code) : Finset ℕ :=
insert 0 (c.table.flatten.filterMap fun o ↦ o.map Prod.fst).toFinsetstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 1 · Used by 1
TheoremCodes denote finite machines#✓fully proved
The decoded machine is supported by the finite set of states of its code.
theorem supports_machine (c : Code) : TM0.Supports c.machine ↑c.statesstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 4
Explicit configurations
StructureExplicit configurations#✓fully proved
A configuration of the simulation consists of a state \(q \in \mathbb{N}\), the list of the cells left of the head (nearest first), the symbol in the cell under the head, and the list of the cells right of the head (nearest first); states and symbols are natural numbers.
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqUsed by 35
DefinitionConfigurations as tuples#✓fully proved
Configurations correspond bijectively to tuples in \(\mathbb{N} \times \mathrm{List}(\mathbb{N}) \times \mathbb{N} \times \mathrm{List}(\mathbb{N})\): a configuration corresponds to the tuple of its state, its cells left of the head, its cell under the head and its cells right of the head.
def Cfg.equivProd : Cfg ≃ ℕ × List ℕ × ℕ × List ℕ where
toFun k := (k.q, k.left, k.head, k.right)
invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩
left_inv _ := rfl
right_inv _ := rflstructure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 1 · Used by 1
DefinitionTM0 configuration of a simulation configuration#✓fully proved
The TM0 configuration of a configuration \(k\) of the simulation has the state of \(k\), the cell under the head of \(k\) as its head cell, and as the halves of its tape left and right of the head the cells of \(k\) left and right of the head, nearest first, followed by infinitely many blanks.
def Cfg.toTM0 (k : Cfg) : TM0.Cfg ℕ ℕ := ⟨k.q, ⟨k.head, ListBlank.mk k.left, ListBlank.mk k.right⟩⟩structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 1 · Used by 6
DefinitionActing on a configuration#✓fully proved
Let \(k\) be a configuration with left cells \(L\) (nearest first), head cell \(h\) and right cells \(R\) (nearest first), let \(q'\) be a state and let \(s\) be an action code. Acting on \(k\) with \(q'\) and \(s\) gives a configuration with state \(q'\), as follows. For \(s = 0\) (move left), its head cell is the first entry of \(L\), or the blank \(0\) if \(L\) is empty, its left cells are \(L\) without its first entry, and its right cells are \(h\) followed by \(R\). For \(s = 1\) (move right), its head cell is the first entry of \(R\), or \(0\) if \(R\) is empty, its right cells are \(R\) without its first entry, and its left cells are \(h\) followed by \(L\). For \(s = a + 2\) (write \(a\)), its head cell is \(a\) and its left and right cells are \(L\) and \(R\).
def Cfg.act (k : Cfg) (q' : ℕ) : ℕ → Cfg
| 0 => ⟨q', k.left.tail, k.left.headI, k.head :: k.right⟩
| 1 => ⟨q', k.head :: k.left, k.right.headI, k.right.tail⟩
| a + 2 => ⟨q', k.left, a, k.right⟩structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 1 · Used by 9
DefinitionOutput of a configuration#✓fully proved
The output of a configuration \(k\) is the list consisting of the symbol under the head of \(k\) followed by the cells right of the head (nearest first), with all trailing blanks \(0\) removed.
def Cfg.output (k : Cfg) : List ℕ := (k.head :: k.right).rdropWhile (· == 0)structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 1 · Used by 12
DefinitionInitial configuration of the code simulation#✓fully proved
The initial configuration of the simulation on a list of bits \(x\) has state \(0\), an empty list of cells left of the head, the head on the first symbol of the input word of \(x\) (the blank \(0\) if \(x\) is empty), and the remaining symbols of the input word, in order, right of the head.
def init (x : List Bool) : Cfg := ⟨0, [], (input x).headI, (input x).tail⟩structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
Uses 2 · Used by 12
DefinitionOne step of a code#✓fully proved
For a code \(c\) and a configuration \(k\) of the simulation, look up the table entry of \(c\) at the state of \(k\) and the symbol under the head of \(k\). If there is no entry, the step is undefined (the machine halts); if the entry is \((q', s)\), the step is the configuration obtained from \(k\) by entering the state \(q'\) and doing the action coded by \(s\).
def step (c : Code) (k : Cfg) : Option Cfg := (c.lookup k.q k.head).map fun e ↦ k.act e.1 e.2structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 4 · Used by 19
DefinitionOne step of a code, or stay when halted#✓fully proved
For a code \(c\) and a configuration \(k\) of the simulation, the configuration after one step of \(c\) from \(k\) if that step is defined, and \(k\) itself if \(c\) halts at \(k\).
def stepOrStay (c : Code) (k : Cfg) : Cfg := (c.step k).getD kstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 3 · Used by 10
DefinitionClocked configuration of a code#✓fully proved
For a code \(c\), a list of bits \(x\) and \(T \in \mathbb{N}\), the configuration of \(c\) on \(x\) after \(T\) steps is obtained from the initial configuration on \(x\) by applying \(T\) times the step of \(c\), where a step leaves a halted configuration unchanged. It is the configuration after \(T\) steps, or the halting configuration if the machine halts earlier.
def cfgAfter (c : Code) (x : List Bool) (T : ℕ) : Cfg := c.stepOrStay^[T] (init x)structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
def init (x : List Bool) : Cfg := ⟨0, [], (input x).headI, (input x).tail⟩CSLibExt/Computability/Machines/Turing/Universal/Code.lean:196
Uses 4 · Used by 12
DefinitionThe clocked evaluator#✓fully proved
Given a code \(c\), a list of bits \(x\) and a clock \(T \in \mathbb{N}\), run the simulation of \(c\) on \(x\) for at most \(T\) steps. If it halts within \(T\) steps, the result is the output of the halting configuration: the tape from the head rightwards, with trailing blanks dropped. Otherwise there is no result.
def evalSteps (c : Code) (x : List Bool) (T : ℕ) : Option (List ℕ) :=
(c.step (c.cfgAfter x T)).elim (some (c.cfgAfter x T).output) fun _ ↦ nonestructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 5 · Used by 21
Agreement with Mathlib's semantics
TheoremExplicit steps agree with the decoded machine#✓fully proved
For every code \(c\) and every configuration \(k\) of the simulation, the decoded TM0 machine of \(c\) halts at the TM0 configuration of \(k\) exactly when the step of \(c\) from \(k\) is undefined, and otherwise its step from the TM0 configuration of \(k\) is the TM0 configuration of the step of \(c\) from \(k\).
theorem step_toTM0 (c : Code) (k : Cfg) :
TM0.step c.machine k.toTM0 = (c.step k).map Cfg.toTM0structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
def Cfg.toTM0 (k : Cfg) : TM0.Cfg ℕ ℕ := ⟨k.q, ⟨k.head, ListBlank.mk k.left, ListBlank.mk k.right⟩⟩CSLibExt/Computability/Machines/Turing/Universal/Code.lean:184
Uses 8 · Used by 3
TheoremThe explicit initial configuration is the machine's#✓fully proved
For a list of bits \(x\), the initial configuration of the simulation on \(x\), read as a configuration of a single-tape machine, is the initial configuration of a single-tape machine on the input word of \(x\).
theorem init_toTM0 (x : List Bool) : (init x).toTM0 = TM0.init (input x)def init (x : List Bool) : Cfg := ⟨0, [], (input x).headI, (input x).tail⟩CSLibExt/Computability/Machines/Turing/Universal/Code.lean:196
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
Uses 4 · Used by 2
TheoremThe output of a configuration as a Mathlib half-tape#✓fully proved
For every explicit configuration \(k\), the half-tape of the Mathlib configuration of \(k\) from the head rightwards (the cell under the head followed by the cells to its right) is the output of \(k\), read with blanks beyond its end.
theorem right₀_toTM0 (k : Cfg) : k.toTM0.Tape.right₀ = ListBlank.mk k.outputstructure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
Uses 3 · Used by 1
TheoremIterated steps of the decoded machine#✓fully proved
Let \(c\) be a code, \(n \in \mathbb{N}\) and \(k\) an explicit configuration. Run the machine of \(c\) for \(n\) steps from the Mathlib configuration of \(k\), and run the explicit simulation of \(c\) for \(n\) steps from \(k\), where a run that reaches a configuration without a successor before completing \(n\) steps has no result. Then the first run has a result exactly when the second does, and its result is the Mathlib configuration of the result of the second.
theorem iterate_step_toTM0 (c : Code) (n : ℕ) (k : Cfg) :
(flip bind (TM0.step c.machine))^[n] (some k.toTM0) =
((flip bind c.step)^[n] (some k)).map Cfg.toTM0structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
structure Cfg where
/-- The state. -/
q : ℕ
/-- The cells left of the head, nearest first. -/
left : List ℕ
/-- The cell under the head. -/
head : ℕ
/-- The cells right of the head, nearest first. -/
right : List ℕ
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:161
def Cfg.toTM0 (k : Cfg) : TM0.Cfg ℕ ℕ := ⟨k.q, ⟨k.head, ListBlank.mk k.left, ListBlank.mk k.right⟩⟩CSLibExt/Computability/Machines/Turing/Universal/Code.lean:184
Uses 6 · Used by 2
TheoremBounded halting of a decoded machine through its simulation#✓fully proved
For a code \(c\), a list of bits \(x\) and \(T \in \mathbb{N}\), the decoded machine of \(c\) halts within \(T\) steps on the input word of \(x\) if and only if the explicit simulation of \(c\), started from the initial configuration on \(x\), reaches after some \(j \le T\) steps a configuration that has no successor step.
theorem haltsWithin_machine_iff (c : Code) (x : List Bool) (T : ℕ) :
HaltsWithin c.machine (input x) T ↔
∃ j ≤ T, ∃ k, (flip bind c.step)^[j] (some (init x)) = some k ∧ c.step k = nonestructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def HaltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) (T : ℕ) : Prop :=
∃ j ≤ T, ∃ d, (flip bind (TM0.step M))^[j] (some (TM0.init l)) = some d ∧ TM0.step M d = noneCSLibExt/Computability/Machines/Turing/Universal/Code.lean:83
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
def init (x : List Bool) : Cfg := ⟨0, [], (input x).headI, (input x).tail⟩CSLibExt/Computability/Machines/Turing/Universal/Code.lean:196
Uses 11 · Used by 1
TheoremDefinedness of the clocked evaluator#✓fully proved
For a code \(c\), a list of bits \(x\) and a clock \(T \in \mathbb{N}\), the clocked evaluator of \(c\) on \(x\) with clock \(T\) returns a value if and only if the simulation of \(c\) has no step from the configuration after \(T\) clocked steps on \(x\) (the configuration after \(T\) steps, or the halting configuration if the machine halts earlier).
theorem isSome_evalSteps_iff_step_eq_none (c : Code) (x : List Bool) (T : ℕ) :
(c.evalSteps x T).isSome ↔ c.step (c.cfgAfter x T) = nonestructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 6 · Used by 2
TheoremClocked halting#✓fully proved
For a code \(c\), a list of bits \(x\) and a clock \(T \in \mathbb{N}\), the clocked evaluator of \(c\) on \(x\) with clock \(T\) returns a value if and only if the machine of \(c\), started on the input word of \(x\), halts within \(T\) steps.
theorem isSome_evalSteps_iff (c : Code) (x : List Bool) (T : ℕ) :
(c.evalSteps x T).isSome ↔ HaltsWithin c.machine (input x) Tstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def HaltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) (T : ℕ) : Prop :=
∃ j ≤ T, ∃ d, (flip bind (TM0.step M))^[j] (some (TM0.init l)) = some d ∧ TM0.step M d = noneCSLibExt/Computability/Machines/Turing/Universal/Code.lean:83
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
Uses 13 · Used by 1
TheoremCharacterization of clocked results#✓fully proved
For a code \(c\), a list of bits \(x\), a clock \(T \in \mathbb{N}\) and a list \(l\) of natural numbers, the clocked evaluator returns \(l\) on \(c\), \(x\) and \(T\) if and only if the configuration of \(c\) after \(T\) clocked steps on \(x\) has no successor step and its output is \(l\).
theorem evalSteps_eq_some_iff_output (c : Code) (x : List Bool) (T : ℕ) (l : List ℕ) :
c.evalSteps x T = some l ↔ c.step (c.cfgAfter x T) = none ∧ (c.cfgAfter x T).output = lstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 6 · Used by 5
TheoremMonotonicity of the single-tape clocked evaluator#✓fully proved
Let \(c\) be a code for a single-tape machine, \(x\) a list of bits, \(l\) a list of natural numbers and \(T \le T'\) natural numbers. If the clocked evaluator returns \(l\) on \(c\) and \(x\) with clock \(T\), then it also returns \(l\) with clock \(T'\).
theorem evalSteps_mono {c : Code} {x : List Bool} {T T' : ℕ} {l : List ℕ}
(h : c.evalSteps x T = some l) (hT : T ≤ T') : c.evalSteps x T' = some lstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 9 · Used by 1
TheoremClocked results agree with the machine's semantics#✓fully proved
Let \(c\) be a code, \(x\) a list of bits, \(T\) a natural number and \(l\) a list of natural numbers. If the clocked evaluator, running \(c\) on \(x\) for at most \(T\) steps, returns \(l\), then the decoded machine of \(c\), started on the input word of \(x\), halts, and the tape from its head rightwards in the halting configuration is \(l\) followed by blanks.
theorem eval_eq_some_of_evalSteps_eq_some {c : Code} {x : List Bool} {T : ℕ} {l : List ℕ}
(h : c.evalSteps x T = some l) :
TM0.eval c.machine (input x) = Part.some (ListBlank.mk l)structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
Uses 16
TheoremUnclocked halting#✓fully proved
For a code \(c\) and a list of bits \(x\), the machine decoded from \(c\) halts on the input word of \(x\) if and only if there is a clock \(T \in \mathbb{N}\) for which the clocked evaluator of \(c\) on \(x\) with clock \(T\) returns a result.
theorem dom_eval_iff_exists_isSome_evalSteps (c : Code) (x : List Bool) :
(TM0.eval c.machine (input x)).Dom ↔ ∃ T, (c.evalSteps x T).isSomestructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def input (x : List Bool) : List ℕ := x.map bitSymCSLibExt/Computability/Machines/Turing/Universal/Code.lean:120
Every finite machine has a code
TheoremUniversality of codes#✓fully proved
Universality of codes, for machines that read bit inputs. Let \(M\) be a single-tape Turing machine with a finite alphabet \(\Gamma\) and a finite set of states that contains the initial state and is closed under the transitions of \(M\), and let \(\iota\) be an injective map from the bits to \(\Gamma\) whose values are not the blank. Then there are a code \(c\) and an injective map \(f\) from \(\Gamma\) to the natural numbers, sending the blank to \(0\) and each \(\iota(b)\) to the symbol of the bit \(b\), such that for every word \(l\) over \(\Gamma\), writing \(f(l)\) for the word obtained by applying \(f\) to each letter: the decoded machine of \(c\) halts on \(f(l)\) exactly when \(M\) halts on \(l\), and its result (the tape from the head rightwards when it halts) is then the result of \(M\) on \(l\) with \(f\) applied to each cell; and for every \(T \in \mathbb{N}\), the decoded machine of \(c\) halts within \(T\) steps on \(f(l)\) if and only if \(M\) halts within \(T\) steps on \(l\).
(So the alphabet has at least three symbols; a machine over a smaller alphabet cannot read a bit input.)
theorem exists_code [Finite Γ] (M : TM0.Machine Γ Λ) {S : Set Λ} (hS : TM0.Supports M S)
(hSf : S.Finite) (ι : Bool → Γ) (hι : Function.Injective ι) (hι0 : ∀ b, ι b ≠ default) :
∃ (c : Code) (f : PointedMap Γ ℕ), Function.Injective f ∧ (∀ b, f (ι b) = bitSym b) ∧
(∀ l, TM0.eval c.machine (l.map f) = (TM0.eval M l).map (ListBlank.map f)) ∧
∀ l T, HaltsWithin c.machine (l.map f) T ↔ HaltsWithin M l Tstructure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
def bitSym (b : Bool) : ℕ := cond b 2 1CSLibExt/Computability/Machines/Turing/Universal/Code.lean:117
def HaltsWithin (M : TM0.Machine Γ Λ) (l : List Γ) (T : ℕ) : Prop :=
∃ j ≤ T, ∃ d, (flip bind (TM0.step M))^[j] (some (TM0.init l)) = some d ∧ TM0.step M d = noneCSLibExt/Computability/Machines/Turing/Universal/Code.lean:83
Uses 6
Primitive recursiveness
TheoremThe clocked evaluator is primitive recursive#✓fully proved
The clocked evaluator is primitive recursive in the code, the input and the clock.
theorem primrec_evalSteps :
Primrec fun p : Code × List Bool × ℕ ↦ p.1.evalSteps p.2.1 p.2.2structure Code where
/-- The transition table, indexed by state, then by symbol. -/
table : List (List (Option (ℕ × ℕ)))
deriving DecidableEqCSLibExt/Computability/Machines/Turing/Universal/Code.lean:105
Uses 14
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.