1 Introduction

A well-known hurdle in numerical computation is caused by accumulation of round-off errors in floating point arithmetic, which can create havoc and lead to catastrophic errors in compound calculations. In safety and critical systems, where reliability of numerical computation is of utmost importance, one way to avoid the pitfalls of floating point arithmetic is to use interval analysis or exact arithmetic. In both interval analysis and exact arithmetic as well as in computable analysis, a real number is represented by a nested shrinking sequence of compact intervals whose intersections is the real number. Similarly, a real n-vector can be represented by a nested sequence of hyper-rectangles in \({\mathbb R}^n\). This leads to a framework in numerical computation and a framework for computational geometry where the inputs of algorithms or programmes are imprecise real numbers or real n-vectors; see for example [3, 5, 6, 9, 10, 14, 15, 17, 21,22,23, 27].

All frameworks for interval analysis and exact real computation are based on functions whose input and output are real intervals. When we compose two such functions, the output of the first function serves as the input to the second function. An implementation of these frameworks in a functional programming language follows this same pattern; see for example the lazy Haskell implementation of IC-Reals for Exact Real Computation [1], which uses linear fractional transformations as developed in [14, 22].

An important feature of working with a calculus consisting of functions with interval or imprecise input/output is that even when we deal with elementary functions such as polynomials we cannot restrict ourselves to their canonical (maximal) extensions to intervals [21]. These canonical extensions take a compact interval to its forward image under the function. In fact, these extensions are not closed under, for example, multiplication. Thus, the real-valued map of a real variable \(x\mapsto x^2\) when implemented with interval input by \(x\mapsto x\times x\), using multiplication of two copies of the input interval, is not the canonical extension of the quadratic map of real numbers: it evaluates for example \([-1,1]^2\) to \([-1,1]\) rather than [0, 1], which is what the canonical extension of the quadratic map evaluates to. In general, we need to work with any Scott continuous map of type \(\mathbf{I}{\mathbb R}\rightarrow \mathbf{I}{\mathbb R}\) or, in higher dimension, of type \(\mathbf{I}{\mathbb R}^n\rightarrow \mathbf{I}{\mathbb R}\), where \(\mathbf{I}{\mathbb R}^n\) denotes the domain of hyper-rectangles of \({\mathbb R}^n\).

In the past 60 years, interval analysis has grown as a distinct interdisciplinary subject to impact on nearly all areas of mathematical and numerical analysis including computer arithmetic, linear algebra, integration, solution of initial value problems and partial differential equations to correct solutions in mathematical optimisation and robotics; see [20]. It is natural to ask if the domain of application of interval analysis and exact computation can be extended to the derivative of functions, i.e., whether one can take a kind of derivative of a map which takes a compact interval or a compact hyper-rectangle as input.

In [11], the notion of a domain-theoretic sub-differentiation of maps which have non-empty and compact intervals as inputs and outputs was introduced. The restriction of these maps to real numbers turns out to be locally Lipschitz maps of type \({\mathbb R}\rightarrow {\mathbb R}\) and the sub-differential restricted to real numbers has been shown to be the same as the Clarke sub-gradient [8]. A major problem, however, is that the framework in [11], which only deals with one-dimensional maps of type \(\mathbf{I}{\mathbb R}\rightarrow \mathbf{I}{\mathbb R}\) is not accompanied with a Stone duality framework and thus, even in dimension one, cannot be used in order to handle program logic and predicate transformers.

In [7], a typed lambda calculus in the framework of an extension of Real PCF [6, 17, 22] was introduced in which in particular continuously differentiable and more generally Lipschitz functions can be defined. Given an expression representing a real-valued function of a real variable in this language, one is able to evaluate the expression on an argument, representing an interval, but also evaluate the generalised derivative, i.e., the L-derivative, equivalently the Clarke gradient, of the expression on an interval. The operational semantics of the language, which is equipped with \(\min \) and a weighed average, enjoys adequacy and a definability result proving that any computable Lipschitz map is definable in it. The denotational semantics is based on domain theory which in principle allows a program logic formulation of the computation, although this challenge has not been taken up yet.

In [13], a point free framework for sub-differentiation of real-valued locally Lipschitz functions on finite dimensional Euclidean spaces has been developed which provides a Stone duality for the Clarke gradient and thus enables a program logic view of differentiation. However, the induced logical framework cannot be employed for the class of functions with imprecise input/output used in exact computation since, as already pointed out, this class necessarily contains general extensions of real-valued locally Lipschitz maps of finite dimensional Euclidean spaces.

In this paper, we formulate a new notion of a tie of functions with imprecise input/output, which, in one dimension, represents a modification of the corresponding notion in [12]. This allows us to develop a Scott continuous sub-differential for functions with hyper-rectangles in \(\mathbb {R}^n\) as inputs and compact intervals in \(\mathbb {R}\) as output, which are used in exact computation. We show that a weaker calculus compared to that for the Clarke sub-gradient is satisfied in this interval framework. In addition we construct a logical framework for sub-differentiation of locally Lipschitz maps of type \(\mathbf{I}\mathbb {R}^n\rightarrow \mathbf{I}\mathbb {R}\). The basic Stone duality results developed in [13] are then extended to sub-differentiation of such interval maps.

1.1 Background

We assume the reader is familiar with basic elements of topology and domain theory. Following the definition in [18], by a domain we mean a continuous dcpo (directed complete partial order). All the domains we use in this paper are bounded complete as well. By \(\mathbf {C}(\mathbb {R}^n)\), we denote the domain of non-empty convex and compact subsets of \({\mathbb R}^n\) ordered with reverse inclusion and augmented with \(\bot =\mathbb {R}^n\) as the bottom element. If \(C_1, C_2\in \mathbf {C}(\mathbb {R}^n)\) then the way-below relation is given by \(C_1\ll C_2\) iff \(C_1^{\circ }\supset C_2\), where \(S^\circ \) is the interior of the set S. By \(\mathbf {I}\mathbb {R}^n\), we denote the sub-domain of non-empty compact hyper-rectangles with faces parallel to coordinate hyper-planes of \(\mathbb {R}^n\). The Euclidean norm of \(x\in {\mathbb R}^n\) is denoted by \(\Vert x\Vert \).

The lattice of open subsets of a topological space X is denoted by \(\varOmega (X)\). The Scott topology of a domain D is, however, written as \(\sigma _D\). The closure of \(S\subset X\) is denoted by \(\overline{S}\). The upper topology, equivalently the Scott-topology, of \(\mathbf {C}(\mathbb {R}^n)\) has a basis of the form

$$ \square O=\{C\in \mathbf {C}(\mathbb {R}^n):C\subset O\}, $$

where O belongs to a basis of open and convex subsets of \(\mathbb {R}^n\).

Given an open set \(a\subset X\) of a topological space and an element \(b\in D\) of a domain D, the single-step function \(b\chi _{a}:X\rightarrow D\) is defined by \(b\chi _{a}(x)=b\) if \(x\in a\) and \(\bot \) otherwise. A non-empty compact real interval x is written as \(x=[x^-,x^+]\). For a map \(f:X\rightarrow Y\) of topological spaces, f[S] denotes the image of the set \(S\subset X\).

The three operations of addition of two vectors, scalar multiplication of a vector and a real number, and the inner product of two vectors can be extended to \(\mathbf{C}({\mathbb R}^n)\) to obtain the following three Scott continuous maps:

  1. (i)

    \(-+-:\mathbf {C}(\mathbb {R}^n)\times \mathbf {C}(\mathbb {R}^n)\rightarrow \mathbf {C}(\mathbb {R}^n)\) with \(A+B=\{a+b:a\in A, b\in B\}\),

  2. (ii)

    \(-\times -:{\mathbb R}\times \mathbf{C}({\mathbb R}^n)\rightarrow \mathbf{C}({\mathbb R}^n)\) with \(rA=\{rx:x\in A\}\), and,

  3. (iii)

    \(-\cdot -:\mathbf {C}(\mathbb {R}^n)\times \mathbf {C}(\mathbb {R}^n)\rightarrow \mathbf {I}\mathbb {R}\) with \(A\cdot B=\{a\cdot b:a\in A, b\in B\}\).

These three operations have well-defined restrictions to \(\mathbf{I}{\mathbb R}^n\). In addition, in this paper, we will consider their higher order extension to sets of sets. For example, if \(a_1,a_2\in \varOmega ({\mathbb R})\) are open subsets, then \(\Box a_1,\Box a_2\in \sigma _{\mathbf{C}({\mathbb R}^n)}\) and we have:

$$ (\square a_1)\cdot (\square a_2):= \{x_1\cdot x_2:x_1\in \square a_1,x_2\in \square a_2\} $$

Moreover:

Proposition 1

  1. (i)

    The modal operator \(\mathord {\Box }:\varOmega ( {\mathbb R}^n)\rightarrow \sigma _{\mathbf{C}({\mathbb R}^n)}\) preserves meets, i.e., \(\mathord {\Box } O_1\wedge \mathord {\Box } O_2=\mathord {\Box } (O_1\wedge O_2)\) for all \(O_1,O_2\in \varOmega ( {\mathbb R}^n)\).

  2. (ii)

    The way-below relation satisfies \(O_1\ll O_2\) if and only if \(\mathord {\Box } O_1\ll \mathord {\Box } O_2\) for all \(O_1,O_2\in \varOmega ( {\mathbb R}^n)\).

  3. (iii)

    If \(O_1,O_2\subset {\mathbb R}^n\) are open hyper-rectangles, then \(\Box (O_1+O_2)=\Box O_1+ \Box O_2\).

  4. (iv)

    If \(O\subset {\mathbb R}^n\) is a convex open set and \(a\subset {\mathbb R}^n\) is a hyper-rectangle, then \(\Box (O\cdot a)=(\Box O)\cdot (\Box a)\).

Next, we present the notion of Clarke’s sub-gradient [4]. Recall that a map \(f:U\subset \mathbb {R}^n\rightarrow \mathbb {R}\), where U is an open set, is locally Lipschitz if all points in U have an open neighbourhood \(O\subset U\) with a constant \(k\ge 0\) such that \(|f(x)-f(y)|\le k\Vert x-y\Vert \) for all \(x,y\in O\). The generalized directional derivative of a locally Lipschitz f at x in the direction of v is defined as follow:

$$ f^{\circ }(x;v)=\limsup _{y\rightarrow x\; t\rightarrow 0^+}\frac{f(y+tv)-f(y)}{t} $$

The Clarke subgradient of f at x, denoted by \(\partial f(x)\) is a convex and compact subset of \(\mathbb {R}^n\) and is defined by:

$$\begin{aligned} \partial f(x)=\{w\in \mathbb {R}^n:f^{\circ }(x;v)\ge w\cdot v \text { for all } v\in \mathbb {R}^n\} \end{aligned}$$
(1)

The sub-gradient function \(\partial f:U\subset {\mathbb R}^n\rightarrow \mathbf{C}({\mathbb R}^n)\) is upper continuous, equivalently Scott continuous. Moreover, the Clarke sub-gradient satisfies a weak calculus. For locally Lipschitz maps \(f,g:U\subseteq {\mathbb R}^n\rightarrow {\mathbb R}\),

  1. (i)

    Sum: \(\partial f(x)+\partial g(x)\supseteq \partial (f+g)(x)\).

  2. (ii)

    Product: \((\partial f(x)) g(x)+ f(x) (\partial g(x))\supseteq \partial (f\cdot g)(x)\)

  3. (iii)

    Chain  rule: For \( f,g:{\mathbb R}\rightarrow {\mathbb R}, \partial f(g(x))\cdot \partial g(x)\supseteq \partial (f\circ g)(x)\).

The notion of the L-derivative, equivalent to the Clarke sub-gradient, for real-valued functions on finite dimensional Euclidean spaces has the following ingredients [8]. A function \(f:U\subset \mathbb {R}^n\rightarrow \mathbb {R}\) has a non-empty generalized Lipschitz constant \(b\in \mathbf {C}(\mathbb {R}^n)\) in a non-empty convex open set \(a\subset \mathbb {R}^n\) if for all \(x,y\in a\) we have \(f(x)-f(y)\in b\cdot (x-y)\). The collection of all functions that have generalized Lipschitz constant b in a is denoted by \(\delta (a,b)\), called the tie of a with b. The collection of all single-step functions \(b\chi _a\) with \(a\subset U\) and \(f\in \delta (a,b)\) is bounded in \((U\rightarrow \mathbf {C}(\mathbb {R}^n))\) and thus the L-derivative of f defined as

$$ \mathcal {L}f=\sup \{b\chi _a:f\in \delta (a,b)\} $$

is Scott-continuous function. Moreover, we have \(\mathcal {L} f=\partial f\).

1.2 Stably Locally Compact Space and Semi-strong Proximity Lattice

We recall that in geometric logic one uses the open sets of a topological space as propositions or semi-decidable properties [25, 26]. If X is a topological space and \(\varOmega (X)\) its lattice of open sets, a propositional geometric theory is constructed as follows: For every open set \(a\in \varOmega (X)\), define a proposition \(P_a\), i.e., every open set of X provides a property or predicate. For open sets a and b with \(a\subseteq b\) stipulate: (i) \(P_a\vdash P_b\). For a family of open sets S, stipulate: (ii) \(P_{\cup S}\vdash \bigvee _{a\in S} P_a\). For a finite family of open sets S, stipulate: (iii) \(\bigwedge _{a\in S}P_a\vdash P_{\cap S}\). The converses of (ii) and (iii) follow from (i). The nullary disjunction in (ii) is interpreted as false and the nullary conjunction in the converse of (iii) is interpreted as truth, i.e., \(P_{\emptyset } \vdash \mathbf {false}\) and \(P_X\vdash \mathbf {truth}\).

We regard \(x\in X\) as a model of the theory in which \(P_a\) is interpreted as true iff \(x\in a\), i.e., iff \(x\in a\), or, a point is a model of a proposition if it is in the open set representing the proposition. It is possible that different points give rise to the same model, i.e., satisfy the same open sets, and it is also possible that a model does not arise by points in X in this way. For so-called sober spaces, as we will define below, we do have a one-to-one correspondence between points and models.

A topological space X is called stably locally compact [2, 18] if it is sober, locally compact and if the intersection of two compact saturated sets is compact. Recall that X is sober if its points are in bijection with the completely prime filters of its lattice of open sets. (A set is saturated if it is the intersection of its open neighbourhoods.) Equivalently, X is stably locally compact if and only if its lattice of open sets is a distributive continuous lattice which is also arithmetic, i.e., its way-below relation satisfies:

$$ O\ll O_1, O_2 \Rightarrow O\ll O_1\wedge O_2 $$

The spaces \({\mathbb R}^n\), \(\mathbf{I}{\mathbb R}^n\) and \(\mathbf{C}({\mathbb R}^n)\) are all stably locally compact spaces. The way-below relation for \(\varOmega (\mathbb {R}^n)\) is given by \(O_1\ll O_2\) iff \(\overline{O_1}\) is compact and \(\overline{O_1}\subset O_2\), whereas the way-below relation in \(\mathbf{C}({\mathbb R}^n)\), and thus \(\mathbf{I}{\mathbb R}^n\), is given by Proposition 1. We can obtain a finitary representation of these spaces by a sub-lattice of open sets as we will now describe.

A semi-strong proximity lattice [13] consists of a tuple \((B; \vee ,\wedge ,0,1;\prec )\) in which \((B;\vee ,\wedge ,0,1)\) is a distributive lattice such that \(\prec \) is a binary relation on B with \(\prec =\prec \circ \prec \) satisfying:

  1. 1.

    \(\forall a\in B\; M\subset _f B.\, M\prec a\Leftrightarrow \bigvee M\prec a\).

  2. 2.

    \(\forall a\in B.\,a\ne 1\Rightarrow a\prec 1\).

  3. 3.

    \(\forall a, a_1, a_2\in B.\,a\prec a_1,a_2\Leftrightarrow a\prec a_1\wedge a_2\).

  4. 4.

    \(\forall a,x,y\in B.\, a\prec x\vee y \Rightarrow \)

    \( \exists x',y'\in B.\, x'\prec x\, \& \, y'\prec y\, \& \,a\prec x'\vee y'\).

Here, \(M\subset _f B\) means that M is a finite (possibly empty) subset of B, and \(M\prec a\) means that \(\forall m\in M.\, m\prec a\).

The relation \(R\subseteq B_1\times B_2\), between two semi-strong proximity lattice, is a localic approximable mapping if it satisfies:

  1. 1.

    \(R\,\circ \prec _2=R\)

  2. 2.

    \(\prec _1 \circ \,R=R\).

  3. 3.

    \(\forall M\subset _f B_1\forall b\in B_2.\, M\,R\,b\iff \bigvee M\,R\,b\).

  4. 4.

    \(\forall a\in B_1.\, a\ne 1\Rightarrow a\, R\, 1\).

  5. 5.

    \( \forall a\in B_1\forall a_1, a_2\in B_2.\, a\,R\, a_1\, \& \, a\, R\, a_2\Leftrightarrow a\, R\, a_1\wedge a_2\).

  6. 6.

    \(\forall a\in B_1\forall M\subset _f B_2.\, a\,R\,\bigvee M\,\Rightarrow \)

    \( \exists N\subset _f B_1.\, a\,\prec _1 \bigvee N\, \& \, \forall n\in N\exists m\in M.\, n\,R\,m\).

The identity approximable mapping on B is \(\prec _B\) and composition of approximable mappings is the usual composition of the relations in the same order as for functions.

Let SL-Compact denote the category of all stably locally compact spaces and continuous functions and let Semi-Strong PL denote the category of semi-strong proximity lattice and approximable mappings. The following functors between these categories establish an equivalence between them [13, 19].

$$ \begin{aligned}&A:\text{ SL-Compact }\rightarrow \text{ Semi-Strong } \text{ PL }\\ {}&G:\text{ Semi-Strong } \text{ PL }\rightarrow \text{ SL-Compact } \end{aligned} $$

Given a stably locally compact space X, fix a basis B of its topology which is closed under finite intersections and let A(X) be the semi-strong proximity lattice based on B. Given a continuous function \(f:X_1\rightarrow X_2\) between two stably locally compact spaces, we have a localic approximable mapping \(A_f:A(X_1)\rightarrow A(X_2)\) given by \(a\,A_f\,b\) iff \(a\ll f^{-1}(b)\).

Given a semi-strong proximity lattice B, the spectrum \(\mathsf{spec (B)}\) of B is the set of all prime filters of B. For \(x\in B\) let \(\mathcal {O}_x=\{F\in \mathsf{spec(B)}:x\in F\}\). The collection of \(\mathcal {O}_x\)’s, \(x\in B\), is a base of a topology over \(\mathsf{spec(B)}\). Put,

$$\begin{aligned} G(B)={spec(B)} \end{aligned}$$

Given a localic approximable mapping \(R:B_1\rightarrow B_2\) define,

$$\begin{aligned} G_R:\mathsf{spec (B_1)}\rightarrow \mathsf{spec(B_2)} \end{aligned}$$

by \(G_R(F)=\{b_2\in B_2:\exists b_1\in F. b_1\, R\,b_2\}\). We have, \(A_{G_R}=R\) and \(G_{A_f}=f\). Thus, the category of semi-strong proximity lattice with approximable mappings is equivalent to the category of stably locally compact spaces and continuous functions [13].

We now construct some canonical bases of \(\mathbf{C}({\mathbb R}^n)\) and \(\mathbf{I}{\mathbb R}^n\), which provide us with the semi-strong proximity lattices these spaces can be represented by. Let \(B^0_{\mathbb {R}^n}\), respectively \(B^0_U\), for \(U\subset {\mathbb R}^n\), be any basis of \(\mathbb {R}^n\), respectively U, that consists of bounded convex open sets and is closed under finite intersections. We let \(B_{\mathbb {R}^n}\), respectively \(B_U\), denote the semi-strong proximity lattice generated by \(B^0_{\mathbb {R}}\), respectively \(B^0_U\). This means that every element of \(B_{\mathbb {R}}\), respectively \(B_U\), is a finite join of elements of \(B^0_{\mathbb {R}^n}\), respectively \(B^0_U\) [13].

It now follows, by Proposition 1, that \(B^0_{\mathbf {C}(\mathbb {R}^n)}=\{\Box a:a\in B_{\mathbb {R}^n}^0\}\) is a basis of the Scott topology \(\sigma _{\mathbf {C}(\mathbb {R}^n)}\), which is closed under finite intersections. Let \(B_{\mathbf {C}(\mathbb {R}^n)}\) be the semi-strong proximity lattice generated by \(B^0_{\mathbf {C}(\mathbb {R}^n)}\). Thus, each element of the semi-strong proximity lattice \(B_{\mathbf {C}(\mathbb {R}^n)}\) is the finite join of elements of \(B^0_{\mathbf {C}(\mathbb {R}^n)}\).

Finally, let \({ \mathcal T}(U)\) be a basis of \(U\subset {\mathbb R}^n\) consisting of open hyper-rectangles in U with faces parallel to the coordinate planes and let \({ \mathcal T}:={ \mathcal T}({\mathbb R}^n)\). Then \(B^0_{\mathbf {I}\mathbb {R}^n}=\{\Box a:a\in { \mathcal T}\}\) is a basis for \(\sigma _{\mathbf{I}{\mathbb R}^n}\). By using \({ \mathcal T}(U)\), we similarly obtain a basis \(B^0_{\mathbf {I}U}\) for \(\mathbf {I}U\subset \mathbf{I}{\mathbb R}^n\). Again by Proposition 1(i) these bases are closed under finite intersections. We let \(B_{\mathbf {I}\mathbb {R}^n}\), respectively, \(B_{\mathbf{I}U}\) be the semi-strong proximity lattices generated by \(B^0_{\mathbf {I}\mathbb {R}^n}\), respectively, \(B^0_{\mathbf{I}U}\). Thus, each element of \(B_{\mathbf {I}\mathbb {R}^n}\), respectively, \(B_{\mathbf{I}U}\), is the finite join of elements of \(B^0_{\mathbf {I}\mathbb {R}^n}\), respectively, \(B^0_{\mathbf{I}U}\).

The functors A and G thus provide a bijection between the two hom-sets:

$$\begin{aligned} (\mathbf {I}U\rightarrow \mathbf {I}\mathbb {R}) \mathrel {\mathop {\leftrightarrows }^{\mathrm {G}}_{\mathrm {A}}} (B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}) \end{aligned}$$

and between the two hom-sets:

$$ (\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n))\mathrel {\mathop {\leftrightarrows }^{\mathrm {G}}_{\mathrm {A}}}(B_{\mathbf {I}U}\rightarrow B_{\mathbf {C}(\mathbb {R}^n)}) $$

These bijections are used later to deduce our Stone duality results.

1.3 Related Work

Differentiation in logical form for functions of type \(U\subseteq \mathbb {R}^n\rightarrow \mathbb {R}\) was introduced in [13]. These maps were represented by localic approximable mappings of type \(B_U\rightarrow B_{\mathbb {R}}\), and the localic approximable mapping of the L-derivative of these functions have the type \(B_U\rightarrow B_{\mathbf {C}(\mathbb {R}^n)}\). The strong tie of a with b, denoted by \(\delta _s(a,b)\), was defined as the collection of all functions \(f:a\subseteq U\rightarrow \mathbb {R}\) such that there exists \(a'\in B_{\mathbb {R}}^0\) and \(b'\in \mathbf {C}(\mathbb {R}^n)\) with \(a\ll a'\), \(b\ll b'\) and \(f\in \delta (a',b')\).

The approximable mappings \(R:B_U\rightarrow B_{\mathbb {R}}\) has Lipschitz constant \(O\in B_{\mathbf {C}(\mathbb {R}^n)}\) in \(a\in B_U\), denoted by \(R\in \varDelta (a,O)\), if we have:

$$ \begin{aligned}&\forall a_1,a_2\prec a,(a_1,a_2)\in \mathsf{Sep}, \exists a_1',a_2'\in B_{\mathbb {R}}.\\ {}&a_1\,R\,a_1', a_2\,R\,a_2',a_1'-a_2'\prec O\cdot (a_1-a_2) \end{aligned} $$

where the separation predicate \(\mathsf{Sep}\subset B_U\times B_U\) means \((a_1,a_2)\in \mathsf{Sep}\) if there exists \(a_1',a_2'\) such that \(a_1\prec a_1', a_2\prec a_2'\) and \(a_1'\wedge a_2'=0\). The strong knot \(\varDelta _s(a,O)\) is defined as the set of approximable mappings \(R:B_U\rightarrow B_{\mathbb {R}}\) such that there exists \(a'\in B_U\), \(O'\in B_{\mathbf {C}(\mathbb {R}^n)}\) with \(a\prec a'\), \(O'\prec O\) and \(R\in \varDelta (a',O')\).

The strong ties and strong knots are dual to each others, i.e., \(R\in \varDelta _s(a,O)\) iff \(G_R\in \delta _s(a,\overline{O})\). The Lipschitzian derivative of \(R:B_U\rightarrow B_{\mathbb {R}}\) is defined as the approximable mapping

$$ \mathsf{L}(R)=\sup \{A_{\overline{O}\chi _a}:R\in \varDelta _s(a,O)\} $$

It turns out that \(\mathsf{L}(R)=A_{\mathcal {L}G_R}\) and we have a weak calculus which matches that for the Clarke sub-gradient stated after Eq. (1), i.e., \( \mathsf{L}(R_1)+\mathsf{L}(R_2)\subseteq \mathsf{L}(R_1+R_2) \) and \( R_1\cdot \mathsf{L}(R_2)+R_2\cdot \mathsf{L}(R_1)\subseteq \mathsf{L}(R_1\cdot R_2) \), and if at least one of \(R_1\) and \(R_2\) is a continuously differentiable approximable mapping then equality holds. A weak form of the chain rule also holds for composition of approximable mappings corresponding to that for the Clarke sub-gradient.

2 L-derivative with Imprecise Inputs

We start by defining a notion of tie for Scott continuous map of type \(f:\mathbf{I}U\rightarrow \mathbf{I}{\mathbb R}\), for an open convex subset \(U\subset {\mathbb R}^n\). From now on, in the rest of the paper, we assume \(f:\mathbf{I}U\rightarrow \mathbf{I}{\mathbb R}\) is Scott-continuous.

Definition 1

Let \(f:\mathbf {I} U\subseteq \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) where \(U\subset \mathbb {R}^n\) is an open set, be Scott continuous and \(a\in { \mathcal T}(U)\), an open hyper-rectangle in U, and \(b\in \mathbf {C}(\mathbb {R}^n)\). We say f has a generalized Lipschitz constant b in \(\square a\) and write \(\delta (\square a,b)\) if we have:

$$ \forall x, y\in \square a, x\cap y=\emptyset .\, f(x)-f(y)\subseteq b\cdot (x-y) $$

In the one dimensional case, this new notion is a modification of that in [12] as we in Definition 1, require the hyper-rectangles x and y to be disjoint, i.e., inconsistent in \(\mathbf{I}U\). Thus, the condition for membership of a tie is weaker. We will need this weaker condition in order to develop the Stone duality result later in the paper.

We show that despite this weaker notion, if \(f\in \delta (\Box a,b)\) with \(b\ne \bot \), then f preserves maximal elements and its restriction to maximal elements gives a Lipschitz map. In other words f is the extension of a classical Lipschitz function in \(\mathbf{I}a\).

Proposition 2

Let \(f\in \delta (\square a,b)\), where \(a\subset \mathbb {R}^n\) is a open hyper-rectangle and \(b\in \mathbf {C}(\mathbb {R}^n)\setminus \{\bot \}\), then for each \(x\in a\), \(f(\{x\})\in \mathbf {I}\mathbb {R}\) is maximal and the induced function \(\hat{f}:a\subset \mathbb {R}^n\rightarrow \mathbb {R}\) is Lipschitz and satisfies:

$$\begin{aligned} \forall x_1,x_2\in a.\, (b\cdot (x_1-x_2))^-\le \hat{f}(x_1)-\hat{f}(x_2)\le (b\cdot (x_1-x_2))^+ \end{aligned}$$
(2)
$$\begin{aligned} \forall x_1,x_2\in a.\,|\hat{f}(x_1)-\hat{f}(x_2)|\le \Vert b\Vert \Vert x_1-x_2\Vert , \end{aligned}$$
(3)

where \(\Vert b\Vert =\max \{\Vert L\Vert |L\in b\}\).

Corollary 1

If \(f\in \delta (\square a,b)\) then \(\hat{f}\in \delta (a,b)\).

Definition 2

We say a Scott continuous function of type \(\mathbf{I}U\subset \mathbf{I}{\mathbb R}^n\rightarrow \mathbf{I}{\mathbb R}\) is locally Lipschitz in \(\square a\), for \(a\in { \mathcal T}(U)\), if it belongs to a tie \(\delta (\square a,b)\) with \(b\ne \bot \).

Given a continuous function \(f:U\subseteq \mathbb {R}^n\rightarrow \mathbb {R}\), its maximal extension to a Scott continuous function \(\mathbf {I}U\subseteq \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) is denoted by \(\mathbf{I}f\) with \(\mathbf {I}f(x)=f[x]\) for \(x\in \mathbf {I}U\) when \(x\ne \bot \) and \(\mathbf{I}f(\bot )=\bot \).

Corollary 2

\(f\in \delta (a,b)\) iff \(\mathbf {I}f\in \delta (\square a,b)\).

If \((A,\sqsubseteq )\) is a dcpo then the consistency predicate \(\mathsf{Con}_{(A,\sqsubseteq )}\) and \(\mathsf{Con}_{(A,\ll )}\) for a finite subset \(\{a_i:i\in I\}\) with respect to \(\sqsubseteq \) and \(\ll \) are defined as follow:

$$ \mathsf{Con}_{(A,\sqsubseteq )}\{a_i:i\in I\}\Longleftrightarrow \exists a\in A,\forall i\in I.\,a_i\sqsubseteq a $$

and

$$ \mathsf{Con}_{(A,\ll )}\{a_i:i\in I\}\Longleftrightarrow \exists a\in A,\forall i\in I.\,a_i\ll a $$

For the collection \((b_i\chi _{a_i})_{i\in I}\) or \((b_i\chi _{\square a_i})_{i\in I}\) for finite indexing set I where \(a_i\in \varOmega (\mathbb {R}^n)\) are open hyper-rectangles and \(b_i\in (D,\sqsubseteq )\), the function space consistency predicate \(\mathsf{Con}_{\mathbb {R}^n\rightarrow D}\) or \(\mathsf{Con}_{\mathbf {I}\mathbb {R}^n\rightarrow D}\) is defined as follows:

$$ \mathsf{Con}_{\mathbb {R}^n\rightarrow D}(b_i\chi _{a_i})_{i\in I}\Longleftrightarrow \forall J\subseteq I.\,[\mathsf{Con}_{(\varOmega (\mathbb {R}^n),\gg )}\{a_i:i\in J\}\Rightarrow \mathsf{Con}_{(D,\sqsubseteq )}\{b_i:i\in J\}] $$
$$ \mathsf{Con}_{\mathbf {I}\mathbb {R}^n\rightarrow D}(b_i\chi _{\square a_i})_{i\in I}\Longleftrightarrow \forall J\subseteq I.\,[\mathsf{Con}_{(\varOmega (\mathbf {I}\mathbb {R}^n),\gg )}\{\square a_i:i\in J\}\Rightarrow \mathsf{Con}_{(D,\sqsubseteq )}\{b_i:i\in J\}]. $$

It follows that the supremum \(\sup _{i\in I}b_i\chi _{a_i}\) exists iff \( \mathsf{Con}_{\mathbb {R}^n\rightarrow D}(b_i\chi _{a_i})_{i\in I}\) and \(\sup _{i\in I}b_i\chi _{\square a_i}\) exists iff \(\mathsf{Con}_{\mathbf {I}\mathbb {R}^n\rightarrow D}(b_i\chi _{\square a_i})_{i\in I}\).

Proposition 3

For any indexing set J the family of step functions \((b_j\chi _{\square a_j})_{j\in J}\) is consistent if \(\bigcap _{j\in J}\delta (\square a_j,b_j)\ne \emptyset \).

Proof

Suppose \(f\in \bigcap _{j\in J}\delta (\square a_j,b_j)\) then \(\hat{f}\in \bigcap _{j\in J}\delta (a_j,b_j)\), and hence \((b_j\chi _{a_j})_{j\in J}\) is consistent, which implies \((b_j\chi _{\square a_j})_{j\in J}\) is consistent. \(\blacksquare \)

Recall that a crescent in \({\mathbb R}^n\) is the intersection of a closed and an open set. Given two points \(p,q\in {\mathbb R}^n\), we denote the closed, respectively open, line segment between them by \([p,q]=\{\lambda p+(1-\lambda )q: 0\le \lambda \le 1\}\), respectively \((p,q)=\{\lambda p+(1-\lambda )q: 0< \lambda <1\}\).

Proposition 4

We have \(\delta (\square a,b)\supseteq \bigcap _{j\in J}\delta (\square a_j,b_j)\) if \(b\chi _{\square a}\sqsubseteq \sup _{j\in J}b_j\chi _{\square a_j}\).

Proof

Let \(g:=\sup _{j\in J}b_j\chi _{\square a_j}\). Suppose \(b\chi _{\square a}\sqsubseteq \sup _{j\in J}b_j\chi _{\square a_j}\), then \(\Box a\subset \bigcup _{j\in J}\Box a_j\) and thus \(a\subset \bigcup _{j\in J} a_j\). In addition, by considering the restriction of g to the maximal elements of \(\mathbf{I}{\mathbb R}^n\), we find that a is partitioned by the open sets \(a_j\), \(j\in J\), into a finite number of disjoint crescents \(c_i\), \(i\in I\), with

$$\begin{aligned} g(\{r\})=\sup _{c_i\subset a_j}b_j\sqsupseteq b \end{aligned}$$

for \(r\in c_i\). Let \(f\in \bigcap _{j\in J}\delta (\square a_j,b_j)\). We show that \(f\in \delta (\square a,b)\). Suppose we have two hyper-rectangles \(x,y\in \Box a\) with \(x\cap y=\emptyset \). Let the points \(p\in x\) and \(q\in y\) be such that \(\Vert p-q\Vert \) is the minimum distance between x and y. Then [pq] is partitioned by the crescents \(c_i\), \(i\in I\), into a finite number of one-dimensional intervals such that the one-dimensional interior of each is contained in \(c_i\) for some \(i\in I\). Let \(r_0,r_1,\ldots ,r_k\in {\mathbb R}^n\) be the boundary points of these intervals ordered from p to q. Then, using the continuity of \(\hat{f}\), we have:

$$\begin{aligned} f(\{r_t\})-f(\{r_{t+1}\})\subseteq \sup _{(r_t,r_{t+1})\subseteq c_j}b_j\cdot (\{r_t\}-\{r_{t+1}\})\subseteq b\cdot ( \{r_{t}\}- \{r_{t+1}\}) \end{aligned}$$

for \(0\le t\le n-1\). Since \(x\in \Box a\), there exists \(j\in J\) with \(x\in \Box a_j\). Moreover, \(x\subseteq a_j\) iff \(r_0\in \overline{a_j}\). Similarly, \(y\subseteq a_j\) iff \(r_k\in \overline{a_j}\). From these relations, we obtain:

$$\begin{aligned} f(x)-f(\{r_0\})\subseteq \sup _{x\subset a_j}b_j\cdot (x-\{r_0\}),\quad f(\{r_k\})-f(y)\subseteq \sup _{y\subset a_j}b_j\cdot (\{r_k\}-y) \end{aligned}$$

Thus,

$$\begin{aligned} f(x)-&f(y)=f(x)-f(\{r_0\})+f(\{r_0\})-\cdots -f(\{r_k\})+f(\{r_k\})-f(y)\\&\quad \subseteq b\cdot (x-\left( \sum _{t=0}^{k-1}f(\{r_t\})-f(\{r_t\})\right) -y)=b\cdot (x-y)\,\blacksquare \end{aligned}$$

Definition 3

The derivative of a Scott continuous map \(f:\mathbf {I}U\subset \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) is the map:

$$ \mathcal {L}f=\sup _{f\in \delta (\square a,b)}b\chi _{\square a}:\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n) $$

where U is a convex open subset of \(\mathbb {R}^n\).

Theorem 1

  1. (i)

    \(\mathcal {L}f\) is well-defined and Scott continuous.

  2. (ii)

    \(f\in \delta (\square a,b)\) iff \(b\chi _{\square a}\sqsubseteq \mathcal {L}f\).

Proof

  1. (i)

    Let the indexing set J be defined by \(j\in J \Longleftrightarrow f\in \delta (\square a_j,b_j)\), then \(f\in \bigcap _{j\in J}\delta (\square a_j,b_j)\). Thus, by Proposition 3 \((b_j\chi _{\square a_j})_{j\in J}\) is consistent therefore, \(\mathcal {L}f=\sup _{f\in \delta (\square a,b)}b\chi _{\square a}\) exists and is Scott continuous.

  2. (ii)

    If \(f\in \delta (\square a,b)\) then clearly \(b\chi _{\square a}\sqsubseteq \mathcal {L}f\). Now take \(a'\ll a\) and \(b'\ll b\). Then \(b'\chi _{\square a'}\ll b\chi _{\square a }\sqsubseteq \mathcal {L}f\) and there exists a finite indexing set J such that \(b'\chi _{\square a'}\sqsubseteq \sup _{j\in J}b_j\chi _{\square a_j}\) and \(f\in \delta (\square a_j,b_j)\) for \(j\in J\). Now by Proposition 4, we have \(\bigcap _{j\in J}\delta (\square a_j,b_j)\subseteq \delta (\square a',b')\), and thus, \(f\in \delta (\square a',b')\). From this, it follows that \(f\in \delta (\square a ,b )\)\(\blacksquare \)

If \(f:U\subseteq {\mathbb R}^n\rightarrow {\mathbb R}\) is a locally Lipschitz map, then the Clarke sub-gradient \(\mathcal{L}f:U\rightarrow \mathbf{C}({\mathbb R}^n)\) extends, by Scott’s extension theory for densely injective spaces [24], to a Scott continuous map \(\mathbf{I}(\mathcal{L}f):\mathbf{I}U\rightarrow \mathbf{C}({\mathbb R}^n)\). We then have:

Proposition 5

$$\begin{aligned} \mathcal{L}(\mathbf{I}f)=\mathbf{I}( \mathcal{L} f) \end{aligned}$$

Proof

This follows from the relation:

$$\begin{aligned} f\in \delta (a,b)\iff \mathbf{I}f\in \delta (\Box a,b), \end{aligned}$$

for all \(a\in \varOmega (U)\) and \(b\in \mathbf{C}({\mathbb R}^n)\)\(\blacksquare \)

The following example shows that in the context of the L-derivative of interval functions, Clarke’s weak calculus no longer holds for Sum.

Example 1

Let \(f,g:\mathbf {I}\mathbb {R}\rightarrow \mathbf {I}\mathbb {R}\) defined by \(f(x)=x\) and \(g(x)=-x\), then \(\mathcal {L}f(x)=\{1\}\) and \(\mathcal {L}g(x)=\{-1\}\) and thus \(\mathcal {L}f(x)+\mathcal {L}g(x)=\{0\}\). On the other hand, \((f+g)(x)=f(x)+g(x)=x-x\) and it follows that \(f+g\notin \delta (\square a,\{0\})\), for any open set \(a\subset {\mathbb R}\), and consequently \(\mathcal {L}(f+g)\ne \{0\}\). Hence, \(\mathcal {L}(f+g)(x)\nsubseteq \mathcal {L}f(x)+\mathcal {L}g(x)\).

We say an interval \([r^-,r^+]\) is positive , respectively negative, if \(r^->0\), respectively \(r^+<0\). The above counter-example is the consequence of the fact that in interval arithmetic, while the relation \((u+v)w\subseteq uw+vw\) always holds for \(u,v,w\in \mathbf{I}{\mathbb R}\), the converse relation \((u+v)w\supseteq uw+vw\) may fail. However, if u and v are both positive or both negative then the converse also holds [21, p. 13].

We can obtain a weak calculus for sum and product of two functions f and g if we first use an operation that is routinely performed in interval analysis, namely to approximate the values \(\mathcal {L}f(x)\) and \(\mathcal {L}g(x)\) with the smallest axes aligned hyper-rectangle containing it, and then assume that the two induced hyper-rectangles have the same sign in each of their components. We now formalise this procedure.

Let \(H:\mathbf{C}({\mathbb R}^n)\rightarrow \mathbf{I}{\mathbb R}^n\) be the map that takes every convex compact set to the smallest axes aligned hyper-rectangle containing it. Then, it is easy to check that H is Scott continuous. Let \(\pi _i:{\mathbb R}^n\rightarrow {\mathbb R}\) be the projection of the ith coordinate and extend it pointwise to its maximal extension \(\mathbf{I}\pi _i:\mathbf{I}{\mathbb R}^n\rightarrow \mathbf{I}{\mathbb R}\). Define the predicate \(\mathsf{Sgn}\subset ( \mathbf{I}{\mathbb R}^n)^2\) by \((x,y)\in \mathsf{Sgn}\) if for each \(i=1,\dots ,n\) the two intervals \(\mathbf{I}\pi _i(x)\) and \(\mathbf{I}\pi _i(y)\) are either both positive or both negative.

Suppose \(x,y,z\in \mathbf {I}\mathbb {R}^n\) and \((y,z)\in \mathsf{Sgn}\), then the interval \(\mathbf{I}\pi _i(y)\mathbf{I}\pi _i(z)\) is positive for each \(i=1\dots ,n\) and we have \(x(y+z)=xy+xz\). In fact,

$$\begin{aligned} \mathbf{I}\pi _i(x)(\mathbf{I}\pi _i(y)+\mathbf{I}\pi _i(z))=\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(y)+\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(z), \end{aligned}$$

and hence:

$$ \begin{aligned} x(y+z)&=\sum _{i=1}^n\mathbf{I}\pi _i(x)(\mathbf{I}\pi _i(y)+\mathbf{I}\pi _i(z))= \sum _{i=1}^n\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(y)+\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(z)\\ {}&=\sum _{i=1}^n\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(y)+\sum _{i=1}^n\mathbf{I}\pi _i(x)\mathbf{I}\pi _i(z)=xy+xz \end{aligned} $$

Proposition 6

Suppose \(f,g:\mathbf{I}U\subseteq \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) are locally Lipschitz functions and \(x\in \mathbf{I}U\) is such that \((H(\mathcal {L}f(x)),H(\mathcal {L}g(x)))\in \mathsf{Sgn}\). Then:

  1. 1.
    $$\begin{array}{rcl} H(\mathcal {L}f(x))+H(\mathcal {L}g(x))&{}\supseteq &{}H(\mathcal {L}(f+g)(x))\\[1ex] \end{array}$$
  2. 2.

    If, in addition, \((f(x),g(x))\in \mathsf{Sgn}\), then we also have:

    $$\begin{array}{rcl} f(x)H(\mathcal {L}g(x))+g(x)H(\mathcal {L}f(x))&{}\supseteq &{} H(\mathcal {L}(fg)(x))\\ \end{array}$$

We will provide the proof for a weak form of the chain rule, which is more involved compared to sum and product. First consider the extended scalar multiplication \(M:\mathbf{C}({\mathbb R}^n)\times \mathbf{I}{\mathbb R}^+\rightarrow \mathbf{C}({\mathbb R}^n)\), where \({\mathbb R}^+\) is the set of non-negative reals, with \(M(b,x)= \{ur:u\in b, r\in x\}\). Then, M is well-defined and Scott continuous. For ease of presentation, we write \(M(b,x)=bx\).

Proposition 7

If \(g:\mathbf {I}U_1\subseteq \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) and \(f:\mathbf {I}U_2\subseteq \mathbf {I}\mathbb {R}\rightarrow \mathbf {I}\mathbb {R}\) and \(\mathsf{Im}(g)\subset \mathbf {I}U_2\) with \((\mathcal {L}f) (g(x))\in \mathbf{I}{\mathbb R}^+\), are Scott-continuous, then:

$$ ((\mathcal {L}f)\circ g)(x) \mathcal {L}g(x)\supseteq \mathcal {L}(f\circ g)(x) $$

3 Lipschitzian Approximable Mapping

Recall that, since \(\mathbf {I}\mathbb {R}^n\), \(\mathbf {C}(\mathbb {R}^n)\) and \(\mathbb {R}^n\) are stably locally compact space and the category of stably locally compact spaces with continuous functions and the category of semi-strong proximity lattice with approximable mappings are equivalent, any continuous function \(f:\mathbf {I}U\subset \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) defines an approximable mapping \(A_f:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) by \(\square aA_f\square a'\Longleftrightarrow \square a\ll f^{-1}(\square a')\). On the other hand any approximable mapping with type \(R:B_{\mathbf {I}\mathbb {R}^n}\rightarrow B_D\), where D is either \(\mathbf {I}\mathbb {R}\) or \(\mathbf {I}\mathbb {R}^n\) or \(\mathbf {C}(\mathbb {R}^n)\), gives us a continuous function \(G_R:\mathbf {I}\mathbb {R}^n\rightarrow D\).

Lemma 1

Let \(f:\mathbf {I}U\subset \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\) be a Scott continuous function such that \(f(\{x\})\) is singleton for all \(x\in U\). Suppose \(a_1\) is an open hyper-rectangle in U and \(a_2\) is an open interval. If \(\hat{f}:U\subset \mathbb {R}^n\rightarrow \mathbb {R}\) is the induced function with \(f(\{x\})=\{\hat{f}(x)\}\) then:

$$ \square a_1\ll f^{-1}(\square a_2) \Rightarrow a_1\ll \hat{f}^{-1}(a_2)\qquad \square a_1\ A_f\ \square a_2 \Rightarrow a_1\ A_{\hat{f}}\ a_2 $$

Recall the definition of the predicate \(\mathsf{Sep}\subset B_{\mathbb {R}}\times B_{\mathbb {R}} \) from Subsect. 1.3.

Definition 4

We say an approximable mapping \(R:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\), where \(U\subset \mathbb {R}^n\) is a convex open set, has Lipschitzian constant O in \(\square a\), with \(O\in B^0_{\mathbb {R}^n}\) and \(a\in { \mathcal T}(U)\), if:

$$ \begin{aligned}&\forall \, a_1, a_2\in { \mathcal T}(U).\,a_1,a_2\prec a\, \& \ (a_1, a_2)\in \mathsf{Sep}\ \exists \, a_1', a_2' \in B_{\mathbb {R}}.\\ {}&\square a_1\, R\, \square a_1',\square a_2\, R\, \square a_2'\ \& \ a_1'- a_2'\prec \, O\cdot ( a_1- a_2), \end{aligned} $$

and we say R is Lipschitzian in \(\Box a\). The set of all approximable mappings with the above property is denoted by \(\varDelta (\square a, O)\), called the knot of \(\square a\) and O.

Note that, by Proposition 1, the last formula in Definition 4 is equivalent to \(\Box a_1'- \Box a_2'\prec \,\Box O\cdot (\Box a_1-\Box a_2)\). Given this equivalence, it is simpler to use the formula without the modal operator \(\Box \) as we have done in this definition. By Proposition 1 and Stone duality, we have:

Proposition 8

Suppose \(f:\mathbf {I}U\rightarrow \mathbf {I}\mathbb {R}\) is a Scott continuous function such that \(f(\{x\})\) is singleton for every \(x\in U\). Then we have: \(A_{\hat{f}}\in \varDelta (a,O)\) if \(A_f\in \varDelta (\square a, O)\).

From \(\varDelta (\square a, O)\), a Lipschitz property of \(G_R\) can be deduced as follows.

Proposition 9

If \(R:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) is an approximable mapping such that \(R\in \varDelta (\square a, O)\) then:

$$ \forall x,y\in \Box a.\,x\cap y=\emptyset \,\Rightarrow \, G_R(x)-G_R(y)\subseteq \overline{O}\cdot (x-y) $$

Proof

Let \(x,y\in \square a\) and \(x\cap y=\emptyset \), then consider \( a_1, a_2\in { \mathcal T}(U)\) such that \((a_1, a_2)\in \mathsf{Sep}\) and \(x\in \square a_1, y\in \square a_2\). Hence, there exist \( a_1',a_2'\in B_{\mathbb {R}}\) such that \(\square a_i\,R\,\square a_i',i=1,2\) and:

$$ a_1'- a_2'\prec O\cdot ( a_1- a_2) $$

By Stone duality we have \(R=R_{G_R}\). Hence \(\square a_i\prec G_R^{-1}(\square a_i'), i=1,2\), and thus:,

$$ G_R(x)-G_R(y)\subseteq O\cdot (a_1-a_2). $$

Since this holds for all sufficiently small \(a_1\) and \(a_2\) that contain x and y respectively, we obtain: \( G_R(x)-G_R(y)\subseteq \overline{O}\cdot (x-y)\)\(\blacksquare \)

Corollary 3

If \(R\in \varDelta (\square a, O)\) then \(G_R\in \delta (\square a,\overline{O})\).

Thus, if \(A_f\) is a Lipschitzian approximable mapping of type \(B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) then f is a Lipschitz function of type \(\mathbf {I}U\rightarrow \mathbf {I}\mathbb {R}\) and hence \(f(\{x\})\) is a singleton for every \(x\in U\) and the induced function \(\hat{f}:U\rightarrow \mathbb {R}\) is also Lipschitz.

Now we are in a position to obtain duality results similar to those in [13] for functions of type \(\mathbf {I}U\subseteq \mathbf {I}\mathbb {R}^n\rightarrow \mathbf {I}\mathbb {R}\).

Proposition 10

Let \(f\in \delta (\square a,b)\) then for every \( a_0\in { \mathcal T}\) such that \( a_0\prec a\) and every \( O\in B^0_{\mathbb {R}^n}\) such that \(b\subset O\) we have \(A_f\in \varDelta (\square a_0,O)\).

Proof

Suppose \(a_0\prec a\). Let \(a_1, a_2\in { \mathcal T}(U)\) with \(( a_1, a_2)\in \mathsf{Sep}\) and \( a_1, a_2\prec a_0\). Then, since \(\overline{a_1}, \overline{a_2}\in \mathbf{I}U\), from definition of the tie \(\delta (\square a,b)\), we have,

$$ \begin{aligned} f(\overline{a_1})-f(\overline{a_2})&\subseteq b\cdot (\overline{a_1}-\overline{a_2})\\ {}&\subseteq O\cdot (a_1-a_2). \end{aligned} $$

Since \(f(\overline{a_1}),f(\overline{a_2})\in \mathbf{I}{\mathbb R}\) are compact, there exist open hyper-rectangles \(a_1',a_2'\in B_{\mathbb {R}}\) such that \(f(\overline{a_i})\subseteq a_i', i=1,2\), and \( a_1'-a_2'\prec O\cdot (a_1-a_2)\). This implies \(A_f\in \varDelta (\square a_0,O)\)\(\blacksquare \)

Example 2

Let \(f:\mathbf {I}\mathbb {R}\rightarrow \mathbf {I}\mathbb {R}\) be given by:

$$ f([x_1,x_2])=[x_1-\delta (x_2-x_1),x_2+\delta (x_2-x_1)] $$

for \(\delta >0\). The restriction \(\hat{f}\) of f to the maximal elements of \(\mathbf {I}\mathbb {R}\) is the identity function of type \(\hat{f}=\text{ Id }:\mathbb {R}\rightarrow \mathbb {R}\). Since \(\mathbf {I}\text{ Id }\ne f\), the map f is not the maximal extension of the identity map \(\text{ Id }\). On the other hand, \(A_f:B_{\mathbf {I}\mathbb {R}}\rightarrow B_{\mathbf {I}\mathbb {R}}\) satisfies \(A_f\in \varDelta (\square {\mathbb R},O)\) iff \((1-\delta ,1+\delta )\subseteq O\). However, \(A_{\hat{f}}\in \varDelta ({\mathbb R},O)\) iff \(1\in O\).

The following two propositions represent a domain isomorphism between the function space \((\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n))\) and the domain of approximable mappings \((B_{\mathbf {I}U}\rightarrow B_{\mathbf {C}(\mathbb {R}^n)})\) ordered by inclusion.

Proposition 11

  1. 1.

    For \(f_1,f_2:\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n)\) we have:

    $$f_1\sqsubseteq f_2\Longleftrightarrow A_{f_1}\subseteq A_{f_2} $$
  2. 2.

    For \(R_1,R_2:B_{\mathbf {I}U}\rightarrow B_{\mathbf {C}(\mathbb {R}^n)}\) we have:

    $$ R_1\subseteq R_2 \Longleftrightarrow G_{R_1}\sqsubseteq G_{R_2} $$

Proposition 12

  1. 1.

    If \((f_i)_{i\in I}\) is a directed set in \(\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n)\), with supremum \(f=\sup _{i\in I}f_i\), then \(\bigcup _{i\in I}A_{f_i}=A_f\) in \(\mathsf{App}(B_{\mathbf {I}U},B_{\mathbf {C}(\mathbb {R}^n)})\).

  2. 2.

    If \((R_i)_{i\in I}\) is a directed set in \(\mathsf{App}(B_{\mathbf {I}U},B_{\mathbf {C}(\mathbb {R}^n)})\) then \(\sup _{i\in I}G_{R_i}=G_R\) in \((\mathbf {I}U\rightarrow \mathbf {C}(\mathbb {R}^n))\) where \(R=\sup _{i\in I}R_i\).

Definition 5

If a is an open hyper-rectangle and O is a basic convex open set then the single-step approximable mapping \(\eta _{(\square a,O)}\) is defined as \(\eta _{(\square a,O)}=A_{\overline{O}\chi _{\square a}}:B_{\mathbf {I}U}\rightarrow B_{\mathbf {C}(\mathbb {R}^n)}\).

For defining the Lipschitzian derivative of an approximable mapping we first need to define the notions of a strong tie and a strong knot.

Definition 6

We say \(f:\mathbf {I}U\rightarrow \mathbf {I}\mathbb {R}\) has a strong set-valued Lipschitz constant \(b\in \mathbf {C}(\mathbb {R}^n)\) in \(\square a\), for \(a\in { \mathcal T}(U)\), denoted by \(f\in \delta _s(\square a,b)\), if there exist \(a'\prec a\) and \(b'\in \mathbf {C}(\mathbb {R}^n)\) with \(b\ll _{\mathbf {C}(\mathbb {R}^n)}b'\) such that \(f\in \delta (\square a',b')\). We call \(\delta _s(\square a,b)\) the strong single-tie of \(\square a\) with b.

From general results about single-step functions, [16] we know that if \(b\chi _{\square a}\ll \mathcal {L}f\), then for every \(x\in \square a\) we have \(b\ll \mathcal {L}f(x)\), and hence, . This means . Moreover .

Similar to Proposition VII.3 in [13] and its corollary, we have:

Proposition 13

If \(f:\mathbf {I}U\rightarrow \mathbf {I}\mathbb {R}\) is locally Lipschitz, then:

$$ f\in \delta _s(\square a,b) \Longleftrightarrow b\chi _{\square a}\ll \mathcal {L}f $$
$$ \mathcal {L}f=\sup \{b\chi _{\square a}:b\chi _{\square a}\ll \mathcal {L}f\}=\sup \{b\chi _{\square a}:f\in \delta _s(\square a,b)\} $$

Definition 7

We say an approximable mapping \(R:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) has strong Lipschitz constant O in \(\square a\), for \(O\in B^0_{{\mathbb R}^n}\) and \(a\in { \mathcal T}(U)\), denoted by \(R\in \varDelta _s(\square a,O)\), if there exist \(a'\in { \mathcal T}(U)\) with \( a\prec a'\) and \(O'\in B^0_{{\mathbb R}^n}\) with \( O'\prec O\) such that \(R\in \varDelta (\square a',O')\).

Proposition 14

  1. 1.

    If \(f\in \delta _s(\square a,b)\) then for all \( O\in B^0_{\mathbb {R}^n}\) with \(b\subset O\) we have \(A_f\in \varDelta _s(\square a, O)\).

  2. 2.

    If \(A_f\in \varDelta _s(\square a, O)\) then there exists \(b\subset O\) such that \(f\in \delta _s(\square a,b)\).

Proof

  1. 1.

    Let \(f\in \delta _s(\square a,b)\) and \(b\subset O\), then there exists \(a'\in { \mathcal T}(U)\) with \( a\prec a'\) and \(b'\) with \(b\ll b'\) such that \(f\in \delta (\square a',b')\). By the interpolation property of \(\prec \) there exists \( a_0\) with \( a\prec a_0 \prec a'\) and \(O_0\) with \(b\subset O_0\prec O\). By Proposition 10 we have \(A_f\in \varDelta (\square a_0,O_0)\) and thus \(A_f\in \varDelta _s(\square a, O)\).

  2. 2.

    Let \(A_f\in \varDelta _s(\square a,O)\) then by the definition of strong knot there exists \( a'\) with \(a\prec a'\) and \(O'\) with \( O'\prec O\) such that \(A_f\in \varDelta (\square a',O')\). By Corollary 3, \(f\in \delta (\square a',\overline{O'})\). By the interpolation property, there exists \( O''\) with, \(O'\prec O''\prec O\). Let \(b'=\overline{O'}\) and \(b=\overline{O''}\) then \(b\prec b'\) and \(f\in \delta (\square a',b')\). Hence, \(f\in \delta _s(\square a,b)\).  \(\blacksquare \)

Finally, we obtain the duality between strong ties and strong knots extending the main result in [13] to functions with interval input and output.

Corollary 4

We have \(R\in \varDelta _s(\square a,O)\) iff \(G_R\in \delta _s(\square a,\overline{O})\). Dually, we have \(f\in \delta _s(\square a,b)\) iff \(A_f\in \varDelta _s(\square a, b^{\circ })\).

Definition 8

Let \(R:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) be a Lipschitzian approximable mapping. The Lipschitzian derivative of R is defied as:

$$ L(R)=\sup \{\eta _{(\square a,O)}:R\in \varDelta _s(\square a, O)\} $$

which is of type \(B_{\mathbf {I}U}\rightarrow B_{\mathbf {C}(\mathbb {R}^n)}\).

The following theorem extends Theorem VII.12 in [13] to functions with interval input and output.

Theorem 2

The Lipschitzian derivative of a Lipschitzian approximable mapping \(R:B_{\mathbf {I}U}\rightarrow B_{\mathbf {I}\mathbb {R}}\) is an approximable mapping and we have: \(L(R)=A_{\mathcal {L}G_R}\).

4 Conclusion

We have developed a notion of sub-differentiation for Scott continuous maps which take hyper-rectangles in a finite dimensional Euclidean spaces to compact real intervals and is itself a Scott continuous map. This extends the domain of application of Interval Analysis to the classical derivative. It also extends Clarke’s theory and that of the L-derivative to functions with imprecise input/output as one encounters in interval analysis and exact real number computation. The classical Clarke operator commutes with the extension operator that extends a non-empty convex and compact valued map of a finite dimensional Euclidean spaces to the space of the hyper-rectangles of the Euclidean space. We have derived a calculus for sub-differentiation of interval maps which is weaker than the corresponding Clarkes calculus for point maps. A Stone duality framework for sub-differentiation of interval maps is also constructed which allows for a program logic view of sub-differentiation. We envisage several areas for immediate further work, namely an implementation of this work in Haskell, an implementation in a theorem prover such as Coq and a derivation of a weak calculus for constructors of approximable mappings which would match the calculus for the interval functions.