Mathematics and Computation

With Alex Simpson and Martín Escardó.

Abstract: We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number computation: the extensional approach, in which one has an abstract datatype of real numbers; and the intensional approach, in which one encodes real numbers using ordinary datatypes. We show that the type hierarchies coincide for second-order types, and we relate this fact to an analogous comparison of type hierarchies over the external and internal real numbers in Dana Scott’s category of equilogical spaces. We do not know whether similar coincidences hold at third-order types. However, we relate this question to a purely topological conjecture about the Kleene-Kreisel continuous functionals over the natural numbers. Finally, we demonstrate that, in the intensional approach to exact real-number computation, parallel primitives are not required for programming second-order total functionals over the reals.

Published in: In Proceedings ICALP 2002, Springer LNCS 2380, pp. 488-500, 2002.

Download: paradigms.pdf, paradigms.ps.gz, paradigms_proofs.ps.gz (long version, with proofs)