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.
