Strong reducibility and degrees. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
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.
theorem
many_one_reducible.mk
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{f : α → β}
(q : β → Prop)
(h : computable f) :
(λ (a : α), q (f a)) ≤₀ q
@[refl]
@[trans]
theorem
many_one_reducible.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop} :
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.
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
@[refl]
@[trans]
theorem
one_one_reducible.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop} :
theorem
one_one_reducible.to_many_one
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop} :
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) :
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)
@[refl]
@[symm]
theorem
many_one_equiv.symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop} :
many_one_equiv p q → many_one_equiv q p
@[trans]
theorem
many_one_equiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop} :
many_one_equiv p q → many_one_equiv q r → many_one_equiv p r
@[refl]
@[symm]
theorem
one_one_equiv.symm
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{p : α → Prop}
{q : β → Prop} :
one_one_equiv p q → one_one_equiv q p
@[trans]
theorem
one_one_equiv.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop} :
one_one_equiv p q → 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} :
one_one_equiv p q → many_one_equiv p q
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 : α ≃ β} :
e.computable → e.symm.computable
theorem
equiv.computable.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{e₁ : α ≃ β}
{e₂ : β ≃ γ} :
e₁.computable → 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
@[simp]
theorem
many_one_equiv_up
{α : Type u_1}
[primcodable α]
{p : α → Prop} :
many_one_equiv (p ∘ ulower.up) p
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} :
theorem
disjoin_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable γ]
{p : α → Prop}
{q : β → Prop}
{r : γ → Prop} :
Computable and injective mapping of predicates to sets of natural numbers.
Equations
- to_nat p = {n : ℕ | p ((encodable.decode α n).get_or_else inhabited.default)}
@[simp]
@[simp]
@[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 α} :
many_one_equiv (to_nat p) p
@[simp]
theorem
many_one_equiv_to_nat
{α : Type u}
[primcodable α]
[inhabited α]
{β : Type v}
[primcodable β]
[inhabited β]
(p : set α)
(q : set β) :
many_one_equiv (to_nat p) (to_nat q) ↔ many_one_equiv p q
A many-one degree is an equivalence class of sets up to many-one equivalence.
Equations
- many_one_degree = quotient {r := many_one_equiv (primcodable.of_denumerable ℕ), iseqv := many_one_degree._proof_1}
Instances for many_one_degree
The many-one degree of a set on a primcodable type.
Equations
@[protected]
theorem
many_one_degree.ind_on
{C : many_one_degree → Prop}
(d : many_one_degree)
(h : ∀ (p : set ℕ), C (many_one_degree.of p)) :
C d
@[protected, reducible]
def
many_one_degree.lift_on
{φ : Sort u_1}
(d : many_one_degree)
(f : set ℕ → φ)
(h : ∀ (p q : ℕ → Prop), many_one_equiv p q → f p = f q) :
φ
Lifts a function on sets of natural numbers to many-one degrees.
Equations
- d.lift_on f h = quotient.lift_on' d f h
@[protected, simp, reducible]
def
many_one_degree.lift_on₂
{φ : Sort u_1}
(d₁ d₂ : many_one_degree)
(f : set ℕ → set ℕ → φ)
(h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), many_one_equiv p₁ p₂ → many_one_equiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) :
φ
Lifts a binary function on sets of natural numbers to many-one degrees.
@[protected, simp]
theorem
many_one_degree.lift_on₂_eq
{φ : Sort u_1}
(p q : set ℕ)
(f : set ℕ → set ℕ → φ)
(h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), many_one_equiv p₁ p₂ → many_one_equiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) :
(many_one_degree.of p).lift_on₂ (many_one_degree.of 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} :
@[protected, instance]
Equations
@[protected, 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
- many_one_degree.has_le = {le := λ (d₁ d₂ : many_one_degree), d₁.lift_on₂ d₂ many_one_reducible many_one_degree.has_le._proof_1}
@[simp]
theorem
many_one_degree.of_le_of
{α : Type u}
[primcodable α]
[inhabited α]
{β : Type v}
[primcodable β]
[inhabited β]
{p : α → Prop}
{q : β → Prop} :
many_one_degree.of p ≤ many_one_degree.of q ↔ p ≤₀ q
@[protected, instance]
Equations
- many_one_degree.partial_order = {le := has_le.le many_one_degree.has_le, lt := preorder.lt._default has_le.le, le_refl := le_refl, le_trans := many_one_degree.partial_order._proof_1, lt_iff_le_not_le := many_one_degree.partial_order._proof_2, le_antisymm := many_one_degree.partial_order._proof_3}
@[protected, instance]
The join of two degrees, induced by the disjoint union of two underlying sets.
Equations
- many_one_degree.has_add = {add := λ (d₁ d₂ : many_one_degree), d₁.lift_on₂ d₂ (λ (a b : set ℕ), many_one_degree.of (sum.elim a b)) many_one_degree.has_add._proof_1}
@[simp]
theorem
many_one_degree.add_of
{α : Type u}
[primcodable α]
[inhabited α]
{β : Type v}
[primcodable β]
[inhabited β]
(p : set α)
(q : set β) :
@[protected, simp]
@[protected, simp]
@[protected, simp]
@[protected, instance]
Equations
- many_one_degree.semilattice_sup = {sup := has_add.add many_one_degree.has_add, le := partial_order.le many_one_degree.partial_order, lt := partial_order.lt many_one_degree.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := many_one_degree.le_add_left, le_sup_right := many_one_degree.le_add_right, sup_le := many_one_degree.semilattice_sup._proof_1}