2.4. Reductions
PolyTimeReducible encA encB A B holds when a function f, computable in polynomial time
from encA to encB, satisfies a ∈ A ↔ f a ∈ B. A reduction is built as a triple: the map, its
cost and its correctness.
example : PolyTimeReducible (encPair encNat encNat) encNat
{p : ℕ × ℕ | p.1 ≤ p.2} {0} :=
⟨fun p => p.1 - p.2, ⊢ ComputableInPolyTime (fun p => p.1 - p.2) (encPair encNat encNat) encNat All goals completed! 🐙,
fun p => p:ℕ × ℕ⊢ p ∈ {p | p.1 ≤ p.2} ↔ (fun p => p.1 - p.2) p ∈ {0} All goals completed! 🐙⟩
Reductions compose (PolyTimeReducible.trans), and P is closed under them
(PolyTimeReducible.mem_P). The library's
checked NP-completeness examples
state deciders, verifiers and reductions in the same plain form.