Reference and computation
pp. 77-106
in: , Treatise on intuitionistic type theory, Berlin, Springer, 2011Abstract
In the early history of computation, one finds algorithms like the Babylonian algorithm for the approximation of square roots, Archimedes' algorithm for the approximation of π, Euclid's algorithm for computing the greatest common divisor of two numbers, al-Khwārizmī's algorithms, etc. All these modes of computation, or algorithms, have in common that they produce a result for every conceivable input. In fact, it is safe to assume that the ancients would view an algorithm as erroneous if it did not always produce a result. Dirichlet's much debated pathological function ϕ was the first function in conflict with this classical notion of algorithm.