Counter machines

InductiveCounter-machine instructions#✓fully proved

A counter-machine instruction is one of: increment register \(r\), decrement register \(r\), or jump to instruction \(q\) if register \(r\) is zero, where the register index \(r\) and the jump target \(q\) are natural numbers.

Decrementing a register that holds \(0\) leaves it at \(0\).

inductive CounterInstr where
  | inc : ℕ → CounterInstr
  | dec : ℕ → CounterInstr
  | jz : ℕ → ℕ → CounterInstr
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Used by 8
Used byCounter-machine decidable predicates · Output of a counter machine · Bounded execution of a counter machine · Counter-machine execution is constant after halting · Counter-machine execution is stable once halted · One step of a counter machine · A counter step is sticky at halting states · Output membership for counter machines

StructureCounter-machine states#✓fully proved

A counter-machine state consists of a program counter, which is a natural number, and the register contents, a function assigning a natural number to every register index \(i \in \mathbb{N}\).

structure CounterState where
  /-- The program counter. -/
  pc : ℕ
  /-- The register contents. -/
  regs : ℕ → ℕ
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Used by 8
Used byOutput of a counter machine · Bounded execution of a counter machine · Counter-machine execution is constant after halting · Counter-machine execution is stable once halted · Initial state of a counter machine · One step of a counter machine · A counter step is sticky at halting states · Output membership for counter machines

DefinitionOne step of a counter machine#✓fully proved

Let \(p\) be a counter-machine program, a list of instructions indexed from \(0\), and let \(s\) be a state with program counter \(c\). If \(c\) is at least the length of \(p\) (the machine has halted), the step leaves \(s\) unchanged. Otherwise it executes instruction \(c\) of \(p\): increment register \(r\) adds \(1\) to register \(r\) and sets the program counter to \(c + 1\); decrement register \(r\) subtracts \(1\) from register \(r\) if it is positive, leaves it at \(0\) otherwise, and sets the program counter to \(c + 1\); jump to \(q\) if register \(r\) is zero leaves the registers unchanged and sets the program counter to \(q\) if register \(r\) holds \(0\) and to \(c + 1\) otherwise.

Because halted states are fixed, the step can be iterated any number of times.

def counterStep (prog : List CounterInstr) (s : CounterState) : CounterState :=
  match prog[s.pc]? with
  | none => s
  | some (.inc r) =>
      { pc := s.pc + 1, regs := Function.update s.regs r (s.regs r + 1) }
  | some (.dec r) =>
      { pc := s.pc + 1, regs := Function.update s.regs r (s.regs r - 1) }
  | some (.jz r q) =>
      { pc := if s.regs r = 0 then q else s.pc + 1, regs := s.regs }
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 2 · Used by 3
Statement usesCounter-machine instructions · Counter-machine states
Used byBounded execution of a counter machine · Counter-machine execution is stable once halted · A counter step is sticky at halting states

DefinitionInitial state of a counter machine#✓fully proved

The initial counter-machine state on a list of inputs \(x_0, \dots, x_{k-1}\) has program counter \(0\), register \(i\) holding \(x_i\) for each \(i < k\), and every other register holding \(0\).

def counterInit (inputs : List ℕ) : CounterState :=
  { pc := 0, regs := fun i ↦ inputs.getD i 0 }
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 1 · Used by 2
Statement usesCounter-machine states
Used byOutput of a counter machine · Output membership for counter machines

DefinitionBounded execution of a counter machine#✓fully proved

For a counter-machine program \(p\), a natural number \(t\) and a state \(s\), the execution of \(p\) for \(t\) steps from \(s\) is the state obtained from \(s\) by applying \(t\) single steps of \(p\).

def counterExecN (prog : List CounterInstr) (t : ℕ) (s : CounterState) : CounterState :=
  (counterStep prog)^[t] s
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 3 · Used by 4
Statement usesCounter-machine instructions · Counter-machine states · One step of a counter machine
Used byOutput of a counter machine · Counter-machine execution is constant after halting · Counter-machine execution is stable once halted · Output membership for counter machines

DefinitionOutput of a counter machine#✓fully proved

The output of a counter-machine program \(p\) on a list of inputs is the partial natural number obtained as follows: run \(p\) from the initial state on those inputs; if for some number \(t\) of steps the program counter is at least the length of \(p\) (the machine has halted), the output is the content of register \(0\) after the least such \(t\); if no such \(t\) exists, the output is undefined.

def counterEval (prog : List CounterInstr) (inputs : List ℕ) : Part ℕ :=
  Nat.rfindOpt fun t ↦
    let s := counterExecN prog t (counterInit inputs)
    if prog.length ≤ s.pc then some (s.regs 0) else Option.none
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 4 · Used by 2
Statement usesCounter-machine instructions · Counter-machine states · Bounded execution of a counter machine · Initial state of a counter machine
Used byCounter-machine decidable predicates · Output membership for counter machines

TheoremA counter step is sticky at halting states#✓fully proved

Past the end of the program the state does not change.

theorem counterStep_sticky {prog : List CounterInstr} {s : CounterState}
    (h : prog.length ≤ s.pc) : counterStep prog s = s
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 3 · Used by 1
Statement usesCounter-machine instructions · Counter-machine states · One step of a counter machine
Used byCounter-machine execution is stable once halted

TheoremCounter-machine execution is stable once halted#✓fully proved

Let \(p\) be a counter-machine program, \(s\) a state and \(t\) a natural number. If the state reached from \(s\) after \(t\) steps of \(p\) has program counter at least the length of \(p\), then the state reached from \(s\) after \(t + 1\) steps equals the state reached after \(t\) steps.

theorem counterExecN_stable {prog : List CounterInstr} {t : ℕ} {s : CounterState}
    (h : prog.length ≤ (counterExecN prog t s).pc) :
    counterExecN prog (t + 1) s = counterExecN prog t s
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 5 · Used by 1
Statement usesCounter-machine instructions · Counter-machine states · Bounded execution of a counter machine
Proof usesOne step of a counter machine · A counter step is sticky at halting states
Used byCounter-machine execution is constant after halting

TheoremCounter-machine execution is constant after halting#✓fully proved

Let \(p\) be a counter-machine program, \(s\) a state, and \(t_1 \le t_2\) natural numbers. If the state reached from \(s\) after \(t_1\) steps of \(p\) has program counter at least the length of \(p\), then the state reached from \(s\) after \(t_2\) steps equals the state reached after \(t_1\) steps.

theorem counterExecN_eq_of_halted {prog : List CounterInstr} {t₁ t₂ : ℕ}
    {s : CounterState}
    (h : prog.length ≤ (counterExecN prog t₁ s).pc) (hle : t₁ ≤ t₂) :
    counterExecN prog t₂ s = counterExecN prog t₁ s
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 4 · Used by 1
Statement usesCounter-machine instructions · Counter-machine states · Bounded execution of a counter machine
Proof usesCounter-machine execution is stable once halted
Used byOutput membership for counter machines

TheoremOutput membership for counter machines#✓fully proved

Let \(P\) be a counter-machine program, let \(x\) be a list of natural-number inputs, and let \(t\) and \(y\) be natural numbers. If the state reached after \(t\) steps of \(P\) from the initial state on \(x\) has program counter at least the length of \(P\) (so the machine has halted) and register \(0\) holds \(y\) in that state, then the output of \(P\) on \(x\) is defined and equals \(y\).

theorem mem_counterEval_of_halted {prog : List CounterInstr} {inputs : List ℕ}
    {y : ℕ} {t : ℕ}
    (hhalt : prog.length ≤ (counterExecN prog t (counterInit inputs)).pc)
    (hout : (counterExecN prog t (counterInit inputs)).regs 0 = y) :
    y ∈ counterEval prog inputs
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 6
Statement usesCounter-machine instructions · Counter-machine states · Output of a counter machine · Bounded execution of a counter machine · Initial state of a counter machine
Proof usesCounter-machine execution is constant after halting

DefinitionCounter-machine decidable predicates#✓fully proved

A predicate \(P\) on the natural numbers is counter-machine decidable when some counter-machine program computes its characteristic function: for every natural number \(n\), the output of the program on the single input \(n\) is defined and equals \(1\) if \(P(n)\) holds and \(0\) otherwise.

def CounterDecidable (P : ℕ → Prop) : Prop :=
  ∃ prog : List CounterInstr, ∀ n, counterEval prog [n] = charFun P n
Sources
  • Minsky, Computation: Finite and Infinite Machines, 1967, §11.
Uses 3
Statement usesCounter-machine instructions · Characteristic function of a set of naturals · Output of a counter machine
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.