Finite-deviation functions are polynomial-time

A function that agrees with the constant empty-output function on all but finitely many inputs is polynomial-time computable. Concretely, for any target function g and finite set S, the function fun s => if s ∈ S then g s else [] belongs to FP: the finite lookup table can be hard-wired into the states of a Turing machine that decides membership in S while scanning the input and then emits the corresponding fixed output, all in linear time.

This is the base case for building up polynomial-time functions — every function with finite support (relative to the empty output) is trivially in FP, regardless of how the values g s are chosen.

The same lookup handles anything that depends on a bounded key: if a polynomial-time function extracts a key of bounded length, then any value or test of that key is polynomial-time, since there are only finitely many keys. The rule applied to the key need not be computable; a constraint given by an alphabet embedding chosen by Classical.choice, say, still runs in polynomial time.

Main definitions

• Complexity.keySet — the strings of bounded length satisfying a predicate

Main results

• ite_mem_finset_mem_FP — fun s => if s ∈ S then g s else [] belongs to FP
• mem_FP_of_bounded_key — a value of a bounded key is polynomial-time
• FPPred.of_bounded_key — so is a test of a bounded key

theorem Complexity.ite_mem_finset_mem_FP (g : List Bool → List Bool) (S : Finset (List Bool)) : (fun (s : List Bool) => if s ∈ S then g s else []) ∈ FP

A function that agrees with the constant empty-output function except on a finite set S — that is, fun s => if s ∈ S then g s else [] — is computable in polynomial (indeed linear) time. The finite table of exceptional values is hard-wired into the lookup machine's states.

Bounded keys

noncomputable def Complexity.keySet (L : ℕ) (Q : List Bool → Prop) : Finset (List Bool)

The strings of length at most L satisfying Q.

Equations

• Complexity.keySet L Q = Finset.filter Q ((Finset.range (L + 1)).biUnion fun (n : ℕ) => Finset.image List.Vector.toList Finset.univ)

theorem Complexity.mem_keySet {L : ℕ} {Q : List Bool → Prop} {s : List Bool} : s ∈ keySet L Q ↔ s.length ≤ L ∧ Q s

theorem Complexity.mem_FP_of_bounded_key {key : List Bool → List Bool} (hkey : key ∈ FP) {L : ℕ} (hL : ∀ (z : List Bool), (key z).length ≤ L) (g : List Bool → List Bool) : (fun (z : List Bool) => g (key z)) ∈ FP

A value of a bounded key is polynomial-time. If key is polynomial-time and its outputs have length at most L, then z ↦ g (key z) is polynomial-time for every g, computable or not.

theorem Complexity.FPPred.of_bounded_key {key : List Bool → List Bool} (hkey : key ∈ FP) {L : ℕ} (hL : ∀ (z : List Bool), (key z).length ≤ L) (Q : List Bool → Prop) : FPPred fun (z : List Bool) => Q (key z)

A test of a bounded key is polynomial-time. If key is polynomial-time and its outputs have length at most L, then z ↦ Q (key z) is a polynomial-time test for every Q, decidable or not.