Undecidability of emptiness for promised recursive deciders

Recursive-language membership is uniformly decidable when a raw program code is promised to halt on every word. Emptiness is not. The reduction below maps an arbitrary source program c to an always-halting decider which, on a word of length k, accepts exactly when c halts on input 0 within bounded-evaluation budget k.

Every generated target code satisfies RecursiveDeciderCode.Valid, independently of whether the source computation halts. Over a nonempty alphabet there are words of every length, so its language is empty exactly when the source does not halt. This would turn a promise algorithm for emptiness into a decider for the halting problem.

The nonempty-alphabet assumption is necessary: over an empty alphabet the only word is [], and emptiness of a valid decider is a single membership query.

def RecursiveDeciderCode.boundedHaltingTest {T : Type} (c : Nat.Partrec.Code) (w : List T) : Bool

The total bounded-halting test used in the emptiness reduction. The word length supplies the finite evaluation budget.

Equations

• RecursiveDeciderCode.boundedHaltingTest c w = (Nat.Partrec.Code.evaln w.length c 0).isSome

theorem RecursiveDeciderCode.boundedHaltingTest_computable₂ {T : Type} [Primcodable T] : Computable₂ boundedHaltingTest

The bounded-halting test is computable jointly in the source code and word.

noncomputable def RecursiveDeciderCode.boundedHaltingCode {T : Type} [Primcodable T] : Nat.Partrec.Code → Nat.Partrec.Code

Effectively compile the bounded-halting test into a raw recursive-language decider code.

Equations

• RecursiveDeciderCode.boundedHaltingCode = RecursiveDeciderCode.compileBool RecursiveDeciderCode.boundedHaltingTest ⋯

theorem RecursiveDeciderCode.boundedHaltingCode_computable {T : Type} [Primcodable T] : Computable boundedHaltingCode

The reduction from source codes to bounded-halting deciders is computable.

theorem RecursiveDeciderCode.boundedHaltingCode_valid {T : Type} [Primcodable T] (c : Nat.Partrec.Code) : Valid (boundedHaltingCode c)

Every code produced by the reduction is valid, whether or not the source program halts.

theorem RecursiveDeciderCode.mem_boundedHaltingCode_iff {T : Type} [Primcodable T] (c : Nat.Partrec.Code) (w : List T) : w ∈ language (boundedHaltingCode c) ↔ (Nat.Partrec.Code.evaln w.length c 0).isSome = true

Membership in the reduced language is precisely bounded halting.

theorem RecursiveDeciderCode.boundedHaltingCode_empty_iff {T : Type} [Primcodable T] [Nonempty T] (c : Nat.Partrec.Code) : language (boundedHaltingCode c) = ∅ ↔ ¬(c.eval 0).Dom

Over a nonempty alphabet, the reduced valid language is empty exactly when the source program does not halt on input zero.

theorem RecursiveDeciderCode.exists_valid_empty {T : Type} [Primcodable T] : ∃ (c : Nat.Partrec.Code), Valid c ∧ language c = ∅

A valid raw code denoting the empty language exists over every computably encoded alphabet.

theorem RecursiveDeciderCode.emptiness_undecidable {T : Type} [Primcodable T] [Nonempty T] : ¬ComputablePredOnPromise Valid fun (c : Nat.Partrec.Code) => language c = ∅

Emptiness is not computable even under the semantic promise that the raw program code is an always-halting word decider.

theorem RecursiveDeciderCode.recursive_computableEmptiness_undecidable {T : Type} [Primcodable T] [Nonempty T] : ¬ComputableEmptiness Recursive language Valid

There is no computable emptiness test for the promised raw-code presentation of the class of recursive languages.