# Strong reducibility and degrees. #

This file defines the notions of computable many-one reduction and one-one reduction between sets, and shows that the corresponding degrees form a semilattice.

## Notations #

This file uses the local notation ⊕' for Sum.elim to denote the disjoint union of two degrees.

## Tags #

computability, reducibility, reduction

def ManyOneReducible {α : Type u_1} {β : Type u_2} [] [] (p : αProp) (q : βProp) :

p is many-one reducible to q if there is a computable function translating questions about p to questions about q.

Equations
• p ≤₀ q = ∃ (f : αβ), ∀ (a : α), p a q (f a)
Instances For

p is many-one reducible to q if there is a computable function translating questions about p to questions about q.

Equations
Instances For
theorem ManyOneReducible.mk {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (q : βProp) (h : ) :
(fun (a : α) => q (f a)) ≤₀ q
theorem manyOneReducible_refl {α : Type u_1} [] (p : αProp) :
p ≤₀ p
theorem ManyOneReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
p ≤₀ qq ≤₀ rp ≤₀ r
theorem reflexive_manyOneReducible {α : Type u_1} [] :
Reflexive ManyOneReducible
theorem transitive_manyOneReducible {α : Type u_1} [] :
Transitive ManyOneReducible
def OneOneReducible {α : Type u_1} {β : Type u_2} [] [] (p : αProp) (q : βProp) :

p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

Equations
Instances For

p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

Equations
Instances For
theorem OneOneReducible.mk {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (q : βProp) (h : ) (i : ) :
(fun (a : α) => q (f a)) ≤₁ q
theorem oneOneReducible_refl {α : Type u_1} [] (p : αProp) :
p ≤₁ p
theorem OneOneReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
p ≤₁ qq ≤₁ rp ≤₁ r
theorem OneOneReducible.to_many_one {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
p ≤₁ qp ≤₀ q
theorem OneOneReducible.of_equiv {α : Type u_1} {β : Type u_2} [] [] {e : α β} (q : βProp) (h : ) :
(q e) ≤₁ q
theorem OneOneReducible.of_equiv_symm {α : Type u_1} {β : Type u_2} [] [] {e : α β} (q : βProp) (h : Computable e.symm) :
q ≤₁ (q e)
theorem reflexive_oneOneReducible {α : Type u_1} [] :
Reflexive OneOneReducible
theorem transitive_oneOneReducible {α : Type u_1} [] :
Transitive OneOneReducible
theorem ComputablePred.computable_of_manyOneReducible {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} (h₁ : p ≤₀ q) (h₂ : ) :
theorem ComputablePred.computable_of_oneOneReducible {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} (h : p ≤₁ q) :
def ManyOneEquiv {α : Type u_1} {β : Type u_2} [] [] (p : αProp) (q : βProp) :

p and q are many-one equivalent if each one is many-one reducible to the other.

Equations
Instances For
def OneOneEquiv {α : Type u_1} {β : Type u_2} [] [] (p : αProp) (q : βProp) :

p and q are one-one equivalent if each one is one-one reducible to the other.

Equations
Instances For
theorem manyOneEquiv_refl {α : Type u_1} [] (p : αProp) :
theorem ManyOneEquiv.symm {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
theorem ManyOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
theorem equivalence_of_manyOneEquiv {α : Type u_1} [] :
Equivalence ManyOneEquiv
theorem oneOneEquiv_refl {α : Type u_1} [] (p : αProp) :
theorem OneOneEquiv.symm {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
theorem OneOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
theorem equivalence_of_oneOneEquiv {α : Type u_1} [] :
Equivalence OneOneEquiv
theorem OneOneEquiv.to_many_one {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
def Equiv.Computable {α : Type u_1} {β : Type u_2} [] [] (e : α β) :

a computable bijection

Equations
Instances For
theorem Equiv.Computable.symm {α : Type u_1} {β : Type u_2} [] [] {e : α β} :
e.Computablee.symm.Computable
theorem Equiv.Computable.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {e₁ : α β} {e₂ : β γ} :
e₁.Computablee₂.Computable(e₁.trans e₂).Computable
theorem Computable.eqv (α : Type u_1) [] :
.Computable
theorem Computable.equiv₂ (α : Type u_1) (β : Type u_2) [] [] :
.Computable
theorem OneOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [] [] {e : α β} (h : e.Computable) {p : βProp} :
OneOneEquiv (p e) p
theorem ManyOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [] [] {e : α β} (h : e.Computable) {p : βProp} :
ManyOneEquiv (p e) p
theorem ManyOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
p ≤₀ r q ≤₀ r
theorem ManyOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
p ≤₀ q p ≤₀ r
theorem OneOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
p ≤₁ r q ≤₁ r
theorem OneOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
p ≤₁ q p ≤₁ r
theorem ManyOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
theorem ManyOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
theorem OneOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
theorem OneOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} (h : ) :
@[simp]
theorem ULower.down_computable {α : Type u_1} [] :
(ULower.equiv α).Computable
theorem manyOneEquiv_up {α : Type u_1} [] {p : αProp} :
ManyOneEquiv (p ULower.up) p
theorem OneOneReducible.disjoin_left {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
theorem OneOneReducible.disjoin_right {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {q : βProp} :
theorem disjoin_manyOneReducible {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
p ≤₀ rq ≤₀ rSum.elim p q ≤₀ r
theorem disjoin_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {p : αProp} {q : βProp} {r : γProp} :
def toNat {α : Type u} [] [] (p : Set α) :

Computable and injective mapping of predicates to sets of natural numbers.

Equations
• = {n : | p (.getD default)}
Instances For
@[simp]
theorem toNat_manyOneReducible {α : Type u} [] [] {p : Set α} :
@[simp]
theorem manyOneReducible_toNat {α : Type u} [] [] {p : Set α} :
@[simp]
theorem manyOneReducible_toNat_toNat {α : Type u} [] [] {β : Type v} [] [] {p : Set α} {q : Set β} :
@[simp]
theorem toNat_manyOneEquiv {α : Type u} [] [] {p : Set α} :
@[simp]
theorem manyOneEquiv_toNat {α : Type u} [] [] {β : Type v} [] [] (p : Set α) (q : Set β) :

A many-one degree is an equivalence class of sets up to many-one equivalence.

Equations
Instances For
def ManyOneDegree.of {α : Type u} [] [] (p : αProp) :

The many-one degree of a set on a primcodable type.

Equations
Instances For
theorem ManyOneDegree.ind_on {C : } (d : ManyOneDegree) (h : ∀ (p : ), C ) :
C d
@[reducible, inline]
abbrev ManyOneDegree.liftOn {φ : Sort u_1} (d : ManyOneDegree) (f : φ) (h : ∀ (p q : ), f p = f q) :
φ

Lifts a function on sets of natural numbers to many-one degrees.

Equations
• d.liftOn f h =
Instances For
@[simp]
theorem ManyOneDegree.liftOn_eq {φ : Sort u_1} (p : ) (f : φ) (h : ∀ (p q : ), f p = f q) :
.liftOn f h = f p
@[reducible]
def ManyOneDegree.liftOn₂ {φ : Sort u_1} (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) (f : φ) (h : ∀ (p₁ p₂ q₁ q₂ : ), ManyOneEquiv p₁ p₂ManyOneEquiv q₁ q₂f p₁ q₁ = f p₂ q₂) :
φ

Lifts a binary function on sets of natural numbers to many-one degrees.

Equations
• d₁.liftOn₂ d₂ f h = d₁.liftOn (fun (p : ) => d₂.liftOn (f p) )
Instances For
@[simp]
theorem ManyOneDegree.liftOn₂_eq {φ : Sort u_1} (p : ) (q : ) (f : φ) (h : ∀ (p₁ p₂ q₁ q₂ : ), ManyOneEquiv p₁ p₂ManyOneEquiv q₁ q₂f p₁ q₁ = f p₂ q₂) :
.liftOn₂ f h = f p q
@[simp]
theorem ManyOneDegree.of_eq_of {α : Type u} [] [] {β : Type v} [] [] {p : αProp} {q : βProp} :
Equations

For many-one degrees d₁ and d₂, d₁ ≤ d₂ if the sets in d₁ are many-one reducible to the sets in d₂.

Equations
@[simp]
theorem ManyOneDegree.of_le_of {α : Type u} [] [] {β : Type v} [] [] {p : αProp} {q : βProp} :
p ≤₀ q

The join of two degrees, induced by the disjoint union of two underlying sets.

Equations
@[simp]
theorem ManyOneDegree.add_of {α : Type u} [] [] {β : Type v} [] [] (p : Set α) (q : Set β) :
@[simp]
theorem ManyOneDegree.add_le {d₁ : ManyOneDegree} {d₂ : ManyOneDegree} {d₃ : ManyOneDegree} :
d₁ + d₂ d₃ d₁ d₃ d₂ d₃
@[simp]
theorem ManyOneDegree.le_add_left (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) :
d₁ d₁ + d₂
@[simp]
theorem ManyOneDegree.le_add_right (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) :
d₂ d₁ + d₂