Undecidability of equivalence 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. Although membership is uniformly decidable under this promise, equivalence is not: there is no single partial-recursive Boolean procedure which terminates on every pair of valid codes and decides whether their languages agree.

The reduction compiles one valid decider for the empty language. Comparing an arbitrary valid code with that fixed code would decide emptiness, contradicting emptiness_undecidable.

theorem RecursiveDeciderCode.equivalence_undecidable {T : Type} [Primcodable T] [Nonempty T] : ¬ComputablePredOnPromise (fun (p : Nat.Partrec.Code × Nat.Partrec.Code) => Valid p.1 ∧ Valid p.2) fun (p : Nat.Partrec.Code × Nat.Partrec.Code) => language p.1 = language p.2

No promise algorithm can decide whether two valid always-halting decider codes denote the same language.

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

Equivalence is not uniformly decidable for recursive languages.

For every nonempty computably encoded alphabet, no partial-recursive Boolean evaluator can halt on all pairs of valid recursive-decider codes and decide equality of their denoted languages.