Emptiness and equivalence problems for programs

DefinitionCodes with empty domain#✓fully proved

The set \(E\) consists of the codes \(c\) of partial recursive functions on \(\mathbb{N}\) that are defined on no input: for every \(n \in \mathbb{N}\), the function computed by \(c\) is undefined at \(n\).

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

Used by 6

Used byEmptiness reduces to equivalence · Emptiness is undecidable · Emptiness is not recognizable · Equivalence is not recognizable · Emptiness is co-recognizable · Nonemptiness is recognizable

TheoremEmptiness is undecidable#✓fully proved

The set \(E\) of codes of partial recursive functions on \(\mathbb{N}\) that are defined on no input is not decidable by multi-stack machines.

By Rice's theorem: the identity function is defined, the empty function is not.

theorem not_tm2Decidable_empty : ¬TM2Decidable EmptyCode

Uses 3 · Used by 1

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

Proof usesRice's theorem for multi-stack machines

Used byEmptiness is not recognizable

TheoremNonemptiness is recognizable#✓fully proved

The set of codes of partial recursive functions \(\mathbb{N} \to \mathbb{N}\) that are defined on at least one input is recognizable by multi-stack machines: some multi-stack machine halts on the binary encoding of a code \(c\) exactly when the function coded by \(c\) is defined on some input.

The machine searches for an input \(n\) and a step bound \(k\) such that the evaluation of \(c\) on \(n\) halts within \(k\) steps.

theorem tm2Recognizable_not_empty : TM2Recognizable fun c ↦ ¬EmptyCode c

Uses 3 · Used by 1

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

Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates

Used byEmptiness is co-recognizable

TheoremEmptiness is co-recognizable#✓fully proved

The set of codes of partial recursive functions \(\mathbb{N} \to \mathbb{N}\) that are defined on no input is co-recognizable by multi-stack machines: some multi-stack machine halts on the binary encoding of a code \(c\) exactly when the function coded by \(c\) is defined on at least one input.

theorem tm2CoRecognizable_empty : TM2CoRecognizable EmptyCode

Uses 3 · Used by 1

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

Proof usesNonemptiness is recognizable

Used byEmptiness is not recognizable

TheoremEmptiness is not recognizable#✓fully proved

The set \(E\) of codes of partial recursive functions on \(\mathbb{N}\) that are defined on no input is not recognizable by multi-stack machines: no multi-stack machine, started on the binary encoding of a code, halts exactly when the code is in \(E\).

Since \(E\) is co-recognizable, it would otherwise be decidable, by Post's theorem.

theorem not_tm2Recognizable_empty : ¬TM2Recognizable EmptyCode

Uses 7 · Used by 1

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

Proof usesCo-recognizability by multi-stack machines · Decidability by multi-stack machines · Emptiness is undecidable · Emptiness is co-recognizable · Post's theorem for multi-stack machines

Used byEquivalence is not recognizable

DefinitionEquivalent codes#✓fully proved

The set \(EQ\) consists of the pairs \((c_1, c_2)\) of codes of partial recursive functions on \(\mathbb{N}\) that recognize the same language, that is, whose computed functions have the same domain: for every \(n \in \mathbb{N}\), the function computed by \(c_1\) is defined at \(n\) if and only if the function computed by \(c_2\) is.

def EqCode (p : Code × Code) : Prop := p.1.eval.Dom = p.2.eval.Dom

Used by 4

Used byEmptiness reduces to equivalence · Halting on zero reduces to equivalence · Equivalence is not co-recognizable · Equivalence is not recognizable

TheoremA code defined nowhere#✓fully proved

There is a code \(e\) of a partial recursive function on \(\mathbb{N}\) whose computed function is the empty partial function, undefined at every input.

theorem exists_code_empty : ∃ e : Code, e.eval = fun _ ↦ Part.none

Used by 1

Used byEmptiness reduces to equivalence

TheoremEmptiness reduces to equivalence#✓fully proved

The set \(E\) of codes of partial recursive functions defined on no input is many-one reducible to the set \(EQ\) of pairs of codes with the same domain: there is a computable map \(f\) from codes to pairs of codes such that, for every code \(c\), \(c \in E\) if and only if \(f(c) \in EQ\).

One can take \(f(c) = (c, e)\) for a code \(e\) defined nowhere.

theorem manyOneReducible_empty_eq : ManyOneReducible EmptyCode EqCode

Uses 3 · Used by 1

Statement usesCodes with empty domain · Equivalent codes

Proof usesA code defined nowhere

Used byEquivalence is not recognizable

TheoremEquivalence is not recognizable#✓fully proved

The set \(EQ\) of pairs of codes of partial recursive functions on \(\mathbb{N}\) with the same domain is not recognizable by multi-stack machines: no multi-stack machine, started on the binary encoding of a pair of codes, halts exactly when the pair is in \(EQ\).

theorem not_tm2Recognizable_eq : ¬TM2Recognizable EqCode

Uses 6

Statement usesEquivalent codes · Recognizability by multi-stack machines

Proof usesCodes with empty domain · Emptiness reduces to equivalence · Emptiness is not recognizable · Recognizability transfers along mapping reductions

DefinitionHalting-on-zero code#✓fully proved

For a code \(c\) of a partial recursive function on \(\mathbb{N}\), the code \(h(c)\) is the composition \(k_0 \circ c \circ k_0\), where \(k_0\) is the code of the constant function \(0\): whatever its input, \(h(c)\) runs \(c\) on \(0\) and, if this halts, outputs \(0\).

def haltsOnZeroCode (c : Code) : Code :=
  Code.comp (Code.const 0) (Code.comp c (Code.const 0))

Used by 2

Used byHalting on zero reduces to equivalence · Halting on zero reduces to totality

TheoremHalting on zero reduces to equivalence#✓fully proved

The set of codes \(c\) of partial recursive functions on \(\mathbb{N}\) that halt on input \(0\) (are defined at \(0\)) is many-one reducible to the set \(EQ\) of pairs of codes with the same domain: there is a computable map \(f\) from codes to pairs of codes such that, for every code \(c\), \(c\) halts on \(0\) if and only if \(f(c) \in EQ\).

One can take \(f(c) = (h(c), k_0)\), where \(h(c)\) runs \(c\) on \(0\) and then outputs \(0\) whatever its input, and \(k_0\) is the code of the constant function \(0\).

theorem manyOneReducible_halting_eq :
    ManyOneReducible (fun c : Code ↦ (c.eval 0).Dom) EqCode

Uses 2 · Used by 1

Statement usesEquivalent codes

Proof usesHalting-on-zero code

Used byEquivalence is not co-recognizable

TheoremEquivalence is not co-recognizable#✓fully proved

The set \(EQ\) of pairs of codes of partial recursive functions on \(\mathbb{N}\) with the same domain is not co-recognizable by multi-stack machines: no multi-stack machine, started on the binary encoding of a pair of codes, halts exactly when the pair is not in \(EQ\).

The complement of halting on \(0\) would reduce to the complement of equivalence.

theorem not_tm2CoRecognizable_eq : ¬TM2CoRecognizable EqCode

Uses 5

Statement usesEquivalent codes · Co-recognizability by multi-stack machines

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

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.