Counter programs with output

A counter program (Turing.CounterProgram) emits bits with its emit instructions. This file records what a run emits: P.ReachesOut w Q s s' out says that the program reaches s' from s on the input w, passing only through configurations satisfying Q, and emits out on the way. Reachability without emissions (Turing.CounterProgram.Reaches) through assignments, comparisons and reads emits nothing (Turing.CounterProgram.Reaches.reachesOut). A counting loop (Turing.CounterProgram.forCode) emits, in order, what its body emits for each value of the counter (Turing.CounterProgram.reachesOut_forCode); a loop counting a run of true bits of the input emits nothing (Turing.CounterProgram.reachesOut_count). A program that reaches a halt, emitting the encoding of the value of a function, computes the function in logarithmic space if its registers stay polynomially bounded (Turing.CounterProgram.computableInLogSpace_of_reachesOut): this is the form of a logarithmic-space transducer.

Main definitions

• Turing.CounterProgram.Active: the configurations at instructions other than halts, with bounded registers.
• Turing.CounterProgram.ReachesOut: reachability, with the bits emitted on the way.
• Turing.CounterProgram.forCode: the code of a counting loop.
• Turing.CounterProgram.blocksCode: a fixed list of blocks at successive labels.

Main results

• Turing.CounterProgram.reachesOut_blocksCode: sequence block outputs and preserve an invariant.
• Turing.CounterProgram.reachesOut_forCode: a counting loop emits what its body emits for each value of the counter.
• Turing.CounterProgram.reachesOut_count: a loop counting a run of true bits of the input.
• Turing.CounterProgram.computableInLogSpace_of_reachesOut: counter programs with output and polynomially bounded registers compute functions in logarithmic space.

References

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

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

The configurations at instructions other than halts, with all registers at most B.

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

P.ReachesOut w Q s s' out: from s, the program reaches s' on the input w, every configuration before s' satisfies Q, and the bits emitted before s' are out.

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

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

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

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

theorem Turing.CounterProgram.ReachesOut.of_eq {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {s s' : Config} {out out' : List Bool} (h : P.ReachesOut w Q s s' out) (h' : out = out') : P.ReachesOut w Q s s' out'

def Turing.CounterProgram.blocksCode {α : Type u_1} (code : α → ℕ → List Instr) (len : α → ℕ) : ℕ → List α → List Instr

Concatenate fixed blocks, placing each after the declared lengths of its predecessors.

theorem Turing.CounterProgram.length_blocksCode {α : Type u_1} (code : α → ℕ → List Instr) (len : α → ℕ) (hlen : ∀ (x : α) (b : ℕ), (code x b).length = len x) (b : ℕ) (xs : List α) : (blocksCode code len b xs).length = (List.map len xs).sum

The length of a sequence of blocks is the sum of their declared lengths.

theorem Turing.CounterProgram.reachesOut_blocksCode {P : CounterProgram} {w : List Bool} {Q : Config → Prop} {α : Type u_1} (code : α → ℕ → List Instr) (len : α → ℕ) (hlen : ∀ (x : α) (b : ℕ), (code x b).length = len x) (out : α → List Bool) (Inv : List ℕ → Prop) {xs : List α} (hblock : ∀ x ∈ xs, ∀ (b : ℕ) (regs : List ℕ), P.CodeAt b (code x b) → Inv regs → ∃ (regs' : List ℕ), P.ReachesOut w Q (b, regs) (b + len x, regs') (out x) ∧ Inv regs') (b : ℕ) (regs : List ℕ) (hcode : P.CodeAt b (blocksCode code len b xs)) (hInv : Inv regs) : ∃ (regs' : List ℕ), P.ReachesOut w Q (b, regs) (b + (List.map len xs).sum, regs') (List.flatMap out xs) ∧ Inv regs'

A fixed list of blocks emits their words in order and preserves a register invariant. Each block's actual length must agree with its declared length at every starting label. Sequencing inserts no transitions between the supplied block runs. The empty list has a zero-step run; a zero-length block still requires its own reachability proof.

theorem Turing.CounterProgram.Reaches.reachesOut {P : CounterProgram} {w : List Bool} {s s' : Config} {B : ℕ} (h : P.Reaches w (P.Running B) s s') : P.ReachesOut w (P.Active B) s s' []

Reachability through assignments, comparisons and reads emits nothing.

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

theorem Turing.CounterProgram.ReachesOut.lt {P : CounterProgram} {w : List Bool} {s' : Config} {out : List Bool} {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.ReachesOut w (P.Active B) (if Expr.eval regs x < Expr.eval regs y then yes else no, regs) s' out) : P.ReachesOut w (P.Active B) (c, regs) s' out

theorem Turing.CounterProgram.ReachesOut.read {P : CounterProgram} {w : List Bool} {s' : Config} {out : List Bool} {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.ReachesOut w (P.Active B) (readLabel onTrue onFalse onEnd w[Expr.eval regs e]?, regs) s' out) : P.ReachesOut w (P.Active B) (c, regs) s' out

theorem Turing.CounterProgram.step_emit {P : CounterProgram} {w : List Bool} {s : Config} {b : Bool} {next : ℕ} (h : P.instr s.1 = Instr.emit b next) : P.step w s = (next, s.2)

theorem Turing.CounterProgram.ReachesOut.emit {P : CounterProgram} {w : List Bool} {s' : Config} {out : List Bool} {B : ℕ} {regs : List ℕ} {c : ℕ} {b : Bool} {next : ℕ} (hc : P.instr c = Instr.emit b next) (hB : ∀ r ∈ regs, r ≤ B) (h : P.ReachesOut w (P.Active B) (next, regs) s' out) : P.ReachesOut w (P.Active B) (c, regs) s' (b :: out)

Counting loops

def Turing.CounterProgram.forCode (b u : ℕ) (bound : Expr) (body exit : ℕ) : List Instr

The code of a counting loop, placed at the label b: register u counts from 0 while its value is less than that of bound, running the body at body for each value; the body continues at b + 2, and the loop exits to exit.

theorem Turing.CounterProgram.reachesOut_forCode {P : CounterProgram} {w : List Bool} {B b u body exit N : ℕ} {bound : Expr} (hP : P.CodeAt b (forCode b u bound body exit)) (Inv : ℕ → List ℕ → Prop) (o : ℕ → List Bool) (hNB : N ≤ B) (hInv : ∀ (k : ℕ) (regs : List ℕ), Inv k regs → regs.getD u 0 = k ∧ Expr.eval regs bound = N ∧ u < regs.length ∧ ∀ r ∈ regs, r ≤ B) (hbody : ∀ k < N, ∀ (regs : List ℕ), Inv k regs → ∃ (regs' : List ℕ), P.ReachesOut w (P.Active B) (body, regs) (b + 2, regs') (o k) ∧ regs'.getD u 0 = k ∧ (∀ r ∈ regs', r ≤ B) ∧ Inv (k + 1) (regs'.set u (k + 1))) (regs : List ℕ) (hB : ∀ r ∈ regs, r ≤ B) (h0 : Inv 0 (regs.set u 0)) : ∃ (regs' : List ℕ), P.ReachesOut w (P.Active B) (b, regs) (exit, regs') (List.flatMap o (List.range N)) ∧ Inv N regs'

A counting loop emits what its body emits for each value of the counter. The invariant Inv k holds of the registers when the counter has the value k; it fixes the value N of the bound and keeps the registers at most B. If the body, run on registers satisfying Inv k for k < N, continues at b + 2 with the counter unchanged, emitting o k, and the incremented registers satisfy Inv (k + 1), then the loop exits with registers satisfying Inv N, emitting o 0 ++ ⋯ ++ o (N - 1).

theorem Turing.CounterProgram.reachesOut_count {P : CounterProgram} {w : List Bool} {B c u exit n : ℕ} {e : Expr} (ρ : ℕ → List ℕ) (hc : P.instr c = Instr.read e (c + 1) exit exit) (hc' : P.instr (c + 1) = Instr.assign u ((Expr.reg u).add (Expr.const 1)) c) (hρ : ∀ j < n, (ρ j).set u (Expr.eval (ρ j) ((Expr.reg u).add (Expr.const 1))) = ρ (j + 1)) (hB : ∀ j ≤ n, ∀ r ∈ ρ j, r ≤ B) (htrue : ∀ j < n, w[Expr.eval (ρ j) e]? = some true) (hend : w[Expr.eval (ρ n) e]? ≠ some true) (j : ℕ) : j ≤ n → P.ReachesOut w (P.Active B) (c, ρ j) (exit, ρ n) []

A read-and-count loop. Label c reads the input at e; on true, label c + 1 increments register u and returns to c, and on anything else the loop exits to exit. The registers ρ j are those after j increments. If the read is true exactly below n on the registers ρ j, then from any ρ j with j ≤ n the loop exits with the registers ρ n, emitting nothing.

Logarithmic space

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

Counter programs with output run in logarithmic space. If on every encoded input enc a the program reaches a halting instruction with final word fin, passing only through configurations at other instructions with registers at most (n + 1) ^ d, where n is the length of the input, if the bits emitted on the way followed by fin are encOut (f a), and if the registers of the halting configuration are at most (n + 1) ^ d too, then f is computable in logarithmic space.