Polynomial-time numbers and tests — definitions

Two predicates that let a polynomial-time construction be stated on natural numbers and propositions instead of on the strings a machine reads and writes.

A number is written in unary, as a string of that many trues. A function from strings to numbers is polynomial-time (UnaryFn) when writing its value in unary is. A test on strings is polynomial-time (FPPred) when a polynomial-time function outputs its verdict as one bit.

Complexitylib.Classes.P.Unary proves that both are closed under the usual arithmetic, comparisons, connectives and bounded loops, so that a function such as z ↦ |z| / 3 can be shown polynomial-time by combining rules.

Main definitions

• Complexity.UnaryFn — a function to ℕ whose value can be written in unary in polynomial time
• Complexity.FPPred — a test decided by a polynomial-time one-bit verdict

def Complexity.UnaryFn (f : List Bool → ℕ) : Prop

A polynomial-time number. UnaryFn f says that writing f z in unary, as f z copies of true, is a polynomial-time function of z.

For example, a randomness or query bound r is time-constructible in the sense of the PCP development exactly when UnaryFn fun x => r x.length.

Equations

• Complexity.UnaryFn f = ((fun (z : List Bool) => List.replicate (f z) true) ∈ Complexity.FP)

def Complexity.FPPred (p : List Bool → Prop) : Prop

A polynomial-time test. FPPred p says that some polynomial-time function outputs a single bit that is true exactly on the strings satisfying p. This is the shape mem_P_of_decisionFn_bool turns into membership in P.

Equations

• Complexity.FPPred p = ∃ (g : List Bool → Bool), (fun (z : List Bool) => [g z]) ∈ Complexity.FP ∧ ∀ (z : List Bool), p z ↔ g z = true