Finiteness problem for programs

DefinitionCodes with finite domain#✓fully proved

A code \(c\) of a partial recursive function \(\varphi_c\) on \(\mathbb{N}\) is finite when the domain of \(\varphi_c\), the set of inputs on which \(c\) halts, is finite. The set of finite codes is denoted \(\mathrm{FIN}\).

def FiniteCode (c : Code) : Prop := c.eval.Dom.Finite

Used by 5

Used byHalting reduces to finiteness · Non-halting reduces to finiteness · Finiteness is not co-recognizable · Finiteness is undecidable · Finiteness is not recognizable

TheoremDomain of the until-halts function#✓fully proved

For a code \(c\) of a partial recursive function, let \(u_c\) be the partial function on \(\mathbb{N}\) that on input \(j\) is undefined if \(c\) halts on input \(0\) within \(j\) steps (the step-bounded evaluation of \(c\) on input \(0\) with bound \(j\) returns a value) and outputs \(0\) otherwise. Then for every \(k \in \mathbb{N}\), \(u_c\) is defined at \(k\) if and only if \(c\) does not halt on input \(0\) within \(k\) steps.

theorem untilHaltsFun_dom {c : Code} {k : ℕ} :
    (untilHaltsFun c k).Dom ↔ (Code.evaln k c 0).isSome = false

Uses 1 · Used by 1

Statement usesDiverging once a code halts on zero

Used byHalting reduces to finiteness

TheoremHalting reduces to finiteness#✓fully proved

The set of codes of partial recursive functions that halt on input \(0\) is many-one reducible to the set of finite codes: there is a computable function \(f\) from codes to codes such that, for every code \(c\), \(c\) halts on input \(0\) if and only if the partial function of \(f(c)\) has finite domain.

theorem manyOneReducible_halting_finite :
    ManyOneReducible (fun c : Code ↦ (c.eval 0).Dom) FiniteCode

Uses 4 · Used by 1

Statement usesCodes with finite domain

Proof usesDiverging once a code halts on zero · Domain of the until-halts function · Parametrized s-m-n theorem

Used byFiniteness is not co-recognizable

TheoremFiniteness is not co-recognizable#✓fully proved

The set of codes of partial recursive functions with finite domain is not co-recognizable by multi-stack Turing machines: no finite multi-stack machine whose input alphabet is identified with \(\{0, 1\}\) halts on the binary encoding of the number of a code \(c\) exactly when the partial function of \(c\) has infinite domain.

theorem not_tm2CoRecognizable_finite : ¬TM2CoRecognizable FiniteCode

Uses 5

Statement usesCodes with finite domain · Co-recognizability by multi-stack machines

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

DefinitionHalts-within function#✓fully proved

For a code \(c\) of a partial recursive function, \(h_c\) is the partial function on \(\mathbb{N}\) that on input \(k\) outputs \(0\) if \(c\) halts on input \(0\) within \(k\) steps (the step-bounded evaluation of \(c\) on input \(0\) with bound \(k\) returns a value) and is undefined otherwise.

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

Used by 2

Used byDomain of the halts-within function · Non-halting reduces to finiteness

TheoremDomain of the halts-within function#✓fully proved

For a code \(c\) of a partial recursive function, let \(h_c\) be the partial function on \(\mathbb{N}\) that on input \(j\) outputs \(0\) if \(c\) halts on input \(0\) within \(j\) steps (the step-bounded evaluation of \(c\) on input \(0\) with bound \(j\) returns a value) and is undefined otherwise. Then for every \(k \in \mathbb{N}\), \(h_c\) is defined at \(k\) if and only if \(c\) halts on input \(0\) within \(k\) steps.

theorem haltsWithinFun_dom {c : Code} {k : ℕ} :
    (haltsWithinFun c k).Dom ↔ (Code.evaln k c 0).isSome = true

Uses 1 · Used by 1

Statement usesHalts-within function

Used byNon-halting reduces to finiteness

TheoremNon-halting reduces to finiteness#✓fully proved

The set of codes of partial recursive functions that do not halt on input \(0\) is many-one reducible to the set of finite codes: there is a computable function \(f\) from codes to codes such that, for every code \(c\), \(c\) does not halt on input \(0\) if and only if the partial function of \(f(c)\) has finite domain.

theorem manyOneReducible_not_halting_finite :
    ManyOneReducible (fun c : Code ↦ ¬(c.eval 0).Dom) FiniteCode

Uses 4 · Used by 1

Statement usesCodes with finite domain

Proof usesHalts-within function · Domain of the halts-within function · Parametrized s-m-n theorem

Used byFiniteness is not recognizable

TheoremFiniteness is not recognizable#✓fully proved

The set of codes of partial recursive functions with finite domain is not recognizable by multi-stack Turing machines: no finite multi-stack machine whose input alphabet is identified with \(\{0, 1\}\) halts on the binary encoding of the number of a code \(c\) exactly when the partial function of \(c\) has finite domain.

theorem not_tm2Recognizable_finite : ¬TM2Recognizable FiniteCode

Uses 5 · Used by 1

Statement usesCodes with finite domain · Recognizability by multi-stack machines

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

Used byFiniteness is undecidable

TheoremFiniteness is undecidable#✓fully proved

The set of codes of partial recursive functions with finite domain is not decidable by multi-stack Turing machines: there is no total function \(f : \mathbb{N} \to \mathbb{N}\) computed by a finite multi-stack machine on binary encodings such that, for every code \(c\) with number \(n_c\), \(f(n_c) = 1\) if and only if the partial function of \(c\) has finite domain.

theorem not_tm2Decidable_finite : ¬TM2Decidable FiniteCode

Uses 4

Statement usesCodes with finite domain · Decidability by multi-stack machines

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

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.