Strong reducibility and degrees.

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

• Robert Soare, Recursively enumerable sets and degrees

Tags

computability, reducibility, reduction

def ManyOneReducible {α : 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)

def «term_≤₀_» : Lean.TrailingParserDescr

p is many-one reducible to q if there is a computable function translating questions about p to questions about q.

Equations

• «term_≤₀_» = Lean.ParserDescr.trailingNode `«term_≤₀_» 1000 1000 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤₀ ") (Lean.ParserDescr.cat `term 1001))

theorem ManyOneReducible.mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} (q : β → Prop) (h : Computable f) : (fun (a : α) => q (f a)) ≤₀ q

theorem manyOneReducible_refl {α : Type u_1} [Primcodable α] (p : α → Prop) : p ≤₀ p

theorem ManyOneReducible.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 reflexive_manyOneReducible {α : Type u_1} [Primcodable α] : Reflexive ManyOneReducible

theorem transitive_manyOneReducible {α : Type u_1} [Primcodable α] : Transitive ManyOneReducible

def OneOneReducible {α : 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)

def «term_≤₁_» : Lean.TrailingParserDescr

p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

Equations

• «term_≤₁_» = Lean.ParserDescr.trailingNode `«term_≤₁_» 1000 1000 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤₁ ") (Lean.ParserDescr.cat `term 1001))

theorem OneOneReducible.mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} (q : β → Prop) (h : Computable f) (i : Function.Injective f) : (fun (a : α) => q (f a)) ≤₁ q

theorem oneOneReducible_refl {α : Type u_1} [Primcodable α] (p : α → Prop) : p ≤₁ p

theorem OneOneReducible.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 OneOneReducible.to_many_one {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : p ≤₁ q → p ≤₀ q

theorem OneOneReducible.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α ≃ β} (q : β → Prop) (h : Computable ⇑e) : (q ∘ ⇑e) ≤₁ q

theorem OneOneReducible.of_equiv_symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α ≃ β} (q : β → Prop) (h : Computable ⇑e.symm) : q ≤₁ (q ∘ ⇑e)

theorem reflexive_oneOneReducible {α : Type u_1} [Primcodable α] : Reflexive OneOneReducible

theorem transitive_oneOneReducible {α : Type u_1} [Primcodable α] : Transitive OneOneReducible

theorem ComputablePred.computable_of_manyOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h₁ : p ≤₀ q) (h₂ : ComputablePred q) : ComputablePred p

theorem ComputablePred.computable_of_oneOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (h : p ≤₁ q) : ComputablePred q → ComputablePred p

def ManyOneEquiv {α : 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

• ManyOneEquiv p q = (p ≤₀ q ∧ q ≤₀ p)

def OneOneEquiv {α : 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

• OneOneEquiv p q = (p ≤₁ q ∧ q ≤₁ p)

theorem manyOneEquiv_refl {α : Type u_1} [Primcodable α] (p : α → Prop) : ManyOneEquiv p p

theorem ManyOneEquiv.symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : ManyOneEquiv p q → ManyOneEquiv q p

theorem ManyOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} : ManyOneEquiv p q → ManyOneEquiv q r → ManyOneEquiv p r

theorem equivalence_of_manyOneEquiv {α : Type u_1} [Primcodable α] : Equivalence ManyOneEquiv

theorem oneOneEquiv_refl {α : Type u_1} [Primcodable α] (p : α → Prop) : OneOneEquiv p p

theorem OneOneEquiv.symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : OneOneEquiv p q → OneOneEquiv q p

theorem OneOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} : OneOneEquiv p q → OneOneEquiv q r → OneOneEquiv p r

theorem equivalence_of_oneOneEquiv {α : Type u_1} [Primcodable α] : Equivalence OneOneEquiv

theorem OneOneEquiv.to_many_one {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : OneOneEquiv p q → ManyOneEquiv 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.eqv (α : Type u_1) [Denumerable α] : (Denumerable.eqv α).Computable

theorem Computable.equiv₂ (α : Type u_1) (β : Type u_2) [Denumerable α] [Denumerable β] : (Denumerable.equiv₂ α β).Computable

theorem OneOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α ≃ β} (h : e.Computable) {p : β → Prop} : OneOneEquiv (p ∘ ⇑e) p

theorem ManyOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α ≃ β} (h : e.Computable) {p : β → Prop} : ManyOneEquiv (p ∘ ⇑e) p

theorem ManyOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : ManyOneEquiv p q) : p ≤₀ r ↔ q ≤₀ r

theorem ManyOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : ManyOneEquiv q r) : p ≤₀ q ↔ p ≤₀ r

theorem OneOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : OneOneEquiv p q) : p ≤₁ r ↔ q ≤₁ r

theorem OneOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : OneOneEquiv q r) : p ≤₁ q ↔ p ≤₁ r

theorem ManyOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : ManyOneEquiv p q) : ManyOneEquiv p r ↔ ManyOneEquiv q r

theorem ManyOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : ManyOneEquiv q r) : ManyOneEquiv p q ↔ ManyOneEquiv p r

theorem OneOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : OneOneEquiv p q) : OneOneEquiv p r ↔ OneOneEquiv q r

theorem OneOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} (h : OneOneEquiv q r) : OneOneEquiv p q ↔ OneOneEquiv p r

@[simp]

theorem ULower.down_computable {α : Type u_1} [Primcodable α] : (ULower.equiv α).Computable

theorem manyOneEquiv_up {α : Type u_1} [Primcodable α] {p : α → Prop} : ManyOneEquiv (p ∘ ULower.up) p

theorem OneOneReducible.disjoin_left {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : p ≤₁ Sum.elim p q

theorem OneOneReducible.disjoin_right {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} : q ≤₁ Sum.elim p q

theorem disjoin_manyOneReducible {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop} : p ≤₀ r → q ≤₀ r → Sum.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} : Sum.elim p q ≤₀ r ↔ p ≤₀ r ∧ q ≤₀ r

def toNat {α : Type u} [Primcodable α] [Inhabited α] (p : Set α) : Set ℕ

Computable and injective mapping of predicates to sets of natural numbers.

Equations

• toNat p = {n : ℕ | p ((Encodable.decode n).getD default)}

@[simp]

theorem toNat_manyOneReducible {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} : toNat p ≤₀ p

@[simp]

theorem manyOneReducible_toNat {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} : p ≤₀ toNat p

@[simp]

theorem manyOneReducible_toNat_toNat {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : Set α} {q : Set β} : toNat p ≤₀ toNat q ↔ p ≤₀ q

@[simp]

theorem toNat_manyOneEquiv {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} : ManyOneEquiv (toNat p) p

@[simp]

theorem manyOneEquiv_toNat {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] (p : Set α) (q : Set β) : ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

def ManyOneDegree : Type

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

Equations

• ManyOneDegree = Quotient { r := ManyOneEquiv, iseqv := ManyOneDegree.proof_1 }

def ManyOneDegree.of {α : Type u} [Primcodable α] [Inhabited α] (p : α → Prop) : ManyOneDegree

The many-one degree of a set on a primcodable type.

Equations

• ManyOneDegree.of p = Quotient.mk'' (toNat p)

theorem ManyOneDegree.ind_on {C : ManyOneDegree → Prop} (d : ManyOneDegree) (h : ∀ (p : Set ℕ), C (ManyOneDegree.of p)) : C d

@[reducible, inline]

abbrev ManyOneDegree.liftOn {φ : Sort u_1} (d : ManyOneDegree) (f : Set ℕ → φ) (h : ∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q) : φ

Lifts a function on sets of natural numbers to many-one degrees.

Equations

• d.liftOn f h = Quotient.liftOn' d f h

@[simp]

theorem ManyOneDegree.liftOn_eq {φ : Sort u_1} (p : Set ℕ) (f : Set ℕ → φ) (h : ∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q) : (ManyOneDegree.of p).liftOn f h = f p

@[reducible]

def ManyOneDegree.liftOn₂ {φ : Sort u_1} (d₁ d₂ : ManyOneDegree) (f : Set ℕ → Set ℕ → φ) (h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) : φ

Lifts a binary function on sets of natural numbers to many-one degrees.

Equations

• d₁.liftOn₂ d₂ f h = d₁.liftOn (fun (p : Set ℕ) => d₂.liftOn (f p) ⋯) ⋯

@[simp]

theorem ManyOneDegree.liftOn₂_eq {φ : Sort u_1} (p q : Set ℕ) (f : Set ℕ → Set ℕ → φ) (h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) : (ManyOneDegree.of p).liftOn₂ (ManyOneDegree.of q) f h = f p q

@[simp]

theorem ManyOneDegree.of_eq_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : α → Prop} {q : β → Prop} : ManyOneDegree.of p = ManyOneDegree.of q ↔ ManyOneEquiv p q

instance ManyOneDegree.instInhabited : Inhabited ManyOneDegree

Equations

• ManyOneDegree.instInhabited = { default := ManyOneDegree.of ∅ }

instance ManyOneDegree.instLE : LE ManyOneDegree

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

Equations

• ManyOneDegree.instLE = { le := fun (d₁ d₂ : ManyOneDegree) => d₁.liftOn₂ d₂ (fun (x1 x2 : Set ℕ) => x1 ≤₀ x2) ManyOneDegree.instLE.proof_1 }

@[simp]

theorem ManyOneDegree.of_le_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : α → Prop} {q : β → Prop} : ManyOneDegree.of p ≤ ManyOneDegree.of q ↔ p ≤₀ q

instance ManyOneDegree.instPartialOrder : PartialOrder ManyOneDegree

Equations

• ManyOneDegree.instPartialOrder = PartialOrder.mk ⋯

instance ManyOneDegree.instAdd : Add ManyOneDegree

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

Equations

• ManyOneDegree.instAdd = { add := fun (d₁ d₂ : ManyOneDegree) => d₁.liftOn₂ d₂ (fun (a b : Set ℕ) => ManyOneDegree.of (Sum.elim a b)) ManyOneDegree.instAdd.proof_1 }

@[simp]

theorem ManyOneDegree.add_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] (p : Set α) (q : Set β) : ManyOneDegree.of (Sum.elim p q) = ManyOneDegree.of p + ManyOneDegree.of q

@[simp]

theorem ManyOneDegree.add_le {d₁ d₂ d₃ : ManyOneDegree} : d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃

@[simp]

theorem ManyOneDegree.le_add_left (d₁ d₂ : ManyOneDegree) : d₁ ≤ d₁ + d₂

@[simp]

theorem ManyOneDegree.le_add_right (d₁ d₂ : ManyOneDegree) : d₂ ≤ d₁ + d₂

instance ManyOneDegree.instSemilatticeSup : SemilatticeSup ManyOneDegree

Equations

• ManyOneDegree.instSemilatticeSup = SemilatticeSup.mk (fun (x1 x2 : ManyOneDegree) => x1 + x2) ManyOneDegree.le_add_left ManyOneDegree.le_add_right ManyOneDegree.instSemilatticeSup.proof_1