The halting language is recursively enumerable

This file proves haltingUnaryLanguage_RE: the language of all halting Turing machines (haltingUnaryLanguage) is recursively enumerable.

Bounded evaluation Nat.Partrec.Code.evaln gives a computable test haltingUnaryTest that, searched over the step budget k, accepts exactly the words whose length decodes to a halting code. A computable search is partial-recursive, hence realizable by a Turing machine, hence RE.

def haltingUnaryTest (k : ℕ) (w : List Unit) : Bool

Bounded halting test for the unary language.

Equations

• haltingUnaryTest k w = (Nat.Partrec.Code.evaln k (Nat.Partrec.Code.ofNatCode w.length) 0).isSome

theorem haltingUnaryTest_computable₂ : Computable₂ haltingUnaryTest

theorem haltingUnaryLanguage_search (w : List Unit) : w ∈ haltingUnaryLanguage ↔ ∃ (k : ℕ), haltingUnaryTest k w = true

theorem haltingUnaryLanguage_RE : is_RE haltingUnaryLanguage

The unary halting language is recursively enumerable.