Guarded polynomial-time reductions

Many reductions are faithful only on instances with some syntactic shape, such as a clause-width bound or well-formed arities, and send every other instance to a fixed rejected instance. This module states that pattern once.

Main results

• Cslib.Complexity.PolyTimeReducible.of_guard: a polynomial-time test g and a polynomial-time map f with a ∈ A ↔ g a = true ∧ f a ∈ B give a reduction from A to B, sending the instances that fail the test to a fixed instance outside B.

theorem Cslib.Complexity.PolyTimeReducible.of_guard {α : Type u_1} {β : Type u_2} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} {g : α → Bool} {f : α → β} (b₀ : β) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encA Turing.MultiTapeTM.encBool) (hf : Turing.MultiTapeTM.ComputableInPolyTime f encA encB) (hb₀ : b₀ ∉ B) (h : ∀ (a : α), a ∈ A ↔ g a = true ∧ f a ∈ B) : PolyTimeReducible encA encB A B

Guarded reduction. If membership in A is a polynomial-time test g together with membership of f a in B, for a polynomial-time map f, then a ↦ if g a then f a else b₀ reduces A to B for any fixed b₀ ∉ B.