Unambiguous polynomial time

UP is defined using polynomial-time verifiers with at most one accepting certificate of the specified polynomial length on every input. Classes.UP.Machine proves the equivalent native finite-machine characterization, preserving accepting-path ambiguity. The coUP extension uses the standard complement-class convention; its containments and reduction closure below are elementary consequences of the corresponding UP results and complement closure of P and parity-P.

Main definitions

• Cslib.Complexity.coUP: complements of UP languages.
• Cslib.Complexity.UP: languages whose characteristic function belongs to #P.

Main results

• Cslib.Complexity.mem_UP: the at-most-one-witness characterization.
• Cslib.Complexity.P_subset_UP, Cslib.Complexity.UP_subset_NP, Cslib.Complexity.UP_subset_ParityP, Cslib.Complexity.coUP_subset_coNP.
• Cslib.Complexity.PolyTimeReducible.mem_UP: closure under polynomial-time reductions.

References

• C. H. Papadimitriou, Computational Complexity

def Cslib.Complexity.UP {α : Type} (enc : α ↪ List Bool) : Set (Set α)

Unambiguous polynomial time: some #P function is bounded by one everywhere and is one exactly on the language Papadimitriou.

theorem Cslib.Complexity.mem_UP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ UP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool ∧ (∀ (a : α), acceptCount V a (Polynomial.eval (enc a).length p) ≤ 1) ∧ ∀ (a : α), a ∈ A ↔ acceptCount V a (Polynomial.eval (enc a).length p) = 1

UP through verifiers: at most one certificate of the specified length accepts on each input, and exactly one accepts on members.

theorem Cslib.Complexity.P_subset_UP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ UP enc

A deterministic decider uses only the empty certificate.

theorem Cslib.Complexity.UP_subset_NP {α : Type} {enc : α ↪ List Bool} : UP enc ⊆ NP enc

An unambiguous verifier is an NP verifier.

theorem Cslib.Complexity.UP_subset_ParityP {α : Type} {enc : α ↪ List Bool} : UP enc ⊆ ParityP enc

An accepting count bounded by one is odd exactly when it is one.

theorem Cslib.Complexity.PolyTimeReducible.mem_UP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ UP encB) : A ∈ UP enc

UP is closed under polynomial-time many-one reductions.

def Cslib.Complexity.coUP {α : Type} (enc : α ↪ List Bool) : Set (Set α)

Complements of unambiguous polynomial-time languages, using the usual co convention.

theorem Cslib.Complexity.mem_coUP {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ coUP enc ↔ Aᶜ ∈ UP enc

@[simp]

theorem Cslib.Complexity.compl_mem_coUP {α : Type} {enc : α ↪ List Bool} {A : Set α} : Aᶜ ∈ coUP enc ↔ A ∈ UP enc

theorem Cslib.Complexity.P_subset_coUP {α : Type} {enc : α ↪ List Bool} : P enc ⊆ coUP enc

Deterministic polynomial time is contained in coUP by closure under complement.

theorem Cslib.Complexity.coUP_subset_coNP {α : Type} {enc : α ↪ List Bool} : coUP enc ⊆ coNP enc

Complementing UP ⊆ NP gives coUP ⊆ coNP.

theorem Cslib.Complexity.coUP_subset_ParityP {α : Type} {enc : α ↪ List Bool} : coUP enc ⊆ ParityP enc

Parity-P is closed under complement, so it contains coUP as well as UP.

theorem Cslib.Complexity.PolyTimeReducible.mem_coUP {α : Type} {enc : α ↪ List Bool} {A : Set α} {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ coUP encB) : A ∈ coUP enc

Polynomial-time reductions preserve coUP by complementing source and target.