Errorless average-case heuristics -- definitions

An errorless heuristic answers yes, answers no, or explicitly fails. It may fail on any input but may never return an incorrect Boolean answer. Average-case complexity bounds the probability of the failure event under a distribution ensemble.

The canonical answer codec uses [] for failure, [false] for rejection, and [true] for acceptance. Consequently, polynomial runtime is stated directly as membership of the encoded answer function in the existing class FP.

inductive Complexity.HeuristicAnswer : Type

The three possible outputs of an errorless heuristic.

• accept : HeuristicAnswer

  Certified yes answer.

• reject : HeuristicAnswer

  Certified no answer.

• failure : HeuristicAnswer

  Explicit failure to answer.

@[instance_reducible]

instance Complexity.instReprHeuristicAnswer : Repr HeuristicAnswer

Equations

• Complexity.instReprHeuristicAnswer = { reprPrec := Complexity.instReprHeuristicAnswer.repr }

def Complexity.instReprHeuristicAnswer.repr : HeuristicAnswer → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.instDecidableEqHeuristicAnswer : DecidableEq HeuristicAnswer

Equations

• Complexity.instDecidableEqHeuristicAnswer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Complexity.HeuristicAnswer.encode : HeuristicAnswer → List Bool

Canonical output encoding: one Boolean bit for an answer, empty for failure.

Equations

• Complexity.HeuristicAnswer.accept.encode = [true]
• Complexity.HeuristicAnswer.reject.encode = [false]
• Complexity.HeuristicAnswer.failure.encode = []

def Complexity.HeuristicAnswer.decode? : List Bool → Option HeuristicAnswer

Decode one canonical errorless-heuristic answer, rejecting every string of length at least two.

Equations

• Complexity.HeuristicAnswer.decode? [] = some Complexity.HeuristicAnswer.failure
• Complexity.HeuristicAnswer.decode? [true] = some Complexity.HeuristicAnswer.accept
• Complexity.HeuristicAnswer.decode? [false] = some Complexity.HeuristicAnswer.reject
• Complexity.HeuristicAnswer.decode? x✝ = none

def Complexity.HeuristicAnswer.complement : HeuristicAnswer → HeuristicAnswer

Swap yes and no while preserving failure.

Equations

• Complexity.HeuristicAnswer.accept.complement = Complexity.HeuristicAnswer.reject
• Complexity.HeuristicAnswer.reject.complement = Complexity.HeuristicAnswer.accept
• Complexity.HeuristicAnswer.failure.complement = Complexity.HeuristicAnswer.failure

def Complexity.HeuristicAnswer.CorrectFor (answer : HeuristicAnswer) (truth : Prop) : Prop

An answer is sound for a proposition. Failure is always sound; the other two cases assert the corresponding truth value.

Equations

• Complexity.HeuristicAnswer.accept.CorrectFor truth = truth
• Complexity.HeuristicAnswer.reject.CorrectFor truth = ¬truth
• Complexity.HeuristicAnswer.failure.CorrectFor truth = True

@[reducible, inline]

abbrev Complexity.HeuristicAlgorithm : Type

A deterministic semantic heuristic before its efficiency and correctness properties are imposed.

Equations

• Complexity.HeuristicAlgorithm = (List Bool → Complexity.HeuristicAnswer)

def Complexity.HeuristicAlgorithm.encoded (A : HeuristicAlgorithm) : List Bool → List Bool

Canonical binary output function computed by a heuristic.

Equations

• A.encoded x = (A x).encode

def Complexity.HeuristicAlgorithm.IsPolynomialTime (A : HeuristicAlgorithm) : Prop

A heuristic runs in deterministic polynomial time when its canonical three-answer encoding belongs to FP.

Equations

• A.IsPolynomialTime = (A.encoded ∈ Complexity.FP)

def Complexity.HeuristicAlgorithm.IsErrorlessFor (A : HeuristicAlgorithm) (L : Language) : Prop

An errorless heuristic never returns an incorrect answer for L.

Equations

• A.IsErrorlessFor L = ∀ (x : List Bool), (A x).CorrectFor (x ∈ L)

def Complexity.HeuristicAlgorithm.complement (A : HeuristicAlgorithm) : HeuristicAlgorithm

Complement a heuristic pointwise, swapping acceptance and rejection.

Equations

• A.complement x = (A x).complement

def Complexity.HeuristicAlgorithm.ofDecision (decide : List Bool → Bool) : HeuristicAlgorithm

Turn a total Boolean decision function into a never-failing heuristic.

Equations

• Complexity.HeuristicAlgorithm.ofDecision decide x = if decide x = true then Complexity.HeuristicAnswer.accept else Complexity.HeuristicAnswer.reject

def Complexity.HeuristicAlgorithm.answerProbability (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (answer : HeuristicAnswer) (n : ℕ) : ℚ

Exact probability of one answer on one ensemble slice.

Equations

• Complexity.HeuristicAlgorithm.answerProbability D A answer n = D.probability n fun (x : List Bool) => A x = answer

def Complexity.HeuristicAlgorithm.failureProbability (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (n : ℕ) : ℚ

Exact failure probability of a heuristic on one ensemble slice.

Equations

• Complexity.HeuristicAlgorithm.failureProbability D A n = D.probability n fun (x : List Bool) => A x = Complexity.HeuristicAnswer.failure

def Complexity.HeuristicAlgorithm.FailsWithProbabilityAtMost (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (δ : ℕ → ℚ) : Prop

Pointwise failure-probability bound across every ensemble slice.

Equations

• Complexity.HeuristicAlgorithm.FailsWithProbabilityAtMost D A δ = ∀ (n : ℕ), Complexity.HeuristicAlgorithm.failureProbability D A n ≤ δ n

noncomputable def Complexity.FiniteEnsemble.languageProbability (D : FiniteEnsemble (List Bool)) (L : Language) (n : ℕ) : ℚ

Exact mass assigned to a language on one ensemble slice. Classical decidability is confined to this finite semantic enumeration.

Equations

• D.languageProbability L n = D.probability n fun (x : List Bool) => x ∈ L

structure Complexity.DistributionalProblem : Type 1

A language together with a parameterized input distribution. No complexity or samplability condition is imposed by the structure itself.

• language : Language

  Decision problem being solved.

• ensemble : FiniteEnsemble (List Bool)

  Distribution ensemble on inputs.

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

Complement the language while retaining exactly the same input ensemble.

Equations

• problem.complement = { language := problem.languageᶜ, ensemble := problem.ensemble }

def Complexity.AvgPAt (δ : ℕ → ℚ) : Set DistributionalProblem

Distributional problems admitting a deterministic polynomial-time errorless heuristic with failure bounded by δ on every slice.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.inversePolynomialFailure (c n : ℕ) : ℚ

Total inverse-polynomial failure bound. It agrees with n⁻ᶜ for positive n and assigns the harmless bound one to the zero slice.

Equations

• Complexity.inversePolynomialFailure c n = 1 / ↑(Nat.max 1 n) ^ c

def Complexity.AvgP : Set DistributionalProblem

Errorless average-case polynomial time: for every inverse-polynomial failure target, a polynomial-time errorless heuristic meets that target.

Equations

• Complexity.AvgP = ⋂ (c : ℕ), Complexity.AvgPAt (Complexity.inversePolynomialFailure c)