Polynomial-time computable functions

PolyTimeFun α β bundles a function with a closed program of the ambient model (Cost.Basic) computing it on encodings (Cost.Encoding), together with an explicit polynomial time bound. Every "there is a polynomial-time Turing machine …" of the blueprint (thm:introspection, thm:oracularization, thm:answer-reduction, thm:parallel-repetition, thm:compression, and the hypothesis and conclusion of lem:recursive-compression) is a PolyTimeFun.

The time bound is data, not an existential: the recursion of [JNVWY, §12] closes by choosing the parameter λ above the concrete overhead polynomials of the toolkit, and that arithmetic needs the polynomials in hand.

The closure library — the combinator toolkit through which all concrete deciders and transformations will be proven polynomial-time (projections, list/string operations, recursion on notation, arithmetic on binary numbers, 𝔽₂-linear algebra, …) — is the main infrastructure investment of this layer (planning/compression-track.md, K2). Only id and comp are stated here to fix the interface; the library grows with the sections that consume it.

theorem MIPRE.Cost.polynomial_eval_mono (p : Polynomial ℕ) {x y : ℕ} (h : x ≤ y) : Polynomial.eval x p ≤ Polynomial.eval y p

Evaluation of a polynomial with natural coefficients is monotone in the argument.

def MIPRE.Cost.Prog.Runs (p : Prog) (x r : Data) (t : ℕ) : Prop

p computes r from the input x at cost t: a run in the environment [x].

Equations

• p.Runs x r t = MIPRE.Cost.Eval [x] p r t

structure MIPRE.Cost.PolyTimeFun (α : Type u_1) (β : Type u_2) [SizedEncoding α] [SizedEncoding β] : Type (max u_1 u_2)

A polynomial-time computable function α → β: a closed program computing it on encodings, with an explicit polynomial bound on the cost in terms of esize of the input.

• toFun : α → β

  The function computed.

• code : Prog

  A program computing toFun on encodings; its input is variable 0.

• closed : Prog.WellScoped 1 self.code

  The program is closed (well-scoped in the one-entry environment).

• timeBound : Polynomial ℕ

  The (explicit) polynomial time bound.

• computes (a : α) : ∃ t ≤ Polynomial.eval (esize a) self.timeBound, self.code.Runs (encode a) (encode (self.toFun a)) t

@[instance_reducible]

instance MIPRE.Cost.PolyTimeFun.instCoeFunForall {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : CoeFun (PolyTimeFun α β) fun (x : PolyTimeFun α β) => α → β

Equations

• MIPRE.Cost.PolyTimeFun.instCoeFunForall = { coe := MIPRE.Cost.PolyTimeFun.toFun }

theorem MIPRE.Cost.PolyTimeFun.esize_apply_le {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (a : α) : esize (F.toFun a) ≤ Polynomial.eval (esize a) F.timeBound

Polynomial-time output-size bound: a run of cost t produces a result of size at most t (Eval.size_le). This is what makes comp below well-bounded.

noncomputable def MIPRE.Cost.PolyTimeFun.id (α : Type u_4) [SizedEncoding α] : PolyTimeFun α α

The identity, in polynomial time: var 0 reads the input at cost esize a + 1. (noncomputable refers only to the bundled Polynomial ℕ, which is noncomputable data in Mathlib.)

Equations

• MIPRE.Cost.PolyTimeFun.id α = { toFun := id, code := MIPRE.Cost.Prog.var 0, closed := Nat.zero_lt_one, timeBound := Polynomial.X + 1, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.id_apply {α : Type u_1} [SizedEncoding α] (a : α) : (id α).toFun a = a

noncomputable def MIPRE.Cost.PolyTimeFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (G : PolyTimeFun β γ) (F : PolyTimeFun α β) : PolyTimeFun α γ

Composition: bind the value of F and run G on it.

Equations

• G.comp F = { toFun := G.toFun ∘ F.toFun, code := F.code.let_ G.code, closed := ⋯, timeBound := F.timeBound + G.timeBound.comp F.timeBound + 1, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (G : PolyTimeFun β γ) (F : PolyTimeFun α β) (a : α) : (G.comp F).toFun a = G.toFun (F.toFun a)

Further combinators for the closure library (deferred to K2; the list is indicative):

• const : β → PolyTimeFun α β (via Cost.Toolkit.constProg);
• pair : PolyTimeFun α β → PolyTimeFun α γ → PolyTimeFun α (β × γ), fst, snd;
• case analysis on a bit, iteration over a list (loop) with a size-bounded body — the Cobham-style recursion principle: if the step function is polynomial-time and the iterate provably shrinks or preserves size, the recursion is polynomial-time;
• binary arithmetic on ℕ, 𝔽₂- and 𝔽_{2^k}-algebra as needed by samplers, deciders, and the answer-reduction verifier.