Cobham's algebra — the working toolkit

Derived members of Complexity.Cobham: the operations a Turing-machine interpreter written inside the algebra needs. Each is a single limited recursion on notation, or a finite composition of such.

Two of these carry the weight. dispatch shows that branching is free: the step functions of recNotation are already selected by the bit being peeled, so a one-step recursion on v 0 is an if-then-else on its leading bit. dropPrefix shows how to move an argument that changes along a recursion — recNotation fixes its parameters, so the changing value has to live in the recursion's value, and iterating tail there gives drop. With drop in hand, takePrefix reads off successive bits, and fixed-width pairing with projections follows.

theorem Complexity.Cobham.of_eq {n : ℕ} {f g : (Fin n → List Bool) → List Bool} (hf : Cobham f) (h : ∀ (v : Fin n → List Bool), f v = g v) : Cobham g

The class respects pointwise equality of functions. Useful because the constructors of Cobham produce syntactically specific lambda terms.

theorem Complexity.Cobham.const {n : ℕ} (s : List Bool) : Cobham fun (x : Fin n → List Bool) => s

Every constant function is in the class: build the constant string bit by bit from empty and the successors.

theorem Complexity.Cobham.comp₂ {n : ℕ} {f : (Fin 2 → List Bool) → List Bool} {g₀ g₁ : (Fin n → List Bool) → List Bool} (hf : Cobham f) (h₀ : Cobham g₀) (h₁ : Cobham g₁) : Cobham fun (v : Fin n → List Bool) => f ![g₀ v, g₁ v]

Composition with two inner functions, packaged for readability: the constructor's Fin-indexed family is awkward to supply when the two components differ.

theorem Complexity.Cobham.comp₃ {n : ℕ} {f : (Fin 3 → List Bool) → List Bool} {g₀ g₁ g₂ : (Fin n → List Bool) → List Bool} (hf : Cobham f) (h₀ : Cobham g₀) (h₁ : Cobham g₁) (h₂ : Cobham g₂) : Cobham fun (v : Fin n → List Bool) => f ![g₀ v, g₁ v, g₂ v]

Composition with three inner functions.

theorem Complexity.Cobham.append : Cobham fun (v : Fin 2 → List Bool) => v 0 ++ v 1

Concatenation is in the class, by limited recursion on notation on the first argument with bound smash (true :: x) (true :: y).

theorem Complexity.Cobham.appendFn {n : ℕ} {g₀ g₁ : (Fin n → List Bool) → List Bool} (h₀ : Cobham g₀) (h₁ : Cobham g₁) : Cobham fun (v : Fin n → List Bool) => g₀ v ++ g₁ v

Concatenation of two members of the class is a member of the class.

theorem Complexity.Cobham.pairing : Cobham fun (v : Fin 2 → List Bool) => pair (v 0) (v 1)

The self-delimiting pairing pair x y = delimit x ++ y is in the class, by limited recursion on notation on x: each peeled bit is doubled onto the recursive value, and the base case emits the separator 01 followed by y. The bound is exact — |pair x y| = |x ++ x| + |y ++ [0,1]|.

theorem Complexity.Cobham.tail : Cobham fun (v : Fin 1 → List Bool) => (v 0).tail

Dropping the leading bit is in the class, by limited recursion on notation: on b :: x both step functions return the peeled tail x, and the argument itself bounds the result.

theorem Complexity.Cobham.dispatch : Cobham fun (v : Fin 3 → List Bool) => caseBit (v 0) (v 1) (v 2)

Bit dispatch is in the class. caseBit (v 0) (v 1) (v 2) is a single limited recursion on notation over v 0: the recursion's own bit-selected step functions do the branching, projecting out v 1 or v 2, and the concatenation of the two branches bounds the result.

theorem Complexity.Cobham.dropPrefix : Cobham fun (v : Fin 2 → List Bool) => List.drop (v 0).length (v 1)

Dropping a prefix of a given length is in the class. v 1 is advanced by one tail per bit of the ruler v 0: the recursion applies tail to its own recursive value, so the changing argument lives in the recursion's value rather than in its parameters — which is what makes it expressible at all.

theorem Complexity.Cobham.takePrefix : Cobham fun (v : Fin 2 → List Bool) => List.take (v 0).length (v 1)

Taking a prefix of a given length is in the class. Each bit of the ruler v 0 appends one more bit of v 1, read off by dispatching on the head of what is still undropped — so dropPrefix and dispatch together give take.

theorem Complexity.Cobham.dispatch₀ : Cobham fun (v : Fin 3 → List Bool) => caseBit₀ (v 0) (v 1) (v 2)

Total bit dispatch is in the class. Same recursion as dispatch, except the base case returns the false branch instead of the empty string — so the empty string reads as false and every flag is genuinely one bit.

theorem Complexity.Cobham.tailFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => (g v).tail

Applying tail to a member of the class.

theorem Complexity.Cobham.iteFn {n : ℕ} {gc gx gy : (Fin n → List Bool) → List Bool} (hc : Cobham gc) (hx : Cobham gx) (hy : Cobham gy) : Cobham fun (v : Fin n → List Bool) => caseBit₀ (gc v) (gx v) (gy v)

Total if-then-else on a flag is in the class.

theorem Complexity.Cobham.andFn {n : ℕ} {g₀ g₁ : (Fin n → List Bool) → List Bool} (h₀ : Cobham g₀) (h₁ : Cobham g₁) : Cobham fun (v : Fin n → List Bool) => andBit (g₀ v) (g₁ v)

The flag connectives are in the class: each is one dispatch₀.

theorem Complexity.Cobham.orFn {n : ℕ} {g₀ g₁ : (Fin n → List Bool) → List Bool} (h₀ : Cobham g₀) (h₁ : Cobham g₁) : Cobham fun (v : Fin n → List Bool) => orBit (g₀ v) (g₁ v)

Disjunction of flags is in the class.

theorem Complexity.Cobham.notFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => notBit (g v)

Negation of a flag is in the class.

theorem Complexity.Cobham.bitAtFn : Cobham fun (v : Fin 2 → List Bool) => bitAt (v 0) (v 1)

Bit extraction is in the class: drop to the marked position and dispatch on what is left.

theorem Complexity.Cobham.headFlagFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => bitAt [] (g v)

Extracting the leading bit of a member of the class, as a flag.

theorem Complexity.Cobham.nonemptyFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => nonemptyFlag (g v)

The nonemptiness flag is in the class. This is the one consumer of the partial dispatcher: both branches are [true], so the flag is [true] exactly when there is a bit to read and [] otherwise.

theorem Complexity.Cobham.matchPrefixFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) (c : List Bool) : Cobham fun (v : Fin n → List Bool) => matchPrefix c (g v)

Matching against a fixed constant is in the class. For each constant the test unfolds into finitely many bit comparisons joined by andFn, so this is a finite composition — the meta-level induction is on the constant, not a recursion inside the algebra.

theorem Complexity.Cobham.takeFn {n : ℕ} {gr gx : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hx : Cobham gx) : Cobham fun (v : Fin n → List Bool) => List.take (gr v).length (gx v)

Taking a prefix of one member of the class at the width of another.

theorem Complexity.Cobham.dropFn {n : ℕ} {gr gx : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hx : Cobham gx) : Cobham fun (v : Fin n → List Bool) => List.drop (gr v).length (gx v)

Dropping a prefix of one member of the class at the width of another.

theorem Complexity.Cobham.lengthPad : Cobham fun (v : Fin 1 → List Bool) => List.replicate (v 0).length false

A block of |x| zeros is in the class, by limited recursion on notation: each peeled bit prepends one 0 to the recursive value, and the argument bounds the result.

theorem Complexity.Cobham.zeroBlockFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) : Cobham fun (v : Fin n → List Bool) => List.replicate (g v).length false

A block of zeros as wide as a member of the class.

theorem Complexity.Cobham.repeatFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (h : Cobham g) (i : ℕ) : Cobham fun (v : Fin n → List Bool) => (List.replicate i (g v)).flatten

Concatenating i copies of a member of the class — a finite composition, so the induction is at the meta level.

theorem Complexity.Cobham.blockFn {n : ℕ} {gr gx : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hx : Cobham gx) (i : ℕ) : Cobham fun (v : Fin n → List Bool) => blockAt (gr v) (gx v) i

Block addressing is in the class. With every field of a configuration padded to the ruler's width, field i is takeFn after dropping i rulers — and i is a fixed natural number, so the drop is a finite concatenation.

theorem Complexity.Cobham.padFn {n : ℕ} {gr gx : (Fin n → List Bool) → List Bool} (hr : Cobham gr) (hx : Cobham gx) : Cobham fun (v : Fin n → List Bool) => padTo (gr v) (gx v)

Fixed-width padding is in the class. With every field of a simulated configuration padded to one ruler's width, field i is recovered by dropping i rulers and taking one — so no self-delimiting decoder is ever needed inside the algebra.

theorem Complexity.Cobham.tableFn {n : ℕ} {g d : (Fin n → List Bool) → List Bool} (hg : Cobham g) (hd : Cobham d) (table : List (List Bool × ((Fin n → List Bool) → List Bool))) (hbranch : ∀ p ∈ table, Cobham p.2) : Cobham fun (v : Fin n → List Bool) => List.foldr (fun (p : List Bool × ((Fin n → List Bool) → List Bool)) (acc : List Bool) => caseBit₀ (matchPrefix p.1 (g v)) (p.2 v) acc) (d v) table

Finite table dispatch is in the class. Matching a member of the class against each of finitely many constant patterns in turn, taking the first branch that fires and a default otherwise, is a finite chain of iteFns.

This is exactly the shape of a Turing machine's transition function: the patterns are the (state, symbols-read) combinations, of which there are finitely many for a fixed machine, and the branches assemble the successor configuration.

theorem Complexity.Cobham.foldr_table_eq (g d val : List Bool) (table : List (List Bool × List Bool)) : (∃ p ∈ table, p.1 <+: g) → (∀ q ∈ table, q.1 <+: g → q.2 = val) → List.foldr (fun (q : List Bool × List Bool) (acc : List Bool) => caseBit₀ (matchPrefix q.1 g) q.2 acc) d table = val

A table of constant patterns is a case analysis. If some entry's pattern prefixes the key, and every entry whose pattern prefixes the key carries the same value, then the fold returns that value — regardless of the order the entries appear in.

Phrasing it as "all matching entries agree" rather than "exactly one matches" avoids having to prove the patterns pairwise distinct: for a transition table the patterns are distinct, but agreement is the weaker and more convenient obligation.

Clocked iteration

The engine of the completeness direction: a machine is simulated by iterating its one-step transition function a polynomial number of times, and both halves of that — the iteration and the polynomial clock — are cheap inside the algebra.

theorem Complexity.Cobham.iterFn {n : ℕ} {e : (Fin n → List Bool) → List Bool} {f j : (Fin (n + 1) → List Bool) → List Bool} (he : Cobham e) (hf : Cobham f) (hj : Cobham j) (hbound : ∀ (c : List Bool) (v : Fin n → List Bool), ((fun (s : List Bool) => f (Fin.cons s v))^[c.length] (e v)).length ≤ (j (Fin.cons c v)).length) : Cobham fun (v : Fin (n + 1) → List Bool) => (fun (s : List Bool) => f (Fin.cons s (Fin.tail v)))^[(v 0).length] (e (Fin.tail v))

Bounded iteration is in the class. Iterating a step function once per bit of a clock string is a single limited recursion on notation: the recursion ignores which bit it peels and simply applies the step to its own recursive value, so h₀ = h₁ = f ∘ Fin.tail. The clock's length is the iteration count, which is why polynomial clocks (exists_pow_clock) give polynomially many steps.

theorem Complexity.Cobham.exists_pow_clock (c d : ℕ) : ∃ (f : (Fin 1 → List Bool) → List Bool), Cobham f ∧ ∀ (v : Fin 1 → List Bool), c * ((v 0).length + 1) ^ d ≤ (f v).length

Clocks. For every constant c and exponent d there is a member of the class whose value on v is at least c · (|v 0| + 1) ^ d bits long — built from constants and smash, which is exactly what smash is for.