The Jump Operator

This file defines the jump operator ⌜ for partial functions relative to an oracle and proves its basic properties, together with the associated notions of recursive enumerability relative to an oracle.

We identify partial recursive functions with recursively enumerable sets by taking their domain: if f : ℕ →. ℕ, then dom f : Set ℕ is {n | n ∈ f.Dom}. These are the terms in which the jump theorems are stated.

def Computability.recursivelyEnumerableIn (O : Set (ℕ →. ℕ)) (A : Set ℕ) : Prop

A set A is recursively enumerable in a set of oracle functions O if it is the domain of a function recursive in O.

Equations

• Computability.recursivelyEnumerableIn O A = ∃ (f : ℕ →. ℕ), Computability.RecursiveIn O f ∧ A = f.Dom

def Computability.recursivelyEnumerableIn₁ {α : Sort u_1} (X : α → ℕ →. ℕ) (A : Set ℕ) : Prop

A set A is recursively enumerable in a family X of oracle functions if it is the domain of a function recursive in the range of X.

Equations

• Computability.recursivelyEnumerableIn₁ X A = ∃ (f : ℕ →. ℕ), Computability.RecursiveIn (Set.range X) f ∧ A = f.Dom

def Computability.recursivelyEnumerableIn₂ (g : ℕ →. ℕ) (A : ℕ → Prop) : Prop

A set A is recursively enumerable in a single oracle g if it is the domain of a function recursive in {g}.

Equations

• Computability.recursivelyEnumerableIn₂ g A = ∃ (f : ℕ →. ℕ), Computability.RecursiveIn {g} f ∧ A = f.Dom

def Computability.recursivelyEnumerable (A : Set ℕ) : Prop

A set A is recursively enumerable if it is the domain of a partial recursive function.

Equations

• Computability.recursivelyEnumerable A = ∃ (f : ℕ →. ℕ), Computability.RecursiveIn ∅ f ∧ A = f.Dom

def Computability.jump (f : ℕ →. ℕ) : ℕ →. ℕ

The jump of f is the diagonal of the universal machine relative to f: f⌜ n = evalo (fun _ => f) (decodeCodeo n) n. Its domain is the halting problem relative to f.

Equations

• (f⌜) n = Computability.evalo (fun (x : Unit) => f) (Computability.decodeCodeo n) n

def Computability.setOracle (A : ℕ → Prop) [DecidablePred A] : ℕ →. ℕ

The oracle corresponding to a decidable set A, returning 0 on elements of A and undefined elsewhere.

Equations

• Computability.setOracle A n = if A n then Part.some 0 else Part.none

def Computability.jumpSet (A : ℕ → Prop) [DecidablePred A] : ℕ → Prop

The jump of a decidable set A: the set of n such that the n-th oracle program halts on input n with oracle A.

Equations

• Computability.jumpSet A n = (Computability.evalo (fun (x : Unit) => Computability.setOracle A) (Computability.decodeCodeo n) n).Dom

@[reducible, inline]

abbrev Computability.W {α : Type} [Primcodable α] (e : ℕ) (f : α → ℕ →. ℕ) : Set ℕ

W e f is the domain of the e-th partial function recursive in the oracle family f.

Equations

• Computability.W e f = (Computability.evalo f (Computability.decodeCodeo e)).Dom

def Computability.«term_⌜» : Lean.TrailingParserDescr

The jump of f is the diagonal of the universal machine relative to f: f⌜ n = evalo (fun _ => f) (decodeCodeo n) n. Its domain is the halting problem relative to f.

Equations

• Computability.«term_⌜» = Lean.ParserDescr.trailingNode `Computability.«term_⌜» 100 0 (Lean.ParserDescr.symbol "⌜")

theorem Computability.jump_recIn (f : ℕ →. ℕ) : TuringReducible f (f⌜)

def Computability.ComputablePredIn {α : Type u_1} (f : ℕ →. ℕ) [Primcodable α] (p : α → Prop) : Prop

A predicate p is computable relative to f if it is decidable and its decision procedure is computable in {f}.

Equations

• Computability.ComputablePredIn f p = ∃ (x : DecidablePred p), Computability.ComputableIn {f} fun (n : α) => decide (p n)

def Computability.REPredIn (f : ℕ →. ℕ) (p : ℕ → Prop) : Prop

A predicate p on ℕ is recursively enumerable relative to f if it is the domain predicate of a function recursive in {f}.

Equations

• Computability.REPredIn f p = ∃ (g : ℕ →. ℕ), Computability.RecursiveIn {f} g ∧ p = fun (n : ℕ) => (g n).Dom

theorem Computability.dom_re_in_jump (f : ℕ →. ℕ) : REPredIn (f⌜) fun (n : ℕ) => (f n).Dom

theorem Computability.ComputablePredIn.decide {α : Type u_1} [Primcodable α] {p : α → Prop} {f : ℕ →. ℕ} [DecidablePred p] (hp : ComputablePredIn f p) : ComputableIn {f} fun (a : α) => decide (p a)

theorem Computability.ComputableIn.computablePred {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : Computable fun (a : α) => decide (p a)) : ComputablePred p

theorem Computability.computablePredIn_iff_computableIn_decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ Computable fun (a : α) => decide (p a)

def Computability.PrimrecPredIn {α : Type u_1} [Primcodable α] {f : ℕ → ℕ} (p : α → Prop) : Prop

PrimrecPredIn p means p : α → Prop is a predicate whose decision procedure is primitive recursive relative to the oracle f.

Equations

• Computability.PrimrecPredIn p = ∃ (x : DecidablePred p), Computability.PrimrecIn' {f} fun (a : α) => decide (p a)

def Computability.Kf (f : ℕ →. ℕ) (n : ℕ) : Prop

The jump set Kf f relative to f: the set of n on which jump f is defined.

Equations

• Computability.Kf f n = ((f⌜) n).Dom

theorem Computability.re_in_trans (A : Set ℕ) (f h : ℕ →. ℕ) : recursivelyEnumerableIn₂ f A → TuringReducible f h → recursivelyEnumerableIn₂ h A