Polynomial-time many-one reductions and NP-completeness

This file defines polynomial-time many-one (Karp) reductions L ≤ₚ L' and the derived notions NPHard and NPComplete, following Arora–Barak (Definitions 2.7, 2.8).

A reduction L ≤ₚ L' is a polynomial-time computable function f (i.e. f ∈ FP) such that x ∈ L ↔ f x ∈ L'. A language is NP-hard when every language in NP reduces to it, and NP-complete when it is additionally a member of NP.

The headline application is SAT.NPComplete_language (Cook–Levin), in Complexitylib/SAT/CookLevin.lean.

def Complexity.MapReducesPoly (L L' : Language) : Prop

Polynomial-time many-one reduction. MapReducesPoly L L' (written L ≤ₚ L') holds when there is a polynomial-time computable function f (f ∈ FP) with x ∈ L ↔ f x ∈ L' for every input x.

Equations

• (L ≤ₚ L') = ∃ f ∈ Complexity.FP, ∀ (x : List Bool), x ∈ L ↔ f x ∈ L'

def Complexity.«term_≤ₚ_» : Lean.TrailingParserDescr

Polynomial-time many-one reduction. MapReducesPoly L L' (written L ≤ₚ L') holds when there is a polynomial-time computable function f (f ∈ FP) with x ∈ L ↔ f x ∈ L' for every input x.

Equations

• Complexity.«term_≤ₚ_» = Lean.ParserDescr.trailingNode `Complexity.«term_≤ₚ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₚ ") (Lean.ParserDescr.cat `term 51))

def Complexity.NPHard (L : Language) : Prop

NP-hardness. L is NP-hard when every language in NP reduces to L in polynomial time.

Equations

• Complexity.NPHard L = ∀ L' ∈ Complexity.NP, L' ≤ₚ L

def Complexity.NPComplete (L : Language) : Prop

NP-completeness. L is NP-complete when it is in NP and NP-hard.

Equations

• Complexity.NPComplete L = (L ∈ Complexity.NP ∧ Complexity.NPHard L)

≤ₚ is a preorder

Reflexivity follows from id ∈ FP, and transitivity follows from closure of FP under composition. The parameterized helper theorems retain the individual dependencies for reuse.

theorem Complexity.MapReducesPoly.refl_of_id_mem (hid : id ∈ FP) (L : Language) : L ≤ₚ L

Reflexivity of ≤ₚ reduces to id ∈ FP.

theorem Complexity.MapReducesPoly.refl (L : Language) : L ≤ₚ L

Polynomial-time many-one reducibility is reflexive.

theorem Complexity.MapReducesPoly.trans_of_comp (hcomp : ∀ (f g : List Bool → List Bool), f ∈ FP → g ∈ FP → g ∘ f ∈ FP) {L₁ L₂ L₃ : Language} (h₁ : L₁ ≤ₚ L₂) (h₂ : L₂ ≤ₚ L₃) : L₁ ≤ₚ L₃

Transitivity of ≤ₚ reduces to FP being closed under composition.

theorem Complexity.MapReducesPoly.trans {L₁ L₂ L₃ : Language} (h₁ : L₁ ≤ₚ L₂) (h₂ : L₂ ≤ₚ L₃) : L₁ ≤ₚ L₃

Polynomial-time many-one reducibility is transitive.

Transporting P membership

theorem Complexity.MapReducesPoly.mem_P {L₁ L₂ : Language} (hred : L₁ ≤ₚ L₂) (hL₂ : L₂ ∈ P) : L₁ ∈ P

Membership in P transports backward along a polynomial-time many-one reduction.

Transporting NP-hardness and NP-completeness

theorem Complexity.NPHard.of_reduction {L₁ L₂ : Language} (h₁ : NPHard L₁) (h₂ : L₁ ≤ₚ L₂) : NPHard L₂

NP-hardness transfers forward along a polynomial-time many-one reduction.

theorem Complexity.NPComplete.of_mem_of_reduction {L₁ L₂ : Language} (h₁ : NPHard L₁) (hmem : L₂ ∈ NP) (h₂ : L₁ ≤ₚ L₂) : NPComplete L₂

A language in NP is NP-complete when an NP-hard language reduces to it.

theorem Complexity.NPComplete.transfer {L₁ L₂ : Language} (h₁ : NPComplete L₁) (hmem : L₂ ∈ NP) (h₂ : L₁ ≤ₚ L₂) : NPComplete L₂

NP-completeness transfers forward along a polynomial-time reduction once membership of the target language in NP is known.