No effective total numbering of all recursive languages

Every individual recursive language has decidable membership, but there is no adequate computable numbering of all recursive languages whose membership relation is uniformly decidable. This distinction matters for ComputableMembership with its default trivial validity promise, which asks for a uniform algorithm taking a language code as an input and terminating on every element of a Primcodable code type.

This does not contradict the usual uniform word problem for an encoded decider. There the raw program is accompanied by the semantic promise that it halts on every input, and the universal evaluator need only terminate on codes satisfying that promise; see Recursive.Decidability.Membership.

The proof is the usual diagonal argument. Given a proposed presentation languageOf, encode a code c by the unary word of length encode c and define a language which disagrees with languageOf c on that word. Uniform decidability makes the diagonal language recursive, while adequacy says that it itself has a code, yielding a contradiction.

theorem Recursive_notComputableMembership {T Code : Type} [DecidableEq T] [Fintype T] [Primcodable T] [Nonempty T] [Primcodable Code] (languageOf : Code → Language T) : ¬ComputableMembership Recursive languageOf

Over any nonempty finite computably encoded alphabet, there is no adequate presentation of all recursive languages with uniformly computable membership.