The non-halting language is not recursively enumerable

This file proves nonHaltingUnaryLanguage_not_RE: the language of all non-halting Turing machines (nonHaltingUnaryLanguage, the complement of haltingUnaryLanguage) is not recursively enumerable.

The argument encodes each partial-recursive code c as the unary word codeUnaryWord c. If the non-halting language were RE, then grammar-membership search after this encoding would make fun c => ¬ (c.eval 0).Dom an REPred, contradicting Mathlib's ComputablePred.halting_problem_not_re.

@[reducible, inline]

abbrev PartrecCode : Type

Equations

• PartrecCode = Nat.Partrec.Code

def codeUnaryWord (c : PartrecCode) : List Unit

The unary word whose length is the code number of a partial-recursive code.

Equations

• codeUnaryWord c = List.map (fun (x : ℕ) => ()) (List.range (Encodable.encode c))

@[simp]

theorem codeUnaryWord_length (c : PartrecCode) : (codeUnaryWord c).length = Encodable.encode c

theorem codeUnaryWord_computable : Computable codeUnaryWord

theorem codeUnaryWord_mem_haltingUnaryLanguage (c : PartrecCode) : codeUnaryWord c ∈ haltingUnaryLanguage ↔ (Nat.Partrec.Code.eval c 0).Dom

theorem REPred_codeUnaryWord_preimage {L : Language Unit} (hL : is_RE L) : REPred fun (c : PartrecCode) => codeUnaryWord c ∈ L

Preimage of an RE unary language along codeUnaryWord is an REPred.

theorem haltingUnary_complement_not_RE : ¬is_RE haltingUnaryLanguageᶜ

The complement of the unary halting language is not RE.

theorem nonHaltingUnaryLanguage_not_RE : ¬is_RE nonHaltingUnaryLanguage

The unary non-halting language is not recursively enumerable.