FNP and TFNP — Definitions

Core definitions for the function/search complexity classes FNP and TFNP, and the OrRelation combinator used to construct TFNP problems from NP ∩ coNP witness pairs.

def Complexity.FNP : Set (List Bool → List Bool → Prop)

FNP is the class of search problems defined by NP relations: binary relations that are polynomially balanced and decidable in polynomial time. A relation R is in FNP if witnesses have poly-bounded length and the pair language {pair(x, y) | R x y} is in P.

Equations

• Complexity.FNP = {R : List Bool → List Bool → Prop | Complexity.PolyBalanced R ∧ Complexity.pairLang R ∈ Complexity.P}

def Complexity.TFNP : Set (List Bool → List Bool → Prop)

TFNP is the class of total FNP search problems: every instance has at least one witness.

Equations

• Complexity.TFNP = {R : List Bool → List Bool → Prop | R ∈ Complexity.FNP ∧ ∀ (x : List Bool), ∃ (y : List Bool), R x y}

def Complexity.OrRelation (R₁ R₂ : List Bool → List Bool → Prop) : List Bool → List Bool → Prop

Combine two witness relations by disjunction. Used to construct TFNP problems from NP ∩ coNP witness pairs: the combined relation accepts any witness valid for either component.

Equations

• Complexity.OrRelation R₁ R₂ x y = (R₁ x y ∨ R₂ x y)