Turing degrees and the Turing jump

InductiveOracle codes#✓fully proved

Oracle codes are the finite programs built from the basic codes \(\mathtt{zero}\), \(\mathtt{succ}\), \(\mathtt{left}\), \(\mathtt{right}\) and \(\mathtt{oracle}\) by the binary constructors \(\mathtt{pair}\), \(\mathtt{comp}\) and \(\mathtt{prec}\) and the unary constructor \(\mathtt{rfind}\). They are the codes for partial recursive functions (constant zero, successor, the two unpairing projections, pairing, composition, primitive recursion and unbounded search) extended by an instruction \(\mathtt{oracle}\) that queries the oracle on its input.

inductive OracleCode where
  | zero : OracleCode
  | succ : OracleCode
  | left : OracleCode
  | right : OracleCode
  | pair : OracleCode → OracleCode → OracleCode
  | comp : OracleCode → OracleCode → OracleCode
  | prec : OracleCode → OracleCode → OracleCode
  | rfind : OracleCode → OracleCode
  | oracle : OracleCode

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, §2 (oracle computations).

Used by 23

Used byThe effective enumeration of oracle codes is computable · Whether a code number decodes · The definedness predicate, by cases on the tag · Decoding oracle codes · The computable decoder inverts the encoder · Fuel-indexed decoder of oracle codes · The fuel-indexed decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder · Decoder soundness · The decoder, by cases on the tag · The Gödel numbering of oracle codes · The Gödel numbering of oracle codes is injective · Depth of an oracle code · Depth is bounded by the code number · Effective enumeration of oracle codes · The effective enumeration is a left inverse of the Gödel numbering · The enumeration of oracle codes is surjective · Evaluation of oracle codes · Fuel-indexed evaluation of oracle codes · Fuel bounds the inputs · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

DefinitionThe Gödel numbering of oracle codes#✓fully proved

Write \(\langle a, b \rangle\) for the pairing of natural numbers equal to \(b^2 + a\) if \(a < b\) and to \(a^2 + a + b\) otherwise. The code number \(\ulcorner c \urcorner\) of an oracle code \(c\) is defined by recursion on \(c\): \(\mathsf{zero}\), \(\mathsf{succ}\), \(\mathsf{left}\), \(\mathsf{right}\) and \(\mathsf{oracle}\) have code numbers \(\langle 0, 0 \rangle\), \(\langle 1, 0 \rangle\), \(\langle 2, 0 \rangle\), \(\langle 3, 0 \rangle\) and \(\langle 8, 0 \rangle\); \(\mathsf{pair}(a, b)\), \(\mathsf{comp}(a, b)\) and \(\mathsf{prec}(a, b)\) have code numbers \(\langle 4, \langle \ulcorner a \urcorner, \ulcorner b \urcorner \rangle \rangle\), \(\langle 5, \langle \ulcorner a \urcorner, \ulcorner b \urcorner \rangle \rangle\) and \(\langle 6, \langle \ulcorner a \urcorner, \ulcorner b \urcorner \rangle \rangle\); and \(\mathsf{rfind}(a)\) has code number \(\langle 7, \ulcorner a \urcorner \rangle\).

This numbering is an injection into \(\mathbb{N}\).

def encodeOracleCode : OracleCode → ℕ
  | .zero => Nat.pair 0 0
  | .succ => Nat.pair 1 0
  | .left => Nat.pair 2 0
  | .right => Nat.pair 3 0
  | .pair a b => Nat.pair 4 (Nat.pair (encodeOracleCode a) (encodeOracleCode b))
  | .comp a b => Nat.pair 5 (Nat.pair (encodeOracleCode a) (encodeOracleCode b))
  | .prec a b => Nat.pair 6 (Nat.pair (encodeOracleCode a) (encodeOracleCode b))
  | .rfind a => Nat.pair 7 (encodeOracleCode a)
  | .oracle => Nat.pair 8 0

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings).

Uses 1 · Used by 12

Statement usesOracle codes

Used byThe effective enumeration of oracle codes is computable · The computable decoder inverts the encoder · The fuel-indexed decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder · Decoder soundness · The Gödel numbering of oracle codes is injective · Depth is bounded by the code number · The effective enumeration is a left inverse of the Gödel numbering · The enumeration of oracle codes is surjective · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

TheoremThe Gödel numbering of oracle codes is injective#✓fully proved

The Gödel numbering of oracle codes is injective.

theorem encodeOracleCode_injective : Function.Injective encodeOracleCode

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings).

Uses 2

Statement usesOracle codes · The Gödel numbering of oracle codes

TheoremPairing is at least its first argument#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing of natural numbers, equal to \(b^2 + a\) if \(a < b\) and to \(a^2 + a + b\) otherwise. For all natural numbers \(a\) and \(b\), \(a \le \langle a, b \rangle\).

theorem pair_ge_fst (a b : ℕ) : a ≤ Nat.pair a b

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

Used by 2

Used byDepth is bounded by the code number · The first unpairing component is at most the number

TheoremPairing is at least its second argument#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing of natural numbers, equal to \(b^2 + a\) if \(a < b\) and to \(a^2 + a + b\) otherwise. For all natural numbers \(a\) and \(b\), \(b \le \langle a, b \rangle\).

theorem pair_ge_snd (a b : ℕ) : b ≤ Nat.pair a b

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

Used by 2

Used byDepth is bounded by the code number · The second unpairing component is at most the number

TheoremPairing with \(4\) strictly increases the second argument#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing of natural numbers, equal to \(b^2 + a\) if \(a < b\) and to \(a^2 + a + b\) otherwise. For every natural number \(x\), \(x < \langle 4, x \rangle\).

theorem pair_four_gt (x : ℕ) : x < Nat.pair 4 x

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

TheoremPairing with a positive first argument strictly increases the second#✓fully proved

Let \(\langle a, b \rangle\) denote the pairing of natural numbers, equal to \(b^2 + a\) if \(a < b\) and to \(a^2 + a + b\) otherwise. For all natural numbers \(t\) and \(x\) with \(t \ge 1\), \(x < \langle t, x \rangle\).

theorem pair_gt_snd_of_pos {t x : ℕ} (ht : 1 ≤ t) : x < Nat.pair t x

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

Used by 3

Used byThe definedness step function is correct · The decoder, by cases on the tag · Depth is bounded by the code number

TheoremThe first unpairing component is at most the number#✓fully proved

Let \(\mathrm{pair} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}\) be the pairing bijection with \(\mathrm{pair}(a, b) = b^2 + a\) if \(a < b\) and \(\mathrm{pair}(a, b) = a^2 + a + b\) otherwise. For every natural number \(n\), the first component of \(\mathrm{pair}^{-1}(n)\) is at most \(n\).

theorem unpair_fst_le (n : ℕ) : n.unpair.1 ≤ n

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

Uses 1 · Used by 2

Proof usesPairing is at least its first argument

Used byThe definedness step function is correct · The decoder, by cases on the tag

TheoremThe second unpairing component is at most the number#✓fully proved

Let \(\mathrm{pair} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}\) be the pairing bijection with \(\mathrm{pair}(a, b) = b^2 + a\) if \(a < b\) and \(\mathrm{pair}(a, b) = a^2 + a + b\) otherwise. For every natural number \(n\), the second component of \(\mathrm{pair}^{-1}(n)\) is at most \(n\).

theorem unpair_snd_le (n : ℕ) : n.unpair.2 ≤ n

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.3 (pairing functions).

Uses 1 · Used by 2

Proof usesPairing is at least its second argument

Used byThe definedness step function is correct · The decoder, by cases on the tag

DefinitionDepth of an oracle code#✓fully proved

Leaves have depth 0; each constructor adds one to the maximum depth of its children.

def oracleCodeDepth : OracleCode → ℕ
  | .zero => 0
  | .succ => 0
  | .left => 0
  | .right => 0
  | .oracle => 0
  | .pair a b => max (oracleCodeDepth a) (oracleCodeDepth b) + 1
  | .comp a b => max (oracleCodeDepth a) (oracleCodeDepth b) + 1
  | .prec a b => max (oracleCodeDepth a) (oracleCodeDepth b) + 1
  | .rfind a => oracleCodeDepth a + 1

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; size bounds).

Uses 1 · Used by 4

Statement usesOracle codes

Used byThe computable decoder inverts the encoder · The fuel-indexed decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder · Depth is bounded by the code number

DefinitionFuel-indexed decoder of oracle codes#✓fully proved

Write \(\langle a, b \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) of the Gödel numbering. Given a fuel \(f\), a tag \(t\) and a payload \(p\), the decoder either returns an oracle code or fails; to decode a number \(n = \langle n_1, n_2 \rangle\) with fuel \(f\) means to run it with fuel \(f\), tag \(n_1\) and payload \(n_2\). With fuel \(0\) it fails. With fuel \(f + 1\), writing \(p = \langle p_1, p_2 \rangle\): if \(p = 0\) and \(t\) is \(0\), \(1\), \(2\), \(3\) or \(8\), it returns the instruction zero, successor, left projection, right projection or oracle query respectively; if \(t\) is \(4\), \(5\) or \(6\), it decodes \(p_1\) and \(p_2\) with fuel \(f\) and, when these give codes \(a\) and \(b\), returns the pairing, composition or primitive recursion code built from \(a\) and \(b\) respectively, failing otherwise; if \(t = 7\), it decodes \(p\) with fuel \(f\) and, when this gives a code \(a\), returns the unbounded search code built from \(a\), failing otherwise; in all other cases it fails.

The recursion is structural in the fuel and uses no classical choice, so the decoder is a computable function; with enough fuel it inverts the Gödel numbering of oracle codes.

Cslib.Decidability.decodeOracleCodeFuel · 34 lines

def decodeOracleCodeFuel : ℕ → ℕ → ℕ → Option OracleCode
  | 0, _, _ => none
  | fuel + 1, tag, payload =>
    if tag = 0 ∧ payload = 0 then some .zero
    else if tag = 1 ∧ payload = 0 then some .succ
    else if tag = 2 ∧ payload = 0 then some .left
    else if tag = 3 ∧ payload = 0 then some .right
    else if tag = 4 then
      match decodeOracleCodeFuel fuel payload.unpair.1.unpair.1
          payload.unpair.1.unpair.2,
        decodeOracleCodeFuel fuel payload.unpair.2.unpair.1
          payload.unpair.2.unpair.2 with
      | some a, some b => some (.pair a b)
      | _, _ => none
    else if tag = 5 then
      match decodeOracleCodeFuel fuel payload.unpair.1.unpair.1
          payload.unpair.1.unpair.2,
        decodeOracleCodeFuel fuel payload.unpair.2.unpair.1
          payload.unpair.2.unpair.2 with
      | some a, some b => some (.comp a b)
      | _, _ => none
    else if tag = 6 then
      match decodeOracleCodeFuel fuel payload.unpair.1.unpair.1
          payload.unpair.1.unpair.2,
        decodeOracleCodeFuel fuel payload.unpair.2.unpair.1
          payload.unpair.2.unpair.2 with
      | some a, some b => some (.prec a b)
      | _, _ => none
    else if tag = 7 then
      match decodeOracleCodeFuel fuel payload.unpair.1 payload.unpair.2 with
      | some a => some (.rfind a)
      | none => none
    else if tag = 8 ∧ payload = 0 then some .oracle
    else none

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 1 · Used by 5

Statement usesOracle codes

Used byDecoding oracle codes · The fuel-indexed decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder · Decoder soundness · The decoder, by cases on the tag

TheoremThe fuel-indexed decoder inverts the encoder#✓fully proved

Write \(\langle a, b \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) of the Gödel numbering. Let \(c\) be an oracle code with Gödel number \(\langle t, p \rangle\). For every fuel \(f\) strictly greater than the depth of \(c\), the fuel-indexed decoder with fuel \(f\), tag \(t\) and payload \(p\) returns \(c\).

theorem decodeOracleCodeFuel_complete : ∀ (c : OracleCode) (fuel : ℕ),
    oracleCodeDepth c < fuel →
    decodeOracleCodeFuel fuel (encodeOracleCode c).unpair.1
      (encodeOracleCode c).unpair.2 = some c

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 4 · Used by 2

Statement usesOracle codes · Fuel-indexed decoder of oracle codes · The Gödel numbering of oracle codes · Depth of an oracle code

Used byThe computable decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder

TheoremDecoder soundness#✓fully proved

Write \(\langle a, b \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) of the Gödel numbering. For every fuel \(f\), tag \(t\), payload \(p\) and oracle code \(c\), if the fuel-indexed decoder with fuel \(f\), tag \(t\) and payload \(p\) returns \(c\), then the Gödel number of \(c\) is \(\langle t, p \rangle\).

Together with the fact that the fuel-indexed decoder inverts the encoder at any fuel above the code depth, this says that the decoder is exactly the inverse of the Gödel numbering on its image.

theorem decodeOracleCodeFuel_sound : ∀ (fuel : ℕ) (tag payload : ℕ)
    (c : OracleCode),
    decodeOracleCodeFuel fuel tag payload = some c →
    encodeOracleCode c = Nat.pair tag payload

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 3 · Used by 5

Statement usesOracle codes · Fuel-indexed decoder of oracle codes · The Gödel numbering of oracle codes

Used byThe effective enumeration of oracle codes is computable · The fuel-indexed decoder agrees with the total decoder · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

TheoremDepth is bounded by the code number#✓fully proved

For every oracle code \(c\), the depth of \(c\) is at most the code number of \(c\) under the Gödel numbering of oracle codes.

theorem oracleCodeDepth_le_encode : ∀ c : OracleCode,
    oracleCodeDepth c ≤ encodeOracleCode c

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; size bounds).

Uses 6 · Used by 2

Statement usesOracle codes · The Gödel numbering of oracle codes · Depth of an oracle code

Proof usesPairing is at least its first argument · Pairing is at least its second argument · Pairing with a positive first argument strictly increases the second

Used byThe computable decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder

DefinitionDecoding oracle codes#✓fully proved

The computable decoder for the Gödel numbering of oracle codes sends a natural number \(n\) to the result of the fuel-indexed decoder with fuel \(n + 1\), tag \(n_1\) and payload \(n_2\), where \((n_1, n_2)\) is the unpairing of \(n\); the result is either an oracle code or undefined. The fuel \(n + 1\) is more than enough, since the depth of an oracle code is at most its code number.

def decodeOracleCode (n : ℕ) : Option OracleCode :=
  decodeOracleCodeFuel (n + 1) n.unpair.1 n.unpair.2

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 2 · Used by 11

Statement usesOracle codes · Fuel-indexed decoder of oracle codes

Used byThe effective enumeration of oracle codes is computable · Whether a code number decodes · The definedness predicate, by cases on the tag · The computable decoder inverts the encoder · The fuel-indexed decoder agrees with the total decoder · The decoder, by cases on the tag · Effective enumeration of oracle codes · The effective enumeration is a left inverse of the Gödel numbering · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

TheoremThe computable decoder inverts the encoder#✓fully proved

For every oracle code \(c\), the computable decoder applied to the Gödel number of \(c\) returns \(c\).

theorem decodeOracleCode_encode (c : OracleCode) :
    decodeOracleCode (encodeOracleCode c) = some c

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 6 · Used by 5

Statement usesOracle codes · Decoding oracle codes · The Gödel numbering of oracle codes

Proof usesThe fuel-indexed decoder inverts the encoder · Depth of an oracle code · Depth is bounded by the code number

Used byThe effective enumeration of oracle codes is computable · The effective enumeration is a left inverse of the Gödel numbering · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

TheoremThe fuel-indexed decoder agrees with the total decoder#✓fully proved

The fuel-indexed decoder agrees with the total decoder whenever the code number is below the fuel: decoding (tag, payload) at any fuel above the code number gives the same result as decoding the code number itself.

theorem decodeOracleCodeFuel_eq_decode {fuel tag payload : ℕ}
    (h : Nat.pair tag payload < fuel) :
    decodeOracleCodeFuel fuel tag payload =
      decodeOracleCode (Nat.pair tag payload)

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 8 · Used by 1

Statement usesOracle codes · Decoding oracle codes · Fuel-indexed decoder of oracle codes

Proof usesThe fuel-indexed decoder inverts the encoder · Decoder soundness · The Gödel numbering of oracle codes · Depth of an oracle code · Depth is bounded by the code number

Used byThe decoder, by cases on the tag

TheoremThe decoder, by cases on the tag#✓fully proved

Write \(\langle t, p \rangle\) for the pairing of natural numbers used by the Gödel numbering of oracle codes, \((p_1, p_2)\) for the unpairing of \(p\) (so that \(\langle p_1, p_2 \rangle = p\)), and \(\mathrm{dec}(n)\) for the result of the computable decoder on \(n\), which is either an oracle code or undefined. Then for all natural numbers \(t\) and \(p\), the value \(\mathrm{dec}\langle t, p \rangle\) is: \(\mathsf{zero}\), \(\mathsf{succ}\), \(\mathsf{left}\), \(\mathsf{right}\) or \(\mathsf{oracle}\) when \(p = 0\) and \(t\) is \(0\), \(1\), \(2\), \(3\) or \(8\) respectively; \(\mathsf{pair}(a, b)\), \(\mathsf{comp}(a, b)\) or \(\mathsf{prec}(a, b)\) when \(t\) is \(4\), \(5\) or \(6\) respectively and \(\mathrm{dec}(p_1) = a\) and \(\mathrm{dec}(p_2) = b\) are both defined; \(\mathsf{rfind}(a)\) when \(t = 7\) and \(\mathrm{dec}(p) = a\) is defined; and undefined in every other case.

For \(t \in \{4, 5, 6, 7\}\) the numbers decoded on the right, \(p_1\), \(p_2\) and \(p\), are at most \(p\) and hence strictly below \(\langle t, p \rangle\), so this is a recursion on the code number.

theorem decodeOracleCode_pair (tag payload : ℕ) :
    decodeOracleCode (Nat.pair tag payload) =
      if tag = 0 ∧ payload = 0 then some .zero
      else if tag = 1 ∧ payload = 0 then some .succ
      else if tag = 2 ∧ payload = 0 then some .left
      else if tag = 3 ∧ payload = 0 then some .right
      else if tag = 4 then
        match decodeOracleCode payload.unpair.1, decodeOracleCode payload.unpair.2 with

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 7 · Used by 1

Statement usesOracle codes · Decoding oracle codes

Proof usesFuel-indexed decoder of oracle codes · The fuel-indexed decoder agrees with the total decoder · Pairing with a positive first argument strictly increases the second · The first unpairing component is at most the number · The second unpairing component is at most the number

Used byThe definedness predicate, by cases on the tag

DefinitionWhether a code number decodes#✓fully proved

For a natural number \(n\), this is the Boolean value that is true exactly when the computable decoder of oracle codes returns an oracle code on \(n\).

By decoder soundness and the inversion of the encoder, this holds exactly when \(n\) is the Gödel number of an oracle code.

def decodeIsSome (n : ℕ) : Bool :=
  (decodeOracleCode n).isSome

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 2 · Used by 7

Statement usesOracle codes · Decoding oracle codes

Used byThe effective enumeration of oracle codes is computable · The definedness predicate, by cases on the tag · The definedness step function is correct · The definedness predicate is primitive recursive · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

TheoremThe definedness predicate, by cases on the tag#✓fully proved

Write \(\langle a, b \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) of the Gödel numbering, and say that a natural number decodes when the computable decoder returns an oracle code on it. Let \(t\) and \(p\) be natural numbers and write \(p = \langle p_1, p_2 \rangle\). Then \(\langle t, p \rangle\) decodes if and only if one of the following holds: \(t\) is \(0\), \(1\), \(2\), \(3\) or \(8\) and \(p = 0\); \(t\) is \(4\), \(5\) or \(6\) and both \(p_1\) and \(p_2\) decode; or \(t = 7\) and \(p\) decodes.

In the recursive cases \(t \ge 1\), so \(p_1\), \(p_2\) and \(p\) are strictly smaller than \(\langle t, p \rangle\).

theorem decodeIsSome_pair (tag payload : ℕ) :
    decodeIsSome (Nat.pair tag payload) =
      if tag = 0 ∧ payload = 0 then true
      else if tag = 1 ∧ payload = 0 then true
      else if tag = 2 ∧ payload = 0 then true
      else if tag = 3 ∧ payload = 0 then true
      else if tag = 4 then decodeIsSome payload.unpair.1 && decodeIsSome payload.unpair.2
      else if tag = 5 then decodeIsSome payload.unpair.1 && decodeIsSome payload.unpair.2
      else if tag = 6 then decodeIsSome payload.unpair.1 && decodeIsSome payload.unpair.2
      else if tag = 7 then decodeIsSome payload
      else if tag = 8 ∧ payload = 0 then true
      else false

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 4 · Used by 1

Statement usesWhether a code number decodes

Proof usesOracle codes · Decoding oracle codes · The decoder, by cases on the tag

Used byThe definedness step function is correct

DefinitionOne step of the course-of-values recursion for definedness#✓fully proved

Write \(\langle a, b \rangle\) for the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\) of the Gödel numbering. The step takes an argument of the unit type, which it ignores, and a list \(L\) of natural numbers; for \(i \in \mathbb{N}\) write \(L_i\) for the entry of \(L\) at position \(i\) (counting from \(0\)), with \(L_i = 0\) when \(i\) is at least the length of \(L\). Let \(m\) be the length of \(L\), and write \(m = \langle t, p \rangle\) and \(p = \langle p_1, p_2 \rangle\). The step always returns a value, namely \(1\) if one of the following holds and \(0\) otherwise: \(t\) is \(0\), \(1\), \(2\), \(3\) or \(8\) and \(p = 0\); \(t\) is \(4\), \(5\) or \(6\) and \(L_{p_1} = L_{p_2} = 1\); or \(t = 7\) and \(L_p = 1\).

Applied to the list whose entry at position \(k < m\) is \(1\) if \(k\) decodes to an oracle code and \(0\) otherwise, it returns the corresponding value for \(m\), because in the recursive cases \(p_1\), \(p_2\) and \(p\) are smaller than \(m\).

Cslib.Decidability.decodeIsSomeStep · 18 lines

def decodeIsSomeStep : Unit → List ℕ → Option ℕ := fun _ L =>
  if (L.length).unpair.1 = 0 then some (if (L.length).unpair.2 = 0 then 1 else 0)
  else if (L.length).unpair.1 = 1 then some (if (L.length).unpair.2 = 0 then 1 else 0)
  else if (L.length).unpair.1 = 2 then some (if (L.length).unpair.2 = 0 then 1 else 0)
  else if (L.length).unpair.1 = 3 then some (if (L.length).unpair.2 = 0 then 1 else 0)
  else if (L.length).unpair.1 = 4 then
    some (if L[(L.length).unpair.2.unpair.1]?.getD 0 = 1 ∧
      L[(L.length).unpair.2.unpair.2]?.getD 0 = 1 then 1 else 0)
  else if (L.length).unpair.1 = 5 then
    some (if L[(L.length).unpair.2.unpair.1]?.getD 0 = 1 ∧
      L[(L.length).unpair.2.unpair.2]?.getD 0 = 1 then 1 else 0)
  else if (L.length).unpair.1 = 6 then
    some (if L[(L.length).unpair.2.unpair.1]?.getD 0 = 1 ∧
      L[(L.length).unpair.2.unpair.2]?.getD 0 = 1 then 1 else 0)
  else if (L.length).unpair.1 = 7 then
    some (if L[(L.length).unpair.2]?.getD 0 = 1 then 1 else 0)
  else if (L.length).unpair.1 = 8 then some (if (L.length).unpair.2 = 0 then 1 else 0)
  else some 0

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Used by 3

Used byThe definedness step function is correct · The definedness predicate is primitive recursive · The course-of-values step for definedness is primitive recursive

TheoremThe course-of-values step for definedness is primitive recursive#✓fully proved

One step of the course-of-values recursion for definedness is primitive recursive as a function of its two arguments, an element of the unit type and a list of natural numbers.

theorem primrec₂_decodeIsSomeStep : Primrec₂ decodeIsSomeStep

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 1 · Used by 1

Statement usesOne step of the course-of-values recursion for definedness

Used byThe definedness predicate is primitive recursive

TheoremThe definedness step function is correct#✓fully proved

For a natural number \(n\), let \(b_n\) be \(1\) if the computable decoder returns an oracle code on \(n\), and \(0\) otherwise. For every natural number \(m\), the one-step function of the course-of-values recursion for definedness, applied to the list \((b_0, b_1, \dots, b_{m-1})\), returns \(b_m\).

theorem decodeIsSomeStep_correct (m : ℕ) :
    decodeIsSomeStep ()
      (List.map (fun n => (decodeIsSome n).toNat) (List.range m)) =
      some ((decodeIsSome m).toNat)

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 6 · Used by 1

Statement usesWhether a code number decodes · One step of the course-of-values recursion for definedness

Proof usesThe definedness predicate, by cases on the tag · Pairing with a positive first argument strictly increases the second · The first unpairing component is at most the number · The second unpairing component is at most the number

Used byThe definedness predicate is primitive recursive

TheoremThe definedness predicate is primitive recursive#✓fully proved

The function \(\mathbb{N} \to \mathbb{N}\) sending \(n\) to \(1\) if \(n\) decodes to an oracle code under the computable decoder and to \(0\) otherwise is primitive recursive.

theorem natPrimrec_decodeIsSome :
    Nat.Primrec (fun n => (decodeIsSome n).toNat)

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 4 · Used by 4

Statement usesWhether a code number decodes

Proof usesOne step of the course-of-values recursion for definedness · The definedness step function is correct · The course-of-values step for definedness is primitive recursive

Used byThe effective enumeration of oracle codes is computable · The Gödel decoder of oracle codes is primitive recursive · The Gödel encoding of oracle codes is primitive recursive · The effective enumeration of oracle codes is primitive recursive

DefinitionEffective enumeration of oracle codes#✓fully proved

The \(n\)-th oracle code is the code that the computable decoder of the Gödel numbering of oracle codes assigns to \(n\), or the basic code \(\mathtt{zero}\) (the constant \(0\) program) when \(n\) is not the number of any code. Because the decoder inverts the Gödel numbering, this is an effective enumeration tied to that numbering, not an arbitrary countable encoding.

def oracleCodeOfNat : ℕ → OracleCode :=
  fun n ↦ (decodeOracleCode n).getD OracleCode.zero

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumerations).

Uses 2 · Used by 5

Statement usesOracle codes · Decoding oracle codes

Used byThe effective enumeration of oracle codes is computable · The Turing jump · The effective enumeration is a left inverse of the Gödel numbering · The enumeration of oracle codes is surjective · The effective enumeration of oracle codes is primitive recursive

TheoremThe effective enumeration is a left inverse of the Gödel numbering#✓fully proved

For every oracle code \(c\), the effective enumeration of oracle codes sends the code number of \(c\) to \(c\).

theorem oracleCodeOfNat_encode (c : OracleCode) :
    oracleCodeOfNat (encodeOracleCode c) = c

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumerations).

Uses 5 · Used by 1

Statement usesOracle codes · The Gödel numbering of oracle codes · Effective enumeration of oracle codes

Proof usesDecoding oracle codes · The computable decoder inverts the encoder

Used byThe enumeration of oracle codes is surjective

TheoremThe enumeration of oracle codes is surjective#✓fully proved

The enumeration of oracle codes is surjective.

theorem oracleCodeOfNat_surjective : Function.Surjective oracleCodeOfNat

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumerations).

Uses 4

Statement usesOracle codes · Effective enumeration of oracle codes

Proof usesThe Gödel numbering of oracle codes · The effective enumeration is a left inverse of the Gödel numbering

TheoremThe Gödel encoding of oracle codes is primitive recursive#✓fully proved

Regard oracle codes as coded by their Gödel numbers, with the computable decoder as decoding. Then the map sending each oracle code to its Gödel number is primitive recursive.

theorem primrec_encodeOracleCode : Primrec encodeOracleCode

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings).

Uses 7

Statement usesOracle codes · Whether a code number decodes · Decoding oracle codes · Decoder soundness · The computable decoder inverts the encoder · The Gödel numbering of oracle codes · The definedness predicate is primitive recursive

TheoremThe Gödel decoder of oracle codes is primitive recursive#✓fully proved

Regard oracle codes as coded by their Gödel numbers. Then the computable decoder, which sends a natural number \(n\) to the oracle code with Gödel number \(n\) when there is one and to no value otherwise, is primitive recursive as a map from natural numbers to optional oracle codes.

theorem primrec_decodeOracleCode : Primrec decodeOracleCode

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (Gödel numberings; decoding).

Uses 7 · Used by 1

Statement usesOracle codes · Whether a code number decodes · Decoding oracle codes · Decoder soundness · The computable decoder inverts the encoder · The Gödel numbering of oracle codes · The definedness predicate is primitive recursive

Used byThe effective enumeration of oracle codes is primitive recursive

TheoremThe effective enumeration of oracle codes is primitive recursive#✓fully proved

Regard oracle codes as coded by their Gödel numbers. Then the effective enumeration of oracle codes, which sends a natural number \(n\) to the oracle code with Gödel number \(n\) when there is one and to the zero code otherwise, is primitive recursive.

theorem primrec_oracleCodeOfNat : Primrec oracleCodeOfNat

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumerations).

Uses 9 · Used by 1

Statement usesOracle codes · Whether a code number decodes · Decoding oracle codes · Decoder soundness · The computable decoder inverts the encoder · The Gödel numbering of oracle codes · The definedness predicate is primitive recursive · Effective enumeration of oracle codes

Proof usesThe Gödel decoder of oracle codes is primitive recursive

Used byThe effective enumeration of oracle codes is computable

TheoremThe effective enumeration of oracle codes is computable#✓fully proved

The effective enumeration of oracle codes is computable.

theorem computable_oracleCodeOfNat : Computable oracleCodeOfNat

Sources

• Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (standard enumerations).

Uses 9

Statement usesOracle codes · Whether a code number decodes · Decoding oracle codes · Decoder soundness · The computable decoder inverts the encoder · The Gödel numbering of oracle codes · The definedness predicate is primitive recursive · Effective enumeration of oracle codes

Proof usesThe effective enumeration of oracle codes is primitive recursive

DefinitionFuel-indexed evaluation of oracle codes#✓fully proved

Write \(\langle a, b \rangle\) for the pairing of natural numbers. For an oracle \(o\) assigning to each natural number a natural number or no value, a fuel \(k\), an oracle code \(c\) and an input \(n\), the evaluator \(E_k(c, n)\) returns a natural number or fails. \(E_0(c, n)\) always fails. \(E_{k+1}(c, n)\) fails if \(n > k\); otherwise, with \(n = \langle a, m \rangle\):

• \(\mathtt{zero}\) returns \(0\), \(\mathtt{succ}\) returns \(n + 1\), \(\mathtt{left}\) returns \(a\) and \(\mathtt{right}\) returns \(m\);
• \(\mathtt{pair}(f, g)\) returns \(\langle E_{k+1}(f, n), E_{k+1}(g, n) \rangle\);
• \(\mathtt{comp}(f, g)\) returns \(E_{k+1}(f, x)\) where \(x = E_{k+1}(g, n)\);
• \(\mathtt{prec}(f, g)\) returns \(E_{k+1}(f, a)\) if \(m = 0\), and if \(m = y + 1\) it returns \(E_{k+1}(g, \langle a, \langle y, i \rangle \rangle)\) where \(i = E_k(\mathtt{prec}(f, g), \langle a, y \rangle)\);
• \(\mathtt{rfind}(f)\) computes \(x = E_{k+1}(f, \langle a, m \rangle)\) and returns \(m\) if \(x = 0\), and \(E_k(\mathtt{rfind}(f), \langle a, m + 1 \rangle)\) otherwise;
• \(\mathtt{oracle}\) returns \(o(n)\), failing if \(o\) has no value at \(n\).

In every case the result fails if any evaluation it uses fails.

Cslib.Decidability.oracleEvaln · 38 lines

def oracleEvaln : (ℕ → Option ℕ) → ℕ → OracleCode → ℕ → Option ℕ
  | _, 0, _ => fun _ => Option.none
  | _o, k + 1, .zero => fun n => do
      guard (n ≤ k)
      return 0
  | _o, k + 1, .succ => fun n => do
      guard (n ≤ k)
      return (Nat.succ n)
  | _o, k + 1, .left => fun n => do
      guard (n ≤ k)
      return n.unpair.1
  | _o, k + 1, .right => fun n => do
      guard (n ≤ k)
      pure n.unpair.2
  | o, k + 1, .pair cf cg => fun n => do
      guard (n ≤ k)
      Nat.pair <$> oracleEvaln o (k + 1) cf n <*> oracleEvaln o (k + 1) cg n
  | o, k + 1, .comp cf cg => fun n => do
      guard (n ≤ k)
      let x ← oracleEvaln o (k + 1) cg n
      oracleEvaln o (k + 1) cf x
  | o, k + 1, .prec cf cg => fun n => do
      guard (n ≤ k)
      n.unpaired fun a n =>
        n.casesOn (oracleEvaln o (k + 1) cf a) fun y => do
          let i ← oracleEvaln o k (.prec cf cg) (Nat.pair a y)
          oracleEvaln o (k + 1) cg (Nat.pair a (Nat.pair y i))
  | o, k + 1, .rfind cf => fun n => do
      guard (n ≤ k)
      n.unpaired fun a m => do
        let x ← oracleEvaln o (k + 1) cf (Nat.pair a m)
        if x = 0 then
          pure m
        else
          oracleEvaln o k (.rfind cf) (Nat.pair a (m + 1))
  | o, k + 1, .oracle => fun n => do
      guard (n ≤ k)
      o n

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, §2 (oracle computations).

Uses 1 · Used by 2

Statement usesOracle codes

Used byEvaluation of oracle codes · Fuel bounds the inputs

TheoremFuel bounds the inputs#✓fully proved

For every oracle \(o\), fuel \(k\), oracle code \(c\) and input \(n\), if the fuel-indexed evaluator with fuel \(k\) returns a value on \(c\) and \(n\) relative to \(o\), then \(n < k\).

theorem oracleEvaln_bound {o : ℕ → Option ℕ} {k c n x}
    (h : x ∈ oracleEvaln o k c n) : n < k

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, §2 (oracle computations).

Uses 2

Statement usesOracle codes · Fuel-indexed evaluation of oracle codes

DefinitionEvaluation of oracle codes#✓fully proved

Let \(o\) be an oracle that assigns to each natural number either a natural number or no value, \(c\) an oracle code and \(n\) a natural number. The value of \(c\) on \(n\) relative to \(o\) is the value returned by the fuel-indexed evaluator of \(c\) on \(n\) relative to \(o\) at the least fuel \(k\) for which that evaluator returns a value; it is undefined when there is no such \(k\).

def oracleEval (o : ℕ → Option ℕ) (c : OracleCode) (n : ℕ) : Part ℕ :=
  Nat.rfindOpt fun k ↦ oracleEvaln o k c n

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, §2 (oracle computations).

Uses 2 · Used by 1

Statement usesOracle codes · Fuel-indexed evaluation of oracle codes

Used byThe Turing jump

DefinitionThe Turing jump#✓fully proved

For a predicate \(P\) on \(\mathbb{N}\), the Turing jump \(P'\) is the predicate that holds at \(n\) exactly when the \(n\)-th oracle code in the effective enumeration of oracle codes, evaluated with the oracle that answers \(1\) at \(m\) if \(P(m)\) holds and \(0\) otherwise, halts on input \(n\). Thus \(P'\) is the diagonal halting set of the universal oracle machine with oracle \(P\).

def Jump (P : ℕ → Prop) : ℕ → Prop :=
  fun n ↦ (oracleEval (fun m ↦ @ite (Option ℕ) (P m) (Classical.propDecidable _) (some 1) (some 0))
    (oracleCodeOfNat n) n).Dom

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 2.1 (the jump).

Uses 2

Statement usesEffective enumeration of oracle codes · Evaluation of oracle codes

DefinitionTuring reducibility of predicates#✓fully proved

A predicate \(P\) on the natural numbers is Turing reducible to a predicate \(Q\) on the natural numbers when the characteristic function of \(P\) is Turing reducible to the characteristic function of \(Q\), that is, partial recursive relative to an oracle for the characteristic function of \(Q\).

def TuringReduciblePred (P Q : ℕ → Prop) : Prop :=
  charFun P ≤ᵀ charFun Q

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 2.2.

Uses 1 · Used by 2

Statement usesCharacteristic function of a set of naturals

Used byTuring reducibility is reflexive · Turing reducibility is transitive

DefinitionTuring equivalence of predicates#✓fully proved

Two predicates \(P\) and \(Q\) on the natural numbers are Turing equivalent when the characteristic function of \(P\) is Turing reducible to the characteristic function of \(Q\) and the characteristic function of \(Q\) is Turing reducible to the characteristic function of \(P\).

def TuringEquivalentPred (P Q : ℕ → Prop) : Prop :=
  charFun P ≡ᵀ charFun Q

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 2.2.

Uses 1

Statement usesCharacteristic function of a set of naturals

DefinitionTuring degree of a predicate#✓fully proved

The Turing degree of a predicate \(P\) on the natural numbers is the Turing degree of its characteristic function, that is, the class of the characteristic function of \(P\) under Turing equivalence of partial functions \(\mathbb{N} \rightharpoonup \mathbb{N}\).

noncomputable def turingDegreeOf (P : ℕ → Prop) : TuringDegree :=
  Quotient.mk _ (charFun P)

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 2.3.

Uses 1

Statement usesCharacteristic function of a set of naturals

TheoremTuring reducibility is reflexive#✓fully proved

Every predicate \(P\) on the natural numbers is Turing reducible to itself.

theorem turingReduciblePred_refl (P : ℕ → Prop) : TuringReduciblePred P P

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 2.4.

Uses 2

Statement usesTuring reducibility of predicates

Proof usesCharacteristic function of a set of naturals

TheoremTuring reducibility is transitive#✓fully proved

For predicates \(P\), \(Q\) and \(R\) on the natural numbers, if \(P\) is Turing reducible to \(Q\) and \(Q\) is Turing reducible to \(R\), then \(P\) is Turing reducible to \(R\).

theorem turingReduciblePred_trans {P Q R : ℕ → Prop}
    (hPQ : TuringReduciblePred P Q) (hQR : TuringReduciblePred Q R) :
    TuringReduciblePred P R

Sources

• Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 2.4.

Uses 2

Statement usesTuring reducibility of predicates

Proof usesCharacteristic function of a set of naturals

40 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.