Undecidability of universality for recursive languages

Recursive languages are presented by raw partial-recursive program codes under the semantic promise RecursiveDeciderCode.Valid that the program halts on every encoded word. Universality is not uniformly decidable even under that promise.

The reduction compiles a source computation c.eval n into an always-halting word decider. On a word of length k, the compiled decider accepts exactly when bounded evaluation has not found the source computation within budget k. Over a nonempty alphabet there are words of every length, so the compiled language is universal exactly when c.eval n does not halt.

The nonempty-alphabet hypothesis is necessary: over the empty alphabet there is only the empty word, so universality of a promised decider is just one membership query.

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

No promise algorithm can decide universality of valid always-halting decider codes. This holds over every nonempty computably encoded alphabet; the algorithm is allowed to diverge on invalid raw codes.

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

Universality cannot be decided uniformly for recursive languages.

The result holds for the standard valid-decider presentation over every nonempty computably encoded alphabet.