Promise problems -- definitions

A promise problem has disjoint yes- and no-instance languages. Inputs outside their union are unconstrained. This module keeps semantic solvers, explicit side-preserving maps, and polynomial-time many-one reductions separate.

Ordinary languages embed as total promise problems with no-instances equal to the complement. Gap problems should use PromiseProblem directly rather than arbitrarily assigning the gap region to one side.

structure Complexity.PromiseProblem : Type

A decision promise consisting of disjoint yes- and no-instance languages.

• yesInstances : Language

  Inputs on which a solver must answer yes.

• noInstances : Language

  Inputs on which a solver must answer no.

• disjoint : Disjoint self.yesInstances self.noInstances

  No input receives conflicting promised answers.

def Complexity.PromiseProblem.promise (problem : PromiseProblem) : Language

The set of inputs on which the problem constrains a solver.

Equations

• problem.promise = problem.yesInstances ∪ problem.noInstances

def Complexity.PromiseProblem.SolvedBy (problem : PromiseProblem) (decide : List Bool → Bool) : Prop

A Boolean function solves a promise problem when it gives the required answer on both promised sides. Its behavior outside the promise is arbitrary.

Equations

• problem.SolvedBy decide = ((∀ x ∈ problem.yesInstances, decide x = true) ∧ ∀ x ∈ problem.noInstances, decide x = false)

def Complexity.PromiseProblem.MapReducesVia (source target : PromiseProblem) (f : List Bool → List Bool) : Prop

An explicit map preserves both sides of a promise reduction.

Equations

• source.MapReducesVia target f = ((∀ x ∈ source.yesInstances, f x ∈ target.yesInstances) ∧ ∀ x ∈ source.noInstances, f x ∈ target.noInstances)

def Complexity.PromiseProblem.MapReducesPoly (source target : PromiseProblem) : Prop

Polynomial-time many-one reduction between promise problems.

Equations

• source.MapReducesPoly target = ∃ f ∈ Complexity.FP, source.MapReducesVia target f

def Complexity.PromiseProblem.complement (problem : PromiseProblem) : PromiseProblem

Swap the promised yes and no sides.

Equations

• problem.complement = { yesInstances := problem.noInstances, noInstances := problem.yesInstances, disjoint := ⋯ }

def Complexity.PromiseProblem.ofLanguage (L : Language) : PromiseProblem

Regard an ordinary language as a total promise problem.

Equations

• Complexity.PromiseProblem.ofLanguage L = { yesInstances := L, noInstances := Lᶜ, disjoint := ⋯ }

def Complexity.PromiseClass (C : Set Language) : Set PromiseProblem

Lift a language class to promise problems by total completions. A promise problem belongs to PromiseClass C when some language in C contains every yes-instance and no no-instance. Behavior outside the promise is unrestricted.

Equations

• Complexity.PromiseClass C = {problem : Complexity.PromiseProblem | ∃ completion ∈ C, problem.yesInstances ⊆ completion ∧ Disjoint completion problem.noInstances}

def Complexity.PromiseP : Set PromiseProblem

Promise problems admitting a deterministic polynomial-time completion.

Equations

• Complexity.PromiseP = Complexity.PromiseClass Complexity.P

def Complexity.PromiseNP : Set PromiseProblem

Promise problems admitting a nondeterministic polynomial-time completion.

Equations

• Complexity.PromiseNP = Complexity.PromiseClass Complexity.NP

def Complexity.PromiseCoNP : Set PromiseProblem

Promise problems admitting a coNP completion.

Equations

• Complexity.PromiseCoNP = Complexity.PromiseClass Complexity.coNP

def Complexity.PromiseHardFor (C : Set Language) (target : PromiseProblem) : Prop

A promise problem is hard for a language class when every total language in the class reduces to it by a side-preserving polynomial-time map.

Equations

• Complexity.PromiseHardFor C target = ∀ L ∈ C, (Complexity.PromiseProblem.ofLanguage L).MapReducesPoly target

def Complexity.PromiseCompleteFor (C : Set Language) (target : PromiseProblem) : Prop

A promise problem is complete for a language class when it belongs to the completion-based promise lift and is hard for every total language in the class.

Equations

• Complexity.PromiseCompleteFor C target = (target ∈ Complexity.PromiseClass C ∧ Complexity.PromiseHardFor C target)

def Complexity.PromiseNPHard (target : PromiseProblem) : Prop

Polynomial-time side-preserving NP-hardness for a promise target.

Equations

• Complexity.PromiseNPHard target = Complexity.PromiseHardFor Complexity.NP target

def Complexity.PromiseNPComplete (target : PromiseProblem) : Prop

Completeness for PromiseNP under side-preserving polynomial reductions.

Equations

• Complexity.PromiseNPComplete target = Complexity.PromiseCompleteFor Complexity.NP target