A Data-type for Differential Calculus
by
Abbas Edalat
Imperial College, London

Computer science has traditionally stayed outside the realm of differential calculus, which has been the exclusive territory of smooth mathematics, often referred to as mainstream mathematics. Using domain theory, we develop a data-type for differential calculus. Based on a new structure in domain theory, we define the derivative of a Scott continuous function on the domain of intervals, and show that this derivative is itself a Scott continuous function. A domain-theoretic generalization of the fundamental theorem of calculus follows. We then construct a domain for differentiable real valued functions of a real variable. The classical C¹ functions, equipped with its C¹ norm, is embedded into the set of maximal elements of this domain, which is a countably based bounded complete continuous domain. The construction can be generalized to C^k and C^\infty functions and to real valued functions of several variables. It can also be extended to analytic functions. As an immediate application, we present a domain-theoretic generalization of Picard's theorem, which provides a data-type for solving differential equations.

Date received: August 9, 2001