Equivalence of Turing machines and recursive functions

TheoremBinary encoding, least significant bit first#✓fully proved

For every natural number \(n \neq 0\), the binary encoding of \(n\) is the list whose first bit is true exactly when \(n\) is odd, followed by the binary encoding of \(\lfloor n/2 \rfloor\).

theorem encodeNat_eq_cons {n : ℕ} (hn : n ≠ 0) :
    encodeNat n = decide (n % 2 = 1) :: encodeNat (n / 2)
Used by 20
Used byThe input encoding of the single-tape emulation is primitive recursive · Halting of a linear bounded automaton on binary codes is decidable · Turing-computable functions are recursive · The halting set of a multi-stack machine is r.e · A predicate recognizable by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine is recursively enumerable · A predicate decided by a multi-tape machine has a recursively enumerable complement · Computable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines · Binary codes of natural numbers in a tape alphabet are primitive recursive · Recovering a word from its input code · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Quadratic run of the padding machine on canonical instances · Doubling pass maps a number block to the block of its double · A bit list without trailing false is the binary code of its value · Addition is correct on canonical numbers · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Emptiness of a linear bounded automaton on computable input slices is undecidable

DefinitionValue of a little-endian bit list#✓fully proved

The value of a list of bits \(b_0, b_1, \dots, b_{m-1}\) is \(\sum_{i < m} [b_i]\, 2^i\), where \([b_i]\) is \(1\) if \(b_i\) is true and \(0\) otherwise. So the first bit is the least significant, and the empty list has value \(0\).

def bitsVal (l : List Bool) : ℕ := l.foldr (fun b n ↦ 2 * n + cond b 1 0) 0
Used by 15
Used byTuring-computable functions are recursive · Input code of a bit word · Input decoding · Computable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines · Recovering a word from its input code · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Value of the empty bit list · Value of a bit list with a leading bit · Value of a list of two-bit digits · A bit list without trailing false is the binary code of its value · Binary code of the value of a bit list · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremRunning a primitive recursive machine is partial recursive#✓fully proved

Let \(\alpha\), \(\sigma\) and \(\beta\) be primitive recursively encodable types, and let \(\mathrm{init} : \alpha \to \sigma\), \(\mathrm{step} : \sigma \to \sigma\), \(\mathrm{halted} : \sigma \to \mathrm{Bool}\) and \(\mathrm{out} : \sigma \to \beta\) be primitive recursive. Then the partial function sending \(a\) to \(\mathrm{out}(\mathrm{step}^k(\mathrm{init}(a)))\), where \(k\) is the least natural number for which \(\mathrm{halted}(\mathrm{step}^k(\mathrm{init}(a)))\) is true, and undefined when there is no such \(k\), is partial recursive.

theorem partrec_run {init : α → σ} {step : σ → σ} {halted : σ → Bool} {out : σ → β}
    (hi : Primrec init) (hs : Primrec step) (hh : Primrec halted) (ho : Primrec out) :
    Partrec fun a ↦ (Nat.rfind fun k ↦ Part.some (halted (step^[k] (init a)))).map
      fun k ↦ out (step^[k] (init a))
Used by 2
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e

TheoremEventually constant functions on ℕ are primitive recursive#✓fully proved

Let \(\beta\) be a primitive recursively encodable type. If \(g : \mathbb{N} \to \beta\) and \(N \in \mathbb{N}\) satisfy \(g(c) = g(N)\) for all \(c \ge N\), then \(g\) is primitive recursive.

theorem primrec_of_eventually_const {g : ℕ → β} (N : ℕ) (hg : ∀ c ≥ N, g c = g N) :
    Primrec g
Used by 1
Used byTuring-computable functions are recursive

TheoremEventually constant functions of a finite parameter are primitive recursive#✓fully proved

Let \(\alpha\) be a finite primitive recursively encodable type and \(\beta\) a primitive recursively encodable type. If \(g : \alpha \to \mathbb{N} \to \beta\) and \(N \in \mathbb{N}\) satisfy \(g(a, c) = g(a, N)\) for all \(a \in \alpha\) and all \(c \ge N\), then \(g\) is primitive recursive as a function of two arguments.

theorem primrec₂_of_eventually_const [Finite α] {g : α → ℕ → β} (N : ℕ)
    (hg : ∀ a, ∀ c ≥ N, g a c = g a N) : Primrec₂ g
Used by 1
Used byUpdating the state from the top of a coded stack is primitive recursive

TheoremJoint primitive recursion over a finite first argument#✓fully proved

Let \(\alpha\), \(\beta\) and \(\sigma\) be primitive recursively encodable types with \(\alpha\) finite, and let \(g : \alpha \to \beta \to \sigma\). If \(b \mapsto g(a, b)\) is primitive recursive for every \(a \in \alpha\), then \(g\) is primitive recursive as a function of two arguments.

theorem primrec₂_of_finite_left [Finite α] {σ : Type*} [Primcodable σ] {g : α → β → σ}
    (hg : ∀ a, Primrec (g a)) : Primrec₂ g
Used by 4
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e · Acceptance by an NTM with finite state and tape alphabets is r.e · The coded step of a single-tape machine is primitive recursive

DefinitionEncoding of functions on a finite type#✓fully proved

For a finite type \(K\) and a primitive recursively encodable type \(\beta\), the primitive recursive encoding of the functions \(K \to \beta\) transported from that of the functions \(\mathrm{Fin}\, n \to \beta\), where \(n\) is the cardinality of \(K\), along a chosen bijection between \(K\) and \(\mathrm{Fin}\, n\).

@[instance_reducible]
noncomputable def primcodableArrow (K : Type*) [Fintype K] (β : Type*) [Primcodable β] :
    Primcodable (K → β) :=
  Primcodable.ofEquiv (Fin (Fintype.card K) → β)
    (Equiv.arrowCongr (Fintype.equivFin K) (Equiv.refl β))
Used by 3
Used byTuring-computable functions are recursive · Updating the state from the top of a coded stack is primitive recursive · The halting set of a multi-stack machine is r.e

DefinitionSymbols a statement may push#✓fully proved

For a finite multi-stack machine, a stack \(k\) and a statement \(q\) over the machine's stack alphabets, labels and internal states, the set of symbols of stack \(k\) consisting of every value, at every internal state, of the symbol function of every push instruction onto stack \(k\) that occurs in \(q\), in either branch of each conditional.

def pushes (k : tm.K) : Turing.TM2.Stmt tm.Γ tm.Λ tm.σ → Set (tm.Γ k)
  | .push k' f q => (if h : k' = k then Set.range (h ▸ f) else ∅) ∪ pushes k q
  | .peek _ _ q => pushes k q
  | .pop _ _ q => pushes k q
  | .load _ q => pushes k q
  | .branch _ q₁ q₂ => pushes k q₁ ∪ pushes k q₂
  | .goto _ => ∅
  | .halt => ∅
Used by 6
Used byProblems in P are decided in polynomial time by single-tape machines · Turing-computable functions are recursive · The coded run simulates the machine's run · Relevant symbols of a stack · The initial stacks have only relevant symbols · Enumeration of the relevant symbols of a stack

DefinitionRelevant symbols of a stack#✓fully proved

For a stack index \(k\), the relevant symbols of stack \(k\) are the symbols \(f(v)\) of \(\Gamma_k\), for every internal state \(v\), over all statements that push \(f\) onto stack \(k\) and occur in the program of some label, together with, when \(k\) is the input stack \(k_0\), every symbol of \(\Gamma_{k_0}\).

Along a run started from an initial configuration, only relevant symbols occur on the stacks.

def relevant (k : tm.K) : Set (tm.Γ k) :=
  (⋃ l, pushes tm k (tm.m l)) ∪ {_x | k = tm.k₀}
Uses 1 · Used by 6
Statement usesSymbols a statement may push
Used byProblems in P are decided in polynomial time by single-tape machines · Turing-computable functions are recursive · The coded run simulates the machine's run · Stacks with only relevant symbols · The initial stacks have only relevant symbols · Enumeration of the relevant symbols of a stack

DefinitionEnumeration of the relevant symbols of a stack#✓fully proved

For a finite multi-stack machine and a stack index \(k\), a list without repetitions whose entries are exactly the relevant symbols of stack \(k\), in an order fixed by choice.

noncomputable def symList (k : tm.K) : List (tm.Γ k) := (relevant_finite tm k).toFinset.toList
Uses 2 · Used by 5
Statement usesSymbols a statement may push · Relevant symbols of a stack
Used byCode of a stack symbol · Turing-computable functions are recursive · Decoding a stack symbol · The coded run simulates the machine's run · Updating the state from the top of a coded stack is primitive recursive

DefinitionCode of a stack symbol#✓fully proved

For a finite multi-stack machine, a stack index \(k\) and a symbol \(x\) of stack \(k\), the code of \(x\) is the position of \(x\) (counting from \(0\)) in the chosen enumeration of the relevant symbols of stack \(k\), or the length of that enumeration if \(x\) is not a relevant symbol.

noncomputable def code (k : tm.K) (x : tm.Γ k) : ℕ :=
  letI := Classical.decEq (tm.Γ k)
  (symList tm k).idxOf x
Uses 1 · Used by 6
Statement usesEnumeration of the relevant symbols of a stack
Used byTuring-computable functions are recursive · Coded stacks · Coded stacks after replacing one stack · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e · The coded execution of a statement

DefinitionDecoding a stack symbol#✓fully proved

For a finite multi-stack machine, a stack index \(k\) and a natural number \(c\), the decoding of \(c\) is the entry at position \(c\) (counting from \(0\)) of the chosen enumeration of the relevant symbols of stack \(k\), and is undefined when \(c\) is at least the length of that enumeration.

noncomputable def decode (k : tm.K) (c : ℕ) : Option (tm.Γ k) := (symList tm k)[c]?
Uses 1 · Used by 4
Statement usesEnumeration of the relevant symbols of a stack
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · Updating the state from the top of a coded stack is primitive recursive · Reading the top of a coded stack

DefinitionStacks with only relevant symbols#✓fully proved

A family of stacks \(S\), consisting of a list \(S_k\) of symbols of \(\Gamma_k\) for each stack index \(k\), has only relevant symbols when for every stack index \(k\), every symbol on \(S_k\) is a relevant symbol of stack \(k\).

def Relevant (S : ∀ k, List (tm.Γ k)) : Prop := ∀ k, ∀ x ∈ S k, x ∈ relevant tm k
Uses 1 · Used by 4
Statement usesRelevant symbols of a stack
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e · The initial stacks have only relevant symbols

DefinitionEncoding of labels#✓fully proved

For a finite multi-stack machine, the primitive recursive encoding of its finite type of labels transported from that of \(\mathrm{Fin}\, n\), where \(n\) is the number of labels, along a chosen bijection between the two.

@[instance_reducible]
noncomputable def primcodableΛ : Primcodable tm.Λ :=
  Primcodable.ofEquiv _ (Fintype.equivFin tm.Λ)
Used by 2
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e

DefinitionEncoding of internal states#✓fully proved

For a finite multi-stack machine, the primitive recursive encoding of its finite type of internal states transported from that of \(\mathrm{Fin}\, n\), where \(n\) is the number of internal states, along a chosen bijection between the two.

@[instance_reducible]
noncomputable def primcodableσ : Primcodable tm.σ :=
  Primcodable.ofEquiv _ (Fintype.equivFin tm.σ)
Used by 3
Used byTuring-computable functions are recursive · Updating the state from the top of a coded stack is primitive recursive · The halting set of a multi-stack machine is r.e

AbbreviationCoded configurations of a multi-stack machine#✓fully proved

For a finite multi-stack machine with label set \(\Lambda\), internal state set \(\sigma\) and stack index set \(K\), a coded configuration is a triple consisting of an optional label in \(\Lambda\) (no label marks a halted configuration), an internal state in \(\sigma\), and an assignment of a list of natural numbers to each \(k \in K\).

abbrev CodedCfg := Option tm.Λ × tm.σ × (tm.K → List ℕ)
Used by 7
Used byTuring-computable functions are recursive · Coding a configuration · The coded step on optional configurations · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e · The coded execution of a statement · The coded step

DefinitionCoded stacks#✓fully proved

For a finite multi-stack machine, the coded stacks of a family \(S\) of stacks assign to each stack index \(k\) the list obtained from the stack \(S_k\) by replacing each symbol with its code.

noncomputable def encStk (S : ∀ k, List (tm.Γ k)) : tm.K → List ℕ :=
  fun k ↦ (S k).map (code tm k)
Uses 1 · Used by 5
Statement usesCode of a stack symbol
Used byTuring-computable functions are recursive · Coding a configuration · Coded stacks after replacing one stack · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e

DefinitionCoding a configuration#✓fully proved

For a finite multi-stack machine, the coded configuration of a configuration \(c\) has the same optional label and internal state as \(c\), and the coded stacks of the stacks of \(c\).

noncomputable def enc (c : tm.Cfg) : CodedCfg tm := (c.l, c.var, encStk tm c.stk)
Uses 2 · Used by 3
Statement usesCoded configurations of a multi-stack machine · Coded stacks
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e

DefinitionReading the top of a coded stack#✓fully proved

Let \(k\) be a stack index of the machine and let \(S\) assign to each stack index \(j\) a list \(S_j\) of natural numbers (codes of symbols). The top of stack \(k\) as read from \(S\) is no symbol when \(S_k\) is empty. Otherwise, if \(c\) is the first entry of \(S_k\), it is the decoding of \(c\): the symbol of \(\Gamma_k\) at position \(c\), counting from \(0\), in the list of relevant symbols of stack \(k\), or no symbol when \(c\) is at least the length of that list.

noncomputable def readTop (k : tm.K) (S : tm.K → List ℕ) : Option (tm.Γ k) :=
  (S k).head?.bind (decode tm k)
Uses 1 · Used by 5
Statement usesDecoding a stack symbol
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · Updating the state from the top of a coded stack is primitive recursive · The halting set of a multi-stack machine is r.e · The coded execution of a statement

DefinitionThe coded execution of a statement#✓fully proved

This mirrors the machine's execution of one statement on stacks of symbol codes. Given a statement \(q\), an internal state \(v\) and coded stacks \(S\) (a list \(S_k\) of natural numbers for each stack index \(k\)), it returns a coded configuration (an optional label, an internal state and coded stacks), by recursion on \(q\). A push of \(f\) onto stack \(k\) followed by \(q'\) replaces \(S_k\) by the code of the symbol \(f(v)\) of stack \(k\) followed by \(S_k\), and continues with \(q'\). A peek at stack \(k\) with update \(f\) followed by \(q'\) continues with \(q'\) from the internal state \(f(v, t)\), where \(t\) is the top of coded stack \(k\) as read from \(S\). A pop is the same as a peek but also removes the first entry of \(S_k\) (if there is one). A load of \(a\) followed by \(q'\) continues with \(q'\) from the internal state \(a(v)\). A branch on \(f\) executes its first statement if \(f(v)\) is true and its second otherwise. A goto \(f\) stops with label \(f(v)\), internal state \(v\) and stacks \(S\), and a halt stops with no label, internal state \(v\) and stacks \(S\).

noncomputable def stepAuxC :
    Turing.TM2.Stmt tm.Γ tm.Λ tm.σ → tm.σ → (tm.K → List ℕ) → CodedCfg tm
  | .push k f q, v, S => stepAuxC q v (Function.update S k (code tm k (f v) :: S k))
  | .peek k f q, v, S => stepAuxC q (f v (readTop tm k S)) S
  | .pop k f q, v, S => stepAuxC q (f v (readTop tm k S)) (Function.update S k (S k).tail)
  | .load a q, v, S => stepAuxC q (a v) S
  | .branch f q₁ q₂, v, S => cond (f v) (stepAuxC q₁ v S) (stepAuxC q₂ v S)
  | .goto f, v, S => (some (f v), v, S)
  | .halt, v, S => (none, v, S)
Uses 3 · Used by 4
Statement usesCoded configurations of a multi-stack machine · Code of a stack symbol · Reading the top of a coded stack
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e · The coded step

DefinitionThe coded step#✓fully proved

For a coded configuration \((l, v, S)\), consisting of an optional label \(l\), an internal state \(v\) and coded stacks \(S\), the coded step is undefined when \(l\) is absent (the configuration has halted). When \(l\) is a label, it is the coded configuration obtained by the coded execution of the program statement of \(l\) from the internal state \(v\) on the coded stacks \(S\).

noncomputable def stepC (c : CodedCfg tm) : Option (CodedCfg tm) :=
  c.1.map fun l ↦ stepAuxC tm (tm.m l) c.2.1 c.2.2
Uses 2 · Used by 4
Statement usesCoded configurations of a multi-stack machine · The coded execution of a statement
Used byTuring-computable functions are recursive · The coded step on optional configurations · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e

TheoremUpdating the state from the top of a coded stack is primitive recursive#✓fully proved

Let \(k\) be a stack index of a finite multi-stack machine, write \(\Gamma_k\) for the alphabet of stack \(k\), and let \(f\) be any function sending an internal state and an optional symbol of \(\Gamma_k\) to an internal state. Then the map sending an internal state \(v\) and coded stacks \(S\) (a list \(S_j\) of natural numbers for each stack index \(j\)) to \(f(v, t)\), where \(t\) is the top of stack \(k\) as read from \(S\), is primitive recursive as a function of two arguments, for the encoding of internal states and the encoding of functions on the finite type of stack indices.

theorem primrec₂_readTop {k : tm.K} {f : tm.σ → Option (tm.Γ k) → tm.σ} :
    Primrec₂ fun (v : tm.σ) (S : tm.K → List ℕ) ↦ f v (readTop tm k S)
Uses 6 · Used by 2
Statement usesEncoding of functions on a finite type · Encoding of internal states · Reading the top of a coded stack
Proof usesDecoding a stack symbol · Eventually constant functions of a finite parameter are primitive recursive · Enumeration of the relevant symbols of a stack
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e

TheoremCoded stacks after replacing one stack#✓fully proved

For a finite multi-stack machine, a family \(S\) of stacks, a stack index \(k\) and a list \(l\) of symbols of stack \(k\), the coded stacks of the family obtained from \(S\) by replacing stack \(k\) with \(l\) are the coded stacks of \(S\) with the entry at \(k\) replaced by the list obtained from \(l\) by replacing each symbol with its code.

theorem encStk_update (S : ∀ k, List (tm.Γ k)) (k : tm.K) (l : List (tm.Γ k)) :
    encStk tm (Function.update S k l) = Function.update (encStk tm S) k (l.map (code tm k))
Uses 2 · Used by 1
Statement usesCode of a stack symbol · Coded stacks
Used byThe coded run simulates the machine's run

DefinitionThe coded step on optional configurations#✓fully proved

For a finite multi-stack machine, the coded step extended to optional coded configurations: it sends the absent configuration to the absent configuration, and a coded configuration \(c\) to the coded step of \(c\), which is itself absent when \(c\) has halted.

noncomputable def optStepC (o : Option (CodedCfg tm)) : Option (CodedCfg tm) := o.bind (stepC tm)
Uses 2 · Used by 3
Statement usesCoded configurations of a multi-stack machine · The coded step
Used byTuring-computable functions are recursive · The coded run simulates the machine's run · The halting set of a multi-stack machine is r.e

TheoremThe coded run simulates the machine's run#✓fully proved

Let \(o\) be either no configuration or a configuration of a finite multi-stack machine all of whose stack symbols are relevant. Let running one step send a running configuration to its successor, and a halted configuration or no configuration to no configuration. Then for every \(j\), applying the coded step on optional configurations \(j\) times to the coding of \(o\) gives the coding of the result of running \(j\) steps from \(o\), and if running \(j\) steps from \(o\) gives a configuration, all of its stack symbols are relevant.

theorem optStepC_iterate (j : ℕ) {o : Option tm.Cfg} (ho : ∀ c ∈ o, Relevant tm c.stk) :
    (optStepC tm)^[j] (o.map (enc tm)) = ((flip bind tm.step)^[j] o).map (enc tm) ∧
      ∀ c ∈ (flip bind tm.step)^[j] o, Relevant tm c.stk
Uses 14 · Used by 2
Statement usesCoded configurations of a multi-stack machine · Stacks with only relevant symbols · Coding a configuration · The coded step on optional configurations
Proof usesCode of a stack symbol · Decoding a stack symbol · Coded stacks · Coded stacks after replacing one stack · Symbols a statement may push · Reading the top of a coded stack · Relevant symbols of a stack · The coded execution of a statement · The coded step · Enumeration of the relevant symbols of a stack
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e

TheoremThe initial stacks have only relevant symbols#✓fully proved

For a finite multi-stack machine and every list \(s\) of symbols of the input alphabet \(\Gamma_{k_0}\), the stacks of the initial configuration with input \(s\) (the list \(s\) on the input stack \(k_0\) and every other stack empty) have only relevant symbols.

theorem relevant_initList (s : List (tm.Γ tm.k₀)) : Relevant tm (initList tm s).stk
Uses 3 · Used by 2
Statement usesStacks with only relevant symbols
Proof usesSymbols a statement may push · Relevant symbols of a stack
Used byTuring-computable functions are recursive · The halting set of a multi-stack machine is r.e

TheoremConfigurations before a reached one are running#✓fully proved

Write \(\mathrm{step}\) for the machine's step map, which is undefined on halted configurations (those with no label), and iterate it as a partial map. Let \(c_0\) and \(c\) be configurations and \(s\) a natural number such that \(s\) steps from \(c_0\) reach \(c\). Then for every \(j < s\), \(j\) steps from \(c_0\) reach some configuration \(c'\), and \(c'\) is running: its label is defined.

theorem running_before_halt {c₀ : tm.Cfg} {s : ℕ} {c : tm.Cfg}
    (hs : (flip bind tm.step)^[s] (some c₀) = some c) {j : ℕ} (hj : j < s) :
    ∃ c', (flip bind tm.step)^[j] (some c₀) = some c' ∧ c'.l.isSome
Used by 1
Used byTuring-computable functions are recursive

TheoremTuring-computable functions are recursive#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) and suppose that some finite multi-stack Turing machine (finitely many stacks, labels and internal states, and a finite input alphabet), together with identifications of its input and output stack alphabets with the booleans, computes \(f\) under the binary encoding of natural numbers (least significant bit first, with \(0\) encoded as the empty list): for every \(n\), the machine started at its main label in its initial internal state, with the encoding of \(n\) on its input stack and all other stacks empty, eventually reaches the halted configuration whose output stack holds the encoding of \(f(n)\), whose other stacks are empty and whose internal state is the initial one. Then \(f\) is computable (recursive).

theorem computable_of_tm2Computable {f : ℕ → ℕ} (h : TM2Computable encodeNat encodeNat f) :
    Computable f
Uses 25 · Used by 3
Proof usesCoded configurations of a multi-stack machine · Stacks with only relevant symbols · Value of a little-endian bit list · Code of a stack symbol · Decoding a stack symbol · Coding a configuration · Coded stacks · Binary encoding, least significant bit first · The coded step on optional configurations · The coded run simulates the machine's run · Running a primitive recursive machine is partial recursive · Encoding of functions on a finite type · Encoding of labels · Encoding of internal states · Eventually constant functions on ℕ are primitive recursive · Joint primitive recursion over a finite first argument · Updating the state from the top of a coded stack is primitive recursive · Symbols a statement may push · Reading the top of a coded stack · Relevant symbols of a stack · The initial stacks have only relevant symbols · Configurations before a reached one are running · The coded execution of a statement · The coded step · Enumeration of the relevant symbols of a stack
Used byMulti-stack decidable predicates are exactly the computable predicates · Mapping reductions are computed by multi-stack machines · Turing computable equals recursive

DefinitionBits as stack symbols#✓fully proved

Let \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\) be the stack alphabet of Mathlib's multi-stack machine \(\mathrm{tr}\) that evaluates partial recursive codes. This is the map from bits to \(\Gamma'\) that sends \(\mathrm{true}\) to \(\mathtt{bit1}\) and \(\mathrm{false}\) to \(\mathtt{bit0}\).

def boolToΓ' : Bool → Γ'
  | true => Γ'.bit1
  | false => Γ'.bit0
Used by 9
Used byThe program of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined · The evaluator's encoding of a one-element list · The evaluator encodes numbers in binary

DefinitionReading a stack symbol as a bit#✓fully proved

The map from the stack alphabet \(\Gamma'\) of Mathlib's code evaluator (symbols \(\mathrm{cons}_l\), \(\mathrm{cons}\), \(\mathrm{bit0}\), \(\mathrm{bit1}\)) to the booleans sends \(\mathrm{bit1}\) to true and every other symbol to false.

def Γ'ToBool : Γ' → Bool
  | Γ'.bit1 => true
  | _ => false
Used by 2
Used byThe program of the wrapped machine · Post-phase of the wrapped machine

TheoremThe evaluator encodes numbers in binary#✓fully proved

For every natural number \(n\), the list of stack symbols by which Mathlib's code evaluator encodes \(n\) is obtained from the binary encoding of \(n\) (least significant bit first) by writing each bit as \(\mathrm{bit1}\) if it is true and as \(\mathrm{bit0}\) if it is false.

theorem trNat_eq_map (n : ℕ) : trNat n = (encodeNat n).map boolToΓ'
Uses 1 · Used by 1
Statement usesBits as stack symbols
Used byThe evaluator's encoding of a one-element list

DefinitionThe stack set \(K'\) is finite#✓fully proved

The set \(K' = \{\mathrm{main}, \mathrm{rev}, \mathrm{aux}, \mathrm{stack}\}\) of the four stacks of Mathlib's multi-stack machine that evaluates partial recursive codes is a finite type whose elements are exactly these four stacks.

@[instance_reducible]
def fintypeK' : Fintype K' :=
  ⟨{K'.main, K'.rev, K'.aux, K'.stack}, fun k ↦ by cases k <;> simp⟩
Used by 1
Used byThe wrapped machine of a code

InductiveAdapter labels#✓fully proved

The type with exactly the five elements pre0, pre1, pre2, post1 and post2, with decidable equality.

They label the wrapped machine's pre-phase, which copies the input bits onto the main stack of Mathlib's code-evaluating machine \(\mathrm{tr}\), and its post-phase, which copies the result back to the output stack.

inductive Phase
  | pre0 | pre1 | pre2 | post1 | post2
  deriving DecidableEq
Used by 12
Used byLabels of the wrapped machine · The program of the wrapped machine · The wrapped machine of a code · Correspondence of labels between the code evaluator and the wrapped machine · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

AbbreviationStack alphabets of the wrapped machine#✓fully proved

Let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates partial recursive codes, with stacks \(K' = \{\mathrm{main}, \mathrm{rev}, \mathrm{aux}, \mathrm{stack}\}\) and alphabet \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\). The stacks of the wrapped machine are indexed by \(K' \sqcup \{\mathrm{false}, \mathrm{true}\}\): each stack in \(K'\) has alphabet \(\Gamma'\), and the two stacks \(\mathrm{false}\) and \(\mathrm{true}\) (the input and output stacks of the wrapped machine) have the alphabet \(\{\mathrm{false}, \mathrm{true}\}\) of bits.

abbrev FΓ : K' ⊕ Bool → Type := Sum.elim (fun _ ↦ Γ') (fun _ ↦ Bool)
Used by 16
Used byConfigurations of the wrapped machine · One step of the wrapped machine · Statements of the wrapped machine · The program of the wrapped machine · The wrapped machine of a code · Lifting stacks of tr · Main phase of the wrapped machine · Stack contents of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined · Simulation relation between the code evaluator and the wrapped machine

AbbreviationSupport of a code#✓fully proved

For a code \(c\), the support of \(c\) is the finite set of labels of Mathlib's code evaluator \(\mathrm{tr}\) that Mathlib associates with evaluating \(c\) under the halting continuation.

It contains the label at which this evaluation starts and is closed under the steps of \(\mathrm{tr}\), so it contains every label reachable from there.

abbrev supp : Finset Λ' := codeSupp c Cont'.halt
Used by 13
Used byLabels of the wrapped machine · The program of the wrapped machine · The wrapped machine of a code · Correspondence of labels between the code evaluator and the wrapped machine · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The start label lies in the support · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

AbbreviationLabels of the wrapped machine#✓fully proved

Let \(c\) be a partial recursive code and let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates such codes. The labels of the wrapped machine for \(c\) form the disjoint union \(\mathrm{Phase} \sqcup \mathrm{supp}(c)\), where \(\mathrm{Phase} = \{\mathrm{pre}_0, \mathrm{pre}_1, \mathrm{pre}_2, \mathrm{post}_1, \mathrm{post}_2\}\) is the set of five adapter labels and \(\mathrm{supp}(c)\) is Mathlib's support of \(\mathrm{tr}\) for \(c\) with the halting continuation: a finite set of labels of \(\mathrm{tr}\) that contains the start label for \(c\) and is closed under the steps of \(\mathrm{tr}\).

abbrev FΛ := Phase ⊕ {l // l ∈ supp c}
Uses 2 · Used by 15
Statement usesAdapter labels · Support of a code
Used byConfigurations of the wrapped machine · One step of the wrapped machine · Statements of the wrapped machine · The program of the wrapped machine · The wrapped machine of a code · Correspondence of labels between the code evaluator and the wrapped machine · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined · Simulation relation between the code evaluator and the wrapped machine

AbbreviationStatements of the wrapped machine#✓fully proved

Let \(c\) be a partial recursive code, and let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates such codes, with stacks \(K' = \{\mathrm{main}, \mathrm{rev}, \mathrm{aux}, \mathrm{stack}\}\) and alphabet \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\). A statement of the wrapped machine for \(c\) is a statement of Mathlib's multi-stack (TM2) Turing machine model whose stacks are indexed by \(K' \sqcup \{\mathrm{false}, \mathrm{true}\}\), where each stack in \(K'\) has alphabet \(\Gamma'\) and the stacks \(\mathrm{false}\) and \(\mathrm{true}\) have the alphabet \(\{\mathrm{false}, \mathrm{true}\}\) of bits, whose labels are the labels of the wrapped machine for \(c\), and whose internal states are the optional symbols of \(\Gamma'\) (a symbol of \(\Gamma'\), or none).

abbrev FStmt := TM2.Stmt FΓ (FΛ c) (Option Γ')
Uses 2 · Used by 4
Statement usesStack alphabets of the wrapped machine · Labels of the wrapped machine
Used byThe program of the wrapped machine · Main phase of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The wrapped machine of a code halts exactly where the code is defined

DefinitionRestricting a statement of the code evaluator to the wrapped machine#✓fully proved

Let \(\mathrm{tr}\) be Mathlib's four-stack machine that evaluates partial recursive codes, and let \(S\) be the support of a code \(c\). A statement \(q\) of \(\mathrm{tr}\) all of whose jump targets lie in \(S\) becomes a statement of the wrapped machine of \(c\) with the same structure: each push, peek and pop acts on the same stack of \(\mathrm{tr}\) inside the wrapped machine with the same function, loads and branches are kept, each jump goes to the same label of \(\mathrm{tr}\), now read as an element of \(S\), and halting becomes a jump to the first post-phase label.

noncomputable def restrict :
    (q : TM2.Stmt (fun _ : K' ↦ Γ') Λ' (Option Γ')) → TM2.SupportsStmt (supp c) q → FStmt c
  | .push k f q, hq => .push (Sum.inl k) f (restrict q hq)
  | .peek k f q, hq => .peek (Sum.inl k) f (restrict q hq)
  | .pop k f q, hq => .pop (Sum.inl k) f (restrict q hq)
  | .load a q, hq => .load a (restrict q hq)
  | .branch p q₁ q₂, hq => .branch p (restrict q₁ hq.1) (restrict q₂ hq.2)
  | .goto l, hq => .goto fun v ↦ Sum.inr ⟨l v, hq v⟩
  | .halt, _ => .goto fun _ ↦ Sum.inl Phase.post1
Uses 5 · Used by 3
Statement usesStatements of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Support of a code
Used byThe program of the wrapped machine · Main phase of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined

TheoremThe start label lies in the support#✓fully proved

For every code \(c\), the label at which Mathlib's code evaluator \(\mathrm{tr}\) begins evaluating \(c\) with the halting continuation belongs to the support of \(c\).

theorem start_mem : trNormal c Cont'.halt ∈ supp c
Uses 1 · Used by 5
Statement usesSupport of a code
Used byThe program of the wrapped machine · Main phase of the wrapped machine · Pre-phase of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

DefinitionThe program of the wrapped machine#✓fully proved

Let \(c\) be a partial recursive code and let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates such codes, with stacks \(\mathrm{main}, \mathrm{rev}, \mathrm{aux}, \mathrm{stack}\) and alphabet \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\). The program of the wrapped machine for \(c\) assigns a statement to each of its labels, namely the five adapter labels \(\mathrm{pre}_0, \mathrm{pre}_1, \mathrm{pre}_2, \mathrm{post}_1, \mathrm{post}_2\) and the labels in Mathlib's finite support \(\mathrm{supp}(c)\) of \(\mathrm{tr}\) for \(c\) with the halting continuation. The internal state \(v\) is a symbol of \(\Gamma'\) or none, the input stack is the bit stack \(\mathrm{false}\) and the output stack is the bit stack \(\mathrm{true}\).

At \(\mathrm{pre}_0\): push \(\mathtt{cons}\) onto \(\mathrm{main}\) and go to \(\mathrm{pre}_1\).

At \(\mathrm{pre}_1\): pop the input stack and set \(v\) to the popped bit as a symbol of \(\Gamma'\) (\(\mathtt{bit1}\) for \(\mathrm{true}\), \(\mathtt{bit0}\) for \(\mathrm{false}\)), or to none if the input stack is empty; if \(v\) is a symbol, push it onto \(\mathrm{rev}\) and go to \(\mathrm{pre}_1\), otherwise go to \(\mathrm{pre}_2\).

At \(\mathrm{pre}_2\): pop \(\mathrm{rev}\) and set \(v\) to the popped symbol (none if \(\mathrm{rev}\) is empty); if \(v\) is a symbol, push it onto \(\mathrm{main}\) and go to \(\mathrm{pre}_2\), otherwise go to the start label of \(\mathrm{tr}\) for \(c\) with the halting continuation, which lies in \(\mathrm{supp}(c)\).

At a label \(l \in \mathrm{supp}(c)\): execute the statement of \(\mathrm{tr}\) at \(l\), acting on the stacks of \(\mathrm{tr}\), where every jump of \(\mathrm{tr}\) becomes a jump to the same label in \(\mathrm{supp}(c)\) and every halt becomes a jump to \(\mathrm{post}_1\).

At \(\mathrm{post}_1\): pop \(\mathrm{main}\) and set \(v\) to the popped symbol (none if \(\mathrm{main}\) is empty); if \(v\) is none or \(\mathtt{cons}\), go to \(\mathrm{post}_2\), otherwise push \(v\) onto \(\mathrm{rev}\) and go to \(\mathrm{post}_1\).

At \(\mathrm{post}_2\): pop \(\mathrm{rev}\) and set \(v\) to the popped symbol (none if \(\mathrm{rev}\) is empty); if \(v\) is a symbol, push onto the output stack the bit that is \(\mathrm{true}\) if \(v = \mathtt{bit1}\) and \(\mathrm{false}\) otherwise, and go to \(\mathrm{post}_2\); otherwise halt.

MetaMathlibExt.TM2Recursive.fwdProg · 25 lines 
noncomputable def fwdProg : FΛ c → FStmt c
  | Sum.inl Phase.pre0 =>
    .push (Sum.inl K'.main) (fun _ ↦ Γ'.cons) (.goto fun _ ↦ Sum.inl Phase.pre1)
  | Sum.inl Phase.pre1 =>
    .pop (Sum.inr false) (fun _ ob ↦ ob.map boolToΓ')
      (.branch Option.isSome
        (.push (Sum.inl K'.rev) (fun v ↦ v.getD default) (.goto fun _ ↦ Sum.inl Phase.pre1))
        (.goto fun _ ↦ Sum.inl Phase.pre2))
  | Sum.inl Phase.pre2 =>
    .pop (Sum.inl K'.rev) (fun _ o ↦ o)
      (.branch Option.isSome
        (.push (Sum.inl K'.main) (fun v ↦ v.getD default) (.goto fun _ ↦ Sum.inl Phase.pre2))
        (.goto fun _ ↦ Sum.inr ⟨trNormal c Cont'.halt, start_mem c⟩))
  | Sum.inr l => restrict c (tr l.1) ((tr_supports c Cont'.halt).2 l.1 l.2)
  | Sum.inl Phase.post1 =>
    .pop (Sum.inl K'.main) (fun _ o ↦ o)
      (.branch (fun v ↦ v.elim true fun g ↦ g = Γ'.cons)
        (.goto fun _ ↦ Sum.inl Phase.post2)
        (.push (Sum.inl K'.rev) (fun v ↦ v.getD default) (.goto fun _ ↦ Sum.inl Phase.post1)))
  | Sum.inl Phase.post2 =>
    .pop (Sum.inl K'.rev) (fun _ o ↦ o)
      (.branch Option.isSome
        (.push (Sum.inr true) (fun v ↦ Γ'ToBool (v.getD default))
          (.goto fun _ ↦ Sum.inl Phase.post2))
        .halt)
Uses 9 · Used by 8
Statement usesStatements of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Restricting a statement of the code evaluator to the wrapped machine · The start label lies in the support · Support of a code · Reading a stack symbol as a bit
Used byOne step of the wrapped machine · The wrapped machine of a code · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined

DefinitionThe wrapped machine of a code#✓fully proved

Let \(c\) be a code for a partial recursive function on lists of natural numbers, and let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates such codes, with stacks \(K' = \{\mathrm{main}, \mathrm{rev}, \mathrm{aux}, \mathrm{stack}\}\) and alphabet \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\). The wrapped machine of \(c\) is the finite multi-stack machine whose stacks are indexed by \(K' \sqcup \{\mathrm{false}, \mathrm{true}\}\), with alphabet \(\Gamma'\) on each stack in \(K'\) and the alphabet of bits on the stacks \(\mathrm{false}\) and \(\mathrm{true}\); its input stack is \(\mathrm{false}\) and its output stack is \(\mathrm{true}\); its labels are the labels of the wrapped machine for \(c\), with main label the first pre-phase adapter label \(\mathrm{pre}_0\); its internal states are the optional symbols of \(\Gamma'\) (a symbol of \(\Gamma'\), or none), with initial state none; and its program is the program of the wrapped machine for \(c\).

noncomputable def fwdTM : FinTM2 where
  K := K' ⊕ Bool
  k₀ := Sum.inr false
  k₁ := Sum.inr true
  Γ := FΓ
  Λ := FΛ c
  main := Sum.inl Phase.pre0
  σ := Option Γ'
  initialState := none
  Γk₀Fin := inferInstanceAs (Fintype Bool)
  m := fwdProg c
Uses 6 · Used by 4
Statement usesStack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · The stack set \(K'\) is finite · The program of the wrapped machine · Support of a code
Used byEvery r.e. predicate is the halting set of a machine with finite alphabets · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined · Computable predicates are decidable by single-tape machines

DefinitionStack contents of the wrapped machine#✓fully proved

Given lists \(a, b, c, d\) of symbols of \(\Gamma'\) and lists \(i, o\) of bits, the stack contents of the wrapped machine with \(a\), \(b\), \(c\) and \(d\) on the stacks main, rev, aux and stack, \(i\) on the input stack and \(o\) on the output stack.

def mkStk (a b c' d : List Γ') (i o : List Bool) : ∀ k, List (FΓ k)
  | Sum.inl K'.main => a
  | Sum.inl K'.rev => b
  | Sum.inl K'.aux => c'
  | Sum.inl K'.stack => d
  | Sum.inr false => i
  | Sum.inr true => o
Uses 1 · Used by 8
Statement usesStack alphabets of the wrapped machine
Used byLifting stacks of tr · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

AbbreviationConfigurations of the wrapped machine#✓fully proved

Let \(c\) be a partial recursive code, and let \(\Gamma' = \{\mathtt{cons}_l, \mathtt{cons}, \mathtt{bit0}, \mathtt{bit1}\}\) be the alphabet of Mathlib's multi-stack machine \(\mathrm{tr}\) that evaluates such codes. A configuration of the wrapped machine for \(c\) is a configuration of Mathlib's multi-stack (TM2) Turing machine model with the stack alphabets and labels of the wrapped machine for \(c\) and internal states the optional symbols of \(\Gamma'\): it consists of an optional current label (none once the machine has halted), an internal state that is a symbol of \(\Gamma'\) or none, and for each stack \(k\) a finite list of symbols of the alphabet of \(k\).

abbrev FCfg := TM2.Cfg FΓ (FΛ c) (Option Γ')
Uses 2 · Used by 10
Statement usesStack alphabets of the wrapped machine · Labels of the wrapped machine
Used byIterated steps of the wrapped machine · One step of the wrapped machine · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined · Simulation relation between the code evaluator and the wrapped machine

AbbreviationOne step of the wrapped machine#✓fully proved

For a partial recursive code \(c\), the step function of the wrapped machine for \(c\) is Mathlib's multi-stack (TM2) step function for the program of the wrapped machine for \(c\). It sends a configuration without a current label (a halted one) to none, and a configuration with current label \(l\) to the configuration obtained by executing the statement that the program assigns to \(l\) on its internal state and stacks.

noncomputable abbrev fstep : FCfg c → Option (FCfg c) := TM2.step (fwdProg c)
Uses 4 · Used by 8
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · The program of the wrapped machine
Used byIterated steps of the wrapped machine · Main phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

AbbreviationIterated steps of the wrapped machine#✓fully proved

Let \(c\) be a partial recursive code and let \(s\) be the map that sends none to none and a configuration \(d\) of the wrapped machine for \(c\) to the result of one step of the wrapped machine on \(d\) (which is none if \(d\) has halted). For \(j \in \mathbb{N}\) and \(x\) either a configuration of the wrapped machine for \(c\) or none, the \(j\)-fold run from \(x\) is \(s^{j}(x)\), the result of applying \(s\) to \(x\) \(j\) times.

noncomputable abbrev frun (j : ℕ) (x : Option (FCfg c)) : Option (FCfg c) :=
  (flip bind (fstep c))^[j] x
Uses 2 · Used by 7
Statement usesConfigurations of the wrapped machine · One step of the wrapped machine
Used byMain phase of the wrapped machine · Post-phase of the wrapped machine · The first post-phase loop of the wrapped machine · Pre-phase of the wrapped machine · The first pre-phase loop of the wrapped machine · The wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

TheoremThe first pre-phase loop of the wrapped machine#✓fully proved

Write \(\Gamma'\) for the stack alphabet of Mathlib's code evaluator. Let \(c\) be a code, \(a\), \(r\), \(x\) and \(y\) lists of symbols of \(\Gamma'\), \(b\) a list of bits of length \(k\) and \(v\) an internal state (a symbol of \(\Gamma'\) or none), and write \(\beta(b)\) for \(b\) with each bit \(\mathrm{true}\) replaced by the symbol bit1 and each bit \(\mathrm{false}\) by the symbol bit0 of \(\Gamma'\). Started at the adapter label pre1 with internal state \(v\), the lists \(a\), \(r\), \(x\) and \(y\) on the stacks main, rev, aux and stack, \(b\) on the input stack and the output stack empty, the wrapped machine of \(c\) is after exactly \(k + 1\) steps at the adapter label pre2 with internal state none, the reversal of \(\beta(b)\) followed by \(r\) on the rev stack, \(a\), \(x\) and \(y\) still on the stacks main, aux and stack, and the input and output stacks empty.

theorem pre1_loop (a b c' d : List Γ') (bits : List Bool) (v : Option Γ') :
    frun c (bits.length + 1) (some ⟨some (Sum.inl Phase.pre1), v, mkStk a b c' d bits []⟩) =
      some ⟨some (Sum.inl Phase.pre2), none,
        mkStk a ((bits.map boolToΓ').reverse ++ b) c' d [] []⟩
Uses 10 · Used by 1
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Iterated steps of the wrapped machine · Stack contents of the wrapped machine · Support of a code
Proof usesOne step of the wrapped machine · The program of the wrapped machine
Used byPre-phase of the wrapped machine

TheoremPre-phase of the wrapped machine#✓fully proved

Let \(c\) be a code and \(b\) a list of bits of length \(k\), and write \(\beta(b)\) for \(b\) with each bit \(0\) replaced by the symbol bit0 and each bit \(1\) by the symbol bit1 of \(\Gamma'\). Started at the adapter label pre0 with empty local state, \(b\) on the input stack and all other stacks empty, the wrapped machine is after exactly \(2(k + 1) + 1\) steps at the label \(\mathrm{trNormal}(c, \mathrm{halt})\) at which Mathlib's code-evaluating machine \(\mathrm{tr}\) starts evaluating \(c\), with empty local state, \(\beta(b)\) followed by the symbol cons on the main stack and all other stacks empty.

theorem pre_phase (bits : List Bool) :
    frun c (bits.length + 1 + (bits.length + 1) + 1)
        (some ⟨some (Sum.inl Phase.pre0), none, mkStk [] [] [] [] bits []⟩) =
      some ⟨some (Sum.inr ⟨trNormal c Cont'.halt, start_mem c⟩), none,
        mkStk (bits.map boolToΓ' ++ [Γ'.cons]) [] [] [] [] []⟩
Uses 12 · Used by 2
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Iterated steps of the wrapped machine · Stack contents of the wrapped machine · The start label lies in the support · Support of a code
Proof usesOne step of the wrapped machine · The program of the wrapped machine · The first pre-phase loop of the wrapped machine
Used byThe wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

TheoremThe first post-phase loop of the wrapped machine#✓fully proved

Write \(\Gamma'\) for the stack alphabet of Mathlib's code evaluator. Let \(c\) be a code, \(b\) a list of bits of length \(k\), \(r\) a list of symbols of \(\Gamma'\), \(o\) a list of bits and \(v\) an internal state (a symbol of \(\Gamma'\) or none), and write \(\beta(b)\) for \(b\) with each bit \(\mathrm{true}\) replaced by the symbol bit1 and each bit \(\mathrm{false}\) by the symbol bit0 of \(\Gamma'\). Started at the adapter label post1 with internal state \(v\), \(\beta(b)\) followed by the symbol cons on the main stack, \(r\) on the rev stack, \(o\) on the output stack and all other stacks empty, the wrapped machine of \(c\) is after exactly \(k + 1\) steps at the adapter label post2 with internal state cons, the reversal of \(\beta(b)\) followed by \(r\) on the rev stack, \(o\) on the output stack and all other stacks empty.

theorem post1_loop (bits : List Bool) (r : List Γ') (o : List Bool) (v : Option Γ') :
    frun c (bits.length + 1) (some ⟨some (Sum.inl Phase.post1), v,
        mkStk (bits.map boolToΓ' ++ [Γ'.cons]) r [] [] [] o⟩) =
      some ⟨some (Sum.inl Phase.post2), some Γ'.cons,
        mkStk [] ((bits.map boolToΓ').reverse ++ r) [] [] [] o⟩
Uses 10 · Used by 1
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Iterated steps of the wrapped machine · Stack contents of the wrapped machine · Support of a code
Proof usesOne step of the wrapped machine · The program of the wrapped machine
Used byPost-phase of the wrapped machine

TheoremPost-phase of the wrapped machine#✓fully proved

Let \(c\) be a code and \(b\) a list of bits of length \(k\), and write \(\beta(b)\) for \(b\) with each bit \(0\) replaced by the symbol bit0 and each bit \(1\) by the symbol bit1 of \(\Gamma'\). Started at the adapter label post1 with empty local state, \(\beta(b)\) followed by the symbol cons on the main stack and all other stacks empty, the wrapped machine is after exactly \(2(k + 1)\) steps in the halting configuration (no label) with empty local state, \(b\) on the output stack and all other stacks empty.

theorem post_phase (bits : List Bool) :
    frun c ((bits.length + 1) + (bits.length + 1))
        (some ⟨some (Sum.inl Phase.post1), none,
          mkStk (bits.map boolToΓ' ++ [Γ'.cons]) [] [] [] [] []⟩) =
      some ⟨none, none, mkStk [] [] [] [] [] bits⟩
Uses 12 · Used by 2
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Iterated steps of the wrapped machine · Stack contents of the wrapped machine · Support of a code
Proof usesOne step of the wrapped machine · The program of the wrapped machine · The first post-phase loop of the wrapped machine · Reading a stack symbol as a bit
Used byThe wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

DefinitionLifting stacks of tr#✓fully proved

Given contents \(s\) of the four stacks main, rev, aux and stack of Mathlib's code-evaluating machine \(\mathrm{tr}\), the stack contents of the wrapped machine that agree with \(s\) on these four stacks and have empty input and output stacks.

def liftStk (s : ∀ _ : K', List Γ') : ∀ k, List (FΓ k) :=
  mkStk (s K'.main) (s K'.rev) (s K'.aux) (s K'.stack) [] []
Uses 2 · Used by 3
Statement usesStack alphabets of the wrapped machine · Stack contents of the wrapped machine
Used byMain phase of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined · Simulation relation between the code evaluator and the wrapped machine

DefinitionCorrespondence of labels between the code evaluator and the wrapped machine#✓fully proved

Let \(c\) be a code for a partial recursive function on lists of natural numbers and let \(\mathrm{tr}\) be Mathlib's multi-stack machine that evaluates such codes. An optional label \(o\) of \(\mathrm{tr}\) (a label, or none for halting) corresponds to an optional label \(o'\) of the wrapped machine for \(c\) when either \(o\) is none and \(o'\) is the first post-phase label \(\mathrm{post}_1\), or \(o\) is a label \(l\) of \(\mathrm{tr}\) that lies in the support \(\mathrm{supp}(c)\) of \(c\) and \(o'\) is \(l\), read as a label of the wrapped machine.

def LabelRel : Option Λ' → Option (FΛ c) → Prop
  | none, o' => o' = some (Sum.inl Phase.post1)
  | some l, o' => ∃ h : l ∈ supp c, o' = some (Sum.inr ⟨l, h⟩)
Uses 3 · Used by 3
Statement usesLabels of the wrapped machine · Adapter labels · Support of a code
Used byMain phase of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined · Simulation relation between the code evaluator and the wrapped machine

DefinitionSimulation relation between the code evaluator and the wrapped machine#✓fully proved

A configuration \(x\) of Mathlib's code evaluator \(\mathrm{tr}\) is related to a configuration \(d\) of the wrapped machine of a code \(c\) when \(d\) has the same internal state as \(x\), the stacks of \(d\) are the four stacks of \(x\) together with empty input and output stacks, and the labels correspond: if \(x\) has halted then \(d\) is at the first post-phase label, and if \(x\) is at a label \(l\) then \(l\) lies in the support of \(c\) and \(d\) is at \(l\).

def TrRel (x : Cfg') (d : FCfg c) : Prop :=
  d.var = x.var ∧ d.stk = liftStk x.stk ∧ LabelRel c x.l d.l
Uses 5 · Used by 2
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Correspondence of labels between the code evaluator and the wrapped machine · Lifting stacks of tr
Used byMain phase of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined

TheoremReachability gives an iteration count#✓fully proved

Let \(\alpha\) be a type, let \(\bot \notin \alpha\), and let \(f : \alpha \to \alpha \cup \{\bot\}\) be a partial step function, where \(f(x) = \bot\) means that no step is possible from \(x\). Extend \(f\) to \(\bar f : \alpha \cup \{\bot\} \to \alpha \cup \{\bot\}\) by \(\bar f(\bot) = \bot\). If \(b \in \alpha\) is reachable from \(a \in \alpha\) under \(f\), that is, \(b\) is obtained from \(a\) by finitely many (possibly zero) steps \(x \mapsto f(x)\) none of which gives \(\bot\), then there is \(N \in \mathbb{N}\) with \(\bar f^{N}(a) = b\).

theorem exists_iterate_eq_of_reaches {α : Type*} {f : α → Option α} {a b : α}
    (h : StateTransition.Reaches f a b) : ∃ N, (flip bind f)^[N] (some a) = some b
Used by 3
Used byA run halts iff it reaches a configuration without successor · Main phase of the wrapped machine · The wrapped machine of a code halts exactly where the code is defined

TheoremMain phase of the wrapped machine#✓fully proved

Let \(c\) be a code and \(f : \mathbb{N} \to \mathbb{N}\) such that \(c\) evaluates to \([f(n)]\) on input \([n]\) for every \(n\). Then for every \(n\) there is \(N\) such that the wrapped machine, started at the label \(\mathrm{trNormal}(c, \mathrm{halt})\) with empty local state, the encoding \(\mathrm{trList}([n])\) on the main stack and all other stacks empty, is after exactly \(N\) steps at the adapter label post1 with empty local state, \(\mathrm{trList}([f(n)])\) on the main stack and all other stacks empty.

theorem main_phase {f : ℕ → ℕ} (hc : ∀ n, c.eval [n] = pure [f n]) (n : ℕ) :
    ∃ N, frun c N (some ⟨some (Sum.inr ⟨trNormal c Cont'.halt, start_mem c⟩), none,
        mkStk (trList [n]) [] [] [] [] []⟩) =
      some ⟨some (Sum.inl Phase.post1), none, mkStk (trList [f n]) [] [] [] [] []⟩
Uses 16 · Used by 1
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Iterated steps of the wrapped machine · Stack contents of the wrapped machine · The start label lies in the support · Support of a code
Proof usesStatements of the wrapped machine · Correspondence of labels between the code evaluator and the wrapped machine · Simulation relation between the code evaluator and the wrapped machine · Reachability gives an iteration count · One step of the wrapped machine · The program of the wrapped machine · Lifting stacks of tr · Restricting a statement of the code evaluator to the wrapped machine
Used byThe wrapped machine computes the function a code evaluates

TheoremThe evaluator's encoding of a one-element list#✓fully proved

For every natural number \(m\), the list of stack symbols by which Mathlib's code evaluator encodes the one-element list \([m]\) is the binary encoding of \(m\) (least significant bit first) with each bit written as \(\mathrm{bit1}\) if it is true and as \(\mathrm{bit0}\) if it is false, followed by the symbol \(\mathrm{cons}\).

theorem trList_singleton (m : ℕ) : trList [m] = (encodeNat m).map boolToΓ' ++ [Γ'.cons]
Uses 2 · Used by 2
Statement usesBits as stack symbols
Proof usesThe evaluator encodes numbers in binary
Used byThe wrapped machine computes the function a code evaluates · The wrapped machine of a code halts exactly where the code is defined

DefinitionThe wrapped machine computes the function a code evaluates#✓fully proved

Let \(c\) be a code and \(f : \mathbb{N} \to \mathbb{N}\) a function such that, for every \(n\), evaluating \(c\) on the one-element list \([n]\) returns \([f(n)]\). Then the wrapped machine of \(c\), with input and output alphabet the booleans, computes \(f\) under the binary encoding of natural numbers (least significant bit first): for every \(n\), started with the encoding of \(n\) on its input stack and all other stacks empty, it eventually halts in its initial internal state with the encoding of \(f(n)\) on its output stack and all other stacks empty.

MetaMathlibExt.TM2Recursive.tm2ComputableOfCode · 41 lines 
noncomputable def tm2ComputableOfCode {f : ℕ → ℕ} (hc : ∀ n, c.eval [n] = pure [f n]) :
    TM2Computable encodeNat encodeNat f where
  tm := fwdTM c
  inputAlphabet := Equiv.refl Bool
  outputAlphabet := Equiv.refl Bool
  outputsFun n :=
    ⟨((encodeNat (f n)).length + 1 + ((encodeNat (f n)).length + 1)) +
        ((main_phase c hc n).choose +
          ((encodeNat n).length + 1 + ((encodeNat n).length + 1) + 1)), by
      have hinit : initList (fwdTM c) ((encodeNat n).map (Equiv.refl Bool).invFun) =
          (⟨some (Sum.inl Phase.pre0), none, mkStk [] [] [] [] (encodeNat n) []⟩ : FCfg c) := by
        simp only [initList]
        congr 1
        funext k
        rcases k with (_ | _ | _ | _) | (_ | _)
        all_goals first
          | rfl
          | (simp only [fwdTM, mkStk, Equiv.refl, ↓reduceDIte]
             change List.map (id : Bool → Bool) _ = _
             exact List.map_id _)
      have hhalt : haltList (fwdTM c) ((encodeNat (f n)).map (Equiv.refl Bool).invFun) =
          (⟨none, none, mkStk [] [] [] [] [] (encodeNat (f n))⟩ : FCfg c) := by
        simp only [haltList]
        congr 1
        funext k
        rcases k with (_ | _ | _ | _) | (_ | _)
        all_goals first
          | rfl
          | (simp only [fwdTM, mkStk, Equiv.refl, ↓reduceDIte]
             change List.map (id : Bool → Bool) _ = _
             exact List.map_id _)
      have key : frun c (((encodeNat (f n)).length + 1 + ((encodeNat (f n)).length + 1)) +
          ((main_phase c hc n).choose +
            ((encodeNat n).length + 1 + ((encodeNat n).length + 1) + 1)))
          (some ⟨some (Sum.inl Phase.pre0), none, mkStk [] [] [] [] (encodeNat n) []⟩) =
          some ⟨none, none, mkStk [] [] [] [] [] (encodeNat (f n))⟩ := by
        rw [frun_add c ((encodeNat (f n)).length + 1 + ((encodeNat (f n)).length + 1)),
          frun_add c (main_phase c hc n).choose, pre_phase, ← trList_singleton,
          (main_phase c hc n).choose_spec, trList_singleton, post_phase]
      rw [hinit, Option.map_some, hhalt]
      exact key⟩
Uses 15 · Used by 2
Statement usesConfigurations of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Adapter labels · Bits as stack symbols · Iterated steps of the wrapped machine · One step of the wrapped machine · The wrapped machine of a code · Main phase of the wrapped machine · Stack contents of the wrapped machine · Post-phase of the wrapped machine · Pre-phase of the wrapped machine · The start label lies in the support · Support of a code · The evaluator's encoding of a one-element list
Used byRecursive functions are Turing-computable · Computable predicates are decidable by single-tape machines

TheoremRecursive functions are Turing-computable#✓fully proved

Every computable function \(f : \mathbb{N} \to \mathbb{N}\) is computed by a finite multi-stack Turing machine (finitely many stacks, labels and internal states) whose input and output alphabets are identified with the booleans, under the binary encoding of natural numbers (least significant bit first, with \(0\) encoded as the empty list): for every \(n\), the machine started with the encoding of \(n\) on its input stack and all other stacks empty eventually halts in its initial internal state with the encoding of \(f(n)\) on its output stack and all other stacks empty.

theorem tm2Computable_of_computable {f : ℕ → ℕ} (hf : Computable f) :
    Nonempty (TM2Computable encodeNat encodeNat f)
Uses 1 · Used by 4
Proof usesThe wrapped machine computes the function a code evaluates
Used byMulti-stack decidable predicates are exactly the computable predicates · Mapping reductions are computed by multi-stack machines · Turing computable equals recursive · A URM-computable total function is computed by a multi-stack Turing machine

TheoremTuring computable equals recursive#✓fully proved

A function \(f : \mathbb{N} \to \mathbb{N}\) is computable (recursive) if and only if some bundled finite multi-stack Turing machine computes it in binary. Here the binary word of \(m \in \mathbb{N}\) is its list of binary digits, least significant first, with \(1\) read as true, \(0\) as false and no leading zeros (so the word of \(0\) is empty). That is, there are such a machine and identifications of its input and output stack alphabets with the booleans such that, for every \(n \in \mathbb{N}\), the machine started at its main label in its initial internal state, with the binary word of \(n\) on its input stack and every other stack empty, reaches the halted configuration whose output stack holds the binary word of \(f(n)\), whose other stacks are empty and whose internal state is the initial one.

theorem computable_iff_nonempty_tm2Computable (f : ℕ → ℕ) :
    Computable f ↔ Nonempty (TM2Computable encodeNat encodeNat f)
Uses 2
Proof usesTuring-computable functions are recursive · Recursive functions are Turing-computable

DefinitionHalting of a multi-stack machine on an input#✓fully proved

A bundled finite multi-stack Turing machine halts on a word \(l\) over its input alphabet when its evaluation from the initial configuration on \(l\) (the main label, the initial internal state, \(l\) on the input stack and every other stack empty) is defined, that is, its run from that configuration reaches a configuration without successor.

def TM2HaltsOn (tm : FinTM2) (l : List (tm.Γ tm.k₀)) : Prop :=
  (StateTransition.eval tm.step (initList tm l)).Dom
Used by 12
Used byRecognizability by multi-stack machines · Multi-stack recognizable predicates are exactly the r.e. predicates · Some multi-stack machine has an undecidable halting set · The halting problem for single-tape machines is undecidable · Halting agrees with evaluation for multi-stack machines · Every r.e. predicate is the halting set of a machine with finite alphabets · Every r.e. predicate is the halting set of a multi-stack machine · R.e. predicates are the halting sets of multi-stack machines · The halting set of a multi-stack machine is r.e · The wrapped machine of a code halts exactly where the code is defined · The recognizer halts iff the multi-stack machine does · R.e. predicates are recognizable by single-tape machines

TheoremA run that stops passes through a configuration without successor#✓fully proved

Let \(f : \sigma \to \mathrm{Option}\ \sigma\) be a step function and \(a \in \sigma\), and write \(f^{(k)}(a) \in \mathrm{Option}\ \sigma\) for the result of \(k\) steps from \(a\): the \(k\)-th iterate, applied to \(\mathrm{some}\ a\), of the map sending \(\mathrm{none}\) to \(\mathrm{none}\) and \(\mathrm{some}\ x\) to \(f(x)\). If \(f^{(k)}(a) = \mathrm{none}\) for some \(k\), then there are \(j \in \mathbb{N}\) and \(b \in \sigma\) with \(f^{(j)}(a) = \mathrm{some}\ b\) and \(f(b) = \mathrm{none}\).

theorem exists_iterate_eq_some_of_eq_none {a : σ} :
    ∀ {k : ℕ}, (flip bind f)^[k] (some a) = none →
      ∃ j b, (flip bind f)^[j] (some a) = some b ∧ f b = none
Used by 2
Used byThe halting set of a multi-stack machine is r.e · The wrapped machine of a code halts exactly where the code is defined

TheoremA run halts iff it reaches a configuration without successor#✓fully proved

Let \(f : \sigma \to \mathrm{Option}\ \sigma\) be a step function and \(a \in \sigma\), and write \(f^{(k)}(a) \in \mathrm{Option}\ \sigma\) for the result of \(k\) steps from \(a\): the \(k\)-th iterate, applied to \(\mathrm{some}\ a\), of the map sending \(\mathrm{none}\) to \(\mathrm{none}\) and \(\mathrm{some}\ x\) to \(f(x)\). The evaluation of \(f\) from \(a\) (the configuration where the run from \(a\) stops) is defined if and only if there are \(k \in \mathbb{N}\) and \(b \in \sigma\) with \(f^{(k)}(a) = \mathrm{some}\ b\) and \(f(b) = \mathrm{none}\).

theorem dom_eval_iff_exists_iterate {a : σ} :
    (StateTransition.eval f a).Dom ↔ ∃ k b, (flip bind f)^[k] (some a) = some b ∧ f b = none
Uses 1 · Used by 3
Proof usesReachability gives an iteration count
Used byThe halting set of a multi-stack machine is r.e · The wrapped machine of a code halts exactly where the code is defined · Halting is halting within some number of steps

TheoremA run stays stopped after a configuration without successor#✓fully proved

Let \(f : \sigma \to \mathrm{Option}\ \sigma\) be a step function and \(a, b \in \sigma\), and write \(f^{(k)}(a) \in \mathrm{Option}\ \sigma\) for the result of \(k\) steps from \(a\): the \(k\)-th iterate, applied to \(\mathrm{some}\ a\), of the map sending \(\mathrm{none}\) to \(\mathrm{none}\) and \(\mathrm{some}\ x\) to \(f(x)\). If \(f^{(k)}(a) = \mathrm{some}\ b\) and \(f(b) = \mathrm{none}\), then \(f^{(m)}(a) = \mathrm{none}\) for every \(m > k\).

theorem iterate_eq_none_of_lt {a b : σ} {k : ℕ} (hk : (flip bind f)^[k] (some a) = some b)
    (hb : f b = none) {m : ℕ} (hm : k < m) : (flip bind f)^[m] (some a) = none
Used by 2
Used byThe wrapped machine of a code halts exactly where the code is defined · Clocked halting

TheoremThe halting set of a multi-stack machine is r.e#✓fully proved

For every bundled finite multi-stack Turing machine and every identification of its input alphabet with the booleans, the predicate on \(\mathbb{N}\) that holds at \(n\) exactly when the machine halts on the binary digits of \(n\) (least significant first, with \(1\) read as true, \(0\) as false and no leading zeros, so that \(0\) gives the empty word) is recursively enumerable.

theorem rePred_tm2HaltsOn (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool) :
    REPred fun n ↦ TM2HaltsOn tm ((Computability.encodeNat n).map e.symm)
Uses 21 · Used by 2
Statement usesHalting of a multi-stack machine on an input
Proof usesCoded configurations of a multi-stack machine · Stacks with only relevant symbols · Code of a stack symbol · A run halts iff it reaches a configuration without successor · Coding a configuration · Coded stacks · Binary encoding, least significant bit first · A run that stops passes through a configuration without successor · The coded step on optional configurations · The coded run simulates the machine's run · Running a primitive recursive machine is partial recursive · Encoding of functions on a finite type · Encoding of labels · Encoding of internal states · Joint primitive recursion over a finite first argument · Updating the state from the top of a coded stack is primitive recursive · Reading the top of a coded stack · The initial stacks have only relevant symbols · The coded execution of a statement · The coded step
Used byMulti-stack recognizable predicates are exactly the r.e. predicates · R.e. predicates are the halting sets of multi-stack machines

TheoremThe wrapped machine of a code halts exactly where the code is defined#✓fully proved

Let \(c\) be a code for a partial recursive function on lists of natural numbers and \(n \in \mathbb{N}\), and suppose that every value of \(c\) on the one-element list \([n]\) is itself a one-element list. Then the wrapped multi-stack machine of \(c\) halts on the binary digits of \(n\) (least significant first, with \(1\) read as true, \(0\) as false and no leading zeros, so that \(0\) gives the empty word) if and only if the evaluation of \(c\) at \([n]\) is defined.

theorem tm2HaltsOn_fwdTM_iff (n : ℕ) (hc : ∀ v ∈ c.eval [n], ∃ m, v = [m]) :
    TM2HaltsOn (fwdTM c) ((Computability.encodeNat n).map (Equiv.refl Bool).symm) ↔
      (c.eval [n]).Dom
Uses 25 · Used by 1
Statement usesHalting of a multi-stack machine on an input · The wrapped machine of a code
Proof usesConfigurations of the wrapped machine · Statements of the wrapped machine · Stack alphabets of the wrapped machine · Labels of the wrapped machine · Correspondence of labels between the code evaluator and the wrapped machine · Adapter labels · Simulation relation between the code evaluator and the wrapped machine · Bits as stack symbols · A run halts iff it reaches a configuration without successor · Reachability gives an iteration count · A run that stops passes through a configuration without successor · Iterated steps of the wrapped machine · One step of the wrapped machine · The program of the wrapped machine · A run stays stopped after a configuration without successor · Lifting stacks of tr · Stack contents of the wrapped machine · Post-phase of the wrapped machine · Pre-phase of the wrapped machine · Restricting a statement of the code evaluator to the wrapped machine · The start label lies in the support · Support of a code · The evaluator's encoding of a one-element list
Used byEvery r.e. predicate is the halting set of a machine with finite alphabets

TheoremEvery r.e. predicate is the halting set of a machine with finite alphabets#✓fully proved

For every recursively enumerable predicate \(p\) on \(\mathbb{N}\) there are a bundled finite multi-stack Turing machine whose stack alphabets are all finite and an identification of its input alphabet with the booleans such that, for every \(n \in \mathbb{N}\), \(p(n)\) holds if and only if the machine halts on the binary digits of \(n\) (least significant first, with \(1\) read as true, \(0\) as false and no leading zeros, so that \(0\) gives the empty word).

theorem exists_finite_tm2HaltsOn_iff_of_rePred {p : ℕ → Prop} (hp : REPred p) :
    ∃ (tm : FinTM2) (_ : ∀ k, Finite (tm.Γ k)) (e : tm.Γ tm.k₀ ≃ Bool),
      ∀ n, p n ↔ TM2HaltsOn tm ((Computability.encodeNat n).map e.symm)
Uses 3 · Used by 3
Statement usesHalting of a multi-stack machine on an input
Proof usesThe wrapped machine of a code · The wrapped machine of a code halts exactly where the code is defined
Used byThe halting problem for single-tape machines is undecidable · Every r.e. predicate is the halting set of a multi-stack machine · R.e. predicates are recognizable by single-tape machines

TheoremEvery r.e. predicate is the halting set of a multi-stack machine#✓fully proved

For every recursively enumerable predicate \(p\) on \(\mathbb{N}\) there are a bundled finite multi-stack Turing machine and an identification of its input alphabet with the booleans such that, for every \(n \in \mathbb{N}\), \(p(n)\) holds if and only if the machine halts on the binary digits of \(n\) (least significant first, with \(1\) read as true, \(0\) as false and no leading zeros, so that \(0\) gives the empty word).

theorem exists_tm2HaltsOn_iff_of_rePred {p : ℕ → Prop} (hp : REPred p) :
    ∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
      ∀ n, p n ↔ TM2HaltsOn tm ((Computability.encodeNat n).map e.symm)
Uses 2 · Used by 3
Statement usesHalting of a multi-stack machine on an input
Proof usesEvery r.e. predicate is the halting set of a machine with finite alphabets
Used byMulti-stack recognizable predicates are exactly the r.e. predicates · Some multi-stack machine has an undecidable halting set · R.e. predicates are the halting sets of multi-stack machines

TheoremR.e. predicates are the halting sets of multi-stack machines#✓fully proved

A predicate \(p\) on \(\mathbb{N}\) is recursively enumerable if and only if there are a bundled finite multi-stack Turing machine and an identification of its input alphabet with the booleans such that, for every \(n \in \mathbb{N}\), \(p(n)\) holds if and only if the machine halts on the binary digits of \(n\) (least significant first, with \(1\) read as true, \(0\) as false and no leading zeros, so that \(0\) gives the empty word).

theorem rePred_iff_exists_tm2HaltsOn {p : ℕ → Prop} :
    REPred p ↔ ∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
      ∀ n, p n ↔ TM2HaltsOn tm ((Computability.encodeNat n).map e.symm)
Uses 3
Statement usesHalting of a multi-stack machine on an input
Proof usesEvery r.e. predicate is the halting set of a multi-stack machine · The halting set of a multi-stack machine is r.e

TheoremRecursive functions are the Turing-computable functions#●ready to prove

A function \(f : \mathbb{N} \to \mathbb{N}\) is computable, that is, total recursive, if and only if some finite multi-stack Turing machine computes it on binary representations: there are a machine with finitely many stacks, internal states and program labels and bijections from its input and output stack alphabets to \(\{0, 1\}\) such that, for every \(n \in \mathbb{N}\), the machine started in its initial state with the binary representation of \(n\) (least significant bit first, with \(0\) written as the empty word) on its input stack and all other stacks empty halts with the binary representation of \(f(n)\) on its output stack, all other stacks empty and its internal state back at the initial state.

public theorem_wanted turing_recursive_equiv (f : ℕ → ℕ) :
    Computable f ↔ Nonempty (TM2Computable encodeNat encodeNat f)
Sources
  • A. M. Turing, On Computable Numbers (1936); S. C. Kleene, General recursive functions of natural numbers (1936). Knill, Some fundamental theorems in mathematics, §23. Problem turing_recursive_equiv of the lean-eval benchmark.
67 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.