After my cat Shadow Marie mistimed her 0300 return to bed and landed 7 pounds of tuxedo attitude directly on my bladder, I found myself awake and thinking about total languages. This paper is her fault. She is acknowledged accordingly.
A proof sketch. Short. Two citations. No novel mathematics.
Total languages are frequently cited in formal verification and AI safety literature as a mechanism for producing verifiable, safe systems. This paper demonstrates that claim is incorrect, using only Rice (1953) and Turing (1936) — results that have been freely available for decades.
Rice's theorem states that no non-trivial semantic property of a program is decidable. Early termination — halting incorrectly, at the wrong point, with wrong output — is a non-trivial semantic property. It is equivalent to Turing's own second proof that the Entscheidungsproblem admits no solution: will this machine ever print this character.
Total languages provide an exit proof. They do not and cannot provide a correct-exit proof. That requires step-by-step verification of execution behavior. That is exactly the halting problem.
Additionally: the halting problem has three states, not two. Will not halt. Will halt correctly. Will halt early and incorrectly. The literature has been doing binary math on a trinary problem.
Novel. The mathematics here belongs entirely to Turing and Rice. This paper only insists their work be read carefully — including the second proof.
- Turing, A.M. (1936). On Computable Numbers, with an Application to the Entscheidungsproblem.
- Rice, H.G. (1953). Classes of Recursively Enumerable Sets and Their Decision Problems.
That's it. That's the literature review.
Shadow Marie. Pink nosed. 7 pounds. Devastating aim.