Set oracles and the Turing join

Mathlib's TuringReducible compares partial functions ℕ →. ℕ. A set of naturals is used as an oracle through its characteristic function: A.oracle is the total partial function with values A.indicator 1, answering 1 on A and 0 off it. Turing reducibility of sets is Turing reducibility of these oracles.

The Turing join f.turingJoin g of two partial functions answers f on even inputs and g on odd inputs, and records the side in the parity of its output. It is the least upper bound of f and g for Turing reducibility, which makes Mathlib's TuringDegree a join-semilattice. For sets, the parity join A.turingJoin B = {2 * x | x ∈ A} ∪ {2 * x + 1 | x ∈ B} has an oracle Turing equivalent to the Turing join of the two oracles, so it is the least upper bound of A and B among sets, and its degree is the supremum of their degrees.

Main definitions

• Set.oracle: the characteristic function of a set of naturals, as an oracle.
• PFun.turingJoin: the Turing join of two partial functions ℕ →. ℕ.
• Set.turingJoin: the parity join of two sets of naturals.
• The SemilatticeSup instance on TuringDegree, whose supremum is induced by the Turing join.

Main results

• ManyOneReducible.turingReducible_oracle: a many-one reduction of sets gives a Turing reduction of their oracles.
• TuringReducible.turingJoin_left, TuringReducible.turingJoin_right, PFun.turingJoin_turingReducible_iff: the Turing join is the least upper bound for Turing reducibility.
• Set.oracle_turingJoin_turingEquivalent: the oracle of the parity join of two sets is Turing equivalent to the Turing join of their oracles.
• Set.oracle_turingJoin_turingReducible_iff: the parity join is the least upper bound of two sets for Turing reducibility.
• TuringDegree.toAntisymmetrization_oracle_turingJoin: the degree of the parity join of two sets is the supremum of their degrees.
• Set.partrec_oracle_iff: partial computability of a set oracle is equivalent to computability of membership.
• Set.turingReducible_empty_iff: reducibility to the empty oracle characterizes computable sets.
• Set.union_turingReducible: if two sets reduce to an oracle, so does their union.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapters III.1 and III.2.
• The Turing join of partial functions, coding both its input and its output by parity, its least-upper-bound lemmas and the SemilatticeSup instance on TuringDegree follow Tanner Duve's Mathlib pull request 37062.

@[simp]

theorem TauCeti.turingDegree_le_iff {f g : ℕ →. ℕ} : toAntisymmetrization TuringReducible f ≤ toAntisymmetrization TuringReducible g ↔ TuringReducible f g

The order on degrees represented by partial functions is Turing reducibility.

noncomputable def Set.oracle (A : Set ℕ) : ℕ →. ℕ

The oracle of a set of naturals: its characteristic function A.indicator 1, as a total partial function.

@[simp]

theorem Set.oracle_apply (A : Set ℕ) (n : ℕ) : A.oracle n = Part.some (A.indicator 1 n)

The oracle of A answers A.indicator 1 n at n.

theorem Set.computableIn_indicator (A : Set ℕ) : ComputableIn {A.oracle} (A.indicator 1)

A set's characteristic function is computable in its own oracle.

theorem Set.turingReducible_iff_computableIn_indicator (A : Set ℕ) (O : ℕ →. ℕ) : TuringReducible A.oracle O ↔ ComputableIn {O} (A.indicator 1)

Reducing a set oracle is equivalent to computing its characteristic function.

@[simp]

theorem Set.oracle_empty : ∅.oracle = fun (x : ℕ) => Part.some 0

The empty set answers zero on every input.

@[simp]

theorem Set.partrec_oracle_iff (A : Set ℕ) : Partrec A.oracle ↔ ComputablePred fun (x : ℕ) => x ∈ A

A set oracle is partial computable exactly when membership in the set is computable.

theorem Set.empty_turingReducible (g : ℕ →. ℕ) : TuringReducible ∅.oracle g

The empty set oracle is Turing reducible to every partial function.

theorem Set.turingReducible_empty_iff (A : Set ℕ) : TuringReducible A.oracle ∅.oracle ↔ ComputablePred fun (x : ℕ) => x ∈ A

A set is Turing reducible to the empty oracle exactly when its membership is computable.

theorem Set.union_turingReducible {A B : Set ℕ} {g : ℕ →. ℕ} (hA : TuringReducible A.oracle g) (hB : TuringReducible B.oracle g) : TuringReducible (A ∪ B).oracle g

If A and B are Turing reducible to an oracle g, so is A ∪ B: take the maximum of the two answers.

theorem ManyOneReducible.turingReducible_oracle {A B : Set ℕ} (h : (fun (x : ℕ) => x ∈ A) ≤₀ fun (x : ℕ) => x ∈ B) : TuringReducible A.oracle B.oracle

A many-one reduction of sets of naturals gives a Turing reduction of their oracles: query the oracle of B at the image of the input.

The Turing join of partial functions

def PFun.turingJoin (f g : ℕ →. ℕ) : ℕ →. ℕ

The Turing join of two partial functions ℕ →. ℕ. It sends 2 * n to 2 * y for each value y of f n, and 2 * n + 1 to 2 * y + 1 for each value y of g n: the parity of the input selects the side, and the parity of the output records it.

@[simp]

theorem PFun.turingJoin_two_mul (f g : ℕ →. ℕ) (n : ℕ) : f.turingJoin g (2 * n) = Part.map (fun (x : ℕ) => 2 * x) (f n)

The Turing join answers f on even inputs, doubling its values.

@[simp]

theorem PFun.turingJoin_two_mul_add_one (f g : ℕ →. ℕ) (n : ℕ) : f.turingJoin g (2 * n + 1) = Part.map (fun (x : ℕ) => 2 * x + 1) (g n)

The Turing join answers g on odd inputs, sending each value y to 2 * y + 1.

theorem TuringReducible.turingJoin_left (f g : ℕ →. ℕ) : TuringReducible f (f.turingJoin g)

A partial function is Turing reducible to its Turing join with any other: query the join at 2 * n and halve the answer.

theorem TuringReducible.turingJoin_right (f g : ℕ →. ℕ) : TuringReducible g (f.turingJoin g)

A partial function is Turing reducible to the Turing join of any other with it: query the join at 2 * n + 1 and halve the answer.

theorem PFun.turingJoin_turingReducible {f g h : ℕ →. ℕ} (hf : TuringReducible f h) (hg : TuringReducible g h) : TuringReducible (f.turingJoin g) h

The Turing join of two partial functions reducible to h is reducible to h: on input n, run the reduction of f or of g at n.div2 according to the parity of n.

theorem PFun.turingJoin_turingReducible_iff {f g h : ℕ →. ℕ} : TuringReducible (f.turingJoin g) h ↔ TuringReducible f h ∧ TuringReducible g h

The Turing join is the least upper bound for Turing reducibility: it is reducible to h exactly when both of its sides are.

theorem TuringReducible.turingJoin {f f' g g' : ℕ →. ℕ} (hf : TuringReducible f f') (hg : TuringReducible g g') : TuringReducible (f.turingJoin g) (f'.turingJoin g')

The Turing join is monotone for Turing reducibility in both arguments.

theorem TuringEquivalent.turingJoin {f f' g g' : ℕ →. ℕ} (hf : TuringEquivalent f f') (hg : TuringEquivalent g g') : TuringEquivalent (f.turingJoin g) (f'.turingJoin g')

The Turing join respects Turing equivalence in both arguments.

Turing degrees form a join-semilattice

@[instance_reducible]

instance TuringDegree.instSemilatticeSup : SemilatticeSup TuringDegree

Turing degrees form a join-semilattice: the supremum of the degrees of f and g is the degree of their Turing join.

@[simp]

theorem TuringDegree.toAntisymmetrization_sup_toAntisymmetrization (f g : ℕ →. ℕ) : toAntisymmetrization TuringReducible f ⊔ toAntisymmetrization TuringReducible g = toAntisymmetrization TuringReducible (f.turingJoin g)

The supremum of the degrees of f and g is the degree of their Turing join.

The parity join of sets

def Set.turingJoin (A B : Set ℕ) : Set ℕ

The parity join {2 * x | x ∈ A} ∪ {2 * x + 1 | x ∈ B} of two sets of naturals.

@[simp]

theorem Set.two_mul_mem_turingJoin {A B : Set ℕ} {n : ℕ} : 2 * n ∈ A.turingJoin B ↔ n ∈ A

An even number 2 * n lies in the parity join of A and B exactly when n ∈ A.

@[simp]

theorem Set.two_mul_add_one_mem_turingJoin {A B : Set ℕ} {n : ℕ} : 2 * n + 1 ∈ A.turingJoin B ↔ n ∈ B

An odd number 2 * n + 1 lies in the parity join of A and B exactly when n ∈ B.

theorem Set.mem_turingJoin {A B : Set ℕ} {n : ℕ} : n ∈ A.turingJoin B ↔ n.div2 ∈ bif n.bodd then B else A

A number n lies in the parity join of A and B exactly when n.div2 lies in B if n is odd, and in A if n is even.

theorem Set.oracle_turingJoin_turingEquivalent (A B : Set ℕ) : TuringEquivalent (A.turingJoin B).oracle (A.oracle.turingJoin B.oracle)

The oracle of the parity join of two sets is Turing equivalent to the Turing join of their oracles.

theorem Set.oracle_turingReducible_turingJoin_left (A B : Set ℕ) : TuringReducible A.oracle (A.turingJoin B).oracle

The oracle of A is Turing reducible to the oracle of the parity join of A and B.

theorem Set.oracle_turingReducible_turingJoin_right (A B : Set ℕ) : TuringReducible B.oracle (A.turingJoin B).oracle

The oracle of B is Turing reducible to the oracle of the parity join of A and B.

theorem Set.oracle_turingJoin_turingReducible_iff {A B : Set ℕ} {h : ℕ →. ℕ} : TuringReducible (A.turingJoin B).oracle h ↔ TuringReducible A.oracle h ∧ TuringReducible B.oracle h

The parity join is the least upper bound of two sets for Turing reducibility: its oracle is reducible to h exactly when the oracles of both sets are.

theorem TuringDegree.toAntisymmetrization_oracle_turingJoin (A B : Set ℕ) : toAntisymmetrization TuringReducible (A.turingJoin B).oracle = toAntisymmetrization TuringReducible A.oracle ⊔ toAntisymmetrization TuringReducible B.oracle

The degree of the parity join of two sets is the supremum of their degrees.