# mathlibdocumentation

computability.reduce

# Strong reducibility and degrees.

This file defines the notions of 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, and deg for the many_one_degree.of a set.

## 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 β] :
(α → Prop)(β → 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) :
(λ (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 β] :
(α → Prop)(β → 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) :
(λ (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) :
(q e) ≤₁ q

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

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} :
p ≤₀ q

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

def many_one_equiv {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
(α → Prop)(β → 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 β] :
(α → Prop)(β → 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 many_one_equiv_setoid {α : Type u_1} [primcodable α] :
setoid (set α)

sets up to many-one equivalence

Equations
def equiv.computable {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
α β → 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} :
(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} :
(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} :
(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} :
(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} :
r r)

theorem many_one_equiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} :
q 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} :
r r)

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

def many_one_degree (α : Type u_1) [primcodable α] :
Type u_1

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

Equations
@[instance]
def many_one_degree.inhabited {α : Type u_1} [primcodable α] :

Equations
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 many_one_degree.le {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
→ Prop

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

Equations
• d₁.le d₂ = d₂ (λ (a : set α) (b : set β), a ≤₀ b) many_one_degree.le._proof_1
@[instance]
def many_one_degree.has_le {α : Type u_1} [primcodable α] :

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

the many-one degree of a set or predicate

Equations
@[simp]
theorem many_one_degree.of_le_of {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (p : α → Prop) (q : β → Prop) :
p ≤₀ q

@[simp]
theorem many_one_degree.of_le_of' {α : Type u_1} [primcodable α] (p q : α → Prop) :
p ≤₀ q

theorem many_one_degree.le_refl {α : Type u_1} [primcodable α] (d : many_one_degree α) :
d.le d

theorem many_one_degree.le_antisymm {α : Type u_1} [primcodable α] {d₁ d₂ : many_one_degree α} :
d₁ d₂d₂ d₁d₁ = d₂

theorem many_one_degree.le_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {d₁ : many_one_degree α} {d₂ : many_one_degree β} {d₃ : many_one_degree γ} :
d₁.le d₂d₂.le d₃d₁.le d₃

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

Given a computable bijection e from α to β, the inverse image from set β to set α lifts to a map on many-one degrees.

Equations
theorem many_one_degree.le_comap_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] (e : α β) (he : e.computable) {d₁ : many_one_degree β} {d₂ : many_one_degree γ} :
d₁).le d₂ d₁.le d₂

theorem many_one_degree.le_comap_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] (e : β γ) (he : e.computable) {d₁ : many_one_degree α} {d₂ : many_one_degree γ} :
d₁.le d₂) d₁.le d₂

def many_one_degree.add {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
many_one_degree β)

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

Equations
@[instance]
def degree_add {α : Type u_1} [denumerable α] :

Equations
theorem many_one_degree.add_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {d₁ : many_one_degree α} {d₂ : many_one_degree β} {d₃ : many_one_degree γ} :
(d₁.add d₂).le d₃ d₁.le d₃ d₂.le d₃

theorem many_one_degree.le_add_left {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (d₁ : many_one_degree α) (d₂ : many_one_degree β) :

theorem many_one_degree.le_add_right {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (d₁ : many_one_degree α) (d₂ : many_one_degree β) :

theorem many_one_degree.add_le' {α : Type u_1} {β : Type u_2} [denumerable α] [primcodable β] {d₁ d₂ : many_one_degree α} {d₃ : many_one_degree β} :
(d₁ + d₂).le d₃ d₁.le d₃ d₂.le d₃

theorem many_one_degree.le_add_left' {α : Type u_1} [denumerable α] (d₁ d₂ : many_one_degree α) :
d₁ d₁ + d₂

theorem many_one_degree.le_add_right' {α : Type u_1} [denumerable α] (d₁ d₂ : many_one_degree α) :
d₂ d₁ + d₂

@[instance]
def many_one_degree.semilattice_sup {α : Type u_1} [denumerable α] :

Equations