17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Domain Theory and Differential Calculus (Functions of one Variable)
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
A data-type for differential calculus is introduced, which is based on domain theory. We define the integral and also the derivative of a Scott continuous function on the domain of intervals, and present a domain-theoretic generalization of the fundamental theorem of calculus. We then construct a domain for differentiable real valued functions of a real variable. The set of classical C1 functions, equipped with its C1 norm, is embedded into the set of maximal elements of this domain, which is a countably based bounded complete continuous domain. This gives a data type for differential calculus. The construction can be generalized to Ck and C∞ functions. As an immediate application, we present a domain-theoretic generalization of Picard?s theorem, which provides a data type for solving differential equations.