Totality problem for programs

DefinitionTotal codes#✓fully proved

A code \(c\) of a partial recursive function is total when it halts on every input: writing \(\varphi_c\) for the partial function on \(\mathbb{N}\) that \(c\) computes, \(\varphi_c(n)\) is defined for every \(n \in \mathbb{N}\).

def TotalCode (c : Code) : Prop := ∀ n, (c.eval n).Dom

Used by 5

Used byHalting on zero reduces to totality · Non-halting on zero reduces to totality · Totality is not co-recognizable · Totality is undecidable · Totality is not recognizable

TheoremHalting on zero reduces to totality#✓fully proved

Writing \(\varphi_c\) for the partial function on \(\mathbb{N}\) computed by a code \(c\) of a partial recursive function, the set of codes \(c\) with \(\varphi_c(0)\) defined is many-one reducible to the set of total codes, the codes that halt on every input: there is a computable function \(f\) from codes to codes such that, for every code \(c\), \(\varphi_c(0)\) is defined if and only if \(f(c)\) is total.

theorem manyOneReducible_halting_total :
    ManyOneReducible (fun c : Code ↦ (c.eval 0).Dom) TotalCode

Uses 2 · Used by 1

Statement usesTotal codes

Proof usesHalting-on-zero code

Used byTotality is not co-recognizable

TheoremTotality is not co-recognizable#✓fully proved

The set of total codes, the codes of partial recursive functions that halt on every input, is not co-recognizable by multi-stack machines: no multi-stack machine halts on the binary encoding of a code \(c\) exactly when \(c\) is not total.

theorem not_tm2CoRecognizable_total : ¬TM2CoRecognizable TotalCode

Uses 5

Statement usesCo-recognizability by multi-stack machines · Total codes

Proof usesHalting on zero reduces to totality · The halting problem is not co-recognizable by multi-stack machines · Recognizability transfers along mapping reductions

DefinitionDiverging once a code halts on zero#✓fully proved

For a code \(c\) of a partial recursive function, this is the partial function \(\mathbb{N} \to \mathbb{N}\) that on input \(k\) is undefined if \(c\) halts on input \(0\) within \(k\) steps of bounded evaluation, and equals \(0\) otherwise.

def untilHaltsFun (c : Code) (k : ℕ) : Part ℕ :=
  bif (Code.evaln k c 0).isSome then Part.none else Part.some 0

Used by 3

Used byHalting reduces to finiteness · Domain of the until-halts function · Non-halting on zero reduces to totality

TheoremNon-halting on zero reduces to totality#✓fully proved

Writing \(\varphi_c\) for the partial function on \(\mathbb{N}\) computed by a code \(c\) of a partial recursive function, the set of codes \(c\) with \(\varphi_c(0)\) undefined is many-one reducible to the set of total codes, the codes that halt on every input: there is a computable function \(f\) from codes to codes such that, for every code \(c\), \(\varphi_c(0)\) is undefined if and only if \(f(c)\) is total.

theorem manyOneReducible_not_halting_total :
    ManyOneReducible (fun c : Code ↦ ¬(c.eval 0).Dom) TotalCode

Uses 3 · Used by 1

Statement usesTotal codes

Proof usesDiverging once a code halts on zero · Parametrized s-m-n theorem

Used byTotality is not recognizable

TheoremTotality is not recognizable#✓fully proved

The set of total codes, the codes of partial recursive functions that halt on every input, is not recognizable by multi-stack machines: no multi-stack machine halts on the binary encoding of a code \(c\) exactly when \(c\) is total.

theorem not_tm2Recognizable_total : ¬TM2Recognizable TotalCode

Uses 5 · Used by 1

Statement usesRecognizability by multi-stack machines · Total codes

Proof usesNon-halting on zero reduces to totality · The halting problem is not co-recognizable by multi-stack machines · Recognizability transfers along mapping reductions

Used byTotality is undecidable

TheoremTotality is undecidable#✓fully proved

The set of total codes, the codes of partial recursive functions that halt on every input, is not decidable by multi-stack machines: no multi-stack machine computes a total function \(f : \mathbb{N} \to \mathbb{N}\) that takes the value \(1\) at the number encoding a code \(c\) exactly when \(c\) is total.

theorem not_tm2Decidable_total : ¬TM2Decidable TotalCode

Uses 4

Statement usesDecidability by multi-stack machines · Total codes

Proof usesDecidable predicates are recognizable by multi-stack machines · Totality is not recognizable

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.