Turing reducibility

DefinitionCharacteristic function of a set of naturals#✓fully proved

The characteristic function of a set \(p\) of natural numbers is the partial function \(\mathbb{N} \rightharpoonup \mathbb{N}\) that is defined at every \(n\), with value \(1\) if \(n \in p\) and value \(0\) otherwise.

noncomputable def charFun (p : ℕ → Prop) : ℕ →. ℕ :=
  open Classical in fun n ↦ Part.some (if p n then 1 else 0)

Used by 15

Used byComputable predicates are closed under computable precomposition · Turing degree of a predicate · Turing equivalence of predicates · Turing reducibility of predicates · Turing reducibility is reflexive · Turing reducibility is transitive · A set is decidable iff its characteristic function is partial recursive · The halting set is not Turing reducible to a decidable set · Decidability transfers down Turing reducibility · Every set is Turing equivalent to its complement · Many-one reducibility implies Turing reducibility · Counter-machine decidable predicates · RAM-decidable predicate · A URM-decidable predicate is computable · URM-decidable predicate

TheoremA set is decidable iff its characteristic function is partial recursive#✓fully proved

A set \(p\) of natural numbers is decidable (computable as a predicate) if and only if its characteristic function is partial recursive.

theorem computablePred_iff_partrec_charFun {p : ℕ → Prop} :
    ComputablePred p ↔ Partrec (charFun p)

Uses 1 · Used by 3

Statement usesCharacteristic function of a set of naturals

Used byComputable predicates are closed under computable precomposition · Decidability transfers down Turing reducibility · A URM-decidable predicate is computable

TheoremDecidability transfers down Turing reducibility#✓fully proved

Let \(p\) and \(q\) be sets of natural numbers such that the characteristic function of \(p\) is Turing reducible to the characteristic function of \(q\). If \(q\) is decidable, then \(p\) is decidable.

theorem ComputablePred.of_turingReducible {p q : ℕ → Prop} (h : charFun p ≤ᵀ charFun q)
    (hq : ComputablePred q) : ComputablePred p

Uses 2 · Used by 1

Statement usesCharacteristic function of a set of naturals

Proof usesA set is decidable iff its characteristic function is partial recursive

Used byThe halting set is not Turing reducible to a decidable set

DefinitionHalting set#✓fully proved

Fix the standard bijective numbering \(n \mapsto c_n\) of the codes of partial recursive functions \(\mathbb{N} \rightharpoonup \mathbb{N}\). The halting set is the set of natural numbers \(n\) such that the partial recursive function with code \(c_n\) is defined at \(0\).

def haltingSet (n : ℕ) : Prop := ((ofNat Code n).eval 0).Dom

Used by 7

Used byEvery recognizable predicate many-one reduces to the halting set · Every recognizable predicate one-one reduces to the halting set · The halting set is recognizable · A predicate is recognizable iff it many-one reduces to the halting set · A predicate is recognizable iff it one-one reduces to the halting set · The complement of the halting set is not many-one reducible to it · The halting set is not Turing reducible to a decidable set

TheoremThe halting set is not Turing reducible to a decidable set#✓fully proved

For every decidable set \(q\) of natural numbers, the characteristic function of the halting set is not Turing reducible to the characteristic function of \(q\).

theorem not_turingReducible_halting {q : ℕ → Prop} (hq : ComputablePred q) :
    ¬charFun haltingSet ≤ᵀ charFun q

Uses 3

Statement usesCharacteristic function of a set of naturals · Halting set

Proof usesDecidability transfers down Turing reducibility

TheoremMany-one reducibility implies Turing reducibility#✓fully proved

If \(p\) and \(q\) are sets of natural numbers and \(p\) is many-one reducible to \(q\), that is, there is a computable \(f : \mathbb{N} \to \mathbb{N}\) with \(n \in p \iff f(n) \in q\) for all \(n\), then the characteristic function of \(p\) is Turing reducible to the characteristic function of \(q\).

theorem turingReducible_of_manyOneReducible {p q : ℕ → Prop} (h : p ≤₀ q) :
    charFun p ≤ᵀ charFun q

Uses 1

Statement usesCharacteristic function of a set of naturals

TheoremEvery set is Turing equivalent to its complement#✓fully proved

For every set \(p\) of natural numbers, the characteristic function of the complement \(\mathbb{N} \setminus p\) and the characteristic function of \(p\) are Turing equivalent: each is Turing reducible to the other.

theorem turingEquivalent_charFun_not (p : ℕ → Prop) : charFun (fun n ↦ ¬p n) ≡ᵀ charFun p

Uses 1

Statement usesCharacteristic function of a set of naturals

TheoremThe complement of the halting set is not many-one reducible to it#✓fully proved

There is no computable function \(f : \mathbb{N} \to \mathbb{N}\) such that, for every \(n\), \(n\) is outside the halting set if and only if \(f(n)\) is in the halting set.

The halting set is recognizable and its complement is not. Since every set is Turing equivalent to its complement, Turing reducibility is strictly coarser than many-one reducibility.

theorem not_manyOneReducible_not_halting : ¬(fun n ↦ ¬haltingSet n) ≤₀ haltingSet

Uses 5

Statement usesHalting set

Proof usesRecognizability by multi-stack machines · The halting problem is not co-recognizable by multi-stack machines · The halting problem is recognizable by multi-stack machines · Recognizability transfers along mapping reductions

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.