Unlimited register machines

DefinitionCode of a URM instruction#✓fully proved

Code of a URM instruction as a natural number: the instruction tag paired with the paired arguments, Z n ↦ pair 0 n, S n ↦ pair 1 n, T m n ↦ pair 2 (pair m n), J m n q ↦ pair 3 (pair m (pair n q)).

def encodeInstr : Instr → ℕ
  | .Z n => Nat.pair 0 n
  | .S n => Nat.pair 1 n
  | .T m n => Nat.pair 2 (Nat.pair m n)
  | .J m n q => Nat.pair 3 (Nat.pair m (Nat.pair n q))
Used by 12
Used byA machine step is a coded step · The URM output after a given number of steps is computable · Tag of an instruction code · Payload of an instruction code · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · Instruction codes by position · Output after a given number of steps · A halted coded state gives a halting machine run · A URM-computable partial function is partial recursive · Bounded execution is primitive recursive in the input and the step bound · A coded step is a machine step

TheoremTag of an instruction code#✓fully proved

For every URM instruction \(I\), unpairing the code of \(I\) gives first component \(0\) if \(I\) is a zero instruction \(Z\,n\), \(1\) if it is a successor instruction \(S\,n\), \(2\) if it is a transfer \(T\,m\,n\), and \(3\) if it is a jump \(J\,m\,n\,q\).

theorem encodeInstr_unpair_fst (instr : Instr) :
    (encodeInstr instr).unpair.1 = match instr with
Uses 1
Statement usesCode of a URM instruction

TheoremPayload of an instruction code#✓fully proved

Write \(\langle a, b \rangle\) for the pairing of natural numbers \(a\) and \(b\). For every URM instruction \(I\), unpairing the code of \(I\) gives second component \(n\) if \(I\) is \(Z\,n\) or \(S\,n\), \(\langle m, n \rangle\) if \(I\) is \(T\,m\,n\), and \(\langle m, \langle n, q \rangle \rangle\) if \(I\) is \(J\,m\,n\,q\).

theorem encodeInstr_unpair_snd (instr : Instr) :
    (encodeInstr instr).unpair.2 = match instr with
Uses 1
Statement usesCode of a URM instruction

DefinitionOne coded URM step#✓fully proved

A coded state is a program counter \(k\) together with a list \(r\) of register contents (in use, the contents of registers \(0, \dots, R\), where \(R\) is the register bound of the program), and a program is given by the list \(c\) of its instruction codes. Write \(c_k\) for entry \(k\) of \(c\), and \(r_j\) for entry \(j\) of \(r\), read as \(0\) when \(j\) is past the end of \(r\); setting an entry past the end of \(r\) leaves \(r\) unchanged. If \(k\) is at least the length of \(c\), the state is halted and has no successor. Otherwise unpair the code \(c_k\) as \((i, a)\). If \(i = 0\), the successor is \((k + 1, r')\) where \(r'\) is \(r\) with entry \(a\) set to \(0\). If \(i = 1\), it is \((k + 1, r')\) where \(r'\) is \(r\) with entry \(a\) set to \(r_a + 1\). If \(i = 2\), unpair \(a\) as \((m, n)\); the successor is \((k + 1, r')\) where \(r'\) is \(r\) with entry \(n\) set to \(r_m\). If \(i = 3\), unpair \(a\) as \((m, b)\) and \(b\) as \((n, q)\); the successor is \((q, r)\) if \(r_m = r_n\) and \((k + 1, r)\) otherwise. Any other tag \(i\) (which never occurs for a genuine instruction code) gives no successor.

Cslib.URM.codedStep · 16 lines 
def codedStep (codes : List ℕ) (pc : ℕ) (regs : List ℕ) : Option (ℕ × List ℕ) :=
  if pc < codes.length then
    if (codes.getD pc 0).unpair.1 = 0 then
      some (pc + 1, regs.set (codes.getD pc 0).unpair.2 0)
    else if (codes.getD pc 0).unpair.1 = 1 then
      some (pc + 1, regs.set (codes.getD pc 0).unpair.2
        (regs.getD (codes.getD pc 0).unpair.2 0 + 1))
    else if (codes.getD pc 0).unpair.1 = 2 then
      some (pc + 1, regs.set (codes.getD pc 0).unpair.2.unpair.2
        (regs.getD (codes.getD pc 0).unpair.2.unpair.1 0))
    else if (codes.getD pc 0).unpair.1 = 3 then
      some ((if regs.getD (codes.getD pc 0).unpair.2.unpair.1 0 =
          regs.getD (codes.getD pc 0).unpair.2.unpair.2.unpair.1 0
        then (codes.getD pc 0).unpair.2.unpair.2.unpair.2 else pc + 1), regs)
    else Option.none
  else Option.none
Used by 8
Used byA machine step is a coded step · Bounded URM execution is stable once halted · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · The coded step is primitive recursive · The one-step function is primitive recursive · One-step function on coded states · A coded step is a machine step

TheoremThe coded step is primitive recursive#✓fully proved

The coded step is primitive recursive, for any fixed list of instruction codes.

theorem primrec_codedStep (codes : List ℕ) :
    Primrec fun s : ℕ × List ℕ ↦ codedStep codes s.1 s.2
Uses 1 · Used by 1
Statement usesOne coded URM step
Used byThe one-step function is primitive recursive

DefinitionRegister bound#✓fully proved

The register bound \(R\) of a URM program \(p\) is the sum, over the instructions of \(p\), of the largest register index each instruction refers to. Every register that an instruction of \(p\) can read or write is at most \(R\).

def regBound : ℕ := (p.map Instr.maxRegister).sum
Used by 14
Used byA machine step is a coded step · Reading the register list · Initial coded state · The initial coded state codes the initial machine state · Length of the register list · Instructions stay within the register bound · A URM-computable partial function is partial recursive · The initial coded state is primitive recursive in the input · Registers read by a program lie within the register bound · A coded step is a machine step · Decoding and re-encoding a coded state gives it back · Register list · Updating a register updates the register list · Written registers lie within the register bound

AbbreviationRegister list#✓fully proved

For a URM program \(p\) with register bound \(R\), the register list of a register state \(\sigma\) is the list \((\sigma(0), \sigma(1), \dots, \sigma(R))\) of the contents of registers \(0, \dots, R\).

abbrev toRegs (σ : Regs) : List ℕ := (List.range (regBound p + 1)).map σ
Uses 1 · Used by 8
Statement usesRegister bound
Used byA machine step is a coded step · Reading the register list · Length of the register list · A URM-computable partial function is partial recursive · A coded step is a machine step · Coded machine state · Decoding and re-encoding a coded state gives it back · Updating a register updates the register list

AbbreviationCoded machine state#✓fully proved

For a URM program \(p\) with register bound \(R\), the coded state of a machine state \(s\) is the pair consisting of the program counter of \(s\) and the register list \((r_0, \dots, r_R)\) of the contents of registers \(0, \dots, R\) of \(s\).

abbrev toCoded (s : State) : ℕ × List ℕ := (s.pc, toRegs p s.regs)
Uses 1 · Used by 8
Statement usesRegister list
Used byA machine step is a coded step · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · A halted coded state gives a halting machine run · The initial coded state codes the initial machine state · A URM-computable partial function is partial recursive · A coded step is a machine step · Decoding and re-encoding a coded state gives it back

AbbreviationDecoding a coded state#✓fully proved

A coded state is a pair \((c, \ell)\) of a natural number \(c\) and a list \(\ell\) of natural numbers. Its machine state has program counter \(c\), and register \(n\) holds the \(n\)-th entry of \(\ell\) (counting from \(0\)) when \(n\) is less than the length of \(\ell\), and \(0\) otherwise.

abbrev ofCoded (c : ℕ × List ℕ) : State := ⟨c.1, fun n ↦ c.2.getD n 0⟩
Used by 1
Used byDecoding and re-encoding a coded state gives it back

TheoremLength of the register list#✓fully proved

For a URM program \(p\) with register bound \(R\) and a register state \(\sigma\), the register list of \(\sigma\) (the contents of registers \(0, \dots, R\)) has length \(R + 1\).

theorem length_toRegs (σ : Regs) : (toRegs p σ).length = regBound p + 1
Uses 2 · Used by 1
Statement usesRegister bound · Register list
Used byDecoding and re-encoding a coded state gives it back

TheoremReading the register list#✓fully proved

Let \(p\) be a URM program with register bound \(R\) and \(\sigma\) a register state. For every \(n\), the entry at position \(n\) of the register list of \(\sigma\), read with default \(0\), is \(\sigma(n)\) if \(n \le R\) and \(0\) otherwise.

theorem getD_toRegs (σ : Regs) (n : ℕ) :
    (toRegs p σ).getD n 0 = if n ≤ regBound p then σ n else 0
Uses 2 · Used by 3
Statement usesRegister bound · Register list
Used byA machine step is a coded step · A URM-computable partial function is partial recursive · A coded step is a machine step

TheoremUpdating a register updates the register list#✓fully proved

Let \(p\) be a URM program with register bound \(R\), let \(\sigma\) be a register state, and let \(n \le R\) and \(v\) be natural numbers. The register list of the state obtained from \(\sigma\) by setting register \(n\) to \(v\) equals the register list of \(\sigma\) with its entry at position \(n\) replaced by \(v\).

theorem toRegs_update (σ : Regs) {n v : ℕ} (hn : n ≤ regBound p) :
    toRegs p (Function.update σ n v) = (toRegs p σ).set n v
Uses 2 · Used by 2
Statement usesRegister bound · Register list
Used byA machine step is a coded step · A coded step is a machine step

TheoremInstructions stay within the register bound#✓fully proved

For a URM program \(p\) with register bound \(R\) and every instruction \(I\) of \(p\), the largest register index referenced by \(I\) is at most \(R\).

theorem maxRegister_le_regBound {instr : Instr} (h : instr ∈ p) :
    instr.maxRegister ≤ regBound p
Uses 1 · Used by 2
Statement usesRegister bound
Used byRegisters read by a program lie within the register bound · Written registers lie within the register bound

TheoremWritten registers lie within the register bound#✓fully proved

Let \(p\) be a URM program with register bound \(R\). If an instruction of \(p\) writes to register \(n\), then \(n \le R\).

theorem writesTo_le_regBound {instr : Instr} {n : ℕ} (h : instr ∈ p)
    (hw : instr.writesTo = some n) : n ≤ regBound p
Uses 2 · Used by 2
Statement usesRegister bound
Proof usesInstructions stay within the register bound
Used byA machine step is a coded step · A coded step is a machine step

TheoremRegisters read by a program lie within the register bound#✓fully proved

Let \(p\) be a URM program. If \(n\) is a register read by some instruction of \(p\), then \(n\) is at most the register bound of \(p\).

theorem reads_le_regBound {instr : Instr} {n : ℕ} (h : instr ∈ p)
    (hr : n ∈ instr.readsFrom) : n ≤ regBound p
Uses 2 · Used by 2
Statement usesRegister bound
Proof usesInstructions stay within the register bound
Used byA machine step is a coded step · A coded step is a machine step

TheoremDecoding and re-encoding a coded state gives it back#✓fully proved

Let \(p\) be a URM program with register bound \(R\), and let \(c\) be a coded state: a program counter together with a list of register contents. If the list has length \(R + 1\), then the coded state, with respect to \(p\), of the machine state decoded from \(c\) is \(c\).

theorem toCoded_ofCoded {c : ℕ × List ℕ} (hlen : c.2.length = regBound p + 1) :
    toCoded p (ofCoded c) = c
Uses 5
Statement usesDecoding a coded state · Register bound · Coded machine state
Proof usesLength of the register list · Register list

TheoremA state that can step is running#✓fully proved

If a state \(s\) of a URM program \(p\) makes a step to some state, then the program counter of \(s\) is less than the number of instructions of \(p\).

theorem pc_lt_of_step {s s' : State} (h : Step p s s') : s.pc < p.length
Used by 1
Used byA machine step is a coded step

TheoremInstruction codes by position#✓fully proved

If the URM program \(p\) has instruction \(I\) at position \(pc\), then the entry at position \(pc\) of the list of instruction codes of \(p\), read with default \(0\), is the code of \(I\).

theorem getD_codes {pc : ℕ} {instr : Instr} (hi : p[pc]? = some instr) :
    (p.map encodeInstr).getD pc 0 = encodeInstr instr
Uses 1 · Used by 2
Statement usesCode of a URM instruction
Used byA machine step is a coded step · A coded step is a machine step

TheoremA machine step is a coded step#✓fully proved

Let \(p\) be a URM program, let \(R\) be the sum over the instructions of \(p\) of the largest register index each one mentions, and let \(s'\) be a state that \(p\) reaches from the state \(s\) in one step. Then the coded step, run on the list of codes of the instructions of \(p\), sends the coded state of \(s\) (its program counter together with the list of the contents of its registers \(0, \dots, R\)) to the coded state of \(s'\).

theorem codedStep_of_step {s s' : State} (h : Step p s s') :
    codedStep (p.map encodeInstr) (toCoded p s).1 (toCoded p s).2 =
      some (toCoded p s')
Uses 11 · Used by 1
Statement usesOne coded URM step · Code of a URM instruction · Coded machine state
Proof usesInstruction codes by position · Reading the register list · A state that can step is running · Registers read by a program lie within the register bound · Register bound · Register list · Updating a register updates the register list · Written registers lie within the register bound
Used byEvery reachable state is reached by bounded execution

TheoremA coded step is a machine step#✓fully proved

Let \(p\) be a URM program and \(s\) a machine state. If one coded URM step, run on the list of codes of the instructions of \(p\) from the coded state of \(s\), yields \(c'\), then there is a machine state \(s'\) such that \(p\) steps from \(s\) to \(s'\) in one step and the coded state of \(s'\) is \(c'\).

theorem step_of_codedStep {s : State} {c' : ℕ × List ℕ}
    (h : codedStep (p.map encodeInstr) (toCoded p s).1 (toCoded p s).2 = some c') :
    ∃ s' : State, Step p s s' ∧ toCoded p s' = c'
Uses 10 · Used by 1
Statement usesOne coded URM step · Code of a URM instruction · Coded machine state
Proof usesInstruction codes by position · Reading the register list · Registers read by a program lie within the register bound · Register bound · Register list · Updating a register updates the register list · Written registers lie within the register bound
Used byBounded execution only reaches codes of reachable states

DefinitionURM-decidable predicate#✓fully proved

A predicate \(P\) on the natural numbers is URM-decidable when some URM program computes its characteristic function: started on any input \(n\) (register \(0\) holding \(n\), all other registers \(0\)), the program halts, and register \(0\) then holds \(1\) if \(P(n)\) holds and \(0\) otherwise.

def Decidable (P : ℕ → Prop) : Prop :=
  ∃ prog : Program, ∀ n, eval prog [n] = Cslib.Decidability.charFun P n
Uses 1 · Used by 4
Statement usesCharacteristic function of a set of naturals
Used byA URM-decidable predicate is computable · A URM-decidable predicate is decidable by a single-tape Turing machine · A URM-decidable predicate is decidable by a multi-stack Turing machine · URM-decidability implies multi-stack decidability

DefinitionURM-recognizable predicates#✓fully proved

A predicate \(P\) on the natural numbers is URM-recognizable when there is a URM program that, started with input \(n\) in register \(0\) and every other register \(0\), halts if and only if \(P(n)\) holds.

def Recognizable (P : ℕ → Prop) : Prop :=
  ∃ prog : Program, ∀ n, (eval prog [n]).Dom ↔ P n
Used by 4
Used byA URM-recognizable predicate is recursively enumerable · A URM-recognizable predicate is recognizable by a single-tape Turing machine · A URM-recognizable predicate is recognizable by a multi-stack Turing machine · URM-recognizability implies multi-stack recognizability

DefinitionOne-step function on coded states#✓fully proved

Given a list of instruction codes, the one-step function sends a coded state \(s\) to the result of one coded URM step from \(s\) when that step is defined, and leaves \(s\) unchanged when it is not (in particular when \(s\) is halted).

def stepFn (codes : List ℕ) : ℕ × List ℕ → ℕ × List ℕ :=
  fun s ↦ (codedStep codes s.1 s.2).getD s
Uses 1 · Used by 7
Statement usesOne coded URM step
Used byBounded execution · Bounded execution unfolds by one step · Bounded URM execution is stable once halted · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · Bounded execution is primitive recursive in the input and the step bound · The one-step function is primitive recursive

TheoremThe one-step function is primitive recursive#✓fully proved

For every list of natural numbers, read as instruction codes, the function on coded states (pairs of a program counter and a register list) that sends a coded state to its successor under one coded step, and a coded state with no successor to itself, is primitive recursive.

theorem primrec_stepFn (codes : List ℕ) : Primrec (stepFn codes)
Uses 3 · Used by 1
Statement usesOne-step function on coded states
Proof usesOne coded URM step · The coded step is primitive recursive
Used byBounded execution is primitive recursive in the input and the step bound

DefinitionBounded execution#✓fully proved

For a list of instruction codes, a number \(t\) and a coded state \(s\), bounded execution applies the one-step function for these codes \(t\) times, starting from \(s\).

def execN (codes : List ℕ) (t : ℕ) (s : ℕ × List ℕ) : ℕ × List ℕ :=
  (stepFn codes)^[t] s
Uses 1 · Used by 10
Statement usesOne-step function on coded states
Used byThe URM output after a given number of steps is computable · Bounded URM execution stays at its halted value · Bounded execution unfolds by one step · Bounded URM execution is stable once halted · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · Output after a given number of steps · A halted coded state gives a halting machine run · A URM-computable partial function is partial recursive · Bounded execution is primitive recursive in the input and the step bound

TheoremBounded execution unfolds by one step#✓fully proved

For a list of instruction codes, a number \(t\) and a coded state \(s\), bounded execution for \(t + 1\) steps from \(s\) is the one-step function applied to the result of bounded execution for \(t\) steps from \(s\).

theorem execN_succ (codes : List ℕ) (t : ℕ) (s : ℕ × List ℕ) :
    execN codes (t + 1) s = stepFn codes (execN codes t s)
Uses 2 · Used by 3
Statement usesBounded execution · One-step function on coded states
Used byBounded URM execution is stable once halted · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution

DefinitionInitial coded state#✓fully proved

For a URM program \(p\) with register bound \(R\) and an input \(x\), the initial coded state has program counter \(0\) and register list \((x, 0, \dots, 0)\) of length \(R + 1\): register \(0\) holds \(x\) and registers \(1, \dots, R\) hold \(0\).

def initCoded (x : ℕ) : ℕ × List ℕ :=
  (0, (List.range (regBound p + 1)).map fun n ↦ if n = 0 then x else 0)
Uses 1 · Used by 9
Statement usesRegister bound
Used byThe URM output after a given number of steps is computable · Bounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution · Output after a given number of steps · A halted coded state gives a halting machine run · The initial coded state codes the initial machine state · A URM-computable partial function is partial recursive · Bounded execution is primitive recursive in the input and the step bound · The initial coded state is primitive recursive in the input

TheoremThe initial coded state is primitive recursive in the input#✓fully proved

The initial coded state is primitive recursive in the input.

theorem primrec_initCoded : Primrec fun x ↦ initCoded p x
Uses 2 · Used by 1
Statement usesInitial coded state
Proof usesRegister bound
Used byBounded execution is primitive recursive in the input and the step bound

TheoremBounded execution is primitive recursive in the input and the step bound#✓fully proved

For a URM program \(p\), the bounded execution of \(p\) for \(t\) steps (\(t\) iterations of the one-step function on the list of instruction codes of \(p\)), started from the initial coded state for input \(x\), is a primitive recursive function of the pair \((x, t)\).

theorem primrec_execN : Primrec fun a : ℕ × ℕ ↦
    execN (p.map encodeInstr) a.2 (initCoded p a.1)
Uses 6 · Used by 1
Statement usesCode of a URM instruction · Bounded execution · Initial coded state
Proof usesThe initial coded state is primitive recursive in the input · The one-step function is primitive recursive · One-step function on coded states
Used byThe URM output after a given number of steps is computable

TheoremThe initial coded state codes the initial machine state#✓fully proved

For a URM program \(p\) and an input \(x\), the initial coded state for \(x\) equals the coded state of the initial machine state with input list \([x]\).

theorem initCoded_eq_toCoded (x : ℕ) : initCoded p x = toCoded p (State.init [x])
Uses 3 · Used by 2
Statement usesInitial coded state · Coded machine state
Proof usesRegister bound
Used byBounded execution only reaches codes of reachable states · Every reachable state is reached by bounded execution

TheoremBounded execution only reaches codes of reachable states#✓fully proved

Let \(p\) be a URM program, \(x\) an input and \(t\) a natural number. Then there is a machine state \(s'\), reachable from the initial state with input list \([x]\) by steps of \(p\), whose coded state equals the result of bounded execution for \(t\) steps on the instruction codes of \(p\) from the initial coded state for \(x\).

theorem execN_toCoded_steps (x : ℕ) (t : ℕ) :
    ∃ s' : State, Steps p (State.init [x]) s' ∧
      toCoded p s' = execN (p.map encodeInstr) t (initCoded p x)
Uses 9 · Used by 1
Statement usesCode of a URM instruction · Bounded execution · Initial coded state · Coded machine state
Proof usesOne coded URM step · Bounded execution unfolds by one step · The initial coded state codes the initial machine state · One-step function on coded states · A coded step is a machine step
Used byA halted coded state gives a halting machine run

TheoremA halted coded state gives a halting machine run#✓fully proved

Let \(p\) be a URM program, \(x\) an input and \(t\) a number. If bounded execution for \(t\) steps on the instruction codes of \(p\) from the initial coded state for \(x\) reaches a program counter at least the length of the list of instruction codes, then \(p\) halts on the input list \([x]\).

theorem halts_of_execN_halted (x t : ℕ)
    (h : (execN (p.map encodeInstr) t (initCoded p x)).1 ≥ (p.map encodeInstr).length) :
    Halts p [x]
Uses 5 · Used by 1
Statement usesCode of a URM instruction · Bounded execution · Initial coded state
Proof usesBounded execution only reaches codes of reachable states · Coded machine state
Used byA URM-computable partial function is partial recursive

TheoremEvery reachable state is reached by bounded execution#✓fully proved

Let \(p\) be a URM program and \(x\) an input. If a machine state \(s\) is reachable from the initial state with input list \([x]\) by steps of \(p\), then for some number \(t\), bounded execution for \(t\) steps on the instruction codes of \(p\) from the initial coded state for \(x\) gives the coded state of \(s\).

theorem exists_execN_eq_of_steps (x : ℕ) {s : State}
    (hs : Steps p (State.init [x]) s) :
    ∃ t, execN (p.map encodeInstr) t (initCoded p x) = toCoded p s
Uses 9 · Used by 1
Statement usesCode of a URM instruction · Bounded execution · Initial coded state · Coded machine state
Proof usesOne coded URM step · A machine step is a coded step · Bounded execution unfolds by one step · The initial coded state codes the initial machine state · One-step function on coded states
Used byA URM-computable partial function is partial recursive

TheoremBounded URM execution is stable once halted#✓fully proved

Let \(c\) be a list of instruction codes, \(s\) a coded state and \(t\) a natural number. If after \(t\) steps of bounded execution of \(c\) from \(s\) the program counter is at least the length of \(c\), then \(t + 1\) steps of bounded execution of \(c\) from \(s\) give the same coded state as \(t\) steps.

theorem execN_succ_of_halted (codes : List ℕ) {t : ℕ} {s : ℕ × List ℕ}
    (h : codes.length ≤ (execN codes t s).1) : execN codes (t + 1) s = execN codes t s
Uses 4 · Used by 1
Statement usesBounded execution
Proof usesOne coded URM step · Bounded execution unfolds by one step · One-step function on coded states
Used byBounded URM execution stays at its halted value

TheoremBounded URM execution stays at its halted value#✓fully proved

Let \(c\) be a list of instruction codes, \(s\) a coded state, and \(t_1 \le t_2\) natural numbers. If after \(t_1\) steps of bounded execution of \(c\) from \(s\) the program counter is at least the length of \(c\), then \(t_2\) steps of bounded execution of \(c\) from \(s\) give the same coded state as \(t_1\) steps.

theorem execN_eq_of_le (codes : List ℕ) {s : ℕ × List ℕ} {t₁ t₂ : ℕ} (hle : t₁ ≤ t₂)
    (h : codes.length ≤ (execN codes t₁ s).1) : execN codes t₂ s = execN codes t₁ s
Uses 2 · Used by 1
Statement usesBounded execution
Proof usesBounded URM execution is stable once halted
Used byA URM-computable partial function is partial recursive

DefinitionOutput after a given number of steps#✓fully proved

For a URM program \(p\), an input \(x\) and a number \(t\), run bounded execution for \(t\) steps on the instruction codes of \(p\) from the initial coded state for \(x\). If the resulting program counter is less than the length of the list of instruction codes, the program is still running and there is no output; otherwise the output is the entry at position \(0\) of the resulting register list, read with default \(0\).

def haltedOutput (x t : ℕ) : Option ℕ :=
  if (execN (p.map encodeInstr) t (initCoded p x)).1 < (p.map encodeInstr).length then
    Option.none
  else some ((execN (p.map encodeInstr) t (initCoded p x)).2.getD 0 0)
Uses 3 · Used by 2
Statement usesCode of a URM instruction · Bounded execution · Initial coded state
Used byThe URM output after a given number of steps is computable · A URM-computable partial function is partial recursive

TheoremThe URM output after a given number of steps is computable#✓fully proved

For every URM program \(p\), the function sending an input \(x\) and a step count \(t\) to the output of \(p\) on \(x\) after \(t\) steps (nothing while \(p\) is still running, the contents of register \(0\) once it has halted) is a computable function of the pair \((x, t)\).

Unbounded search over \(t\) then shows that URM evaluation is partial recursive.

theorem computable₂_haltedOutput : Computable₂ (haltedOutput p)
Uses 5 · Used by 1
Statement usesOutput after a given number of steps
Proof usesCode of a URM instruction · Bounded execution · Initial coded state · Bounded execution is primitive recursive in the input and the step bound
Used byA URM-computable partial function is partial recursive

TheoremA URM-computable partial function is partial recursive#✓fully proved

Let \(f\) be a partial function from \(\mathbb{N}\) to \(\mathbb{N}\). Suppose some URM program has the following property for every natural number \(x\): started with \(x\) in register \(0\) and all other registers \(0\), it halts exactly when \(f(x)\) is defined, and then it holds \(f(x)\) in register \(0\). Then \(f\) is partial recursive.

The URM evaluation is the unbounded search for the first halting step of the coded execution.

theorem partrec_of_computable (hf : URM.Computable 1 (fun inputs ↦ f (inputs 0))) :
    Partrec f
Uses 12 · Used by 3
Proof usesThe URM output after a given number of steps is computable · Code of a URM instruction · Bounded execution · Bounded URM execution stays at its halted value · Every reachable state is reached by bounded execution · Reading the register list · Output after a given number of steps · A halted coded state gives a halting machine run · Initial coded state · Register bound · Coded machine state · Register list
Used byA URM-decidable predicate is computable · A URM-recognizable predicate is recursively enumerable · A URM-computable total function is computed by a multi-stack Turing machine

TheoremA URM-decidable predicate is computable#✓fully proved

If a predicate \(P\) on the natural numbers is URM-decidable, then it is a computable predicate: its Boolean decision function, sending \(n\) to whether \(P(n)\) holds, is computable.

theorem Decidable.computablePred {P : ℕ → Prop} (h : Decidable P) : ComputablePred P
Uses 4 · Used by 2
Statement usesURM-decidable predicate
Proof usesCharacteristic function of a set of naturals · A set is decidable iff its characteristic function is partial recursive · A URM-computable partial function is partial recursive
Used byA URM-decidable predicate is decidable by a single-tape Turing machine · A URM-decidable predicate is decidable by a multi-stack Turing machine

TheoremA URM-recognizable predicate is recursively enumerable#✓fully proved

A URM-recognizable predicate is recursively enumerable.

theorem Recognizable.rePred {P : ℕ → Prop} (h : Recognizable P) : REPred P
Uses 2 · Used by 2
Statement usesURM-recognizable predicates
Proof usesA URM-computable partial function is partial recursive
Used byA URM-recognizable predicate is recognizable by a single-tape Turing machine · A URM-recognizable predicate is recognizable by a multi-stack Turing machine

TheoremA URM-decidable predicate is decidable by a single-tape Turing machine#✓fully proved

A URM-decidable predicate is decidable by a single-tape Turing machine.

theorem Decidable.singleTapeDecidable {P : ℕ → Prop} (h : Decidable P) :
    Cslib.Decidability.SingleTapeDecidable P
Uses 4
Statement usesPredicates decidable by a single-tape Turing machine · URM-decidable predicate
Proof usesSingle-tape decidable predicates are exactly the computable predicates · A URM-decidable predicate is computable

TheoremA URM-decidable predicate is decidable by a multi-stack Turing machine#✓fully proved

A URM-decidable predicate is decidable by a multi-stack Turing machine.

theorem Decidable.tm2Decidable {P : ℕ → Prop} (h : Decidable P) :
    Cslib.Decidability.TM2Decidable P
Uses 4 · Used by 1
Statement usesDecidability by multi-stack machines · URM-decidable predicate
Proof usesMulti-stack decidable predicates are exactly the computable predicates · A URM-decidable predicate is computable
Used byURM-decidability implies multi-stack decidability

TheoremA URM-recognizable predicate is recognizable by a single-tape Turing machine#✓fully proved

A URM-recognizable predicate is recognizable by a single-tape Turing machine.

theorem Recognizable.singleTapeRecognizable {P : ℕ → Prop} (h : Recognizable P) :
    Cslib.Decidability.SingleTapeRecognizable P
Uses 4
Statement usesPredicates recognizable by a single-tape Turing machine · URM-recognizable predicates
Proof usesSingle-tape recognizable predicates are exactly the r.e. predicates · A URM-recognizable predicate is recursively enumerable

TheoremA URM-recognizable predicate is recognizable by a multi-stack Turing machine#✓fully proved

A URM-recognizable predicate is recognizable by a multi-stack Turing machine.

theorem Recognizable.tm2Recognizable {P : ℕ → Prop} (h : Recognizable P) :
    Cslib.Decidability.TM2Recognizable P
Uses 4 · Used by 1
Statement usesRecognizability by multi-stack machines · URM-recognizable predicates
Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates · A URM-recognizable predicate is recursively enumerable
Used byURM-recognizability implies multi-stack recognizability

TheoremA URM-computable total function is computed by a multi-stack Turing machine#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\). Suppose there is a URM program that, for every \(n \in \mathbb{N}\), started with \(n\) in register \(0\) and all other registers \(0\), halts with \(f(n)\) in register \(0\). Then there is a multi-stack Turing machine that computes \(f\) with input and output numbers written in binary: started on the binary word of \(n\), it halts with the binary word of \(f(n)\).

theorem urmComputable_to_tm2 {f : ℕ → ℕ}
    (h : Cslib.URM.Computable 1 fun inputs ↦ Part.some (f (inputs 0))) :
    Nonempty (Turing.TM2Computable Computability.encodeNat Computability.encodeNat f)
Sources
  • Sipser, Introduction to the Theory of Computation, 3rd ed., §3.1 (Church–Turing thesis) and §3.3 (equivalence of models).
Uses 2
Proof usesA URM-computable partial function is partial recursive · Recursive functions are Turing-computable

TheoremURM-decidability implies multi-stack decidability#✓fully proved

Every predicate \(P\) on \(\mathbb{N}\) that is URM-decidable is decidable by a multi-stack Turing machine.

theorem urmDecidable_to_tm2Decidable {P : ℕ → Prop} (h : Cslib.URM.Decidable P) :
    TM2Decidable P
Sources
  • Sipser, Introduction to the Theory of Computation, 3rd ed., §3.1 (Church–Turing thesis).
Uses 3
Statement usesDecidability by multi-stack machines · URM-decidable predicate
Proof usesA URM-decidable predicate is decidable by a multi-stack Turing machine

TheoremURM-recognizability implies multi-stack recognizability#✓fully proved

Every predicate \(P\) on \(\mathbb{N}\) that is URM-recognizable is recognizable by a multi-stack Turing machine.

theorem urmRecognizable_to_tm2Recognizable {P : ℕ → Prop} (h : Cslib.URM.Recognizable P) :
    TM2Recognizable P
Sources
  • Sipser, Introduction to the Theory of Computation, 3rd ed., §3.1 (Church–Turing thesis).
Uses 3
Statement usesRecognizability by multi-stack machines · URM-recognizable predicates
Proof usesA URM-recognizable predicate is recognizable by a multi-stack Turing machine
47 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.