Seventeenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2002)

Paper: Domain Theory and Differential Caluculus (Functions of one variable) (at LICS 2002)

Authors: Abbas Edalat Andre Lieutier


We introduce a data type for differentiable functions in the framework of domain theory. Using a new structure, called tie of maps, which provide finitary information about the differential properties of a Scott continuous map, we define the derivative of a Scott continuous function on the domain of intervals, which is itself a Scott continuous function. This leads to a domain-theoretic generalization of the fundamental theorem of calculus. The central part of this work is to construct a domain for differentiable real valued functions of a real variable. The classical C^1 functions, equipped with its C^1 norm, is embedded into the set of maximal elements of this domain, which is a countably based bounded complete continuous domain with an effective structure. The construction can be generalized to C^k and C^infinity functions and, in future, to functions of several variables and analytic functions. While the question of computability for differentiable functions have been studied in the literature, this seems to be the first time that a proper data type for differential calculus is proposed which brings smooth mathematics in the realm of domain theory and type theory. As an immediate application, we present a domain-theoretic and effective generalization of Picard's theorem, which provides a data type and an algorithm for solving differential equations given by a vector field and an initial condition. At each step of computation of this algorithm, one gets an approximation which is an interval piecewise polynomial function with rational coefficients that provides precise information on the solution.


    author = 	 {Abbas Edalat and Andre Lieutier},
    title = 	 {Domain Theory and Differential Caluculus (Functions of one
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}