mathlib documentation

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

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
theorem many_one_reducible.mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} (q : β → Prop) :
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

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) :
computable ffunction.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) :

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

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

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

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 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 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} :
many_one_equiv p 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} :
many_one_equiv q 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} :
one_one_equiv p 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} :
one_one_equiv q 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} :

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

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

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

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
theorem one_one_reducible.disjoin_left {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → Prop} {q : β → Prop} :

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

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 ≤₀ rsum.elim p q ≤₀ r

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

def many_one_degree.le {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
many_one_degree αmany_one_degree β → 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
@[instance]
def many_one_degree.has_le {α : Type u_1} [primcodable α] :

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

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) :

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

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 : α β) :

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 γ} :
(many_one_degree.comap e he 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 (many_one_degree.comap e he d₂) d₁.le d₂

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

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 β) :
d₁.le (d₁.add d₂)

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

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₂