Undecidability of Emptiness for RE Languages

This file proves that emptiness cannot be decided for recursively enumerable (RE) languages. More precisely, the predicate "the partial function computed by code c has empty domain" is not computable.

The proof uses Rice's theorem (ComputablePred.rice): any computable semantic property of programs must be trivial (satisfied by all partial-recursive functions or by none). We exhibit two partial-recursive functions that separate the property — the everywhere-undefined function fun _ => Part.none (empty domain) and the constant zero function pure 0 (total) — to derive a contradiction.

Main results

• RE_emptiness_undecidable — the predicate "code c halts on no input" is not computably decidable.

theorem RE_emptiness_undecidable : ¬ComputablePred fun (c : Nat.Partrec.Code) => ∀ (n : ℕ), ¬(c.eval n).Dom

Emptiness is undecidable for RE languages.

There is no algorithm that, given a code c for a partial-recursive function, decides whether c halts on no input (i.e., whether the domain of c.eval is empty).

Proof. Apply Rice's theorem to the semantic property C = {f : ℕ →. ℕ | ∀ n, ¬(f n).Dom}. The everywhere-undefined function fun _ ↦ Part.none is partial-recursive (Nat.Partrec.none) and lies in C, while the constant zero function pure 0 is partial-recursive (Nat.Partrec.zero) and does not lie in C. Hence C is a non-trivial semantic property, so by Rice's theorem it is not computably decidable.

theorem recursivelyEnumerable_computableEmptiness_undecidable {RE : Set (Language Unit)} : ¬ComputableEmptiness RE partrecCodeDomainLanguageOf

Emptiness for RE codes is not uniformly computable.