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 β]
(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 : α → β), computable 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.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop}
(a : p ≤₀ q)
(a_1 : q ≤₀ r) :
p ≤₀ r
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
- p ≤₁ q = ∃ (f : α → β), computable f ∧ function.injective f ∧ ∀ (a : α), p a ↔ q (f a)
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.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop}
(a : p ≤₁ q)
(a_1 : q ≤₁ r) :
p ≤₁ r
theorem
one_one_reducible.to_many_one
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop}
(a : p ≤₁ q) :
p ≤₀ q
theorem
one_one_reducible.of_equiv
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{e : α ≃ β}
(q : β → Prop)
(h : computable ⇑e) :
theorem
one_one_reducible.of_equiv_symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{e : α ≃ β}
(q : β → Prop)
(h : computable ⇑(e.symm)) :
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)
(a : computable_pred 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
- many_one_equiv p q = (p ≤₀ q ∧ q ≤₀ p)
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
- one_one_equiv p q = (p ≤₁ q ∧ q ≤₁ p)
theorem
many_one_equiv.symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop}
(a : many_one_equiv p q) :
many_one_equiv q p
theorem
many_one_equiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop}
(a : many_one_equiv p q)
(a_1 : many_one_equiv q r) :
many_one_equiv p r
theorem
one_one_equiv.symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop}
(a : one_one_equiv p q) :
one_one_equiv q p
theorem
one_one_equiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop}
(a : one_one_equiv p q)
(a_1 : one_one_equiv q r) :
one_one_equiv p r
theorem
one_one_equiv.to_many_one
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop}
(a : one_one_equiv p q) :
many_one_equiv p q
sets up to many-one equivalence
Equations
- many_one_equiv_setoid = {r := many_one_equiv _inst_1, iseqv := _}
def
equiv.computable
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
(e : α ≃ β) :
Prop
a computable bijection
Equations
- e.computable = (computable ⇑e ∧ computable ⇑(e.symm))
theorem
equiv.computable.symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{e : α ≃ β}
(a : e.computable) :
theorem
equiv.computable.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{e₁ : α ≃ β}
{e₂ : β ≃ γ}
(a : e₁.computable)
(a_1 : e₂.computable) :
(e₁.trans e₂).computable
theorem
computable.equiv₂
(α : Type u_1)
(β : Type u_2)
[denumerable α]
[denumerable β] :
(denumerable.equiv₂ α β).computable
theorem
one_one_equiv.of_equiv
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{e : α ≃ β}
(h : e.computable)
{p : β → Prop} :
one_one_equiv (p ∘ ⇑e) p
theorem
many_one_equiv.of_equiv
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{e : α ≃ β}
(h : e.computable)
{p : β → Prop} :
many_one_equiv (p ∘ ⇑e) p
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 : many_one_equiv p q) :
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 : many_one_equiv q 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 : one_one_equiv p q) :
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 : one_one_equiv q 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 : many_one_equiv p q) :
many_one_equiv p r ↔ many_one_equiv q 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}
(h : many_one_equiv q r) :
many_one_equiv p q ↔ many_one_equiv p 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 : one_one_equiv p q) :
one_one_equiv p r ↔ one_one_equiv q 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}
(h : one_one_equiv q r) :
one_one_equiv p q ↔ one_one_equiv p r
A many-one degree is an equivalence class of sets up to many-one equivalence.
Equations
@[instance]
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}
(a : p ≤₀ r)
(a_1 : 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 β]
(d₁ : many_one_degree α)
(d₂ : 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₂.
@[instance]
Equations
- many_one_degree.has_le = {le := many_one_degree.le _inst_1}
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) :
(many_one_degree.of p).le (many_one_degree.of q) ↔ p ≤₀ q
@[simp]
theorem
many_one_degree.of_le_of'
{α : Type u_1}
[primcodable α]
(p q : α → Prop) :
many_one_degree.of p ≤ many_one_degree.of q ↔ p ≤₀ q
theorem
many_one_degree.le_antisymm
{α : Type u_1}
[primcodable α]
{d₁ d₂ : many_one_degree α}
(a : d₁ ≤ d₂)
(a_1 : 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 γ}
(a : d₁.le d₂)
(a_1 : d₂.le d₃) :
d₁.le d₃
def
many_one_degree.comap
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
(e : α ≃ β)
(he : e.computable)
(d : many_one_degree β) :
Given a computable bijection e from α to β, the inverse image from set β to set α lifts
to a map on many-one degrees.
Equations
- many_one_degree.comap e he d = quotient.lift_on' d (λ (p : set β), many_one_degree.of (p ∘ ⇑e)) _
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 β]
(d₁ : many_one_degree α)
(d₂ : many_one_degree β) :
many_one_degree (α ⊕ β)
the join of two degrees, induced by the disjoint union of two underlying sets
Equations
- d₁.add d₂ = quotient.lift_on₂' d₁ d₂ (λ (a : set α) (b : set β), many_one_degree.of (sum.elim a b)) many_one_degree.add._proof_1
@[instance]
Equations
- degree_add = {add := λ (d₁ d₂ : many_one_degree α), many_one_degree.comap (denumerable.equiv₂ α (α ⊕ α)) degree_add._proof_1 (d₁.add d₂)}
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 γ} :
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 β} :
@[instance]
Equations
- many_one_degree.semilattice_sup = {sup := has_add.add degree_add, le := has_le.le many_one_degree.has_le, lt := partial_order.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}