%\nopagenumbers
\documentclass[11pt,a4paper,amssym]{article}

\usepackage{amssymb}
\textwidth=14cm
 \usepackage{graphicx}
\input{diagrams}
%\usepackage{acmconf}
%
\newcommand{\R}{{\mathbb R}}
\newcommand{\lp}{\lesssim}
\newcommand{\eqdef}{\stackrel{\rm {\mbox{\small{def}}}}{=}}
\newcommand{\ifdef}{\stackrel{\rm {\small{def}}}{\iff}}
\newcommand{\gp}{\gtrsim}
\newcommand{\wai}{\mbox{$\omega$-algebraic I-category}}
\newcommand{\wa}{\mbox{$\omega$-algebraic}}
\newcommand{\itemi}{\item[{\rm(i)}]}
\newcommand{\itemii}{\item[{\rm(ii)}]}
\newcommand{\itemiii}{\item[{\rm(iii)}]}
\newcommand{\itemiv}{\item[{\rm(iv)}]}
\newcommand{\itemv}{\item[{\rm(v)}]}
\newcommand{\itemvi}{\item[{\rm(vi)}]}
\newcommand{\itemvii}{\item[{\rm(vii)}]}
\newcommand{\itemviii}{\item[{\rm(viii)}]}
\newcommand{\IR}{{\bf I}{\mathbb R}}
\newcommand{\bigsqcap}{\mbox{{\huge $\sqcap$}}}
\newcommand{\Ii}{{\bf I}{[0,1]}}
\newcommand{\rat}{\rightarrowtail}
\newcommand{\dhva}{\VerticalMap\empty|\empty|\dhvvee}
\newcommand{\limUnderline}{\mathop{\underline{\lim}}}
\newcommand{\limOverline}{\mathop{\overline{\lim}}}
\newcommand{\uha}{\VerticalMap\uhvee|\empty|\empty}
\newcommand{\uta}{\VerticalMap \empty|\empty|\uhvee}
\newcommand{\Ra}{\Rightarrow}\newcommand{\I}{{\bf I}}
\newcommand{\wtr}{\triangleleft}
\newcommand{\tr}{\trianglelefteq}
\newcommand{\trm}{\trianglelefteq^{m}}
%\newcommand{\dtr}{\ll^o}
\newcommand{\sem}[1]{[\mkern-2.5mu[#1]\mkern-2.5mu]}
\newcommand{\dtr}{\mathrel{\triangleleft\mkern-2mu\triangleleft}}
\newcommand{\dtrm}{\dtr^m}
%\newcommand{\dtr}{\triangleleft\hspace{-.06in}\triangleleft\hspace{.05in}}
%\newcommand{\dtrm}{\triangleleft\hspace{-.06in}\triangleleft^m\hspace{.05in}}
%\newcommand{\dtrm}{\ll^{m}}
\newcommand{\is}{information system}
\newcommand{\Is}{Information system}
\newcommand{\sge}{\sqsupseteq}
\newcommand{\sle}{\sqsubseteq}
\newcommand{\ra}{\rightarrow}
\newcommand{\cat}[1]{\mbox{\bf #1}}
\newcommand{\omcat}[1]{\mbox{$\omega$-{\bf #1}}}
\newcommand{\catbot}[1]{\mbox{$\mbox{\bf #1}_\bot$}}
\newcommand{\omcatbot}[1]{\mbox{$\omega$-$\mbox{\bf #1}_\bot$}}
%\newcommand{\catpar}[3]{\mbox{$\mbox{\bf #1}_{#2}~{#3}$}}

\newcommand{\fsp}[2]{\mbox{$[#1 \longrightarrow #2]$}}
\newcommand{\sfsp}[2]{\mbox{$[#1 \stackrel{s}{\longrightarrow} #2]$}}
\newcommand{\secfsp}[1]{$\Bigl[[#1 \rightarrow #1] \longrightarrow
                      [#1 \rightarrow #1] \Bigr]$}
 
\newcommand{\fromto}[3]{\mbox{$#1\colon #2\rightarrow #3$}}
\newcommand{\implies}{\mathrel{\mbox{$\Longrightarrow$}}}
%\newcommand{\iff}{\mathrel{\mbox{$\Longleftrightarrow$}}}
\newcommand{\tra}{\twoheadrightarrow}
\newcommand{\tfa}{\twoheadleftarrow}
\newcommand{\tla}{\twoheadleftarrow} 
\newcommand{\da}{\mathord{\downarrow}}
\newcommand{\ua}{\mathord{\uparrow}}
\newcommand{\dda}{\mathord{\hbox{\makebox[0pt][l]{\lower .6mm
                           \hbox{$\downarrow$}}$\downarrow$}}}
\newcommand{\dua}{\mathord{\hbox{\makebox[0pt][l]{\raise .6mm
                           \hbox{$\uparrow$}}$\uparrow$}}}
\newcommand{\step}[2]{\mbox{$#1\searrow #2$}}
\newcommand{\stepp}[2]{\mbox{$#1\searrow_{D^0} #2$}}
\newcommand{\steppp}[2]{\mbox{$#1\searrow_{D^0_{{\sf r}}} #2$}}

 
\newcommand{\xtb}{\mbox{${\bf X}~\top_\bot$ }}
\newcommand{\id}[1]{\mbox{\sf id$_{#1}$}}

\newcommand{\qede}{\rule[-.3mm]{.8mm}{3mm} \par \medbreak} 
%\newcommand{\qed}{\rule[-.3mm]{.8mm}{3mm} \par \medbreak}
%\newcommand{\qed}{\rule[-.3mm]{.8mm}{3mm}}
\def\qed{{$\square$}}

\def\pushright#1{{\parfillskip=0pt\widowpenalty=10000
  \displaywidowpenalty=10000\finalhyphendemerits=0
  \leavevmode\unskip\nobreak\hfil\penalty50\hskip.2em\null
  \hfill{#1}\par}}

\newcommand{\rqed}{\pushright{\qed}}

\def\pushright#1{{\parfillskip=0pt\widowpenalty=10000
  \displaywidowpenalty=10000\finalhyphendemerits=0
  \leavevmode\unskip\nobreak\hfil\penalty50\hskip.2em\null
  \hfill{#1}\par}}
\newtheorem{aaxiom}{\bf Ax}
\newtheorem{axiom}{\bf Axiom} 
\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{defin}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark} 
\newenvironment{definition}
  {\begin{defin}\rm}{\end{defin}}
\newtheorem{ex}[theorem]{Example}
\newenvironment{example}{\begin{ex}\rm}{\end{ex}}
\newtheorem{prob}{Problem}
\newenvironment{problem}{\begin{prob}\rm}{\end{prob}}
\newtheorem{exer}[theorem]{Exercise}
\newenvironment{exercise}{\begin{exer}\rm}{\end{exer}}
%\newtheorem{re}[theorem]{Remark}
%\newenvironment{remark}{\begin{re}\rm}{\end{re}}
\newenvironment{proof}
  {\begin{trivlist}\item[\hskip\labelsep{\bf Proof}]}{\end{trivlist}}
 
\newcommand{\dsup}{\mathop{
                   \bigsqcup{}~{\makebox[0pt]{  $\scriptstyle\uparrow$}}}}
 
%\newcommand{\less}{<}

\newenvironment{propositionp}{%
\addtocounter{theorem}{-1}\renewcommand{\thetheorem}{\arabic{section}.\arabic{theorem}$'$}%
\begin{proposition}}%
{\end{proposition}\renewcommand{\thetheorem}{\arabic{theorem}}}

 
\newcommand{\defind}[1]{{\em #1}\index{#1}}
\newcommand{\defindv}[2]{{\em #1}\index{#2}}
\newcommand{\symind}[2]{#1\index{#2}}
 
\newcommand{\ch}[1]{\includeonly{ch#1}}
\newcommand{\showlabels}{\input{shlabels}}

\title{{\bf \mbox{Domain Theory and Differential Calculus}}\\(Functions
of one Variable)}
\author{{\bf Abbas Edalat}\\ Department of Computing, Imperial College, London, UK\\\\
{\bf Andr\'e Lieutier}\\Dassault Systemes Provence and\\ LMC/IMAG, Aix-en-Provence and Grenoble, France}
\date{}
\begin{document}
\maketitle
\begin{abstract}
  
 
  We introduce a domain-theoretic framework for differential calculus.
  We define the set of primitive maps and also the derivative of a Scott
  continuous function on the domain of intervals, and show that they are dually related, providing an extension of the classical duality of differentiation and integration as in the fundamental theorem of calculus. We then construct a domain for differentiable real valued
  functions of a real variable. The set of classical $C^1$ functions,
  equipped with its $C^1$ norm, is embedded into the set of maximal
  elements of this countably based, bounded complete
  continuous domain. This domain also provides a model for the differential properties of piecewise $C^1$ functions, locally Lipschitz functions and more generally of all continuous functions. We thus obtain a data type for differential calculus.
  As an immediate application, we present a domain-theoretic
  generalization of Picard's theorem, which provides a data type for
  solving differential equations.
 

\end{abstract}

\section{Introduction}
We introduce a domain-theoretic framework for
differentiable functions, which leads to a data type for
differentiable functions and a data type for solving
differential equations. Differential calculus, introduced  by Newton and
Leibnitz in the 17th century, has provided the foundation of modern
science and technology and is the basis of applied mathematics,
mathematical physics and scientific computation. By constructing data types for differential calculus, we seek to bring smooth mathematics
into the realm of computer science.

The key element in our framework is the notion of the {\em set of primitive maps} of a Scott continuous function on the domain of intervals,
which is derived here from basic principles. First, the
concept of an {\em interval derivative} of a Scott continuous function
is introduced. A non-trivial interval derivative of a classical
continuous function at an open interval is given by a compact interval
whose left and right end points are, respectively, a lower and an upper Lipschitz constant for the
function in that open interval. An interval derivative at an open
interval thus corresponds to a single-step function, and the
collection of interval derivatives is in bijective correspondence
with the collection of single-step functions. The natural concept of interval derivative at an open
interval, and its corresponding single-step function, can be
generalized to Scott continuous functions of the domain of
intervals. The set of primitive maps of a single-step function is then
defined as the collection, or the {\em single-step tie}, of all Scott continuous functions which have
interval derivatives corresponding to the single-step function. Using the
fact that any Scott continuous function can be constructed from single-step functions, the set of primitive maps of a Scott continuous function
can then be defined as a collection, or {\em tie}, of Scott continuous
functions with interval derivatives represented by the integrand. 

The interval derivative of a Scott continuous function gives local
information on the differential properties of the function. By
collecting all such information, we move from a local to a global
viewpoint and 
define the derivative of a Scott continuous function on the domain of
intervals, which is itself shown to be a Scott continuous function.
This is in sharp contrast to the situation in classical analysis in
which a continuous function may not have a derivative at a point or
indeed at any point at all. In the domain-theoretic world, such
irregularities do not occur and the derivative of any Scott continuous
function is itself a function of the same type.



The central part of this work is the construction of a domain $D^1$ for
differentiable real valued functions of a real variable. This domain
is a subset of the product of two copies of the domain of Scott
continuous interval-valued functions
on the domain of intervals, where the subset is characterized
by a consistency relation between two Scott continuous functions. In a
consistent pair of functions, the first function represents an
approximation to the $C^1$ function itself while the second function
in the pair gives an approximation to the derivative of this $C^1$
function. The consistency relation is Scott closed and decidable on
basis elements, which shows that $D^1$ is a countably based bounded
complete continuous domain with an effective structure. The set of classical
$C^1$ functions, equipped with its $C^1$ norm, is embedded into the
set of maximal elements of $D^1$. Furthermore, the set of piecewise $C^1$ functions, the set of locally Lipschitz functions and the set of all continuous functions are each embedded into the set of maximal elements of $D^1$, thereby giving a model for the differential properties of various types of functions. 

Whereas the question of
computability for differentiable functions has been studied in the
literature~\cite{PR89,Wei00}, this seems to be the first time that 
data types for differential calculus are proposed which brings
this subject into the discipline 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 about the solution, even when both the initial
condition and the specifying vector field are given with
uncertainty. 

Another application of this work will be to provide an effective
version of what is referred to as the implicit function theorem, which
is a main tool in the study of manifolds. In the one variable case
considered in this paper, 
the effective version of the implicit function theorem provides an
algorithm to obtain the isolated roots of differentiable functions. In
multi-variate differential calculus, which will be treated in
a future paper, the implicit function theorem is used extensively in geometric design of smooth curves and surfaces.
Since the functions defining the curves or surfaces used in CAD
software can be of various concrete classes (piecewise polynomial,
rational, trigonometric as well as more ``exotic" classes of smooth
functions), the use of abstract classes representing $C^k$ functions
allows us to design generic algorithms for solving systems of equations
arising for example in surface intersections, ray shooting, and many
other geometric operators.  In fact, the data type introduced here
can provide a sound mathematical framework on top of which these existing
practices could be founded~\cite{HMSP95, SSP99}. 



The present work is the continuation of the 10 year old project for
constructing domain-theoretic computational models in various subjects
including fractal geometry, measure and integration, real number
computation, computational geometry and solid
modelling~\cite{Eda93,Eda94,Law96,EH96,Esc96,EE00,EP97,ES97,Eda97,EL99}.





\section{The interval domain function spaces}\label{step}

We assume the reader is familiar with the basic notions in domain
theory; our main references for the subject
are~\cite{GHKLMS80,AJ94,SLG94,AC98}. 
For any dcpo (directed complete partial order) $A$, let ${\sf Con}_{(A,\sle)}$ and ${\sf Con}_{(A,\ll)}$ denote, respectively, the
consistency predicate with respect to $\sqsubseteq$ and $\ll$, i.e.

\[{\sf Con}_{(A,\sle)}(a_1,a_2,\dots a_n)\iff \exists a\in A.a_i\sqsubseteq
a\mbox{  for all
$1\leq i\leq n$}.\]

\[{\sf Con}_{(A,\ll)}(a_1,a_2,\dots a_n)\iff \exists a\in A.a_i\ll a\mbox{ for all
$1\leq  i\leq n$}.\]
We often write ${\sf Con}_\sle$ and ${\sf Con}_\ll$ for ${\sf Con}_{(A,\sle)}$ and ${\sf Con}_{(A,\ll)}$ respectively.
For dcpo's $(D,\sqsubseteq_D)$ and
$(E,\sqsubseteq_E)$, the single-step function $\step{a}{b}:D\to E$ is defined by
\[(\step{a}{b})(x)=\left\{\begin{array}{cc}b&\mbox{if } a\ll x\\
\bot& \mbox{otherwise}.\\
\end{array}\right.\]
In this paper, we will only work with continuous Scott domains (i.e.\ bounded complete $\omega$-continuous
dcpo's). The general form of a step function from a continuous Scott domain
 $(D,\sqsubseteq_D)$ to another one
$(E,\sqsubseteq_E)$ is as follows. Consider the collection
$(\step{a_i}{b_i})_{i\in I}$ where $I$ is a finite set. Define the function space consistency predicate ${\sf Con}_{D\to E}(u)$  by:
\[{\sf Con}_{D\to E}((\step{a_i}{b_i})_{i\in I}) \iff\forall
J\subseteq I.({\sf Con}_{(D,\ll)}(\{a_i\,|\,i\in J\})\Rightarrow {\sf Con}_{(E,\sle)}(\{b_i\,|\,i\in J\})).\]
Then the lub $\bigsqcup_{i\in I}\step{a_i}{b_i}$ exists iff
${\sf Con}_{D\to E}((\step{a_i}{b_i})_{i\in I})$. When the lub
exists, it takes a finite number of values and it is given by: 
\[(\bigsqcup_{i\in I}\step{a_i}{b_i})(x)=\bigsqcup_{a_i\ll x} b_i.\]



The ordering of step functions is given by:

\[(\bigsqcup_{i\in I}\step{a_i}{b_i})\sqsubseteq (\bigsqcup_{j\in J}\step{c_j}{d_j})\iff \forall i\in
I. b_i\sqsubseteq \bigsqcup_{c_j\sle a_i}d_j.\]

The way-below ordering of step functions is given by:

\[(\bigsqcup_{i\in I}\step{a_i}{b_i})\ll (\bigsqcup_{j\in J}\step{c_j}{d_j})\iff \forall i\in
I. b_i\ll\bigsqcup_{c_j\ll a_i}d_j.\]

For any dcpo's $D$ and $E$, the collection of all lubs
$(\bigsqcup_{i\in I}\step{a_i}{b_i})$ of consistent
step functions with $a_i\in B$ and $b_i\in B'$, where $B$ and $B'$ are
bases for $D$ and $E$ respectively, gives a basis for $D\rightarrow E$.

We consider the function spaces $D^0[0,1]=(\I[0,1]\to \IR)$ and
$D^0_{{\sf r}}[0,1]=([0,1]\to \IR)$; here $\I[0,1]$ is the continuous Scott
domain of the compact intervals of $[0,1]$ ordered by reverse
inclusion, and $\IR$ is the continuous Scott
domain of the compact intervals of $\R$ together with $\R$ ordered by reverse
inclusion. Note that $D^0[0,1]$ is the collection of Scott continuous
interval-valued functions of an interval variable, whereas
$D^0_{{\sf r}}[0,1]$ is the collection of Scott continuous interval-valued
functions of a {\em real} variable; hence the subscript ${\sf r}$ in $D^0_{{\sf r}}[0,1]$. We sometimes write $D^0$ for $D^0[0,1]$
and $D^0_{{\sf r}}$ for $D^0_{{\sf r}}[0,1]$. The choice of $[0,1]$ is simply for
convenience. In practice, we sometimes replace $[0,1]$ by a
non-trivial compact interval $a=[\underline{a},\overline{a}]$, a
relatively compact open interval $a^\circ=(\underline{a},\overline{a})$ (with
$\underline{a}<\overline{a}$) or even $\IR$. Recall that any continuous function
$f:[0,1]\to \R$ has a canonical extension
$\I f:\I [0,1]\to \IR$ given by $({\bf I}f)(x)=f(x)$, for $x\in{\bf
  I}[0,1]$, where $f(x)$ is the direct image of the interval $x$. In particular the three basic arithmetic functions,
addition, subtraction and multiplication, extend pointwise to Scott
continuous functions $\IR\to\IR$ which, for convenience, we denote
simply by $+$, $-$ and $\times$, i.e.\ for $x,y\in\IR$ we write
$x*y=\{u*v\,|\,u\in x,v\in y\}$ where $*\in\{+,-,\times\}$. As usual
we set $a*b=\bot$ if $a=\bot$ or $b=\bot$ for $*\in\{+,-,\times\}$. 


A function $f:[0,1]\to\IR$, given by two functions
$f^-,f^+:[0,1]\to\R$ with $f(x)=[f^-(x),f^+(x)]$, is continuous with
respect to the Euclidean topology on $[0,1]$ and the Scott topology on
$\IR$ iff $f^-$ and $f^+$ are, respectively, lower and upper
semi-continuous functions. In this case, $f$ will have a Scott
continuous extension to $\I [0,1]$, which, by overloading notation, we
denote by $\I f=\I [f^-,f^+]: \I [0,1]\to \IR$; it is given by $\I f(x)=\bigsqcap
\{f(y)\;|\;y\in x\}$. The mapping ${\cal E}:D^0_{{\sf r}}\to D^0$ with
${\cal E}(f)={\bf I}f$ is Scott continuous and injective. Thus we
consider $D^0_{{\sf r}}$ as a subdomain of $D^0$. The Scott continuous map
${\cal I}:D^0\to D^0_{{\sf r}}$ with ${\cal I}:f\mapsto \lambda x.\, 
f(\{x\})$ in effect sends a function to its restriction on the maximal elements of
${\bf I}[0,1]$. We have ${\cal I}\circ
  {\cal E}=1_{D^0_{{\sf r}}}$ and ${\cal E}\circ {\cal I}\sge 1_{D^0}$ where $1_A$
  is the identity function on the dcpo $A$. In fact, we put  ${\cal
    M}={\cal E}\circ {\cal I}$; then ${\cal M}(f)$ is the greatest
  function in $D^0$ whose restriction to the maximal elements
  coincides with that of $f$~\cite{EE00}. We can deduce the action
  of ${\cal I}$ and ${\cal E}$ on step functions. We write $a\searrow_A b$ for
  the single-step function $\step{a}{b}$ in the domain $A$. However, since we
  will only be concerned with step functions in $D^0$ and $D^0_{{\sf r}}$ we
  write $a\searrow_{D^0} b$ simply as  $a\searrow b$ and  $a\searrow_{D^0_{{\sf r}}} b$
  as $a\searrow_{{\sf r}} b$. For any finite set $I$ we have: ${\cal I}(\bigsqcup_{i\in I}{a_i}\searrow{b_i})=\bigsqcup_{i\in
    I}{a_i}\searrow_{\sf r}{b_i}$ while 
\[{\cal E}(\bigsqcup_{i\in
    I}a_i\searrow_{{\sf r}}b_i)=\bigsqcup\{(\sqcap_{\mbox{}_{j\in
    J}}{a_j})\searrow\sqcap_{\mbox{}_{j\in J}}{b_j}\,|\, J\subseteq I \mbox{
    with }\bigcup_{j\in
    J}a_j^\circ\mbox{ connected}\}.\]
These formulas extend by continuity to all suprema of step
functions. We have
\begin{equation}\label{consd0-d}{\sf Con}_{D^0}(a_i\searrow
  b_i)_{i\in I} \iff {\sf Con}_{D^0_{{\sf r}}}(a_i\searrow_{{\sf r}} b_i)_{i\in I}\end{equation}  

Any mapping $f\in
D^0_{{\sf r}}$ is given by a lower and an upper semi-continuous function $f^-$
and $f^+$ respectively such that $f(x)=[f^-(x),f^+(x)]$. More
generally, the restriction of a Scott
continuous function $f\in D^0$ to the maximal elements
induces a lower and an upper semi-continuous functions
$f^-,f^+:[0,1]\to\R$ given by $f(\{x\})=[f^-(x),f^+(x)]$. Clearly, $f$
preserves maximal elements iff $f^-=f^+$, in which case the induced
map $f^-=f^+:[0,1]\to\R$ is continuous with respect to the Euclidean
topology; for convenience, we denote this induced map simply by $f$
itself and write ``the induced map $f:[0,1]\to\R$''. 

It is convenient to define a more general basis for $D^0$ and $D^0_{{\sf r}}$,
which we will define as follows. By a {\em rational} polynomial
we mean a polynomial with rational coefficients.  
\begin{definition}
A continuous function $p:[v,w]\to\R$ is a {\em piecewise (rational) 
  polynomial} if there exists a partition $v=c_0<c_1\cdots <c_{n-1}<
c_n=w$ of $[v,w]$ such that $c_i$ ($i=0,\cdots,n$) are real (rational)
numbers 
 and each restriction $p\restriction_{[c_{i-1},c_i]}$ is a (rational)
 polynomial. We call $p$ a {\em piecewise
  semi-rational polynomial} if $c_i$ ($i=0,\cdots,n$) are algebraic
numbers and each restriction $p\restriction_{[c_{i-1},c_i]}$ is a
rational polynomial up to an additive algebraic number (i.e.\ all
the coefficients are rational except possibly the constant term which
is an algebraic number).
\end{definition}



Let $a\in \I[0,1]$ and let $p,q:[\underline{a},\overline{a}]\to \R$ be
piecewise (rational or semi-rational) polynomials satisfying $p(x)\leq
q(x)$ for $x\in a^\circ$. We define the ({\em rational or semi-rational) polynomial step function} $\step{a}{[p,q]}:\I[0,1]\to\IR$ by 
\[(\step{a}{[p,q]})(x)=\left\{\begin{array}{cc}\I[p,q](x)&\mbox{ if } a\ll x\\
\bot& \mbox{ otherwise}.\\
\end{array}\right.\]

Clearly, by choosing $p$ and $q$ to be the constant polynomials $\underline{b}$ and $\overline{b}$ we obtain an ordinary step function, i.e.\ $\step{a}{[\underline{b},\overline{b}]}=\step{a}{b}$.
The consistency relation for a finite set of polynomial step functions is given by:
$\{\step{a_i}{[p_i,q_i]}\;|\; i\in I\}\in{\sf Con}_0$ iff \[ \forall J\subseteq I.\; {\sf Con}_\ll\{a_i\;|\; i\in J\}\Ra \forall i,k\in J\;\forall x\in(\bigsqcup_{j\in J}a_j)^\circ.\;p_i(x)\leq q_k(x).\]
The collection of consistent finite sets of rational (or semi-rational)
polynomial step functions forms a basis for $D^0$ which we call the
{\em rational (or semi-rational) polynomial basis}. We also get a similar
basis for $D^0_{{\sf r}}$ with its similar consistency relation; in fact $({a}\searrow_{{\sf r}}{[p,q]})={\cal I}({a}\searrow{[p,q]})$
is given by
\[({a}\searrow_{{\sf r}}{[p,q]})(x)=\left\{\begin{array}{cc}\I[p,q](x)&\mbox{ if }
    x\in a^\circ\\
\bot& \mbox{ otherwise}.\\
\end{array}\right.\]


Consider a step function $f=\bigsqcup_{i\in I}\{(a_i\searrow b_i)\}$. The end points
of the compact intervals $a_i$, ($i\in I$), partition $[0,1]$ into a
finite number of intervals (open, closed or half-open, half-closed) 
of $[0,1]$, called the {\em
associated intervals} of the step function, with the property that
$f(\{x\})$ is a constant compact interval for $x$ in each of these
intervals. For a polynomial step function
$f=\bigsqcup_{i\in I}\{(a_i\searrow[p_i,q_i])\}$, the compact interval
$f(\{x\})$ is bounded by two fixed piecewise polynomials in each of the associated intervals.

We define the domain of $h:{\bf
I}[0,1]\rightarrow {\bf I}{\Bbb R}$ by $$Dom(h)=\{x\in[0,1]|
h(\{x\})\neq \bot\}$$
\subsection{Embedding of classical functions }

Let $C^0[0,1]$ be, as usual, the set of real-valued continuous functions
on $[0,1]$ with the sup norm; its topology is the same as the compact
open topology. Furthermore, for an integer $k\geq 1$, we let
$C^k[0,1]$ denote the set of functions with
continuous $k$th derivative on $[0,1]$ equipped with the norm
$||f||=\max\{\sup|f^{(n)}|\,|\,0\leq n\leq k\}$,where $f^{(n)}$ is the
$n$th derivative of $f$.

Define,
$\Gamma^0:C^0[0,1]\rightarrow D^0[0,1]$ by $\Gamma^0(f)={\bf
  I}f$. Recall that an embedding is a continuous injection which maps
open subsets to relatively open subsets in its image.

\begin{theorem}\label{embedding}
The mapping $\Gamma^0$ is an embedding into a proper subset
of the maximal elements of $D^0$
\end{theorem}
\begin{proof}

We use the way-below relation both for domains such as $D^0$ and for
the lattice $\Omega X$ of the open subsets of a locally quasi-compact topological
space $X$. 

The function $g:{\bf
I}[0,1]\rightarrow {\bf
I}{\Bbb R}$ with 
\begin{equation}\label{maxnonclassic}g(x)=\left\{\begin{array}{ll}\{0\}& \mbox{if } {\overline{x}}<1/2\\[1ex] 
\{1\}&\mbox{if } {\underline{x}}>1/2 \\[1ex] 
[0,1]&\mbox{if } 1/2\in x\\\end{array}
\right.\end{equation}
is maximal but is not the extension of any function in $C^0[0,1]$.

Continuity: We have \[{\bf I}f=\bigsqcup_{i\in I}\{a_i\searrow b_i|
a_i\searrow b_i\ll_{D^0} {\bf I}f\}=\bigsqcup_{i\in I}\{a_i\searrow b_i|
\dua a_i\ll_{\Omega \I[0,1]} ({\bf I}f)^{-1}(\dua b_i)\}.\] Hence any open set containing ${\bf I}f$
contains a step function $\bigsqcup_{i\in J}a_i\searrow b_i$, for some
finite indexing set $J$, with $\dua 
a_i\ll f^{-1}(\dua b_i)$ ($i\in J$) which contains ${\bf I}f$. But the
open set $\bigcap_{i\in J}({a_i},b_i^\circ)$ (of the compact open topology) contains $f$
and is mapped into $\dua (\bigsqcup_{i\in J}a_i\searrow b_i)$.

Openness: Let $(C,O)$ be an open set of the compact-open topology
containing the continuous $f:[0,1]\rightarrow {\Bbb R}$. Then there
exists a decreasing sequence $C_i$ of finite unions of intervals such
that $C=\bigcap_{i\in\omega}C_i$. By Scott continuity of ${\bf I}f$,
there exists an $i\in\omega$ such that $({\bf
I}f)(C_i)=f(C_i)\subseteq O$. Suppose $C_i=\bigcup_{j=1}^nA_j$ where
each $A_j$ is a compact interval. Since $f(A_j)$ is compact, there
exist open sets $B_j$  with $f(A_j)\subseteq
B_j\subseteq O$ and $\overline {B_j}\subseteq O$, for $1\leq j\leq
n$. Then ${\bf
I}f\in \dua (A_j\searrow B_j)$  for $1\leq j\leq n$. Moreover,
$(\Gamma^0)^{-1}( \dua (A_j\searrow B_j))\subseteq (C,O)$. Hence $\Gamma^0$
is a topological embedding.~\qed



\end{proof}Recall that an {\em adjunction} between posets $A$ and $B$ is a pair
of monotone maps $l:A\to B$, called lower adjoint, and $u:B\to A$,
called upper adjoint, with $u\circ l\sge 1_A$
and $l\circ u\sle 1_B$. Then, we have: 
\begin{proposition}\cite{AJ94}\label{adjunction}
\begin{itemize}
\itemi $u\circ l\circ u=u$ and  $l\circ u\circ l=l$.
\itemii The image of $u$ and the image of $l$ are order-isomorphic and
the isomorphism is given by the restrictions of $u$ and $l$ to
$\mbox{im}(l)$ and $\mbox{im}(u)$. 
\itemiii $l$ is surjective iff $l\circ u=1_B$ iff $u$ is injective.
\itemiv $l$ preserves all existing suprema, $u$ preserves all existing
infima.
\itemv Suppose $A$ is a dcpo and $B$ is a continuous domain, then $u$
is Scott continuous if $l$ preserves the way-below relation.~\qed
\end{itemize}
\end{proposition}
Recall also that a section-retraction pair $(s,r)$ between dcpo's $B$ and
$A$ is a pair of continuous maps $r:A\to B$ and $s:B\to A$ such that
$r\circ s=1_B$. If $A$ is a continuous dcpo then $\mbox{Im}(r)\subseteq B$ is a
continuous dcpo and the image of any basis of $A$ under $r$ is a basis
for $\mbox{Im}(r)$.
A section-retraction is a {\em section-inflation pair} if
$s\circ r\sge 1_A$. In other words a section-inflation pair
is a continuous adjunction $(u,l)$ such that $l\circ u=1_B$.
 
Consider the map $\Gamma^0_{{\sf r}}={\cal I}\circ\Gamma^0:C^0\to D^0_{{\sf r}}$; then
$\Gamma^0_{{\sf r}}$ is essentially the inclusion map if we consider $C^0$ as
a subset of $D^0_{{\sf r}}$, i.e.\ by identifying the real valued map $x\mapsto
f(x)$ with the map $x\mapsto \{f(x)\}$ . Note that ${\cal I}$,
being a continuous inflation, preserves the way-below relation and is
hence an open map. Thus, we also have:
\begin{corollary}
 $\Gamma^0_{{\sf r}}:C^0\to D^0_{{\sf r}}$ is an embedding into a proper subset
 of the maximal elements of $D^0_{{\sf r}}$.
\end{corollary}
\section{Primitive maps of a Scott continuous function}
In classical analysis, the primitive maps, or the indefinite integrals, of a continuous
function $f:[0,1]\to\R$ can be considered as the family of continuous
functions $\{F+a\;|\; a\in\R\}$ where $F:[0,1]\to\R$ is differentiable
with $F'=f$. In this section, we seek the analogous concept in domain
theory. In order to define the primitive maps of a Scott
continuous function, which in the spirit of classical analysis is
expected to be a family of Scott continuous functions, we first
introduce the notion of an {\em interval derivative} of a Scott
continuous function.

\subsection{Interval derivative}The idea of an interval
derivative can be motivated by considering the case of a classical
function or its canonical interval domain extension. Suppose, for some open
interval $a\subseteq [0,1]$ and a compact interval $b\subseteq \R$,
the function $f:[0,1]\ra\R$ satisfies $\underline{b}(x-y)\leq
f(x)-f(y)\leq \overline{b}(x-y)$ for all $x,y\in a^\circ$ with $y\leq
x$; note that if $f$ is in fact $C^1$ this will be equivalent to
$\underline{b}\leq f'(x)\leq \overline{b}$ for all  $x\in a^\circ$. We say
that $\underline{b}$ and $\overline{b}$ are, respectively, a {\em lower
Lipschitz constant} and
an {\em upper Lipschitz constant} for $f$ at the open interval $a$. Then we can think of $b$ as an interval derivative for $f$ at
$a$. The above inequalities can be expressed in terms of $\I
f:\I[0,1]\ra \IR$ to give: $b(\{x\}-\{y\})\sle \I f
(\{x\})-\I f(\{y\})$ for all $\{x\},\{y\}\gg a$. This latter condition is
now generalized as follows to define the notion of an interval derivative.

\begin{definition}\label{deftie}
The continuous function $f:{\bf I}[0,1]\ra{\bf I}{\mathbb R}$ has {\em 
an interval derivative} $b\in {\bf I}{\mathbb R}$ in $a\in{\bf
I}[0,1]$ if $f$ satisfies the following differential property: for all $x_1,x_2\in{\bf I}[0,1]$ with $a\ll x_1$ and $a\ll 
x_2$, $b(x_1-x_2)\sqsubseteq f(x_1)-f(x_2)$.
The {\em single-step tie}
$\delta(a,b)\subseteq D^0[0,1]$ of $a$ with $b$ 
is the collection of all functions in $D^0[0,1]$ which have an interval
derivative $b$ in $a$. 
\end{definition}
\begin{proposition}\label{geometric}
\begin{itemize}
\itemi If $f\in \delta(a,b)$, for $b\neq \bot$, then $f(\{x\})$ is maximal for each $x\in
  a^\circ$ and the induced function
  ${f}:(\underline{a},\overline{a})\to \R$ is Lipschitz and for
all $u,v\in a^\circ$ with $v\leq u$ we have $\underline{b}(u-v)\leq
{{f}(u)-{f}(v)}\leq \overline{b}(u-v)$. 
\itemii  
For $f:(\underline{a},\overline{a})\to {\mathbb R}$, with $a\subseteq
[0,1]$ a non-trivial interval, we have ${\bf I}f\in\delta(a,b)$ iff
$f$ is Lipschitz and for
all $u,v\in a^\circ$ with $v\leq u$ we have $\underline{b}(u-v)\leq
{f(u)-f(v)}\leq \overline{b}(u-v)$. 
\end{itemize}
\end{proposition}
\begin{proof}
(i) Suppose $f\in \delta(a,b)$, but $f(\{y\})$ is not maximal. Let
$\epsilon>0$ be small enough so that $x=[y-\epsilon,y+\epsilon]\subseteq
a^\circ$. The diameter of $b(x-x)$ can be made arbitrarily small by
choosing $\epsilon$ small. However, since $b(x-x)\sle f(x)-f(x)$, it follows
that the diameter of $b(x-x)$ is larger than the diameter of
$f(x)-f(x)$ which is larger than the diameter of $f(\{y\})$. This
contradiction establishes the proof.

(ii) If ${\bf I}f\in\delta(a,b)$ and $\underline{a}<v\leq u<\overline{a}$, then
by putting $x=\{u\}$ and $y=\{v\}$ we get $b(\{u\}-\{v\})\sle
 {\bf I}f(\{u\}- {\bf I}f(\{v\})$, in other words $\underline{b}(u-v)\leq
f(u)-f(v)\leq \overline{b}(u-v)$. For the other implication, assume
that $x,y\gg a$ and $z\in {\bf I}f(x)-{\bf I}f(y)$. Then $z=f(u)-f(v)$ for
some $u\in x$ and $v\in y$. Hence, $\frac{z}{u-v}\in b$ and it follows
that $z\in b(x-y)$.\qed
\end{proof}

From Proposition~\ref{geometric}, we get a simple geometric
characterization for $\I f\in \delta(a,b)$ for a classical function $f\in C^0[0,1]$. Let
$L(x,\underline{b})$ and $L(x,\overline{b})$ be the straight lines
through the point $(x,f(x))$, for $x\in a^\circ$, with slopes
$\underline{b}$ and $\overline{b}$ respectively. We have ${\bf
I}f\in\delta(a,b)$ iff the graph of $f$ at $(x,f(x))$, for each $x\in
a^\circ$, is locally contained within the closed region bounded
anti-clockwise from $L(x,\underline{b})$ to $L(x,\overline{b})$ (see
Figure~\ref{geomint}).


\begin{figure}[ht]\begin{center}
\includegraphics*[scale=.25]{figure2.eps}
\caption{Geometric interpretation of interval derivative}
\label{geomint}\end{center}
\end{figure}


\begin{example}\label{examples} 
\begin{itemize}
\itemi 
If $f_1:x\mapsto |x|:\R \to{\mathbb R}$ is the absolute value function
and $a\subset \R$ is any compact interval with $0\in a^\circ$, then
$\I f_1\in\delta(a,[-1,1])$. 
\itemii If $f_2:x\mapsto x^2\sin\frac{1}{x}:\R \to{\mathbb R}$ (with $f(0)=0$), then
$\I f_2\in\delta([-1,1],[-3,3])$.
\itemiii  If $f_3:x\mapsto x\sin\frac{1}{x}:\R \to{\mathbb R}$ (with
$f(0)=0$), then, for any compact interval $a$ with $0\in a^\circ$, we have
$\I f_2\in\delta(a,b)$ iff $b=\bot$.
\itemiv If $g\in D^0[0,1]$ is the function given by
Equation~\ref{maxnonclassic}, then for any compact interval
$a\subseteq [0,1]$ with $1/2\in a^\circ$, we have
$g\in\delta(a,b)$ iff $b=\bot$.
\end{itemize}
\end{example}
 

The following proposition justifies our definition of interval
derivative.
\begin{proposition}\label{classicC1}
For $f\in C^1[0,1]$, the following conditions are equivalent.
\begin{itemize}
\item[(i)] ${\bf I}f\in\delta(a,b)$.
\item[(ii)] $\forall z\in a^\circ.\;\underline{b}\leq f'(z)\leq
\overline{b}$.
\item[(iii)] $a\searrow b\sle {\bf I}f'$.
\end{itemize}
\end{proposition}
\begin{proof}

\noindent (i) $\iff$ (ii). This follows from Proposition~\ref{geometric} and the mean value theorem.



\noindent (iii) $\Ra$ (ii). Since $a\ll \{z\}$ for all $z\in a^\circ$, it 
follows from $\step{a}{b}\sle\I f'$ that $b\sle \I f'\{z\}$ for
$a\ll\{z\}$. 

\noindent (ii) $\Ra$ (iii). From (ii), we get $b\sle \I f'(x)$ for $a\ll
x$. Hence $\step{a}{b}\sle \I f'$.\qed

\end{proof}
For each rational $a$ and rational $b$, the tie $\delta(a,b)$ is a family of
functions in $D^0$ with a finitary differential property as specified in Definition~\ref{deftie}; similarly $\mbox{Im}(\Gamma^0)\cap\delta(a,b)$ gives a family of functions in
$C^0$ with a finitary differential property.
Note that \begin{itemize}
\item[(i)] $f\sle g\;\Ra\; (f\in\delta(a,b)\;\Ra\; g\in\delta(a,b))$,
i.e.\ $\delta(a,b)$ is an upper subset of $\I[0,1]\ra\IR$.

\item[(ii)] If $f=g+\{c\}$ for some $c\in\R$, then
$f\in\delta(a,b)\iff g\in\delta(a,b)$.
\end{itemize}
We will see at the end of this section that $\delta(a,b)$ is defined
as the set of primitive maps of $a\searrow b$. However, in order to
define the set of the primitive maps of a Scott continuous function in
general, we first need to study and generalize the notion of single-step ties. 

\subsection{Ties and their properties}
We will now study the single-step ties and their
generalizations. First we note that single-step ties share some common
properties with single-step functions. 
\begin{proposition}\label{singletie}
We have $\delta(a,b)\supseteq \delta(c,d)$ iff $c\sle a$ and
$b\sle d$.
\end{proposition}
\begin{proof}
The ``if'' part follows immediately from the definition of
$\delta(a,b)$. To show the ``only if'' part, assume $\delta(a,b)\supseteq
\delta(c,d)$ holds but not $c\sle a$. Let $g:[0,1]\ra\R$ be the
linear partial function defined by 
\[g(x)=\left\{\begin{array}{cl}
\underline{d}x&x\in c^\circ\\
(\underline{b}-1)x&x\in (a\setminus c)^\circ\\
\bot&\mbox{otherwise}
\end{array}\right.\]
Then $\I g\in\delta(c,d)$ but $\I g\notin\delta(a,b)$. On the other hand 
if $b\sle d$ does not hold, consider the function $f:c^\circ \ra\R$
with $f(x)=tx$ for $t\in d\setminus b$. Then, $\I
f\in\delta(c,d)\setminus\delta(a,b)$.~\qed
\end{proof}

%


\begin{corollary}\label{singletiecor}
We have $\delta(a,b)=\delta(c,d)\iff a=c\;\&\; b=d$.
Furthermore $ \delta(a,b)\supseteq \delta(c,d)$ iff $\step{a}{b}\sle
\step{c}{d}$.~\qed
\end{corollary}

In analogy with step functions we now have the following definition.
\begin{definition}\label{genstep}
A {\em step tie} of $D^0$ is any non-empty finite intersection $\bigcap_{1\leq
    i\leq n}\delta(a_i,b_i)\subset D^0$. A {\em tie} of $D^0$ is any
  non-empty intersection  $\Delta=\bigcap_{i\in I}\delta(a_i,b_i)\subset
  D^0$. The {\em domain} of $\Delta$  is
  $\mbox{dom}(\Delta)=\bigcup_{i\in I}\{a_i^\circ\,|\,b_i\neq
  \bot\}$. 
\end{definition}
A step tie with rational intervals gives us a family of functions with
a {\em finite} set of given differential properties, and a tie gives a
family of functions with a set of given differential
properties. Similar to Proposition~\ref{geometric}, we have the
following result. Recall that a function $f:O\to \R$ defined on the
open set $O\subseteq \R$ is {\em locally Lipschitz} if it is Lipschitz
in a neighbourhood of any point in $O$.
\begin{proposition}If $\Delta\subset D^0$ is a tie and $f\in \Delta$,
  then $f(\{x\})$ is maximal for $x\in \mbox{dom}(\Delta)$ and the induced
  real valued function on $ \mbox{dom}(\Delta)$ is locally Lipschitz. In
  particular, if ${\bf I}f\in \Delta$ then $f$ is locally Lipschitz in
  $\mbox{dom}(\Delta)$.
\end{proposition}
\begin{proof}
Let $x\in \mbox{dom}(\Delta)$. Then there exists a step tie $\delta(a,b)$
with $x\in a^\circ$ and $\Delta\subseteq \delta(a,b)$ and the result
follows from Proposition~\ref{geometric}~\qed. 
\end{proof}
We now aim to establish a necessary and sufficient condition for a family of
step ties $(\delta(a_i,b_i))_{i\in I}$ to be consistent. Let
$g=\bigsqcup_{i\in I}\step{a_i}{b_i}$ and put
$g(\{x\})=[g^-(x),g^+(x)]$. Assume $k:\mbox{dom}(g)\ra\R$ is any
Lebesgue integrable function with $g^-\leq k\leq g^+$ and $\mu$ the
Lebesgue measure on $[0,1]$. Let $(O_t)_{t\in C}$ be the set of
connected components of $\mbox{dom}(g)$ and fix $c_t\in O_t$ for each $t\in
C$. Define
\[\begin{array}{cccc}
f:&[0,1]&\ra&\R_\bot\\
&x&\mapsto&\left\{\begin{array}{ll}\int_{c_t}^xk\,d\mu&x\in O_t\\
\bot&x\notin\mbox{dom}(g)\\\end{array}\right.\\\end{array}\]
\begin{lemma}\label{integstep}
With $f$ as defined above, we have: $\I f \in\bigcap_{i\in I}\delta(a_i,b_i)$.
\end{lemma}
\begin{proof}
We show
that $\I f \in\delta(a_i,b_i)$ for each $i\in I$. Let
$x,y\in a_i^\circ$ with $x>y$. For any $z\in a_i^\circ$, we have $b_i\sle
g\{z\}$. Hence \begin{equation}\label{derivinterval1}\underline{b_i}\leq g^-(z)\leq
k(z)\leq g^+(z)\leq \overline{b_i},\end{equation} which implies that
$[x,y]\subseteq\mbox{dom}(g)$, i.e.\ $x$ and $y$ belong to the same
component $O_t$, say, of $\mbox{dom}(g)$. This gives: $f(x)-f(y)=\int^x_{c_t}k\,d\mu- 
\int^y_{c_t}k\,d\mu=\int_y^xk\,d\mu$.
By Equation~\ref{derivinterval1}, we obtain $\underline{b_i}(x-y)\leq
f(x)-f(y)\leq \overline{b_i}(x-y)$, i.e.\ $\I {f}\in\delta(a_i,b_i)$.~\qed
\end{proof}


\begin{proposition}\label{tiestep}
 For any indexing set $I$, $\bigcap_{i\in
I}\delta(a_i,b_i)\neq\emptyset$ iff the family of step functions
$(\step{a_i}{b_i})_{i\in I}$ is consistent.
\end{proposition}
\begin{proof}
The ``Only if'' part. Suppose there exists $f\in\bigcap_{i\in
I}\delta(a_i,b_i)$ but $(\step{a_i}{b_i})_{i\in I}$ is not 
consistent. Then there is a finite subfamily
$(\step{a_i}{b_i})_{i\in J}$, for $J\subseteq I$, which is not
consistent, i.e.\ ${\sf Con}_\ll(a_i)_{i\in J}$ but not
${\sf Con}_\sqsubseteq(b_i)_{i\in J}$. Therefore there exists a
pair, say $\delta({a_1},{b_1})$ and $\delta({a_2},{b_2})$, in this finite
subfamily such that $a_1^\circ \cap a_2^\circ\neq\emptyset$ with
$b_1\cap b_2=\emptyset$. Assume without loss of generality that
$\overline{b_2}<\underline{b_1}$. Take maximal elements
$\{x_1\}$ and $\{x_2\}$ with $x_2<x_1$ and $x_1,x_2\in (a_1\cap
a_2)^\circ$. Then 
$b_1(\{x_1\}-\{x_2\})$ and $b_2(\{x_1\}-\{x_2\})$ are disjoint. 

Since by assumption $f\in\delta({a_1},{b_1})\cap\delta({a_2},{b_2})$,
we have
\[b_1(\{x_1\}-\{x_2\})\sle f(\{x_1\})-f(\{x_2\})\]
\[b_2(\{x_1\}-\{x_2\})\sle f(\{x_1\})-f(\{x_2\})\]
which gives a contradiction, since the two intervals on the left hand side are
disjoint. 

The ``If'' part. By assumption, $g=\bigsqcup_{i\in I}\step{a_i}{b_i}$
exists and, thus, the result follows from Lemma~\ref{integstep} by
taking $k=g^-$, say.~\qed
\end{proof}

\begin{corollary}\label{finiteintersection}
$\bigcap_{i\in
I}\delta(a_i,b_i)\neq\emptyset$ iff for any finite subfamily
$J\subseteq I$ we have $\bigcap_{i\in
J}\delta(a_i,b_i)\neq\emptyset$.
\end{corollary}
\begin{proposition}\label{tiestepgen}
$\delta(a,b)\supseteq\bigcap_{i\in I}\delta(a_i,b_i)$ if
$a\searrow b\sle\bigsqcup_{i\in I}\step{a_i}{b_i}$.
\end{proposition}
\begin{proof}
Let $b\sle\bigsqcup_{a_i\sle
a}b_i$ and assume $f\in\bigcap_{i\in I}\delta(a_i,b_i)$. Let $a\ll
x_1,x_2$. For each $i\in I$ with $a_i\sle a$ we have:
\[b_i(x_1-x_2)\sle f(x_1)-f(x_2).\]
By the Scott continuity of product of two intervals and our assumption, we get:
\[b(x_1-x_2)\sle \bigsqcup_{a_i\sle a}b_i(x_1-x_2)\sle f(x_1)-f(x_2),\]
as required~\qed.
\end{proof}
\begin{corollary}\label{equality}
$\bigcap_{i\in I}\delta(a_i,b_i)\supseteq\bigcap_{i\in
J}\delta(a_i,b_i)$ if $\bigsqcup_{i\in I}\step{a_i}{b_i}\sle
\bigsqcup_{i\in J}\step{a_i}{b_i}$.
\end{corollary}Let $(T^1[0,1], \supseteq)$ be the poset of ties of $D^0$ ordered by
reverse inclusion.
\begin{proposition}\label{L1=dcpo}
$(T^1[0,1],\supseteq)$ is a dcpo.
\end{proposition}
\begin{proof}
Suppose $(\Delta_j)_{j\in J}$ is a directed set with respect to the partial order $\supseteq$, i.e.\ $\Delta_{j_1}\cap
\Delta_{j_2}\neq \emptyset$ for $j_1,j_2\in J$. Let $\Delta_j=\bigcap_{i\in
I_j}\delta(a_i,b_i)$, where we assume $I_{j_1}\cap I_{j_2}=\emptyset$ for $j_1\neq j_2$. Consider the collection
$(\delta(a_i,b_i))_{i\in\bigcup_{j\in J}I_j}$. By
Corollary~\ref{finiteintersection}, it suffices to show that any
finite subfamily of this collection has non-empty
intersection. Suppose $i_t\in\bigcup_{j\in J}I_j$ for $1\leq t\leq
n$. Then $\delta(a_{i_t},b_{i_t})\in \Delta_{j_t}$ for some $j_t\in I$ ($1\leq t\leq
n$). By assumption $\bigcap_{1\leq t\leq
n}\Delta_{j_t}\neq\emptyset$. Hence, $\bigcap_{1\leq t\leq
n}\delta(a_{i_t},b_{i_t})\supseteq\bigcap_{1\leq t\leq
n}\Delta_{j_t}\neq\emptyset$.~\qed
\end{proof}
We are finally in a position to define the set of primitive maps of a
Scott continuous function; in fact now we can do more and define the
integral operator which gives the set of primitive maps of any Scott
continuous function as follows.
\begin{definition}
The {\em integral operator} $\int:D^0\to T^1$ is defined by
$\int(\bigsqcup_{i\in I}\step{a_i}{b_i})=\bigcap_{i\in
  I}\delta(a_i,b_i)$. We usually write $\int (f)$ as $\int f$ and
call it the set of primitive maps of $f$.
\end{definition}
\begin{proposition}\label{intcont}
The integral operator is well-defined, onto and continuous.
\end{proposition}
\begin{proof}
By Corollary~\ref{equality}, $\int$ is well-defined and monotone. By Proposition~\ref{tiestep}, it is onto. Let
$(g_i)_{i\in I}$ be a directed set in $D^0$ with $g_i=\bigsqcup_{j\in
  I_i}\step{a_j}{b_j}$. Then, $\int\bigsqcup_{i\in I}g_i=\int\bigsqcup_{i\in I}\bigsqcup_{j\in
  I_i}\step{a_j}{b_j}=\bigcap_{i\in I}\bigcap_{j\in
  I_i}\step{a_j}{b_j}= \bigcap_{i\in I}\int g_i=\bigsqcup_{i\in
  I}\int g_i$.~\qed
\end{proof}

\section{Derivative of a Scott continuous function}
Given a Scott continuous function $f:\I [0,1]\to \IR$, the relation
$f\in \delta(a,b)$, for some intervals $a$ and $b$, provides,
as we have seen, finitary information about the local differential
properties of $f$. By collecting all such local information, we
obtain the complete differential properties of $f$, namely\ its derivative. For clarity, we will denote by $\frac{df}{dx}$ the new notion of the domain-theoretic derivative of a Scott continuous function $f$ and write as $f'$ the classical derivative of a classical continuous function $f$.

\begin{definition}
The {\em derivative} of a continuous function $f:\I [0,1]\ra \IR$ is
the map \[\frac{df}{dx}=\bigsqcup_{f\in\delta(a,b)}\step{a}{b}:\I
[0,1]\ra\I \R.\]
\end{definition}

\begin{theorem}\label{derivative1}
\begin{itemize}
\itemi $\frac{df}{dx}$ is well-defined and Scott continuous.
\itemii If $f\in C^1[0,1]$ then $\frac{d\I f}{dx}=\I f'$.
\itemiii $f\in\delta(a,b)$ iff $\step{a}{b}\sle \frac{df}{dx}$.\end{itemize}
\end{theorem}
\begin{proof}
(i) Let the indexing set $I$ be defined by $i\in I\iff f\in
\delta(a_i,b_i)$. Then $\bigcap_{i\in
I}\delta(a_i,b_i)\neq\emptyset$. Hence, $(\step{a_i}{b_i})_{i\in I}$
is consistent. Therefore, $\frac{df}{dx}=\bigsqcup_{i\in
I}\step{a_i}{b_i}$ exists and is Scott continuous.

(ii) By Proposition~\ref{classicC1}, we have: $\I f\in\delta(a,b)\iff\step{a}{b}\sle\I
f'$. Hence, $\I f'=\bigsqcup_{\I f\in\delta(a,b)}\step{a}{b}$.

(iii) Obvious.~\qed

\end{proof}
Note the significance of Theorem~\ref{derivative1}. In classical
  mathematics, the derivative of a continuous function $f:[0,1]\to \R$
  at a point $x\in [0,1]$ may not exist and in fact $f$ may be
  nowhere differentiable; even if the derivative $f'(x)$ exists at all points
  $x\in[0,1]$, the map $x\mapsto f'(x):[0,1]\to\R$ may not be
  continuous. Such ``irregularities'' do not happen in the
  domain-theoretic world. In fact, {\em
    any}
  Scott continuous function $f:\I [0,1]\ra \IR$ is differentiable and
  its derivative $\frac{df}{dx}:\I
[0,1]\ra\I \R$ is a Scott continuous map, i.e.\ has the same type as
$f$ itself.


\begin{proposition}\label{notmaximal=bot}\begin{itemize}\itemi 
Let $f:\I [0,1]\ra \IR$ be Scott continuous. Suppose for some
$z\in[0,1]$, $f(\{z\})$ is not maximal, then $\frac{df}{dx}(\{z\})=\bot$.
\itemii Suppose $f\in D^0$. If
$\frac{df}{dx}(\{y\})=\{c\}$ is maximal, then $f$ sends maximal
elements to maximal elements in a neighbourhood $U$ of $y$ and the
derivative of the induced 
restriction $f:U\to \R$ exists at $y$ and $f'(y)=c$.
\itemiii If $g:[0,1]\to \R$ is a bounded, integrable function, and
  $f:[0,1]\to \R$ is a (classical) indefinite integral of $g$, i.e.\ $f(y)=\int_0^yg\,d\mu$,
  then $\limUnderline g(y)\leq
  \limUnderline\frac{f(x)-f(y)}{x-y}$,
  $\limOverline\frac{f(x)-f(y)}{x-y}\leq \limOverline g(y)$ and 
$\frac{d{\bf I}f}{dx}(\{y\})\sge
  [\limUnderline g(y),\limOverline g(y)]$. 
\end{itemize}
\end{proposition}
\begin{proof}
(i) By Proposition~\ref{geometric}, for $b\neq \bot$, we have $f\in\delta({a},{b})\Ra z\notin a^\circ$. Hence, 
\[\frac{df}{dx}(\{z\})=\bigsqcup\{{b}|f\in\delta(a,b)\,\&
\,z\in a^\circ\}=\bot.\]
(ii) We have $\{c\}=\frac{df}{dx}(\{y\})=\bigsqcup\{b\,|\,y\in
a^\circ\;\&\; f\in\delta(a,b)\}$. For any neighbourhood $O$ of $c$ in
$\R$, there exists $b$ with $c\in b^\circ$ and $b\subset O$ such that there exists
$a\in \I[0,1]$ with $y\in a$ and $f\in\delta(a,b)$. By
Proposition~\ref{geometric}(i), this implies firstly that $f(\{x\})$ is maximal
for each $x\in a^\circ$ and secondly that the
restriction $f:a^\circ\to \R$ satisfies
$\frac{f(x)-f(y)}{x-y}\in b\subseteq O$ for all $x\in a^\circ$ with
$x\neq y$, i.e.\ $\lim_{x\to y}\frac{f(x)-f(y)}{x-y}=c$.

(iii) Let $\epsilon>0$ be given. There exists a neighbourhood 
$(\underline{a},\overline{a})$ of $y$ such that for all $x\in a^\circ$:\[
-\epsilon +\limUnderline g(y)\leq g(x)\leq
\epsilon+\limOverline g(y).\]
Integration on $[x,z]$ yields:
\[(-\epsilon +\limUnderline g(y))(z-x)\leq  f(z)-f(x)\leq
(\epsilon+\limOverline g(y))(z-x).\]Thus ${\bf I}f\in
\delta(a,[-\epsilon
+\limUnderline g(y),\epsilon+\limOverline g(y)])$ and the first
two inequalities follow. Since $\epsilon>0$ is arbitrary,
we also get \[\frac{d{\bf I}f}{dx}(\{y\})=\bigsqcup \{b\,|\,y\in
  a^\circ,{\bf I}f\in\delta(a,b)\}\sge [\limUnderline g(y),\limOverline g(y)].\qquad\mbox{\qed}\]


\end{proof}
\begin{example}
The derivatives of the canonical extensions of $f_1$,
$f_2$, $f_3$ and $g$ of Example~\ref{examples} are given
by 
\[\begin{array}{lll}\frac{d\I f_1}{dx}(y)=\left\{\begin{array}{ll}\{-1\}& \mbox{if } {\overline{y}}<0\\[1ex] 
\{1\}&\mbox{if } {\underline{y}}>0 \\[1ex] 
[-1,1]&\mbox{if } 0\in y\\\end{array}
\right.&&

\frac{d\I f_2}{dx}(y)=\left\{\begin{array}{ll}\I f'(y)& \mbox{if }
    0\notin y\\[1ex] 
[-1,1]&\mbox{if } 0\in y\\\end{array}
\right.\end{array}\]
\[\begin{array}{lll}\frac{d\I f_3}{dx}(y)=\left\{\begin{array}{ll}\I f'(y)& \mbox{if }
    0\notin y\\[1ex] 
\bot&\mbox{if } 0\in y\\\end{array}
\right.&& \frac{d\I g}{dx}(y)=\left\{\begin{array}{ll}\{0\}& \mbox{if }
    1/2\notin y\\[1ex] 
\bot&\mbox{if } 1/2\in y\\\end{array}
\right.\end{array}                         \]
\end{example}
Note that the classical derivative of $f_2$ exists at $0$ but the
derivative is not continuous at $0$.

The operator 
\[\begin{array}{cccc}
\frac{d}{dx}:&D^0[0,1]&\ra&D^0[0,1]\\
&f&\mapsto &\frac{df}{dx}\\
\end{array}\]
is easily seen to be monotone but not continuous. In fact the
derivative of any step function $\bigsqcup_{i\in I}\step{a_i}{b_i}$
for intervals $b_i$ ($i\in I)$ with 
non-zero length is the bottom function. Since, for example, the
function $\I f$, where $f=0$ is a constant function, can be constructed as the lub of an increasing
chain of such step functions, it follows that $\frac{d}{dx}$ is not continuous. In Section~\ref{C1-functions}, we will
define what we will call the continuous derivative operator. Finally, we note that the
definition of the derivative together with Theorem~\ref{derivative1} and
Proposition~\ref{notmaximal=bot} easily extend to $D^0_{{\sf r}}$.

 
We finally obtain the generalization of Theorem~\ref{derivative1}(iii) to ties, which established a duality between primitive maps and differentiation.
\begin{corollary}\label{difftie}
$f\in\int g$ iff $g\sle \frac{df}{dx}$.
\end{corollary}
\begin{proof}Let $g=\bigsqcup_{i\in I}\step{a_i}{b_i}$, then by Theorem~\ref{derivative1}(iii):
\[f\in \int g\iff f\in\bigcap_{i\in I}\delta(a_i,b_i)\iff \forall
i\in I.\;\step{a_i}{b_i}\sle \frac{df}{dx}\iff \bigsqcup_{i\in
  I}\step{a_i}{b_i}\sle \frac{df}{dx}.\qquad\mbox{\qed}\]
\end{proof}

\section{Ties of $D^0_{{\sf r}}$ and the fundamental theorem of calculus}

Having studied ties of $D^0$, we now consider
the similar notion for $D^0_{{\sf r}}$.  The information ordering for the ties of
$D^0_{{\sf r}}$ has a simple characterization which we will determine here.

The {\em single-step tie}
$\delta_{{\sf r}}(a,b)\subset D^0_{{\sf r}}$ is simply the restriction of
$\delta(a,b)$ to the subdomain $D^0_{{\sf r}}$, in other words
$\delta_{{\sf r}}(a,b)={\cal I}(\delta(a,b)\cap {\cal E}(D^0_{{\sf r}}))$; more generally, a {\em tie} of
$D^0_{{\sf r}}$ is given by
$\bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)={\cal I}((\bigcap_{i\in
  I}\delta(a_i,b_i))\cap {\cal E}(D^0_{{\sf r}}))$ for any tie $\bigcap_{i\in
  I}\delta(a_i,b_i)$ of $D^0$. Notice that, by
Proposition~\ref{geometric}(i), any step tie of $D^0_{{\sf r}}$ is essentially a
collection of classical Lipschitz functions. In particular, for $f\in
D^0_{{\sf r}}$ and $b\neq\bot$, we have: 
$f\in\delta_{{\sf r}}(a,b)$ iff the image of $a^\circ$ under $f$ is a subset of maximal
elements of $\IR$ and the induced map $f:a^\circ \to \R$
satisfies $\underline{b}(x-y)\leq f(x)-f(y)\leq \overline{b}(x-y)$ for all
$x\geq y$ with $x,y\in a^\circ$. Clearly $\delta_{{\sf r}}(a,b)\supseteq
\delta_{{\sf r}}(c,d)$ iff $a\subseteq c$ and $d\subseteq b$. 
\begin{proposition}\label{teid0-d}\begin{itemize}
\itemi 
$f\in \bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)\iff {\cal E}(f)\in
\bigcap_{i\in I}\delta(a_i,b_i)$.
\itemii ${\cal I}(f)\in \bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)$ if $f\in
\bigcap_{i\in I}\delta(a_i,b_i)$.
\end{itemize}
\end{proposition}
\begin{proof}
(i) We have $f\in \bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)$ iff $f={\cal I}(g)$ for some
$g\in \bigcap_{i\in I}\delta(a_i,b_i)\cap {\cal E}(D^0_{{\sf r}})$ iff
$f={\cal I}(g)$ and $g\in \bigcap_{i\in I}\delta(a_i,b_i)\cap {\cal
  E}(D^0_{{\sf r}})$ with $g={\cal E}(h)$ for some $h\in D^0_{{\sf r}}$. Since
${\cal I}\circ {\cal E}=1_{D^0_{{\sf r}}}$ the latter condition gives $h=f$ and the
result follows.

(ii) If $f\in \bigcap_{i\in I}\delta(a_i,b_i)$ then ${\cal E}\circ
{\cal I}(f)\in  \bigcap_{i\in I}\delta(a_i,b_i)$ since ties are upper
sets. The result follows by (i).~\qed
\end{proof}


\begin{proposition}\label{tiestep0}
 For any indexing set $I$, $\bigcap_{i\in
I}\delta_{{\sf r}}(a_i,b_i)\neq\emptyset$ iff the family of step functions
$({a_i}\searrow_{{\sf r}}{b_i})_{i\in I}$ is consistent.
\end{proposition}
\begin{proof}
This follows immediately by Propositions~\ref{tiestep} and~\ref
{teid0-d}(i) together with Equation~\ref{consd0-d}.~\qed
\end{proof}



We also have the following counterparts of Proposition~\ref{tiestep},
Corollary~\ref{equality} and Proposition~\ref{L1=dcpo} for ties in $D^0_{{\sf r}}$:
\begin{proposition}\label{tiestepgen0}
$\delta_{{\sf r}}(a,b)\supseteq\bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)$ if
${a}\searrow_{{\sf r}}{b}\sle\bigsqcup_{i\in I}{a_i}\searrow_{{\sf r}}{b_i}$.
\end{proposition}
\begin{proof}
This can be proved by the same method used to prove
Proposition~\ref{tiestep}.~\qed
\end{proof}
\begin{corollary}\label{equality0}
$\bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)\supseteq\bigcap_{i\in
J}\delta_{{\sf r}}(a_i,b_i)$ if $\bigsqcup_{i\in I}{a_i}\searrow_{{\sf r}}{b_i}\sle
\bigsqcup_{i\in J}{a_i}\searrow_{{\sf r}}{b_i}$.\qed
\end{corollary}Let $(T^1_{{\sf r}}[0,1], \supseteq)$ be the poset of ties of $D^0_{{\sf r}}$ ordered by
reverse inclusion.
\begin{proposition}\label{L10=dcpo}
$(T^1_{{\sf r}}[0,1],\supseteq)$ is a dcpo.~\qed
\end{proposition}
Furthermore, the integral map $\int_{{\sf r}}:D^0_{{\sf r}}\to T^1_{{\sf r}}$ defined by
$\int_{{\sf r}}\bigsqcup_{i\in I}{a_i}\searrow_{{\sf r}}{b_i}=\bigcap_{i\in
  I}\delta_{{\sf r}}(a_i,b_i)$ is well-defined, onto and continuous; it satisfies $\int_{{\sf r}}=
  {\cal I}\circ \int\circ {\cal E}$. For convenience we write $\int$
  for $\int_{{\sf r}}$ when no ambiguity can arise.

We have the following counterpart of Corollary~\ref{difftie},
\begin{corollary}\label{difftie1}
For $f,g\in D^0_{{\sf r}}$, we have: $f\in\int g$ iff $g\sle \frac{df}{dx}$.~\qed
\end{corollary} 
\begin{corollary}\label{difftie2}
If $f,g\in D^0_{{\sf r}}$ are extensions of classical $C^0$ function, then we have: $f\in\int g$ iff $g=\frac{df}{dx}$.~\qed
\end{corollary} 
It follows from Corollary~\ref{difftie2}, that the duality of differentiation and primitive functions in Corollary~\ref{difftie1} can be considered as an extension of the classical fundamental theorem of calculus to functions of type $D^0_{{\sf r}}$.


  The information order in $T^1_{{\sf r}}$ has an elementary
  characterization, which we will now determine. Define the function
\[r:D^0_{{\sf r}}\to  ([0,1]^2\to \IR)\]
by:
\[r^-(g):(x,y)\mapsto
\left\{\begin{array}{cll}\int^y_xg^-\,d\mu&&\mbox{$x,y$ in the same component of $\mbox{dom}(g)$}\\
\bot&&\mbox{otherwise,}\end{array}\right.\]
and,

\[r^+(g):(x,y)\mapsto \left\{\begin{array}{cll}\int^y_xg^+\,d\mu&&\mbox{$x,y$ in the same component of $\mbox{dom}(g)$}\\
\bot&&\mbox{otherwise.}\end{array}\right.\]
By the monotone convergence theorem $r$ is a Scott continuous
function. We also define the Scott continuous map $[s,t]:D^0_{{\sf r}}\to ([0,1]^2\to \IR)$ with  
\[s(g):(x,y)\mapsto \left\{\begin{array}{cll}r^-(g)(x,y)&& \mbox{if }x\leq y\mbox{ with $x,y$ in the same component of $\mbox{dom}(g)$}\\-r^+(g)(y,x)&&\mbox{if }y\leq x\mbox{ with $x,y$ in the same component of $\mbox{dom}(g)$}\\
\bot&&\mbox{otherwise.}\end{array}\right.\]

\[t(g):(x,y)\mapsto \left\{\begin{array}{cll}r^+(g)(x,y)&&\mbox{if }x\leq y\mbox{ with $x,y$ in the same component of $\mbox{dom}(g)$}\\-r^-(g)(y,x)&&\mbox{if }y\leq x\mbox{ with $x,y$ in the same component of $\mbox{dom}(g)$}\\
\bot&&\mbox{otherwise.}\end{array}\right.\]




\begin{proposition}\label{charac}
\begin{itemize}
\itemi Let $\Delta\in T^1_{{\sf r}}$ and consider any $g\in D^0_{{\sf r}}$ with
$\Delta=\int g$. Then $\lambda y.\,s(g)(x,y)$ and $\lambda
y.\,t(g)(x,y)$ are in $\Delta$, both vanishing at $x$. Moreover, we have:
\[ h\in \Delta\iff r^-(g)(x,y)\leq h(y)-h(x)\leq r^+(g)(x,y),\]
for all $x,y$ belonging to the same component of $\mbox{dom}(g)$ with $x\leq y$.
\itemii The functions $\lambda y.\,s(g)(x,y)$ and $\lambda y.\,t(g)(x,y)$ are respectively the least and greatest functions $h\in\Delta$ with $h(x)=0$.
\itemiii The following are equivalent:
\begin{itemize}
\item $\int g_1\supseteq \int g_2$,
\item $g_1^-\leq g_2^-$ a.e.~and $g_2^+\leq g_1^+$ a.e.,
\item for all $x,y$ with
$x\leq y$ we have: $r^-(g_1)(x,y)\leq r^-(g_2)(x,y)$
and $r^+(g_2)(x,y)\leq r^+(g_1)(x,y)$, 
\item  $s(g_1)\leq
s(g_2)$ and $t(g_1)\geq t(g_2)$.
\end{itemize} 
\itemiv $\int g_1=\int g_2$ iff $g_1^-=g_2^-$ a.e.\ and
$g_1^+=g_2^+$ a.e. \itemv $\delta_{{\sf r}}(a,b)\ll \bigcap_{i\in
  I}\delta_{{\sf r}}(a_i,b_i)$ if $a\searrow_{{\sf r}} b\ll \bigsqcup_{i\in
  I}a_i\searrow_{{\sf r}} b_i$. \end{itemize}\end{proposition}
\begin{proof}
  (i) Let $g=\bigsqcup_{i\in I}{a_i}\searrow{b_i}$ with $\int
  g=\Delta$. Take $x,y$ in the same component of $\mbox{dom}(g)$ with
  $x\leq y$. Note that if $h\in \Delta$, then, being locally Lipschitz (and hence absolutely continuous)
  in $\mbox{dom}(\Delta)=\mbox{dom}(g)$, $h$ is differentiable a.e.\ 
  (with respect to the Lebesgue measure) in $\mbox{dom}(g)$ and $h$ is
  equal to the integral of its derivative, i.e.\ 
  $h(y)-h(x)=\int^y_xh'\,d\mu$~\cite[Sections 17.17 and 18.17]{HS75}. In the following
  whenever we write $h'(x)$ in a relation, it is meant that the
  relation holds whenever $h'(x)$ exists, which is a.e. We have,
  $h\in\bigcap_{i\in I}\delta_{{\sf r}}(a_i,b_i)$ iff $\forall i\in I,\,x\in
  a_i^\circ.\;\underline{b_i}\leq h'(x)\leq \overline{b_i}$ iff
  $\sup_{x\in a_i^\circ}\underline{b_i}\leq h'(x)\leq \inf_{x\in
    a_i^\circ}\overline{b_i}$ iff $h'(x)\in\bigsqcup_{x\in a_i^\circ}b_i$
  iff $\forall x\in \mbox{dom}(g).\;g^-(x)\leq h'(x)\leq g^+(x)$ iff
  $\int_x^yg^-\,d\mu\leq h(y)-h(x)\leq \int_x^yg^+\,d\mu$, for all
  $x,y$ belonging to the same component of $\mbox{dom}(g)$ with $x\leq
  y$.

(ii) By part (i) any $h\in \Delta$ with $h(x)=0$ satisfies:
$s(g)(x,y)\leq h(y)\leq t(g)(x,y)$ for all $x,y$ in the same component
of $\mbox{dom}(g)$. On the other hand, by Lemma~\ref{integstep}, the maps $\lambda y.\,s(g)(x,y)$ and
$\lambda y.\,t(g)(x,y)$ belong to $\Delta$ for any $x\in
\mbox{dom}(g)$. 

(iii) This follows from parts (i) and (ii).

(iv) Immediate consequence of part (iii).

(v) Assume $a\searrow_{{\sf r}} b\ll \bigsqcup_{i\in
  I}a_i\searrow_{{\sf r}} b_i$, i.e.\ $\bigsqcup_{a_i\ll a}b_i\gg b$. Let
$(\Delta_i)_{i\in J}$ be a directed set of ties with $\bigcap_{i\in
  I}\delta_{{\sf r}}(a_i,b_i)\supseteq \bigcap_{i\in J} \Delta_i$. Take $g_i\in
D^0_{{\sf r}}$ with $\Delta_i=\int g_i$ for all $i\in J$ and let
$g=\bigsqcup_{i\in I}a_i\searrow_{{\sf r}}b_i$. From $a\searrow_{{\sf
    r}}b\ll g$ we
get $b\ll g(a)$. Put $c=g(a)$, so that $\underline{b}<\underline{c}$
and $\overline{c}<\overline{b}$. Then, for all $x,y,z \in
a$ with $y\geq z\geq x$ we have: $\underline{c}\leq g^-(z)$ and
$g^+(z)\leq \overline{c}$. Integrating from $x$ to $y$, by part (i) we get:  
\[    \underline{b}   (y-x)        <\underline{c}(y-x)\leq s(g)(x,y)\leq
\sup_{i\in J}s(g_i)(x,y)\]
\[\inf_{i\in J}t(g_i)(x,y)\leq t(g)(x,y)\leq
\overline{c}(y-x)<\overline{b}(y-x).\]
Thus, for the directed set of continuous maps $(\lambda x.\,\lambda
y.s(g_i)(x,y)-\underline{b}(y-x))_{i\in J}$, we have:
\[\sup_{i\in J}(\lambda x.\,\lambda
y.s(g_i)(x,y)-\underline{b}(y-x))\geq
s(g(x,y))-\underline{b}(y-x))>0.\]
It follows that the directed family of continuous functions 
\[(\lambda x.\,\lambda
y.\min(s(g_i(x,y))-\underline{b}(y-x),s(g)-\underline{b}(y-x)))_{i\in
  J}\]
converges monotonically, thus uniformly, to the
function $ \lambda x.\,\lambda
y.s(g)-\underline{b}(y-x)>0$  on the compact set
$\{(x,y)\in [0,1]^2\,|\,x\geq y\}$. Therefore, there exists $i\in J$
such that $\lambda x.\,\lambda
y.\min(s(g_i(x,y))-\underline{b}(y-x),s(g)-\underline{b}(y-x)))>0$ and
thus $\lambda x.\,\lambda
y.s(g_i(x,y))-\underline{b}(y-x)>0$. Similarly there exists $i\in J$
such that $\lambda x.\,\lambda
y.t(g_i(x,y))-\underline{b}(y-x)<0$. Hence there exists $i\in J$ with 
$\lambda x.\,\lambda
y.s(g_i(x,y))-\underline{b}(y-x)>0$ and $\lambda x.\,\lambda
y.t(g_i(x,y))-\underline{b}(y-x)<0$.
It follows, by
part (i) again, that
$\delta(a,b)\supseteq \Delta_i$ as required.\qed\end{proof}

The characterization of the information ordering for $T^1$ is far more
involved than Proposition~\ref{charac} for $T^1_{{\sf r}}$; we will present
it in a future paper.



\section{The Domain of $C^1$ functions}\label{C1-functions}

We now define the domain of $C^1$ functions. Consider the relation
${\sf Cons}\subset D^0\times D^0$ defined by $(f,g)\in {\sf Cons}$ if
$\ua\hspace{-.05cm} f\cap \int g\neq \emptyset$. We will show that
this relation is Scott closed and decidable on basis elements. 
\begin{proposition}\label{inf-family} Let $g\in D^0$ and $(f_i)_{i\in I}$ be a
  non-empty family of functions $f_i:\mbox{dom} (g)\to
\R$ with $\I f_i\in\int g$ for all $i\in I$. If $h_1=\inf_{i\in
  I}f_i$ is real-valued then $\I h_1\in \int g$. Similarly, if
$h_2=\sup_{i\in I}f_i$ is real-valued, then $\I h_2\in \int g$.
\end{proposition}
\begin{proof}
Suppose $h_1$ is real-valued. Let $\step{a}{b}\sle g$. From Proposition~\ref{geometric}, we
have $\underline{b}(u-v)\leq f_i(u)-f_i(v)\leq \overline{b}(u-v)$ for
all $u,v\in a^\circ$ with $u>v$ and all $i\in I$. Taking infimum, we get $\underline{b}(u-v)\leq h_1(u)-h_1(v)\leq
\overline{b}(u-v)$ and, by Proposition~\ref{geometric}, $\I h_1\in
\delta(a,b)$, as required. The case of $h_2$ is similar.~\qed
\end{proof}

Let
$L[0,1]$ be the set of partial maps of
$[0,1]$ into the extended real line. Consider
the two dcpo's  $(L[0,1],\leq)$ and $(L[0,1],\geq)$. Define the maps
$s:D^0\times D^0\to (L,\leq)$ and $t:D^0\times D^0\to (L,\geq)$ by \[s:(f,g)\mapsto
\inf\{h:\mbox{dom}(g)\to \R\,|\, \I h\in \int g \;\&\; h\geq
f^-\}\] \[t:(f,g)\mapsto
\sup\{h:\mbox{dom}(g)\to \R\,|\, \I h\in \int g \;\&\; h\leq
f^+\}.\] We use the convention that the infimum and the
supremum of the empty set are $\infty$ and $-\infty$, respectively. Note
that given a connected component $A$ of $\mbox{dom}(g)$ with $A\cap \mbox{dom}(f)=\emptyset$, then $s(f,g)(x)=-\infty$ and
$t(s,f)(x)=\infty$ for $x\in A$.
\begin{proposition}~\label{coniff}
The following are equivalent:
\begin{itemize}
\itemi $(f,g)\in{\sf Cons}$.
\itemii $s(f,g)\leq t(f,g)$.
\itemiii There exists $h:\mbox{dom}(g)\to \R$ with $\I h\in \int g$
and $f^-\leq h\leq f^+$
on $\mbox{dom}(g)$.\end{itemize}
\end{proposition}
\begin{proof}If $\mbox{dom}(f)\cap \mbox{dom}(g)=\emptyset$, then the
  three statements hold trivially. So assume in the following proof that $\mbox{dom}(f)\cap
  \mbox{dom}(g)\neq\emptyset$.
 
\noindent(ii) $\Ra$ (i). Suppose $s(f,g)\leq t(f,g)$. Then, $f\sqcup \I s(f,g)\in
\ua\hspace{-.05cm} f\cap \int g$ and hence
$(f,g)\in{\sf Cons}$. 

\noindent(i) $\Ra$ (ii). Suppose
$(f,g)\in{\sf Cons}$. Assume $h\in \ua\hspace{-.05cm} f\cap \int
g$. Then, the induced map $h:\mbox{dom}(g)\ra \R$ satisfies $\I h\in \int
g$. Hence, $f^-\leq h\leq f^+$ and thus $s(f,g)\leq t(f,g)$.

\noindent(ii) $\Ra$ (iii). Suppose $s(f,g)\leq t(f,g)$. Put $h=s(f,g)$.

\noindent(iii) $\Ra$ (ii). We have $s(f,g)\leq h\leq t(f,g)$.~\qed

\end{proof}

\begin{proposition}\label{stcont}
The maps $s$ and $t$ are Scott continuous.
\end{proposition}
\begin{proof}
Consider the map $s$. If $f_1\sle f_2$ and $g_1\sle g_2$, then we have
$\int g_1\supseteq \int g_2$ and $f_1^-\leq f_2^-$ and it follows
that $s(f_1,g_1)\leq s(f_2,g_2)$. Let $\{(f_i,g_i)\}_{i\in \omega}$ be
an increasing chain and put $f=\bigsqcup_{i\in\omega} f_i$ and $g=\bigsqcup_{i\in\omega}g_i$. To show the continuity of $s$ we need to show that $\mbox{sup}_is(f_i,g_i)\geq
s(f,g)$ on any connected component of $\mbox{dom}(g)=\bigcup_{i\in\omega}\mbox{dom}(g_i)$. Take
any such connected component $A\subseteq \mbox{dom}(g)$. If $A\cap
\mbox{dom}(f) =\emptyset$ then $s(f,g)=-\infty$ on $A$ and the result
follows. Assume that $A\cap
\mbox{dom}(f)\neq\emptyset$, i.e., $\mbox{dom}f_{i_0}\cap
\mbox{dom}g_{i_0}\neq \emptyset$ for some $i_0\in\omega$. If
$s(f_i,g_i)=\infty$ on $A\cap \mbox{dom}(g_i)$ for some $i\geq i_0$,
then $\mbox{sup}_{i\in\omega}s(f_i,g_i)=\infty$ on $A$ and the result follows
again. Otherwise, assume without loss of generality that $-\infty <s(f_i,g_i)<\infty$ on $A\cap
\mbox{dom}(g_i)$ for all $i\in\omega$. 
Then from $\I (s(f_i,g_i))\hspace{-1ex}\restriction_A\in \int g_i$ it follows
that $\forall i\geq j.\;\I (s(f_i,g_i))\hspace{-1ex}\restriction_A\in\int g_j$, and hence, by
Proposition~\ref{inf-family}, $\I (\sup_{i\in
  \omega}(s(f_i,g_i)\hspace{-1ex}\restriction_A))\in \int g_j$. Thus $\I (\sup_{i\in
  \omega}s(f_i,g_i))\hspace{-1ex}\restriction_A\in \bigsqcup_j\int g_j=\int \bigsqcup
g_j$. On the other hand, $s(f_i,g_i)\geq f_i^-$ on $A$ implies
$\sup_{i\in\omega}s(f_i,g_i)\geq f_i^-$ on $A$ and hence $\sup_{i\in\omega}s(f_i,g_i)\geq
f^-$ on $A$. This shows that $s$ is continuous. Similarly
$t$ is continuous.~\qed
\end{proof}
\begin{corollary}
The relation ${\sf Cons}$ is Scott closed.
\end{corollary}
\begin{proof}
Let $(f_i,g_i)_{i\in I}\subset D^0\times D^0$ be a directed family
with $(f_i,g_i)\in {\sf Cons}$ for all $i\in I$. Then, by
Proposition~\ref{coniff}, $s(f_i,g_i)\leq t(f_i,g_i)$ for all $i\in
I$. Hence, $s(f,g)=\sup_{i\in I} s(f_i,g_i)\leq \inf_{i\in I} t(f_i,g_i)=t(f,g)$.~\qed
\end{proof}
\begin{corollary}\label{leastgreatest}
Let $(f,g)\in {\sf Cons}$. Then in each connected component $O$ of
the domain of definition of $g$ which intersects the domain of
definition of $f$, there exist two locally Lipschitz functions $s:O\ra {\mathbb R}$ and  $t:O\ra {\mathbb R}$ such that ${\bf I}s,{\bf I}t\in \ua\hspace{-.05cm} f\cap \int g$ and for each $u\in \ua\hspace{-.05cm} f\cap \int g$, we have $u(\{x\})=\{v(x)\}$ with $s(x)\leq v(x)\leq t(x)$ for all $x\in O$ (see Figure~\ref{twocons}).
\end{corollary}


\begin{figure}[ht]\begin{center}
\includegraphics*[scale=.5]{consistent.eps}
\caption{Two pairs of functions in ${\sf Cons}$}
\label{twocons}\end{center}
\end{figure}


Next we will show that ${\sf Cons}$ is decidable on (rational or
semi-rational polynomial) basis elements. First we note the following
general property.
\begin{proposition}\label{algebpoly}
If $\alpha,\beta:[v,w]\to\R$ are two piecewise semi-rational polynomials,
then the relation $\alpha\leq \beta$ (i.e.\ $\forall x\in[v,w].\;\alpha(x)\leq \beta(x)$) is
decidable.~\qed
\end{proposition} 

\begin{lemma}\label{leastconsistent}Let $f,g\in D^0[0,1]$ be semi-rational
  basis elements with $(f,g)\in {\sf Cons}$. Then the functions $s(f,g)$ and $t(f,g)$ are piecewise semi-rational
  polynomials in each connected component of $\mbox{dom}(g)$
  with non-empty intersection with $\mbox{dom}(f)$. \end{lemma} 
\begin{proof}

Fix a connected component $O=(v,w)$ of $\mbox{dom}(g)$ with $O\cap
\mbox{dom}(f)\neq \emptyset$. Then, for $x\in O$, we have
$s(f,g)(x)=\sup_{y\in O\cap\mbox{dom}(f)}S_{(f,g)}(x,y)$ where $S_{(f,g)}:O\times (O\cap \mbox{dom}(f))\to \R$ with
\[S_{(f,g)}(x,y)=\left\{\begin{array}{ll}f^-(y)+\int^x_yg^-(u)\,du&x\geq y\\[1ex]
f^-(y)-\int_x^yg^+(u)\,du&x<y\end{array}\right.\]
In other words, $s(f,g)$ is the upper envelop of the one parameter family of functions
$x\mapsto S_{(f,g)}(x,y)$. We will now construct $s$ explicitly, which gives a
constructive proof of the lemma.
Consider the
common refinement ${\cal A}=\{c_0,c_1,c_2,\cdots,c_n\}$, with $v=c_0<c_1<c_2<\cdots<c_n=w$, of the two partitions of $O$ by the associated
intervals of $f$ and $g$ as described in Section~\ref{step}. In the
open intervals $(c_{i-1},c_i)$ ($i=1,\cdots,n$), the restrictions
$f^-{\restriction_{(c_{i-1},c_i)}}={p_i}^{-}$ and
$f^+{\restriction_{(c_{i-1},c_i)}}={p_i}^{+}$ are
polynomials. Let
$q^-,q^+:[v,w]\to \R$ be the continuous piecewise polynomial functions
with, say, $q^-(v)=q^+(v)=0$ such that for all $x\in O\setminus {\cal A}$ we
have $(q^-)'(x)=g^-(x)$ and  $(q^+)'(x)=g^+(x)$. Let $q_i^-$ and
$q_i^+$ be, respectively, the restrictions of $q^-$ and $q^+$ to
$[c_{i-1},c_i]$. Then for $y\in (c_{i-1},c_i)$ we have:
$S_{(f,g)}(x,y)=p_i^-(y)+Q_i(x,y)$ with
\[Q_i(x,y)=\left\{\begin{array}{ll}q^-(x)-{q_i}^-(y)&x\geq y\\
q^+(x)-{q_i}^+(y)&x<y\end{array}\right.,\]
where $Q_i:[v,w]\times [c_{i-1},c_i]\to \R$ is a continuous piecewise
polynomial function. For fixed $x\in[v,w]$, the left and
right partial derivatives of $Q_i$ with respect to $y\in
(c_{i-1},c_i)$ exist and are given by 
\[\frac{\partial^-Q_i(x,y)}{\partial y}=-(q^+_i)'(y)\qquad \frac{\partial^+Q_i(x,y)}{\partial y}=-(q^-_i)'(y).\] 
The upper envelop can be expressed as, 
\[s(f,g)(x)=\sup_{1\leq i\leq n}(\sup_{y\in[c_{i-1},c_i]}(p_i^-(y)+Q_i(x,y))).\]
The graph of the upper envelop for $y\in[c_{i-1},c_i]$, i.e.\ the
graph of
\[x\mapsto\sup_{y\in[c_{i-1},c_i]}p_i^-(y)+Q_i(x,y)\] contains a finite
number of segments each of which can be one of two types:
\begin{itemize}
\item A segment of the graph of $p_i^-$ in an interval
  $[\alpha,\beta]\subseteq [c_{i-1},c_i]$, where, for
  $y\in [\alpha,\beta]$, the graph of $x\mapsto Q_i(x,y)$ is, in a
  neighbourhood of $y$, below the tangent to $p_i^-$ at $y$. For this to
  happen, we must have the following two necessary conditions:
\begin{itemize}
\item $\alpha=c_{i-1}$ or
  $(p^-_i)'(\alpha)=(q^+_i)'(\alpha)$
  or $(p^-_i)'(\alpha)=(q^-_i)'(\alpha)$. 
\item $\beta=c_{i}$ or
  $(p^-_i)'(\beta)=(q^+_i)'(\beta)$
  or $(p^-_i)'(\beta)=(q^-_i)'(\beta)$.
\end{itemize}
\item A segment of the graph of $x\mapsto p^-_i(y)+Q_i(x,y)$ for some
  $y\in [c_{i-1},c_i]$, where either $y=c_{i-1}$ or $y=c_{i}$
  or, else,
$(p_i^-)'(y)=(q^+_i)'(y)$
  or $(p^-i)'(y)=(q^-_i)'(y)$.
\end{itemize}
Let $K_i=\{c_{i-1},c_i\}\cup
\{y\in(c_{i-1},c_i)\,|\,(p^-_i)'(y)=(q_i^+)'(y)\mbox { or } (p^-_i)'(y)=(q_i^-)'(y)\}$.
Since $p_i^-$, $q_i^-$ and $q_i^+$ are semi-rational polynomials, $K_i$ is,
for each $i=1,\cdots,n$, a
finite set of algebraic numbers and we have:
\begin{equation}\label{sup-in-single}\sup_{y\in[c_{i-1},c_i]}p^-_i(y)+Q_i(x,y)=\sup_{y\in
  K_i}p^-_i(y)+Q_i(x,y).\end{equation}
Recalling the definition of $Q_i$, we see that for each $y\in K_i$, we
have 
\[p^-_i(y)+Q_i(x,y)=\left\{\begin{array}{ll}
    q^-(x)+\gamma^-&x\geq y\\
q^+(x)+\gamma^+&x< y,\\\end{array}\right.\]
where $\gamma^-=p^-_i(y)-q_i^-(y)$ and $\gamma^+=p^-_i(y)-q_i^+(y)$ are
algebraic numbers. Recall that comparison of algebraic numbers is
decidable. It follows that the supremum in Equation~\ref{sup-in-single} consists of a continuous
piecewise polynomial function such that each polynomial defining the
function is a rational polynomial translated by an algebraic number and
defined on an interval with algebraic endpoints.

Now put $K=\bigcup_{1\leq i\leq n}K_i=\{d_j\,|\, 0\leq j\leq
m\}$ with $v=d_0<d_1<\cdots<d_m=w$. Then, there are rational
polynomials $r_j$ and algebraic numbers
$\gamma_j$ ($1\leq j\leq
m$) such that $s(f,g)(x)=r_j(x)+\gamma_j$ for $x\in[d_{j-1},d_j]$, as required. 
Similarly, it follows that $t(f,g)$ is a piecewise semi-rational polynomial in $O$.~\qed








\end{proof}
\begin{theorem}
The relation ${\sf Cons}\subseteq D^0[0,1]\times D^0[0,1]$ is
decidable on the basis of semi-rational polynomial
step functions.
\end{theorem}
\begin{proof}
Let $f,g\in D^0[0,1]$ be semi-rational polynomial step functions.
 We note that $(f,g)\in
{\sf Cons}$ iff $(f,g)$ is consistent in each connected open component of $\mbox{dom}(g)$ with
non-empty intersection with $\mbox{dom}(f)$. Fix a connected
component $O$ of the domain of $g$. Then, using the notations in
Lemma~\ref{leastconsistent}, $(f,g)$ will be consistent in
$O$ iff $\forall x\in O.\,s(f,g)(x) \leq f^+(x)$. Since $s(f,g)$ and $f^+$ are
piecewise semi-rational polynomials, it follows by
Proposition~\ref{algebpoly}, that the relation $\forall
x\in O.\,s(f,g)(x)\leq f^+(x)$, and hence the relation ${\sf Cons}$, is decidable.~\qed

\end{proof}

\begin{definition}
The {\em domain of $C^1$ functions} on $[0,1]$ is the subdomain of $(D^0[0,1])^2$ given by 
\[D^1[0,1]=\{(f,g)\in (D^0[0,1])^2|(f,g)\in {\sf Cons}\}.\]
\end{definition}
\begin{corollary}
$D^1[0,1]$ is an $\omega$-continuous bounded complete dcpo which can
be given an effective structure.
\end{corollary}
\begin{proof}
We simply note that $D^1[0,1]$ is a Scott-closed subset of the $\omega$-continuous bounded complete dcpo $({\bf
I}[0,1]\ra \I \R)^2$ and is therefore itself an
$\omega$-continuous bounded complete dcpo. Because ${\sf Cons}$ is
decidable on the basis of step functions (and also on the polynomial
step functions), $D^1[0,1]$ can be provided with an effective
structure. More specifically, we start with a standard effective
structure on $D^0[0,1]$ (a standard enumeration of the basis of rational step functions, with decidable
predicates for $\sle_{D^0}$, $\ll_{D^0}$, ${\sf Con}_{(D^0,\sle)}$ and
${\sf Con}_{(D^0,\ll)}$ when restricted to the basis; see~\cite{Smy77,Plo81}). We take the
product of the effectively given $D^0[0,1]$ with itself, together with the decidable
${\sf Cons}$ on the pairs of basis elements. Since the basic
relations in $D^1[0,1]$ are obtained componentwise from that of
$(D^0[0,1])\times (D^0[0,1])$, we will obtain
an enumeration of the induced basis of $D^1[0,1]$ with decidable predicates for 
$\sle_{D^1}$, $\ll_{D^1}$, ${\sf Con}_{(D^1,\sle)}$ and
${\sf Con}_{(D^1,\ll)}$ when restricted to this basis.~\qed 
\end{proof}

\begin{proposition}\label{f'=g}
Let $(f,g)\in D^1$ such that $f$ and $g$ preserve maximal elements in
some open set $O\subseteq \mbox{dom}(f)\cap \mbox{dom}(g)$. Then for all
$x\in O$, the induced maps ${f},{g}:O\to \R$ satisfy
${f}'(x)={g}(x)$ for all $x\in O$~\qed.
\end{proposition}Let the {\em derivative operator} 
$$\frac{D}{Dx}:D^1[0,1]\to D^0[0,1]$$
be the projection to the second component, i.e.\ $\frac{D}{Dx}(f,g)=g$.
Then $\frac{D}{Dx}$ is clearly continuous and we have:
\begin{proposition}
\[\frac{D}{Dx}(f,g)\sle \bigsqcap\{\frac{d}{dx}\I
h\,|\,\I h\in\uparrow\hspace{-.15cm} f\cap \int g\}.\]
\end{proposition}
\begin{proof}
If $\I h\in\uparrow\hspace{-.15cm} f\cap \int g$, then $g\sle \frac{d}{dx}\I
h$ by
Corollary~\ref{difftie}~\qed.
\end{proof}

Let $\Gamma^1:C^0[0,1]\to D^1[0,1]$ be defined by  $\Gamma^1(f)=(\I
f,\frac{d\I f}{dx})$.

\begin{theorem}
The map $\Gamma^1$ is an embedding into the set of maximal elements of $D^1$.
\end{theorem}
\begin{proof}
We first check that $\Gamma^1$ is well-defined. By Corollary~\ref{difftie}, we have $\I
f\in\intop \frac{d\I f}{dx}$ and thus, $(\I
f,\frac{d\I f}{dx})\in D^1$. We now show that $(\I
f,\frac{d\I f}{dx})$ is maximal. If $\frac{d\I f}{dx}  \sle g$ and $(\I f,g)\in D^1$ then for any $a\searrow b \sle g$ we have $\I f\in \int g \subseteq \delta(a,b)$, which implies $a\searrow b\sle \frac{d\I f}{dx}$, thus $g \sle \frac{d\I f}{dx}$, i.e., $ g=\frac{d\I f}{dx}$ and $(f,\frac{d\I f}{dx})$ is maximal. That $\Gamma^1$ is an embedding follows from Theorem~\ref{embedding}.~\qed
\end{proof}
The map $\Gamma^1$ restricts to give an embedding of locally Lipschitz functions into the set of maximal elements of $D^1$. Note that  $f\in C^0[0,1]$ is locally Lipschitz iff $\frac{d\I f}{dx}(y)\neq\bot$ for all $y\in\I [0,1]$. Also $\Gamma^1$ restricts to give an embedding of piecewise $C^1$ functions into the set of maximal elements of $D^1$. It is easy to see that a function $f\in C^0[0,1]$ is piecewise $C^1$ iff $\frac{d\I f}{dx}(\{y\})$ is non-maximal for all but a finite number of $y\in[0,1]$. Moreover, if we consider $C^1$ functions with their $C^1$ norm we obtain:
\begin{corollary}
The map $\Gamma^1$ restricts to give a topological embedding  $\Gamma^1:C^1[0,1]\to D^1[0,1]$, which makes the following
diagram commute:\[\begin{diagram}
C^1[0,1]&\rTo^{\frac{d}{dx}}&C^0[0,1]\\
\dTo^{\Gamma^1}&&\dTo_{\Gamma^0}\\
D^1[0,1]&\rTo_{\frac{D}{Dx}}&D^0[0,1]\quad \mbox{\qed}\\
\end{diagram}\]
\end{corollary}
Finally, we note that analogously we can define 
\[D^1_{\sf r}=\{(f,g)\in D^0_{\sf r}\times D^0_{\sf r}\mid  (f,g)\in \ua\hspace{-.05cm} f\cap \int_{\sf r} g\neq \emptyset\},\] and all the results in this section will have their analogues for  $D^1_{\sf r}$.


\section{Solution of differential equations}

Consider a vector field $v:O\to\R$ for some open subset $O\subseteq
\R^2$ and a point $(t_0,x_0)\in O$. The following theorem, whose proof
is based on Banach fix-point theorem, is referred to as Picard's
theorem and is at the foundation of the theory of differential equations.
\begin{theorem}\cite{KF75} If $v$ is continuous in $O$ and uniformly
Lipschitz in the second argument then the initial value
problem $\dot{x}=v(t,x)$ with $x(t_0)=x_0$ has a unique solution in a
neighbourhood of $t_0$ and can be obtained as the unique
fix-point of the operator:
\[P:f\mapsto \lambda
t.(x_0+\int_{t_0}^tv(t,f(t))\;dt):C^0[t_0-\delta,t_0+\delta]\to C^0[t_0-\delta,t_0+\delta] .\]
in some small enough neighbourhood $|t-t_0|\leq \delta$.\qquad\qed
\end{theorem}
Picard's theorem can be easily extended to vector fields
$v:O\to\R^{n}$, with $O\subseteq \R^{n+1}$,
which gives a basis for solving systems of ordinary differential
equations. In this section we present a domain-theoretic version of
this theorem for $n=1$ which, like Picard's theorem can easily be
extended to any dimension $n\geq 1$.

The above classical operator can be reformulated as the composition of two
operators
$U,A_v:(C^0[t_0-\delta,t_0+\delta])^2\to
(C^0[t_0-\delta,t_0+\delta])^2$ on pairs $(f,g)$, where $f$
gives approximation to the solution and $g$ gives approximation to the 
derivative of the solution. The map $A_v$ upgrades the information
on the derivative and $U$ upgrades the information on the
function itself:
\[U(f,g)=(\lambda
t.(x_0+\int_{t_0}^tg \;dt),g)\qquad\qquad A_v(f,g)=(f,\lambda
t.v(t,f(t)).\]
We have $P(f)=\pi_0(U\circ A_v(f,g))$, for any $g$, 
where $\pi_0$ is projection to the first component. The unique
fix-point $(f,g)$ of $U\circ A_v$ will satisfy: $f'=g=\lambda
t.v(t,f(t))$. 

We consider a domain-theoretic framework for differential equations and
define similar operators in that setting. We define:
\[\begin{array}{cccc} H:&(\I[0,1]\times \IR\to\IR)\times D^0&\to&D^0 \\
\end{array}\]
by \[\begin{array}{cccc}
H(v,f):&t&\mapsto&v(t,f(t)).\\
\end{array}\]
In
analogy with the classical vector field above, we
consider $v\in (\I[0,1]\times \IR\to\IR)$ as an interval-valued vector
field with interval input. The map
$H$ is Scott continuous and we put $H_v:D^0\to D^0$ with $H_v(f)=H(v,f)$.
Let 
\[{\sf Ap}:(\I[0,1]\times \IR\to\IR)\times (D^0\times D^0)\rightarrow D^0\times D^0\] with
${\sf Ap}(v,(f,g))=(f,H(v,f))$ and let ${\sf Ap}_v:D^0\times
D^0\rightarrow D^0\times D^0$ with ${\sf Ap}_v(f,g)={\sf Ap}(v,(f,g))$ . Also define 
\[{\sf Up}:D^1\rightarrow D^1\] with
${\sf Up}(f,g)=(\I [s(f,g),t(f,g)],g)$ and put ${\sf Up}_1(f,g)=\I [s(f,g),t(f,g)]$.


\begin{proposition}\label{f_g=sup}
\begin{itemize}
\itemi The maps ${\sf Ap}_v$ and ${\sf Up}$ are continuous. 
\itemii ${\sf Up}_1(f,g)\sge (\bigsqcup\{h|\uparrow\hspace{-.15cm} h\cap
\int g=\uparrow\hspace{-.15cm} f\cap\int g\})$.
\itemiii ${\sf Up}_1({\sf Up}_1(f,g),g)={\sf Up}_1(f,g)$.
\end{itemize}
\end{proposition}
\begin{proof}
(i) The continuity of ${\sf Ap}$ follows from the
continuity of $H$, the continuity of
${\sf Up}$ from the
continuity of $s$ and $t$ (Proposition~\ref{stcont}). 

(ii) Note that for
$k_1,k_2\in C^0$, with $k_1\leq k_2$, we have $\I [k_1,k_2]=\I
k_1\sqcap \I k_2$.  Let $h\in D^0$ satisfy $\uparrow\hspace{-.15cm} h\cap
\int g=\uparrow\hspace{-.15cm} f\cap\int g$. Since $\I
s(f,g),\I t(f,g)\sge h$, we get 
\[{\sf Up}_1(f,g)=\I[s(f,g),t(f,g)]=(\I s(f,g))\sqcap (\I t(f,g))\sge h.\]

(iii) Recall that, for each component $O$ of $\mbox{dom}(g)$ which
intersects $\mbox{dom}(f)$, the map $s(f,g):O\to \R$ is the least
function $h\in C^0(O)$ with $h\geq f^-$ and $\I h\in\int
g$; the dual property holds for $t(f,g)$. Since ${\sf Up}_1(f,g)=\I
[s(f,g),t(s,f)]\in\int g$ we get:
$s({\sf Up}_1(f,g),g)=s(f,g)$ and $t({\sf Up}_1(f,g),g)=t(f,g)$.~\qed
\end{proof}

Unlike ${\sf Up}$, the map ${\sf Ap}_v$
does not take $D^1[0,1]$ to itself. We need to work in a
subdomain of $D^1[0,1]$, dependent on $v$, which is preserved by
${\sf Ap}_v$. In order to define such a subdomain we first
define a stronger version of consistency. We say that $(f,g)\in D^1$
is {\em strongly consistent}, and write $(f,g)\in {\sf SCons}$, if $(f,h)\in{\sf Cons}$ for all $h\sge g$.


 



\begin {proposition} \label{strongcons}
If $(f,g)\in {\sf SCons}$ then:
\begin{itemize}
\item[(i)] $(f,h)\in {\sf SCons}$ for all $h\sge g$.
\item[(ii)] ${\sf Up}(f,g)\in {\sf SCons}$.
\end{itemize}
\end {proposition}


\begin{proof}
(i) is trivial. To see (ii), let $h\sge g$. Since $(f,g)\in
{\sf SCons}$, we have $(f,h)\in {\sf Cons}$. But then
${\sf Up}(f,h)=({\sf Up}_1(f,h), h)\in
{\sf Cons}$. Now, by the monotonicity of ${\sf Up}_1$, we have:
 ${\sf Up}_1(f,g) \sqsubseteq {\sf Up}_1(f,h)$
 and therefore $({\sf Up}_1(f,g), h)\in {\sf Cons}$. 
This shows that ${\sf Up}(f,g) = ({\sf Up}_1(f,g), g)\in {\sf SCons}$.
\end{proof}


\begin {proposition} \label{scclosed}
Strong consistency is closed under taking lubs of increasing chains, that is, if
$(f_i,g_i)\in {\sf SCons}$ where $(f_i)$ and $(g_i)$ are increasing
chains in $D^1$. Then

$$(\bigsqcup f_i,\bigsqcup g_i)\in{\sf SCons}$$
\end {proposition}
\begin{proof}

Suppose $(f_i,g_i)\in {\sf SCons}$ where $(f_i)_{i\in\omega}$ and $(g_i)_{i\in\omega}$ are increasing
chains in $D^1$. We want to show that $(\bigsqcup_{i\in\omega} f_i,\bigsqcup_{i\in\omega} g_i)\in {\sf SCons}$.
Let $\bigsqcup_{i\in\omega} g_i \sqsubseteq g$. Then $g_i\sqsubseteq g$ for all
$i\geq 0$. Hence, by strong consistency of $(f_i,g_i)$, we have $(f_i,g)\in
{\sf Cons}$. Since ${\sf Cons}$ is Scott closed we get $(\bigsqcup_{i\in\omega} f_i,g)\in
{\sf Cons}$.~\qed


\end{proof}
We now define a subdomain of $D^1[0,1]$ which is preserved by the
updating maps. Let $D_v^1=\{(f,g)\in D^1|(f,g)\in{\sf SCons}\quad\&\quad g\sle H(v,f)\}$. 

\begin{proposition}
$D_v^1$ is a dcpo and the two maps ${\sf Ap}_v$ and ${\sf Up}$ take $D_v^1$ into itself.
\end{proposition}
\begin{proof}
By Proposition~\ref{scclosed}, ${\sf SCons}$ is closed under the lubs of
increasing chains. On the other hand suppose $((f_i,g_i))_{i\in\omega}$ is an increasing chain with
$g_i\sle H(v,f_i)$ for $i\in\omega$. Then by continuity
of $H_v$ we get $\bigsqcup_{i\in\omega}g_i\sle \bigsqcup_{i\in\omega} H(v,f_i)=\bigsqcup_{i\in\omega}H_v(f_i)=H_v(\bigsqcup_{i\in\omega}f_i)$. 

Let $(f,g)\in D_v^1$. Then ${\sf Ap}_v(f,g)=(f,H(v,f))$. Since
$g\sle H(v,f)$ and $(f,g)\in{\sf SCons}$, by
Proposition~\ref{strongcons}(i), we get the strong consistency of
$(f,H(v,f))$. It follows that ${\sf Ap}_v(f,g)\in D_v^1$, as the second
condition is trivially satisfied. On the other hand, ${\sf
  Up}(f,g)=({\sf Up}_1(f,g),g)\in{\sf SCons}$ by
Proposition~~\ref{strongcons}(ii). Finally, by monotonicity of $H_v$
we get: $g\sle H_v(f)\sle H_v({\sf Up}(f,g))$. Hence, ${\sf Up}(f,g)\in D_v^1$.~\qed 

\end{proof}




We have now a domain-theoretic generalization of the Picard's
theorem. Let $P_v:D_v^1\to D_v^1$ be given by $P_v={\sf Up}\circ {\sf Ap}_v$.
For $(f_0,g_0)\in D_v^1$, let $D^1_{v,(f_0,g_0)}=\ua\hspace{-.05cm}
(f_0,g_0)\cap D_v^1$. Then  $D^1_{v,(f_0,g_0)}$ is a dcpo with least
element $(f_0,g_0)$. Thus we obtain:
\begin{theorem}\label{domainpicard}
The restriction
$P_{v,(f_0,g_0)}={P_v}\restriction_{D^1_{v,(f_0,g_0)}}:D^1_{v,(f_0,g_0)}\rightarrow D^1_{v,(f_0,g_0)}$
has a least fix-point $(f_s,g_s)$ with $f_0\sqsubseteq f_s$ and
$g_0\sqsubseteq g_s$.
\end{theorem}


 
\subsection{Width of the fix-point $f_s$}We first obtain a bound for
the update ${\sf Up}(f,g)$.
\begin{proposition}\label{gendef}We have $h \in \int g $ iff, for all $x,x_1,x_2\in {\bf I}[0,1]$ 
with  $x \sqsubseteq x_1,x_2$,
 we have 
$(x_2 - x_1) g(x) \sqsubseteq h(x_2) - h(x_1).$
\end{proposition}
\begin{proof}
The ``only if'' part. Let $\step{a}{b}\sle g$, then a simple calculation shows that for all
$x_1,x_2\sge x$ we have:
\[(x_2-x_1)(\step{a}{b})(x)\sle (x_2-x_1)b\sle h(x_2)-h(x_1).\]
Taking the supremum over all step functions way-below $g$, the result
follows by the Scott continuity of the interval product $-\times
-:(u,v)\mapsto uv:\IR\times \IR\to \IR$.

The ``if part''. Let $\step{a}{b}\sle g$. It suffices to show that
$h\in\delta(a,b)$. Suppose $x_1,x_2\gg a$ and put $x=x_1\sqcap
x_2$. Then $x\gg a$ and $x_1,x_2\sge x$. Thus,
\[(x_2-x_1)b=(x_2-x_1)(\step{a}{b})(x)\sle (x_2-x_1)g(x)\sle
h(x_2) - h(x_1),\]
and, hence, $h\in \delta(a,b)$.~\qed
\end{proof}
\begin{corollary}\label{gendefmax}
$\I h\in\int g$ iff, for all $x,y\in\mbox{dom}(g)$ with
$x\leq y$, we have: \[(y-x)\underline{g([x,y])}\leq f(y)-f(x)\leq (y-x)\overline{g([x,y])}.\]

\end{corollary}


Assume now that $h \in \ua\hspace{-.05cm}f \cap \int g$.
For all $x,x_1,x_2\in {\bf I}[0,1]$, with $x\sle x_1,x_2 $, from Proposition~\ref{gendef}, we get:

\begin{equation}  \label{up_2}
f(x_1) + (x_2 - x_1) g(x) \sqsubseteq h(x_1) + (x_2 - x_1)  g(x)
\sqsubseteq h(x_2) -h(x_1) +h(x_1)\sle h(x_2)   
\end{equation}
and, therefore:
\begin{equation}  \label{up_3}
\bigsqcup\left\{ f(x_1) + (x_2 - x_1)g(x)\;  |\;  x\sle x_1 \;\&\;x\sge x_2\right\} \sqsubseteq h(x_2). 
\end{equation}

By Proposition~\ref{f_g=sup}(ii), it follows that:
\begin{equation}  \label{up_4}
{\sf Up} (f,g)(x_2) \sqsupseteq \bigsqcup\left\{ f(x_1) + (x_2 - x_1)g(x)\;  |\;  x\sle x_1 \;\&\;x\sge x_2\right\}. 
\end{equation}
Let $(f_s,g_s)$ be the fix-point of Theorem~\ref{domainpicard}, so
that ${\sf Up}(f_s,g_s) = f_s$.
Hence, by Equation~\ref{up_4}, we have:
\[
f_s(x_2) \sqsupseteq \bigsqcup\left\{ f_s(x_1) + (x_2 - x_1) g_s(x)\;  |\; x\sle x_1 \;\&\;x\sge x_2\right\}.
\]
In particular,
for real numbers $t_1$ and $t_2$, with $t_1 < t_2$,
considered as maximal elements of ${\bf I}[0,1]$, 

\begin{equation}  \label{width_2}
f_s(t_2) \sqsupseteq f_s(t_1) + (t_2 - t_1) g_s([t_1,t_2]), 
\end{equation}
where for convenience we have written $t_i$ for $\{t_i\}$. 

We denote the width of an interval $a$ by
$w(a)=\overline{a}-\underline{a}$. For $f\in D^0[0,1]$, let $w_f:[0,1]\to{\mathbb R}$ be
given
by $w_f(x)=w(f(\{x\})$. From Equation~\ref{width_2} we get:
\begin{equation}  \label{width_3}
w_{f_s}(t_2) \leq w_{f_s}(t_1) + (t_2 - t_1) w_{g_s}([t_1,t_2]). 
\end{equation}
Let $S$ be the set of all finite increasing sequences \[p=\{t_0,t_1,t_2,\cdots,t_n\,|\,t_0<t_1<t_2<..<t_n=t\}.\]
We have from Equation~\ref{width_3}:
\begin{equation}  \label{width_4}
w_{f_s}(t) \leq w_{f_s}(t_0) + \sum_{i=1,n} w_{g_s}([t_{i-1},t_i]) (t_i - t_{i-1}).  
\end{equation}
For a given sequence $p=\{t_0,t_1,t_2,\ldots,t_n|t_0<t_1<t_2<..<t_n=t\}$,
we denote by $\Theta_p$ the
classical step function defined, for 
$u\in [t_0,t]$ by $\Theta_p(u) = w_{g_s}([t_{i-1},t_i])$ if $u\in (t_{i-1},t_i)$
and $\Theta_p(t_i) = \max(w_{g_s}([t_{i-1},t_i]),w_{g_s}([t_i,t_{i+1}]) )$.
Equation ~\ref{width_4} can be written as:
\begin{equation}  \label{width_5}
w_{f_s}(t) \leq w_{f_s}(t_0) + \int_{t_0}^t \Theta_p(u) du
\end{equation}

Consider the family of sequences $(p_k)_{k\in \omega}$ where 
\[p_k = \{t_0, t_0 + 2^{-k}[t-t_0], t_0 + 2\cdot 2^{-k}[t-t_0],t_0 + 3\cdot 2^{-k}[t-t_0],...,t_0 + 2^k\cdot 2^{-k}[t-t_0]\}.\]
The sequence
$\Theta_{p_k}$ is decreasing and converges
 pointwise to $w_{g_s}$, which is upper semi-continuous. Hence, by the monotone convergence theorem, we have from
Equation~\ref{width_5}: 
\begin{proposition}\label{width_6}
\[w_{f_s}(t) \leq w_{f_s}(t_0) + \int_{t_0}^t w_{g_s}(u) du.\]
\end{proposition}

\subsection{The Lipschitz case}

Let  $(f_s,g_s)$ be the fix-point of the theorem, we have:
\begin{equation}  \label{width_7}
g_s(u) = {v}(u,f_s(u))
\end{equation}

We assume now that ${v:\I[0,1]\times \IR\to \IR}$ satisfies a
Lipschitz-like condition with constant $K$ with respect to its second
argument uniformly in the maximal elements of its first argument; in
other words,
for any maximal element (i.e.\ real) $t$, we assume:
$
w({v}(t,X)) \leq K w(X)$. Equation~\ref{width_7} then gives: $
w(g_s(u)) \leq K w(f_s(u)),$
which, together with Proposition~\ref{width_6} leads to
\[
w_{f_s}(t) \leq w_{f_s}(t_0) + K \int_{t_0}^t w_{f_s}(u) du.
\]
A simple inductive proof shows that for each integer $n\geq 0$:
\[
w_{f_s}(t)\]\[ \leq w_{f_s}(t_0) (1+ K(t-t_0)+\cdots
+K^n(t-t_0)^n/n!
+ K^n  \int_{t_0}^t  \int_{t_0}^{u_0}  \cdots \int_{t_n}^{u_n} w_{f_s}(u_n) du_0
du_1 \cdots du_n).
\]
Since $f_s$ is bounded, we have a bound $B$ on $w_{f_s}(u_n)$
and the remainder is bounded by:
\[
 K^n  \int_{t_0}^t  \int_{t_0}^{u_0}  \cdots \int_{t_n}^{u_n} w_{f_s}(u_n) du_0
du_1 \cdots du_n\]\[
\leq  K^n  B \int_{t_0}^t  \int_{t_0}^{u_0}  \cdots \int_{t_n}^{u_n} du_0 du_1
\cdots du_n = K^n (t-t_0)^{(n+1)}/(n+1)!
\]
This remainder goes to $0$ when $n \rightarrow \infty$ for any fixed $t$.
By taking the limit we obtain: $
w_{f_s}(t) \leq w_{f_s}(t_0)e^{K(t-t_0)}$.
Since, the same holds for $t<t_0$, we conclude that:
\begin{proposition}\label{width_12}
\[w_{f_s}(t) \leq w_{f_s}(t_0)e^{K|t-t_0|}.\mbox{\qed}\]
\end{proposition}


\subsection{Picard's theorem revisited}
\begin{proposition}\label{nestedscon}
If $(\step{T_i}{X_i})_{i\in I}$ is a
family of consistent step functions, then $(\bigsqcup_{i\in
  I}(\step{T_i}{X_i}),\step{(\bigsqcap_{i\in I}T_i)}{B})$
is a strongly consistent pair iff $X_i-X_j\sle (T_i-T_j)B$ for all $i,j\in
I$.
\end{proposition}
\begin{proof}
First note that for $i,j\in I$ we have $X_i-X_j\sle (T_i-T_j)B$ iff,
for each $u\in B$, there exists a straight line with slope $u$ which
intersects the four vertical sides of the rectangles $(T_i,X_i)$ and
$(T_j,X_j)$ when $i\neq j$, or the two  vertical sides of $(T_i,X_i)$
when $i=j$. The ``only if part'' then follows immediately. For the
``if'' part, fix $u\in B$. For each unordered pair $i,j\in I$,
consider the family ${\cal L}_{ij}$ of parallel straight lines with slope $u$, which intersect
the four vertical sides of the rectangles $(T_i,X_i)$ and
$(T_j,X_j)$ when $i\neq j$, or the two  vertical sides of $(T_i,X_i)$
when $i=j$. For a given unordered pair $i,j\in I$, let
$l_{ij}$ and $g_{ij}$ be, respectively, the infimum and the supremum
of the non-empty set $\{L(0)\,|\, L\in {\cal L}_{ij}\}$. By assumption and
the above observation the
set of intervals $\{[l_{ij},g_{ij}]\,|\,i,j\in I\}$ have
pairwise nonempty intersections. Hence,
$I=\bigcap_{i,j\in I}[l_{ij},g_{ij}]\neq\emptyset$ and any line with
slope $u$ passing through any point of $I$ intersects the two
vertical
edges of $(T_i,X_i)$ for all $i\in I$.~\qed
\end{proof}
\begin{theorem}
Let $v:O\to {\mathbb R}$ be continuous in the open set $O\subseteq
{\mathbb R}^2$ and $(t_0,x_0)\in O$. If $v$ is Lipschitz in its second
argument uniformly in the first argument, then the solution of the
initial value problem $\dot{x}=v(t,x)$ with $x(t_0)=x_0$ given by the
classical Picard's theorem coincides with the domain-theoretic
solution.
\end{theorem}
\begin{proof}
Let $A\subset O$ be a compact rectangle with $(t_0,x_0)\in
A^\circ$ such that, for some $M>0$, we have $|v(t,x)|\leq M$ for all $(t,x)\in A$. Let
$(T_i,X_i)_{i\in\omega}$ be any shrinking nested sequence of
  compact rectangles such that:
\begin{itemize}
\item  $(T_i,X_i)\subset A^\circ$ all $i\in\omega$,
\item $(t_0,x_0)$ is the centre of $(T_i,X_i)$ for all $i\in\omega$, 
\item $w(X_i)=Mw(T_i)$ for all $i\in\omega$, and,
\item $\bigsqcup_i(T_i,X_i)=(\{t_0\},\{x_0\})$.
\end{itemize}
We now consider the domain-theoretic Picard's theorem for the
canonical extension $\I
v:\I T_0\times \IR\to \IR$. Let $B=[-M,M]$, then $v$ satisfies: $\step{A}{B}\sle
\I v$. By Proposition~\ref{nestedscon}, $(f_0,g_0)=(\bigsqcup_{i\in
  \omega}\step{T_i}{X_i},\step{T_0}{B})$
is strongly consistent. Furthermore, we have $
H_{\I v}(f_0)\sge g_0$ since, for any $T\in \I T_0$, we obtain
\[H_{\I v}(f_0)(T)=\I v(T,(\bigsqcup_{i\in
  \omega}\step{T_i}{X_i})(T))\sqsupseteq \I v(T,X_0)\sqsupseteq
B\sqsupseteq g_0(T).\] Since $f_s(\{t_0\})\sqsupseteq
f_0(\{t_0\})=\{x_0\}$, Proposition~\ref{width_12} implies that
$w_{f_s}=0$. Since $\I v$ preserves maximal elements, it follows from
$g_s=H(\I v,f_s)$ that $w_{g_s}=0$ and $f_s$ and $g_s$
preserve maximal elements. Now, by
Proposition~\ref{f'=g}, it follows that the induced maps $f_s,g_s:T_0\to
\R$ satisfy $f_s'=g_s$ and hence $f_s'(t)=v(t,f_s(t))$, by the fix-point equation for $g_s$.~\qed
\end{proof}
See~\cite{EKL03} for an algorithmic framework for solving initial value problems based on this method.


\section{Implicit function theorem}
As explained in the Introduction, a main application of the
domain-theoretic model for differential calculus is to obtain
piecewise smooth finitary 
approximations of curves and surfaces which are defined implicitly by,
say, $f(\vec{x})=0$ where $f:[0,1]^n\to \R$ is a $C^k$ function of $n$
variables. 

For functions of a single variable, which is the object of
this paper, the implicit function theorem takes a very simple form: if $f\in C^1[0,1]$ and $f(x_0)=0$ with $f'(x_0)>0$ for some
$x_0\in (0,1)$, then $x_0$ is an isolated root of
$f(x)=0$. Suppose now that $f$ and $f'$ are computable maps in the
sense of classical recursion theory~\cite{PR89}. Then $\I f$ and $\I
f'$ are computable~\cite{ES97} and can be approximated effectively by an
increasing sequence of step functions $f=\bigsqcup_{i\in\omega}f_i$
and $g=\bigsqcup_{i\in\omega}g_i$. Since $(\I f,\I f')\in
{\sf Cons}$, it follows that $(f_i,g_i)\in {\sf Cons}$ for all
$i\in\omega$. From $f'(x_0)>0$ it follows that for some $i\in\omega$
we have $\underline{g_i(\{x_0\})}>0$ and thus the piecewise linear (or
piecewise rational or semi-rational polynomial) functions
$s(f_i,g_i)$ and $t(f_i,g_i)$ are both strictly increasing in a
small neighbourhood of $x_0$. Therefore, they have computable roots $v_i$ and
$w_i$ respectively with $x_0\in[w_i,v_i]$. In the limit we have
$\{x_0\}=\bigcap_{i\in\omega}[w_i,v_i]$. This then gives us an
algorithm to compute $x_0$ up to any desired accuracy.


\section{Conclusion} We have developed the two notions of 
the set of primitive maps and the derivative of a Scott continuous map and have shown that they are dually related similar to the duality of differentiation and integration in the fundamental theorem of calculus. We
have also constructed a domain-theoretic data type
for $C^1$ functions in differential calculus, which
extends the applications of domain theory and type theory to smooth
mathematics. This domain also provides us with a model for the differential properties of piecewise $C^1$ functions, locally Lipschitz functions and, more generally, continuous functions. A domain-theoretic generalization of Picard's theorem in
this framework allows us to solve for the solution of differential
equations in such a way that at each stage of computation the approximation is
bounded from below and above by two piecewise polynomial functions.

The domain construction for $C^1$ functions and many other results in
this paper can be generalized
to $C^k$ and $C^\infty$ functions and to functions of
several variables; these will be dealt with in future papers.  

We are also developing and implementing the algorithmic framework
for solving differential equations using the domain-theoretic version
of Picard's theorem. One needs to approximate elementary functions
efficiently from above and below by piecewise rational polynomial
functions. In order to avoid the ubiquitous problem of a rapid growth
in the size of integers in rational arithmetic, one applies a sound
rounding of the coefficients of the polynomials used onto a dyadic
grid.

From a theoretical view point, the extension of the domain-theoretic
framework for differential calculus to $C^k$ functions of several
variables now remain a priority. Such an
extension will allow us to develop domain-theoretic effective version
of the inverse and implicit functions theorem which are the building
blocks of multi-dimensional differential calculus with, in particular,
applications to
approximation of curves and surfaces. 

\section*{Acknowledgements}
We thank John Howroyd, Marko Krznari\'c and Ali Khanban for various
discussions. This work has been supported by EPSRC. 

\bibliographystyle{plain}
\bibliography{biblio}





\end{document}
















\begin{center}
\begin{figure}[ht]
\includegraphics*[scale=0.25]{figure1.eps}
\caption{}
\label{membership}
\end{figure}
\end{center}
\begin{center}
\begin{figure}[ht]
\includegraphics*[scale=0.25]{figure2.eps}
\caption{}
\label{membership}
\end{figure}
\end{center}

\begin{center}
\begin{figure}[ht]
\includegraphics*[scale=0.25]{figure4.eps}
\caption{}
\label{membership}
\end{figure}
\end{center}



\begin{center}
\begin{figure}[ht]
\includegraphics*[scale=.5]{consistent.eps}
\caption{}
\label{membership}
\end{figure}
\end{center}
\bibliographystyle{plain}
\bibliography{biblio}





























%%%%%%%%%%%%%%%%%%%%%

\section{Picard's theorem}

Assume $T_B\in{\bf I}[0,1]$ and $B,X_B\in{\bf I}{\mathbb R}$ with
$(T_B,X_B)\searrow B\sqsubseteq F$. Let $T_0\in{\bf I}[0,1]$ with
$T_B\ll T_0$ and $X_0\in {\bf I}{\mathbb R}$ with $X_B\ll X_0$. Assume 
that $B=[\underline{B},\overline{B}]$ with $\underline{B}\geq 0$ (the
other cases are similar).

Let 

$y_{11}=\overline{B}(\underline{T_B}-\underline{T_0})+\underline{X_0}$.

\vspace{.3cm}
$y_{12}=\overline{B}(\underline{T_B}-\overline{T_0})+\overline{X_0}$.
\vspace{.3cm}


$y_{21}=\overline{B}(\overline{T_B}-\underline{T_0})+\underline{X_0}$.

\vspace{.3cm}
$y_{22}=\overline{B}(\overline{T_B}-\overline{T_0})+\overline{X_0}$.

\vspace{.3cm}

and assume:

\vspace{.3cm}

(i) $\overline{B}(\overline{T_0}-\underline{T_0})\leq
\overline{X_0}-\underline{X_0}$.\vspace{.3cm}

(ii) $\underline{X_B}< y_{12}$ and $\overline{X_B}> y_{21}$.\vspace{.3cm}

(iii) $\underline{X_B}+\overline{B}(\overline{T_B}-\underline{T_B})<\overline{X_B}$.\vspace{.3cm}

Then:

\begin{proposition}There exists $X_s$ with $X_B\ll X_s\ll X_0$ such that 
$(f,g)=(T_0\searrow X_0)\sqcup (T_B\searrow X_s),T_B\searrow B)\in D_F$.
\end{proposition}
\begin{proof}
$T_0\searrow X_B$ and $T_B\searrow B)$ are
strongly consistent iff $T_0\searrow X_B$ and $T_B\searrow {\overline{B}})$
are
strongly consistent iff condition (i). Conditions (ii) and (iii) will
ensure there is $X_s$ contained in $X_B$ such that the $(T_0\searrow
X_0)\sqcup (T_B\searrow X_s),T_B\searrow B)$ is strongly consistent
and belongs to $D_F$.
\end{proof}

Therefore we get a least fix-point for $P_F$ subject to the initial
conditions $(f,g)$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55
 Furthermore, $\frac{d}{dx}$ is
not linear. For example, if $f$ is the identity function ($f(x)=x$) and
$g$ its negation $(g(x)=-x)$, then
$\frac{d(f+g)}{dx}\neq\frac{df}{dx}+\frac{dg}{dx}=\lambda
x.(1-1)=\lambda x.0$.
However, if $\frac{df}{dx}(a)$ and $\frac{dg}{dx}(a)$ are both
nonnegative intervals (consisting of nonnegative real numbers), then
it is easily checked that
$\frac{d(f+g)}{dx}=\frac{df}{dx}+\frac{dg}{dx}$. Similarly if they are 
both nonpositive.
------------------------------
\begin{proof}
The ``if part'' is trivial. To see the ``only if'' part, assume $f\in
\delta_{{\sf r}}(a,b)$ and let $X,Y\ll a$. Then by taking infimum  on both
sides of $(x-y)b\sle f(x)-f(y)$ with respect
to $x\in X$
first and with respect to $y\in Y$ next we get: $(X-y)b\sle
\bigsqcap_{x\in X}f(x)-f(y)={\cal E}(f)(X)-f(y)$ and $(X-Y)b\sle {\cal
  E}(f)(X)-{\cal E}(f)(X)$ as required.~\qed
\end{proof}
C^1/_\equiv&\pile{\rTo^{\frac{d}{dx}/_{\equiv}}\\\lTo_{\int^x}}&C^0\\
\dTo^{{\cal P}(\Gamma^0_{{\sf r}})}&&\dTo_{\Gamma^0_{{\sf r}}}\\
T^0_{{\sf r}}&\pile{\rTo^{\hat{\frac{d}{dx}}}\\\equiv\\\lTo_{{\bf \int}}}&\mbox{Im}(\hat{\frac{d}{d{
      x}}})\equi D^0_{{\sf r}}/\sim\\
\end{diagram}\qquad\mbox{\qed}\]


We use Domain Theory to synthesize two major paradigms of modern
Science and Technology: (i) Differential Calculus, introduced by
Newton and Leibnitz in the 17th century and put on a rigorous basis
by Cauchy in the 19th century, and, (ii) Computer Science and the
theory of Algorithms and Data Structures, pioneered by Alan Turing in
the 20th century. With this goal in mind, we introduce a
domain-theoretic framework for differential calculus. The indefinite
integral and also the derivative of a Scott continuous function on the
domain of intervals are defined and a domain-theoretic generalization
of the fundamental theorem of calculus is presented. In the
domain-theoretic setting any Scott continuous function has a Scott
continuous derivative which contrasts sharply with the classical
situation, in which a continuous function may not have a derivative at
any point.  We then construct a domain for differentiable real valued
functions of a real variable. The set of classical continuously
differentiable functions 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. As an
immediate application, we present a domain-theoretic generalization of
Picard's theorem, which provides a data type for solving differential
equations.
  and Corollary~\ref{difftie} 