Programming with polynomial-time string functions

⚠️ Unreviewed by Bolton

Cobham's theorem makes FP a programming language: a function is polynomial-time exactly when it belongs to the algebra, so a construction can be written as a composition of small pieces instead of assembled as a machine. This file collects the glue that makes the two levels interoperate.

The algebra is stated at every arity, over vectors of arguments, while FP is unary; the bridge is the pairing. binFn_mem_FP turns a two-argument member of the algebra into an FP closure rule, and the rest of the file is that rule applied to the toolkit of Complexitylib.Classes.P.Cobham.Internal.StringOps and Complexitylib.Classes.P.Cobham.Internal.Algebra.

Main results

• Cobham.fstBlockFn, Cobham.sndBlockFn — the pair decoders, in the algebra
• unFn_mem_FP, binFn_mem_FP — algebra members become FP closure rules
• dropLenFn_mem_FP, orBitFn_mem_FP, lenLeFlagFn_mem_FP, eqFlagFn_mem_FP — the rules this gives
• constFn_mem_FP — every constant is polynomial-time
• mem_FP_of_eq — FP respects pointwise equality

theorem Complexity.Cobham.fstBlockFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => pairFst (g v)

The first pair decoder is in the algebra, being polynomial-time.

theorem Complexity.Cobham.sndBlockFn {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) : Cobham fun (v : Fin n → List Bool) => pairSnd (g v)

The second pair decoder is in the algebra.

theorem Complexity.mem_FP_of_eq {f g : List Bool → List Bool} (hf : f ∈ FP) (h : ∀ (z : List Bool), f z = g z) : g ∈ FP

FP respects pointwise equality of functions — the counterpart of Cobham.of_eq, needed because these closure rules produce syntactically specific lambda terms.

From the algebra to FP closure rules

theorem Complexity.unFn_mem_FP {g : List Bool → List Bool} (hg : Cobham fun (v : Fin 1 → List Bool) => g (v 0)) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => g (a z)) ∈ FP

A one-argument member of the algebra is an FP closure rule.

theorem Complexity.binFn_mem_FP {g : List Bool → List Bool → List Bool} (hg : Cobham fun (v : Fin 2 → List Bool) => g (v 0) (v 1)) {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => g (a z) (b z)) ∈ FP

A two-argument member of the algebra is an FP closure rule. The two levels differ only in how arguments are presented: the algebra takes a vector, FP takes the pairing of the two values.

The rules

theorem Complexity.dropLenFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => List.drop (a z).length (b z)) ∈ FP

Dropping a prefix at another value's width is polynomial-time.

theorem Complexity.orBitFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => orBit (a z) (b z)) ∈ FP

Disjunction of flags is polynomial-time.

theorem Complexity.andBitFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => andBit (a z) (b z)) ∈ FP

Conjunction of flags is polynomial-time.

theorem Complexity.notBitFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => notBit (a z)) ∈ FP

Negation of a flag is polynomial-time.

theorem Complexity.lenLeFlagFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => Cobham.lenLeFlag (a z) (b z)) ∈ FP

The length comparison is polynomial-time.

theorem Complexity.eqFlagFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => Cobham.eqFlag (a z) (b z)) ∈ FP

The equality test is polynomial-time.

theorem Complexity.blockAtFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) (i : ℕ) : (fun (z : List Bool) => blockAt (a z) (b z) i) ∈ FP

Reading a fixed field of a block-aligned string is polynomial-time.

theorem Complexity.padToFn_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => padTo (a z) (b z)) ∈ FP

Padding to a ruler's width is polynomial-time.