Counter programs with random access to the input

A counter program (Turing.CounterProgram) is a finite list of instructions over a fixed number of registers holding natural numbers. An instruction assigns to a register the value of an arithmetic expression (Turing.CounterProgram.Expr: constants, registers, sums, truncated differences, products, quotients, remainders and binary digit tests), branches on a comparison of two expressions, branches on the input bit at the position given by an expression (or on its absence past the end of the input), emits an output bit, or halts with a final output word. Labels are natural numbers; a label outside the program halts.

Counter programs are the classical description of logarithmic-space algorithms: a constant number of counters, each bounded by a polynomial in the input length, with random read-only access to the input. A program whose registers stay at most (n + 1) ^ d on inputs of length n computes a function in logarithmic space (Turing.CounterProgram.computableInLogSpace), as a query machine (Turing.QueryMachine) whose steps are computed in space linear in the binary registers. For programs that never emit, the hypotheses can be established with a reachability predicate (Turing.CounterProgram.Reaches) that records an invariant of the states passed through (Turing.CounterProgram.computableInLogSpace_of_reaches). Programs that emit are treated with the reachability predicate that records the emitted bits (Turing.CounterProgram.ReachesOut). The parts of the simulation by a query machine live in the namespace Turing.CounterProgram.Simulation.

Main definitions

• Turing.CounterProgram.Expr, Turing.CounterProgram.Instr: expressions and instructions.
• Turing.CounterProgram: counter programs.
• Turing.CounterProgram.Config: configurations, a label and the values of the registers.
• Turing.CounterProgram.step, Turing.CounterProgram.Reaches: steps and reachability.
• Turing.CounterProgram.Running: the configurations at running instructions, with bounded registers.
• Turing.CounterProgram.CodeAt: a list of instructions placed at a label.
• Turing.CounterProgram.toQueryMachine: a counter program as a query machine.

Main results

• Turing.CounterProgram.Expr.eval_inSpace: expressions are evaluated in linear space.
• Turing.CounterProgram.Reaches.assign, Turing.CounterProgram.Reaches.lt, Turing.CounterProgram.Reaches.read: stepping through running instructions.
• Turing.CounterProgram.computableInLogSpace: counter programs with polynomially bounded registers run in logarithmic space.
• Turing.CounterProgram.computableInLogSpace_of_reaches: the same, for programs without emissions, from a reachability statement.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

inductive Turing.CounterProgram.Expr : Type

Arithmetic expressions over the registers.

• const (k : ℕ) : Expr

  A constant.

• reg (i : ℕ) : Expr

  The value of a register.

• add (a b : Expr) : Expr

  A sum.

• sub (a b : Expr) : Expr

  Truncated subtraction.

• bit (a i : Expr) : Expr

  A binary digit, with value zero or one.

• mul (a b : Expr) : Expr

  A product.

• div (a b : Expr) : Expr

  A quotient, 0 for the divisor 0.

• mod (a b : Expr) : Expr

  A remainder; the remainder of a by 0 is a.

@[instance_reducible]

instance Turing.CounterProgram.instInhabitedExpr : Inhabited Expr

def Turing.CounterProgram.Expr.eval (regs : List ℕ) : Expr → ℕ

The value of an expression; a register outside the list reads 0.

@[simp]

theorem Turing.CounterProgram.Expr.eval_const (regs : List ℕ) (k : ℕ) : eval regs (const k) = k

@[simp]

theorem Turing.CounterProgram.Expr.eval_reg (regs : List ℕ) (i : ℕ) : eval regs (reg i) = regs.getD i 0

@[simp]

theorem Turing.CounterProgram.Expr.eval_add (regs : List ℕ) (a b : Expr) : eval regs (a.add b) = eval regs a + eval regs b

@[simp]

theorem Turing.CounterProgram.Expr.eval_sub (regs : List ℕ) (a b : Expr) : eval regs (a.sub b) = eval regs a - eval regs b

@[simp]

theorem Turing.CounterProgram.Expr.eval_bit (regs : List ℕ) (a i : Expr) : eval regs (a.bit i) = ((eval regs a).testBit (eval regs i)).toNat

@[simp]

theorem Turing.CounterProgram.Expr.eval_mul (regs : List ℕ) (a b : Expr) : eval regs (a.mul b) = eval regs a * eval regs b

@[simp]

theorem Turing.CounterProgram.Expr.eval_div (regs : List ℕ) (a b : Expr) : eval regs (a.div b) = eval regs a / eval regs b

@[simp]

theorem Turing.CounterProgram.Expr.eval_mod (regs : List ℕ) (a b : Expr) : eval regs (a.mod b) = eval regs a % eval regs b

def Turing.CounterProgram.Expr.pow (e : Expr) : ℕ → Expr

A power of an expression.

def Turing.CounterProgram.Expr.sum : List Expr → Expr

The sum of a list of expressions.

@[simp]

theorem Turing.CounterProgram.Expr.eval_pow (regs : List ℕ) (e : Expr) (k : ℕ) : eval regs (e.pow k) = eval regs e ^ k

@[simp]

theorem Turing.CounterProgram.Expr.eval_sum (regs : List ℕ) (es : List Expr) : eval regs (sum es) = (List.map (fun (e : Expr) => eval regs e) es).sum

inductive Turing.CounterProgram.Instr : Type

Instructions of counter programs, with natural numbers as labels.

• assign (i : ℕ) (e : Expr) (next : ℕ) : Instr

  Assign to register i the value of e, then go to next.

• lt (a b : Expr) (yes no : ℕ) : Instr

  Go to yes if the value of a is less than that of b, to no otherwise.

• read (e : Expr) (onTrue onFalse onEnd : ℕ) : Instr

  Read the input bit at the position given by e: go to onTrue on true, onFalse on false, and onEnd past the end of the input.

• emit (b : Bool) (next : ℕ) : Instr

  Emit the bit b, then go to next.

• halt (out : List Bool) : Instr

  Halt, emitting the word out.

@[instance_reducible]

instance Turing.CounterProgram.instInhabitedInstr : Inhabited Instr

def Turing.CounterProgram.Instr.IsStep : Instr → Prop

The instructions that neither emit nor halt.

@[reducible, inline]

abbrev Turing.CounterProgram.Instr.accept : Instr

Halting with output [true], the verdict of a decider that accepts.

@[reducible, inline]

abbrev Turing.CounterProgram.Instr.reject : Instr

Halting with output [false], the verdict of a decider that rejects.

def Turing.CounterProgram.Instr.maxLabel : Instr → ℕ

The largest label an instruction jumps to.

structure Turing.CounterProgram : Type

A counter program: a list of instructions, indexed by their labels, over a fixed number of registers.

A program assembled from blocks of code writes its code as List.flatten [b₀, b₁, …]. Then rfl quickly reads off the instruction at a label (Turing.CounterProgram.instr), and Turing.CounterProgram.codeAt_of_prefix places a block. Written as b₀ ++ b₁ ++ ⋯, which associates to the left, the same code makes each such lookup far slower.

• code : List Instr

  The instructions; the instruction at label c is the c-th one.

• registers : ℕ

  The number of registers.

@[reducible, inline]

abbrev Turing.CounterProgram.Config : Type

The configurations: a label and the values of the registers.

def Turing.CounterProgram.instr (P : CounterProgram) (c : ℕ) : Instr

The instruction at a label; outside the program, a halt with empty output.

def Turing.CounterProgram.init (P : CounterProgram) : Config

The initial configuration: label 0, all registers 0.

def Turing.CounterProgram.readLabel (onTrue onFalse onEnd : ℕ) : Option Bool → ℕ

The label a read jumps to, given the bit read.

def Turing.CounterProgram.Instr.query (i : Instr) (regs : List ℕ) : ℕ

The position an instruction reads, or 0 if it does not read.

def Turing.CounterProgram.Instr.exec (i : Instr) (s : Config) (b : Option Bool) : Config

The configuration after an instruction, given the input bit read.

def Turing.CounterProgram.Instr.emitted : Instr → List Bool

The bits an instruction emits.

def Turing.CounterProgram.Instr.halts : Instr → Bool

Whether an instruction halts.

def Turing.CounterProgram.Instr.finish : Instr → List Bool

The final word of a halting instruction.

def Turing.CounterProgram.query (P : CounterProgram) (s : Config) : ℕ

The position read in a configuration, or 0 if the instruction does not read.

def Turing.CounterProgram.exec (P : CounterProgram) (s : Config) (b : Option Bool) : Config

The configuration after the instruction at the current label, given the input bit read.

def Turing.CounterProgram.emitted (P : CounterProgram) (s : Config) : List Bool

The bits emitted by the instruction at the current label.

def Turing.CounterProgram.halted (P : CounterProgram) (s : Config) : Bool

Whether the instruction at the current label halts.

def Turing.CounterProgram.finish (P : CounterProgram) (s : Config) : List Bool

The final word of a halting configuration.

def Turing.CounterProgram.toQueryMachine (P : CounterProgram) : QueryMachine Config

A counter program as a query machine.

def Turing.CounterProgram.step (P : CounterProgram) (w : List Bool) (s : Config) : Config

A step of a counter program on the input w.

def Turing.CounterProgram.run (P : CounterProgram) (w : List Bool) (t : ℕ) : Config

The configuration after t steps on the input w.

theorem Turing.CounterProgram.step_eq (P : CounterProgram) (w : List Bool) (s : Config) : P.step w s = if P.halted s = true then s else P.exec s w[P.query s]?

theorem Turing.CounterProgram.run_succ (P : CounterProgram) (w : List Bool) (t : ℕ) : P.run w (t + 1) = P.step w (P.run w t)

theorem Turing.CounterProgram.step_of_isStep (P : CounterProgram) (w : List Bool) {s : Config} (h : (P.instr s.1).IsStep) : P.step w s = P.exec s w[P.query s]?

theorem Turing.CounterProgram.step_assign (P : CounterProgram) (w : List Bool) {s : Config} {i : ℕ} {e : Expr} {next : ℕ} (h : P.instr s.1 = Instr.assign i e next) : P.step w s = (next, s.2.set i (Expr.eval s.2 e))

theorem Turing.CounterProgram.step_lt (P : CounterProgram) (w : List Bool) {s : Config} {x y : Expr} {yes no : ℕ} (h : P.instr s.1 = Instr.lt x y yes no) : P.step w s = (if Expr.eval s.2 x < Expr.eval s.2 y then yes else no, s.2)

theorem Turing.CounterProgram.step_read (P : CounterProgram) (w : List Bool) {s : Config} {e : Expr} {onTrue onFalse onEnd : ℕ} (h : P.instr s.1 = Instr.read e onTrue onFalse onEnd) : P.step w s = (readLabel onTrue onFalse onEnd w[Expr.eval s.2 e]?, s.2)

Reachability

def Turing.CounterProgram.Reaches (P : CounterProgram) (w : List Bool) (Q : Config → Prop) (s s' : Config) : Prop

P.Reaches w Q s s': from s, the program reaches s' on the input w, and every configuration before s' satisfies Q. This is the reflexive and transitive closure of the steps from configurations satisfying Q, stated with a number of steps, the form in which the runs of Turing.CounterProgram.computableInLogSpace are given.

theorem Turing.CounterProgram.Reaches.refl {P : CounterProgram} {w : List Bool} {Q : Config → Prop} (s : Config) : P.Reaches w Q s s

theorem Turing.CounterProgram.Reaches.trans {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {s s' s'' : Config} (h : P.Reaches w Q s s') (h' : P.Reaches w Q s' s'') : P.Reaches w Q s s''

theorem Turing.CounterProgram.Reaches.single {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {s : Config} (hs : Q s) : P.Reaches w Q s (P.step w s)

One step from a configuration satisfying Q.

theorem Turing.CounterProgram.Reaches.head {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {s s' : Config} (hs : Q s) (h : P.Reaches w Q (P.step w s) s') : P.Reaches w Q s s'

theorem Turing.CounterProgram.Reaches.mono {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {s s' : Config} {Q' : Config → Prop} (h : P.Reaches w Q s s') (hQ : ∀ (s : Config), Q s → Q' s) : P.Reaches w Q' s s'

Running configurations

def Turing.CounterProgram.Running (P : CounterProgram) (B : ℕ) (s : Config) : Prop

The configurations at an assignment, a comparison or a read, with all registers at most B.

theorem Turing.CounterProgram.Reaches.assign {P : CounterProgram} {w : List Bool} {s' : Config} {B : ℕ} {regs : List ℕ} {c i : ℕ} {e : Expr} {next : ℕ} (hc : P.instr c = Instr.assign i e next) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Running B) (next, regs.set i (Expr.eval regs e)) s') : P.Reaches w (P.Running B) (c, regs) s'

Stepping through an assignment.

theorem Turing.CounterProgram.Reaches.lt {P : CounterProgram} {w : List Bool} {s' : Config} {B : ℕ} {regs : List ℕ} {c : ℕ} {x y : Expr} {yes no : ℕ} (hc : P.instr c = Instr.lt x y yes no) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Running B) (if Expr.eval regs x < Expr.eval regs y then yes else no, regs) s') : P.Reaches w (P.Running B) (c, regs) s'

Stepping through a comparison.

theorem Turing.CounterProgram.Reaches.read {P : CounterProgram} {w : List Bool} {s' : Config} {B : ℕ} {regs : List ℕ} {c : ℕ} {e : Expr} {onTrue onFalse onEnd : ℕ} (hc : P.instr c = Instr.read e onTrue onFalse onEnd) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Running B) (readLabel onTrue onFalse onEnd w[Expr.eval regs e]?, regs) s') : P.Reaches w (P.Running B) (c, regs) s'

Stepping through a read.

Placing code

def Turing.CounterProgram.CodeAt (P : CounterProgram) (b : ℕ) (l : List Instr) : Prop

P.CodeAt b l: the instructions of l are at the labels from b on.

theorem Turing.CounterProgram.codeAt_nil {P : CounterProgram} {b : ℕ} : P.CodeAt b []

theorem Turing.CounterProgram.codeAt_cons {P : CounterProgram} {b : ℕ} {l : List Instr} {ins : Instr} : P.CodeAt b (ins :: l) ↔ P.instr b = ins ∧ P.CodeAt (b + 1) l

theorem Turing.CounterProgram.codeAt_append {P : CounterProgram} {b : ℕ} {l₁ l₂ : List Instr} : P.CodeAt b (l₁ ++ l₂) ↔ P.CodeAt b l₁ ∧ P.CodeAt (b + l₁.length) l₂

theorem Turing.CounterProgram.CodeAt.flatMap_range {P : CounterProgram} {b : ℕ} {f : ℕ → List Instr} {m : ℕ} (hf : ∀ (i : ℕ), (f i).length = m) {k : ℕ} : P.CodeAt b (List.flatMap f (List.range k)) → ∀ i < k, P.CodeAt (b + m * i) (f i)

The blocks of a code made of blocks of a fixed length.

theorem Turing.CounterProgram.codeAt_of_code_eq {P : CounterProgram} {l pre post : List Instr} (h : P.code = pre ++ l ++ post) : P.CodeAt pre.length l

Code placed in a program made of pieces.

theorem Turing.CounterProgram.codeAt_of_prefix {P : CounterProgram} {b : ℕ} {l : List Instr} (h : l <+: List.drop b P.code) : P.CodeAt b l

Code read off a program: l is at b when the code from label b on starts with l. For code written as List.flatten of its blocks, codeAt_of_prefix ⟨_, rfl⟩ places a block.

The parts of a step, in linear space

theorem Turing.CounterProgram.Expr.eval_inSpace (e : Expr) : MultiTapeTM.ComputableInSpace (fun (regs : List ℕ) => eval regs e) (MultiTapeTM.encList MultiTapeTM.encNat) MultiTapeTM.encNat fun (regs : List ℕ) => ((MultiTapeTM.encList MultiTapeTM.encNat) regs).length

Expressions are evaluated in linear space in the binary registers.

The parts of the simulation of a counter program by a query machine.

@[reducible, inline]

abbrev Turing.CounterProgram.Simulation.encConfig : Config ↪ List Bool

The encoding of configurations: the label and the registers, in binary.

@[reducible, inline]

abbrev Turing.CounterProgram.Simulation.encConfigRead : Config × Option Bool ↪ List Bool

The encoding of a configuration with the bit read.

theorem Turing.CounterProgram.Simulation.evalConfig_inSpace (e : Expr) : MultiTapeTM.ComputableInSpace (fun (s : Config) => Expr.eval s.2 e) encConfig MultiTapeTM.encNat fun (s : Config) => (encConfig s).length

theorem Turing.CounterProgram.Simulation.fst_inSpace : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => x.1) encConfigRead encConfig fun (x : Config × Option Bool) => (encConfigRead x).length

theorem Turing.CounterProgram.Simulation.regs_inSpace : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => x.1.2) encConfigRead (MultiTapeTM.encList MultiTapeTM.encNat) fun (x : Config × Option Bool) => (encConfigRead x).length

theorem Turing.CounterProgram.Simulation.evalConfigRead_inSpace (e : Expr) : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => Expr.eval x.1.2 e) encConfigRead MultiTapeTM.encNat fun (x : Config × Option Bool) => (encConfigRead x).length

theorem Turing.CounterProgram.Simulation.query_inSpace {P : CounterProgram} : MultiTapeTM.ComputableInSpace P.query encConfig MultiTapeTM.encNat fun (s : Config) => (encConfig s).length

theorem Turing.CounterProgram.Simulation.halted_inSpace {P : CounterProgram} : MultiTapeTM.ComputableInSpace P.halted encConfig MultiTapeTM.encBool fun (s : Config) => (encConfig s).length

theorem Turing.CounterProgram.Simulation.finish_inSpace {P : CounterProgram} : MultiTapeTM.ComputableInSpace P.finish encConfig MultiTapeTM.encBits fun (s : Config) => (encConfig s).length

theorem Turing.CounterProgram.Simulation.label_inSpace : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => x.1.1) encConfigRead MultiTapeTM.encNat fun (x : Config × Option Bool) => (encConfigRead x).length

theorem Turing.CounterProgram.Simulation.emitted_inSpace {P : CounterProgram} : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => P.emitted x.1) encConfigRead MultiTapeTM.encBits fun (x : Config × Option Bool) => (encConfigRead x).length

theorem Turing.CounterProgram.Simulation.exec_inSpace {P : CounterProgram} : MultiTapeTM.ComputableInSpace (fun (x : Config × Option Bool) => P.exec x.1 x.2) encConfigRead encConfig fun (x : Config × Option Bool) => (encConfigRead x).length

Logarithmic space

def Turing.CounterProgram.maxLabel (P : CounterProgram) : ℕ

The largest label the program jumps to.

theorem Turing.CounterProgram.Instr.exec_fst_le {i : Instr} (hi : i.halts = false) (s : Config) (b : Option Bool) : (i.exec s b).1 ≤ i.maxLabel

theorem Turing.CounterProgram.Instr.exec_snd_length (i : Instr) (s : Config) (b : Option Bool) : (i.exec s b).2.length = s.2.length

theorem Turing.CounterProgram.run_fst_le (P : CounterProgram) (w : List Bool) (t : ℕ) : (P.run w t).1 ≤ P.maxLabel

The labels of a run are bounded by the largest label of the program.

theorem Turing.CounterProgram.run_snd_length (P : CounterProgram) (w : List Bool) (t : ℕ) : (P.run w t).2.length = P.registers

The number of registers is fixed.

theorem Turing.CounterProgram.Simulation.length_encConfig_le (P : CounterProgram) {N d : ℕ} {s : Config} (hl : s.1 ≤ P.maxLabel) (hn : s.2.length = P.registers) (hr : ∀ r ∈ s.2, r ≤ (N + 1) ^ d) : (encConfig s).length ≤ (2 * (MultiTapeTM.encNat P.maxLabel).length + 1 + P.registers * (2 * d + 3)) * (N.log2 + 1)

theorem Turing.CounterProgram.computableInLogSpace (P : CounterProgram) {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (time : α → ℕ) (hhalt : ∀ (a : α), P.halted (P.run (enc a) (time a)) = true) (hpre : ∀ (a : α), ∀ t < time a, P.halted (P.run (enc a) t) = false) (hf : ∀ (a : α), encOut (f a) = P.toQueryMachine.output (enc a) (time a)) (hbound : ∃ (d : ℕ), ∀ (a : α), ∀ t ≤ time a, ∀ r ∈ (P.run (enc a) t).2, r ≤ ((enc a).length + 1) ^ d) : MultiTapeTM.ComputableInLogSpace f enc encOut

Counter programs run in logarithmic space. Let a counter program halt on every encoded input enc a, first after time a steps, with output encOut (f a). If its registers along these runs stay at most (n + 1) ^ d, where n is the length of the input, then f is computable in logarithmic space.

theorem Turing.CounterProgram.computableInLogSpace_of_reaches (P : CounterProgram) {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (d : ℕ) (h : ∀ (a : α), ∃ (s : Config), P.Reaches (enc a) (P.Running (((enc a).length + 1) ^ d)) P.init s ∧ P.instr s.1 = Instr.halt (encOut (f a)) ∧ ∀ r ∈ s.2, r ≤ ((enc a).length + 1) ^ d) : MultiTapeTM.ComputableInLogSpace f enc encOut

Counter programs without emissions run in logarithmic space, stated with reachability: if on every encoded input enc a the program reaches a halting instruction with final word encOut (f a), passing only through assignments, comparisons and reads, and its registers stay at most (n + 1) ^ d until then, where n is the length of the input, then f is computable in logarithmic space.