# mathlibdocumentation

computability.reduce

# 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.

## References

• [Robert Soare, Recursively enumerable sets and degrees][soare1987]

## Tags

computability, reducibility, reduction

def many_one_reducible {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (p : α → Prop) (q : β → Prop) :
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)
theorem many_one_reducible.mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} (q : β → Prop) (h : computable f) :
(λ (a : α), q (f a)) ≤₀ q

theorem many_one_reducible_refl {α : Type u_1} [primcodable α] (p : α → Prop) :
p ≤₀ p

theorem many_one_reducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
p ≤₀ qq ≤₀ rp ≤₀ r

theorem reflexive_many_one_reducible {α : Type u_1} [primcodable α] :

theorem transitive_many_one_reducible {α : Type u_1} [primcodable α] :

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

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

Equations
theorem one_one_reducible.mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} (q : β → Prop) (h : computable f) (i : function.injective f) :
(λ (a : α), q (f a)) ≤₁ q

theorem one_one_reducible_refl {α : Type u_1} [primcodable α] (p : α → Prop) :
p ≤₁ p

theorem one_one_reducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
p ≤₁ qq ≤₁ rp ≤₁ r

theorem one_one_reducible.to_many_one {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :
p ≤₁ qp ≤₀ q

theorem one_one_reducible.of_equiv {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {e : α β} (q : β → Prop) (h : computable e) :
(q e) ≤₁ q

theorem one_one_reducible.of_equiv_symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {e : α β} (q : β → Prop) (h : computable (e.symm)) :
q ≤₁ (q e)

theorem reflexive_one_one_reducible {α : Type u_1} [primcodable α] :

theorem transitive_one_one_reducible {α : Type u_1} [primcodable α] :

theorem computable_pred.computable_of_many_one_reducible {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : computable_pred q) :

theorem computable_pred.computable_of_one_one_reducible {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₁ q) :

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

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

Equations
def one_one_equiv {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (p : α → Prop) (q : β → Prop) :
Prop

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

Equations
theorem many_one_equiv_refl {α : Type u_1} [primcodable α] (p : α → Prop) :

theorem many_one_equiv.symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :

theorem many_one_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :

theorem equivalence_of_many_one_equiv {α : Type u_1} [primcodable α] :

theorem one_one_equiv_refl {α : Type u_1} [primcodable α] (p : α → Prop) :

theorem one_one_equiv.symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :

theorem one_one_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :

theorem equivalence_of_one_one_equiv {α : Type u_1} [primcodable α] :

theorem one_one_equiv.to_many_one {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :

def equiv.computable {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (e : α β) :
Prop

a computable bijection

Equations
theorem equiv.computable.symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {e : α β} :

theorem equiv.computable.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {e₁ : α β} {e₂ : β γ} :
e₁.computablee₂.computable(e₁.trans e₂).computable

theorem computable.eqv (α : Type u_1) [denumerable α] :

theorem computable.equiv₂ (α : Type u_1) (β : Type u_2) [denumerable α] [denumerable β] :

theorem one_one_equiv.of_equiv {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {e : α β} (h : e.computable) {p : β → Prop} :

theorem many_one_equiv.of_equiv {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {e : α β} (h : e.computable) {p : β → Prop} :

theorem many_one_equiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : q) :
p ≤₀ r q ≤₀ r

theorem many_one_equiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : r) :
p ≤₀ q p ≤₀ r

theorem one_one_equiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : q) :
p ≤₁ r q ≤₁ r

theorem one_one_equiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : r) :
p ≤₁ q p ≤₁ r

theorem many_one_equiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : q) :

theorem many_one_equiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : r) :

theorem one_one_equiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : q) :

theorem one_one_equiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : r) :

@[simp]
theorem ulower.down_computable {α : Type u_1} [primcodable α] :

theorem many_one_equiv_up {α : Type u_1} [primcodable α] {p : α → Prop} :
p

theorem one_one_reducible.disjoin_left {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :
p ≤₁ q

theorem one_one_reducible.disjoin_right {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :
q ≤₁ q

theorem disjoin_many_one_reducible {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
p ≤₀ rq ≤₀ r q ≤₀ r

theorem disjoin_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
q ≤₀ r p ≤₀ r q ≤₀ r

def to_nat {α : Type u} [primcodable α] [inhabited α] (p : set α) :

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

Equations
@[simp]
theorem to_nat_many_one_reducible {α : Type u} [primcodable α] [inhabited α] {p : set α} :

@[simp]
theorem many_one_reducible_to_nat {α : Type u} [primcodable α] [inhabited α] {p : set α} :

@[simp]
theorem many_one_reducible_to_nat_to_nat {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] {p : set α} {q : set β} :

@[simp]
theorem to_nat_many_one_equiv {α : Type u} [primcodable α] [inhabited α] {p : set α} :
p

@[simp]
theorem many_one_equiv_to_nat {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] (p : set α) (q : set β) :
(to_nat q)

def many_one_degree  :
Type

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

Equations
def many_one_degree.of {α : Type u} [primcodable α] [inhabited α] (p : α → Prop) :

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

Equations
theorem many_one_degree.ind_on {C : many_one_degree → Prop} (d : many_one_degree) (h : ∀ (p : set ), C ) :
C d

def many_one_degree.lift_on {φ : Sort u_1} (d : many_one_degree) (f : → φ) (h : ∀ (p q : → Prop), f p = f q) :
φ

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

Equations
@[simp]
theorem many_one_degree.lift_on_eq {φ : Sort u_1} (p : set ) (f : → φ) (h : ∀ (p q : → Prop), f p = f q) :
h = f p

@[simp]
def many_one_degree.lift_on₂ {φ : Sort u_1} (d₁ d₂ : many_one_degree) (f : → φ) (h : ∀ (p₁ p₂ q₁ q₂ : → Prop), p₂ q₂f p₁ q₁ = f p₂ q₂) :
φ

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

Equations
@[simp]
theorem many_one_degree.lift_on₂_eq {φ : Sort u_1} (p q : set ) (f : → φ) (h : ∀ (p₁ p₂ q₁ q₂ : → Prop), p₂ q₂f p₁ q₁ = f p₂ q₂) :
f h = f p q

@[simp]
theorem many_one_degree.of_eq_of {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] {p : α → Prop} {q : β → Prop} :

@[instance]

Equations
@[instance]

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 many_one_degree.of_le_of {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] {p : α → Prop} {q : β → Prop} :
p ≤₀ q

@[instance]

Equations
@[instance]

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

Equations
@[simp]
theorem many_one_degree.add_of {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] (p : set α) (q : set β) :

@[simp]
theorem many_one_degree.add_le {d₁ d₂ d₃ : many_one_degree} :
d₁ + d₂ d₃ d₁ d₃ d₂ d₃

@[simp]
theorem many_one_degree.le_add_left (d₁ d₂ : many_one_degree) :
d₁ d₁ + d₂

@[simp]
theorem many_one_degree.le_add_right (d₁ d₂ : many_one_degree) :
d₂ d₁ + d₂

@[instance]

Equations