Computable values can be classical
Val Breazu-Tannen, Albert R. Meyer · 1987
In programming languages of universal power, the computational integers must be distinguished from the classical integers because of the “divergent” integer. Even the equational theory corresponding to evaluation of integer expressions is distinct from the theory of classical integers, and classical reasoning about computational integers yields inconsistencies. We show that there exist “programming languages”, actually extensions of the polymorphic lambda calculus, that have tremendous computing power and yet whose computational integers, or any other algebraically specified abstract data type, coincide with their classical counterpart. In particular, the equational theory of the programming language is a conservative extension of the theory of the underlying base types as given by algebraic data type specifications.