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][soare1987]
Tags #
computability, reducibility, reduction
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)
Instances For
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))
Instances For
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)
Instances For
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))
Instances For
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)
Instances For
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)
Instances For
a computable bijection
Equations
- e.Computable = (Computable ⇑e ∧ Computable ⇑e.symm)
Instances For
A many-one degree is an equivalence class of sets up to many-one equivalence.
Equations
- ManyOneDegree = Quotient { r := ManyOneEquiv, iseqv := ManyOneDegree.proof_1 }
Instances For
The many-one degree of a set on a primcodable type.
Equations
- ManyOneDegree.of p = Quotient.mk'' (toNat p)
Instances For
Lifts a function on sets of natural numbers to many-one degrees.
Equations
- d.liftOn f h = Quotient.liftOn' d f h
Instances For
Lifts a binary function on sets of natural numbers to many-one degrees.
Instances For
Equations
- ManyOneDegree.instInhabited = { default := ManyOneDegree.of ∅ }
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 }
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 }