mathlib3 documentation

computability.reduce

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.

Equations
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]
theorem many_one_reducible_refl {α : Type u_1} [primcodable α] (p : α Prop) :
p ≤₀ p
@[trans]
theorem many_one_reducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α Prop} {q : β Prop} {r : γ Prop} :
p ≤₀ q 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
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]
theorem one_one_reducible_refl {α : Type u_1} [primcodable α] (p : α Prop) :
p ≤₁ p
@[trans]
theorem one_one_reducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α Prop} {q : β Prop} {r : γ Prop} :
p ≤₁ q q ≤₁ r p ≤₁ r
theorem one_one_reducible.to_many_one {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α Prop} {q : β Prop} :
p ≤₁ q p ≤₀ 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 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
@[refl]
theorem many_one_equiv_refl {α : Type u_1} [primcodable α] (p : α Prop) :
@[symm]
theorem many_one_equiv.symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α Prop} {q : β Prop} :
@[trans]
theorem many_one_equiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {p : α Prop} {q : β Prop} {r : γ Prop} :
@[refl]
theorem one_one_equiv_refl {α : Type u_1} [primcodable α] (p : α Prop) :
@[symm]
theorem one_one_equiv.symm {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α Prop} {q : β Prop} :
@[trans]
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 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₂ : β γ} :
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 : 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} (h : 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} (h : 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} (h : 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} (h : many_one_equiv p 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 : many_one_equiv 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} (h : one_one_equiv p 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 : one_one_equiv q r) :
@[simp]
theorem many_one_equiv_up {α : Type u_1} [primcodable α] {p : α Prop} :
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} :
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 α} :
@[simp]
theorem many_one_equiv_to_nat {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] (p : set α) (q : set β) :

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

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

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
@[protected, simp]
theorem many_one_degree.lift_on_eq {φ : Sort u_1} (p : set ) (f : set φ) (h : (p q : Prop), many_one_equiv p q f p = f q) :
@[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.

Equations
@[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₂) :
@[simp]
theorem many_one_degree.of_eq_of {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] {p : α Prop} {q : β Prop} :
@[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
@[simp]
theorem many_one_degree.of_le_of {α : Type u} [primcodable α] [inhabited α] {β : Type v} [primcodable β] [inhabited β] {p : α Prop} {q : β Prop} :
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[simp]
@[protected, simp]
theorem many_one_degree.add_le {d₁ d₂ d₃ : many_one_degree} :
d₁ + d₂ d₃ d₁ d₃ d₂ d₃
@[protected, simp]
theorem many_one_degree.le_add_left (d₁ d₂ : many_one_degree) :
d₁ d₁ + d₂
@[protected, simp]
theorem many_one_degree.le_add_right (d₁ d₂ : many_one_degree) :
d₂ d₁ + d₂