The language LRTp is a non-deterministic language for exact real number computation. It has been shown that all computable rst order relations in the sense of Brattka are de nable in the language. If we restrict the language to single-valued total relations (e.g. functions), all polynomials are de nable in the language. In this paper we show that the non-deterministic version of the limit operator, which allows to de ne all computable rst order relations, when restricted to single-valued total inputs, produces single-valued total outputs. This implies that not only the polynomials are de nable in the language but also all computable rst order functions.
Scott [
when restricted to single-valued total relations, e.g. functions. In that direction
LRT, with its sequential, non-deterministic semantics, seemed naturally suited
to a relational view of computation. In [
the language, we show that the limit operator when restricted to single-valued
total inputs, produces single-valued total outputs. We use the argument stated
by [
LRTp is tied to the call-by-partial-value evaluation de ned in [
The paper is organized as follows: after the foundations, in Section 3 we present the notions of strongly convergence of programs. In Section 4, we introduce the language LRTp. In Section 5, we present the program that computes the limitation (in some places called limit) operator and we prove that it strongly convergence for single-valued inputs. Finally, Section 6 is devoted to conclusions. 2 2.1
Continuous relations
ural numbers to other metric spaces, particularly to R. Continuity is a necessary condition for e ectiveness, and yet the fact that R is connected means there are no non-constant continuous functions, e.g., from R to the discrete space N.
de ne R(x) := fy 2 Y j xRyg. For B Y , de ne R 1(B) := fx 2 X : R(x) \ B 6= ;g, and let dom(R) = R 1(Y ) = fx 2 X j R(x) 6= ;g. Thus we think of a relation as a partial function from X to non-empty subsets of Y . For this reason, we follow Brattka by usually writing f , g, etc., as names for binary relations.
If X and Y are topological spaces, then f is said to be continuous if and only if f 1(V ) is open in X whenever V is open in Y . Also f is said to have closed images if f (x) is closed in Y for every x 2 X. Additionally, f is said to be single-valued if f (x) is a singleton in Y for every x 2 X.
If X and Y are topological (or metric) spaces, then X Y denotes the standard topological (metric) product.
Clearly, for a function h between spaces, the graph of h is a continuous relation if and only if h is continuous in the usual sense. In particular, the graphs of projection maps for cartesian products are continuous. If the codomain is T1, graphs of functions also have closed images. Furthermore, any relation f is continuous if and only if f (A) f (A) for every A dom(f ). Note that A ranges only over subsets of dom(f ), not over all subsets of X. This jibes with our interpretation of f (x) = ; as meaning that f is unde ned at x.
On the other hand, for continuous relations f : X $ Y and g : Y $ Z, de ne g f by (g f )(x) := (g f )(x); if f (x) dom(g); ;; otherwise. where g f is the usual relational composition. A simple exercise shows that continuous relations are closed under .
By de nition, g f has closed images. The graph of the identity function on a space Y satis es f = I f if and only if f has closed images, and similarly for g = g I. So de nes composition for a category of topological (or metric) spaces in which the morphisms are continuous relations with closed images. This can be taken to be the ambient category for Brattka's recursive relations. Note that the graphs of projections on products of T1 spaces are continuous with closed image. So the category can be given a monoidal structure.
bn 2 Bn.
Limitation In a (complete) metric space, a sequence fBngn of subsets is strongly Cauchy provided that for each i and each bi 2 Bi, bi is the i-th element of a strong Cauchy sequence fbngn for which bn 2 Bn for each n. In other words, all elements of Bi participate in some strong Cauchy sequence obtained from the sets Bn. For such a sequence of subsets, de ne limi!1 Bi to consist of all limits (in the usual sense) of all strong Cauchy sequences hbnin such that
N $ Y , the limitation combinator is de ned by lim[C](a) := limn!1 Cn(a); Cn strongly Cauchy, where Cn(a) = C(a; n); ;; otherwise. 2.2
The interval domain
The set R of non-empty connected compact subsets of the Euclidean real line forms a continuous dcpo when ordered by reverse inclusion: x v y i x y.
We regard elements of R as \partial real numbers"; the v-maximal intervals are singletons, corresponding to \total numbers". That is, the continuous map x 7! fxg embeds R as maximal elements, making R into a domain model for R. The dcpo R, however, does not have a least element. By adding a least element, corresponding to the completely under-speci ed partial real number R, we obtain a bounded complete continuous domain R?.
For any x 2 R?, we write x = inf x and x = sup x so that x = [x; x], and de ne x := x x:
The upper bound of a subset A R? is T A when this is not empty. Alternatively,
G A = \ A = sup x; inf x :
x2A x2A The way-below relation of R? is given by x y i x < y and y < x.
This amounts to y being a subset of the interior of x. Of course R = ? a for any compact interval a. The intervals with distinct rational end-points form a basis for R?.
For basis element a, consider the partial function x 7! a t x de ned when a and x are consistent. This join map has a total continuous extension: joinax = 8 a t x; a and x are consistent; <
fag ; x < a; : fag ; a < x.
Lemma 1. For basis elements a and b, 1. joinajoinb = joinatb if a t b exists; 2. joinajoinb = ka if b < a; 3. joinajoinb = ka if a < b; where kx denotes the constant map x 7! fxg. Thus joina v joinajoinb always holds.
Each basis element a is also associated with a positive a ne map rrconsa : R ! R given by x 7! ax + a. Taking images, rrconsa extends to a strict continuous map on R?. These maps form a left group action on R?. Because of this, we will think of the basis of R? as itself forming a group, writing ab for concatenation, a 1 for inverse and I for the identity (that is, the interval [0; 1], corresponding to the identity a ne map).
Lemma 2. For basis elements a and b, 1. rrconsajoinb = joinabrrconsa; 2. rrconsarrconsb = rrconsab;
The functions rrconsa and joina are said to be strongly convergent, meaning that they send maximal elements to maximal elements. In addition, the functions rrconsa are all homeomorphisms (rrconsarrconsa 1 = rrconsI = id), so they also send non-maximal elements to non-maximal elements. 2.3
The Hoare powerdomain
mantics for sequential, non-deterministic real number computation requires the
Hoare powerdomain (PH ). That is, starting from the assumption that some
functorial powerdomain is needed to model non-determinism, general
considerations about continuity show that the Hoare powerdomain is the only one that
can be used. We refer the reader to the cited work for an explanation. In that
work, however, the fact that PH is actually a free construction is not used
explicitly (though certain de nitions in the semantics depend on it implicitly). In
this section, we review the basic facts about PH as the construction of free
inationary semi-lattices. The reader may consult [
continuous binary operation [ : X X ! X that satis es the usual semi-lattice laws. Such a semi-lattice is in ationary if x v x [ y. It is not hard to see that idempotency is equivalent to [ = idX , and in ationarity to idX X v [, where : X ! X X is the diagonal map. Since these two conditions constitute a Galois connection between [ and , if [ exists it is unique.
If f : X ! Y is a continuous map and (Y; [) is an in ationary semi-lattice, then there is a unique continuous map f : PH (X) ! Y that preserves [ for which f = f , where is the unit of the powerdomain monad. There is also a unique continuous map fb: PH (X) ! PH (Y ) de ned by fb := PH (f ).
automatically to formal joins of non-empty sets: For A X, take the closure of A under [. This is automatically a directed set and hence has a supremum, which we denote by S A. If the generating domain has a least element, then so does PH (X). So S is de ned for all subsets of PH (X).
Concretely, elements of PH (X) are non-empty Scott closed subsets of X, the unit sends x 2 X to the closure of fxg. Also, [ is simply binary union, and S is closure of union.
Hoare powerdomain is a monoidal monad with natural transformation m : PH (X) PH (Y ) ! PH (X Y ) satisfying the usual coherence conditions. In concrete terms, m(A; B) := A B.
given by the functor PH itself, the unit : X ! PH (X), the formal union [: PH (X) PH (X) ! PH (X) and the transformation m : PH (X) PH (Y ) ! PH (X Y ).
preserves [ if f (x [ y) = f (x) [ f (y). 3
ask when a continuous function F : PH (D) ! PH (E) corresponds naturally to a continuous single-valued relation from X to Y . The next de nition answer this question.
De nition 2. Suppose X is a topological space, EX is a domain model for X with embedding eX and d 2 PH (EX ). Let uX (d) := fx 2 X j X (x) v dg = ( X ) 1(#d) X := eX :
We said that u is single-valued if there is a unique x 2 X such that uX (d) = fxg. The subscripts will be ommited when possible.
Furthermore, suppose that Y is a second space and EY is a corresponding domain model. It is said that a relation f from X to Y is captured by F : PH (EX ) ! PH (EY ) (written f F ) i for each x 2 dom(f ), f (x) = u(F ( X (x))). Moreover, say that a single-valued relation f from X to Y is strongly captured by F : PH (EX ) ! PH (EY ) (written f F ) if and only if for each x 2 dom(f ), f (x) = u(F ( X (x))), i.e. u is single-valued. Say that f is exactly captured by F (written f ' F ) i f
F and dom(f ) = fx 2 X j u(F ( (x))) 6= ;g:
f
F and
dom(f ) = fx 2 X j u(F ( (x))) 6= ;; u is single-valuedg :
Say that d 2 PH (EX ) is convergent provided that d =S f (x) j x 2 u(d)g: Say that d 2 PH (EX ) is strongly convergent provided that d = (x) where x is the unique value of the single-valued function u(d). Also say that d is divergent provided that (x) 6v d for all x 2 X. Moreover, say that d is strongly divergent provided that either (x) 6v d for all x 2 X or u(d) is not single-valued. Say that continuous F : PH (EX ) ! PH (EY ) is disciplined provided that it preserves [ and for each x 2 X, F ( X (x)) is either convergent or divergent. Also, say that continuous F : PH (EX ) ! PH (EY ) is strongly disciplined provided that for each x 2 X, F ( X (x)) is either strongly convergent or strongly divergent.
For the remainder of this section, we assume that X, Y , EX , EY , and embeddings eX , eY are xed.
We can veri ed that, for any singleton fxg X, fxg = u( (x)), to see this, (x) is a directed set with supremum x, hence x 2 u( (x)), as x is the only element belonging to fxg then fxg = u( (x)).
In [
ciplined, there is a unique relation that is exactly strongly captured by F , this relation is a continuous relation with single-valued image.
are closed under unions, and trivially the empty relation is captured. So there is a maximal relation strongly captured by F . Clearly, the condition on domains means that this maximal relation is exactly strongly captured and any strongly captured relation is contained in an exactly strongly captured relation.
fd 2 EX j u(F (d)) \ U 6= ;; u single-valuedg which is clearly an upper subset of EX . For directed D, if u(F (F D)) \ U 6= ;, and u is single-valued then for some x 2 X, (eX (x)) v F F (D).
De ne f : X $ Y by f (x) = u(F ( (eX (x)))) for single valued u. Because u only yields singletons, f has single-valued images. As, F is strongly disciplined, dom(f ) agrees precisely with the de nition of \exact strongly capture." It remains to verify that f F . Suppose fxg = u(d). Then d = (eX (x)) [ d0 where u(d0) = ;. As F is strongly disciplined, u(F (d)) = u(F ( (eX (x)))) = f (x).
lations with closed images and disciplined functions. Disciplined functions are
closed under composition. Moreover, if F and G are disciplined, f and g are
continuous with closed images, f F and g G and these \type check" in the
obvious way, then (g f ) (G F ) [
Theorem 1. Strongly disciplined functions are closed under composition. Moreover, if F and G are strongly disciplined, f and g are continuous with singlevalued images, f F and g G and these \type check" in the obvious way, then (g f ) (G F ).
Proof. Closure under composition for preservation of [ follows from the general theory of power domains. By de nition of strongly disciplined, there is a unique z such that fzg = u(G(F ( (x)))) for all x in the domain of f , hence z 2 G(F ( (x))).
Conversely, if there are unique y and z such that fzg = u(G( (y))) and fyg = u(F ( (x))) then (z) v G( (y)) v G(F ( (x))). So G F is disciplined.
Strongly discipline is related to the operational concept of strong
convergence discussed at length in [
that allow a form of call-by-value, which we refer to as call-by-partial-value. In
[
The domains R?, T? and N? clearly can be equipped with measurements: in R?, M (a) = a; in T?, M (true) = M (false) = 0; in N?, M (n) = 0; and in all of these M (?) = 1. In a nite product of domains with measurements, a measurement on a tuple is obtained by taking the minimum measurement of the components. For any positive p, any domain D with least element and with measurement M , the function pvp : D ! D given by pvp(a) = a if M (a) < p and pvp(a) = ? otherwise is continuous. Its extension to PH D satis es pdvp(d) v d and allows us to isolate the maximal part of an element d 2 PH (D) that can be written S (a) where all elements of A have \small" measurement. As p decreases, pav2pAdecreases as well. Importantly, each pdvp(d) is the identity map when restricted to convergent d, and Fp pdvp is the identity on R?. 4
for real number computation. In LRT, parallel conditional pif is replaced by a
non-deterministic test rtestl;r. In this section, we describe a variant of LRT.
The language LRTp di ers from LRT in three ways: products of ground types
are made explicit, the type I for the compact interval [0; 1] is eliminated in favor
of a type corresponding to R, and a let construct is introduced that provides
for call-by-partial-value semantics. This language is described at length in [
Syntax Syntactically, the type system for LRTp is given by := := nat j bool j real := j j ( ! )
in the third clause, general types. As usual, we associate ! right to left, and omit parentheses when we can.
x 2 V ariable; P ::= x j n j true j false j (+1)(P ) j ( 1)(P ) j (= 0)(P ) j if P then P else P j rrconsa(P ) j joina(P ) j rtestl;r(P ) j
x :P j P P j YP j let x = P in P j priP j hP0; : : : ; Pni where (+1)(P ); ( 1)(P ) and (= 0)(P ) amount for successor, predecessor and equality for zero respectively; the subscripts of the constructs rrcons and join are proper rational intervals and those of rtest are rational numbers. In the let construct, the rst term P must be of basic type.
let hx0; : : : ; xni = P1 in P2 where the notation hx0; : : : ; xni stands for a variable of the appropriate product type and where free occurrences of xi in P2 abbreviate prihx0; : : : ; xni.
4.2
Denotational Semantics
We de ne denotational semantics [[ ]]p for LRTp subject to a positive real number parameter p in such a way that [[M ]]p is semi-continuous in p and Fp [[M ]]p corresponds to call-by-name interpretation. The idea is to employ pvp (see page 8) in the interpretation of the let construct to ignore di erences due to \badly" divergent behavior. As p increases, the semantics ignores less. We use
booleans (T?), natural numbers (N?) and compact intervals (R?), respectively.
B [[bool]] := T?;
B [[nat]] := N?;
B [[real]] := R?: Finite products are interpreted the usual way: B [[ ]] := B [[ ]] B [[ ]]. Basic types are interpreted as Hoare powerdomains of nite products:
[[true]]p = (true); [[false]]p = (false); with syntactic sugar [[if M then N else P ]]p := [[if]]p( [[M ]]p; [[N ]]p; [[P ]]p) [[pri]]p = bi; where i is the usual projection map. Tuples are interpreted by [[hX1; : : : ; Xni]]p := m( [[X1]]p; : : : ; [[Xn]]p)
construct enforces what we refer to as call-by-partial-value.
[[let x = M in N ]]p := [[N ]]p (x=pdvp( [[M ]]p))
Heirseththeeusnyitm, bfbol:s= ;PbH; (fa),ndf mdendoetreisvethfreomtranthspeoHseoaorfefp:oXwer!domPaHi(nY m),omnadis:
the natural transformation PH (X0) : : : PH (Xn) ! PH (X0 : : : Xn). The
functions (+1), ( 1), (= 0) are the standard interpretations in the Scott model of
PCF [
In [
Lemma 4. The constants (+1), ( 1), (= 0), joina, rrconsa and pri denote strongly disciplined functions but not the constant rtestl;r.
Proof. The convergence requirement is straightforward. That rtestl;r is not strongly disciplined follows by de nition.
Notice that although rtestl;r is not strongly convergent, it can be used to
de ne strongly convergent functions as is shown in [
Lemma 5. The semantics [[ ]]p is semi-continuous in p: for bounded A R+, G [[M ]]p = [[M ]]sup A: p2A Moreover, de ne [[]]1 exactly as [[]]p for all cases except
[[let x = M in N ]]1 := [[N ]]1 (x= [[M ]]1)) Then [[M ]]1 = Fp [[M ]]p.
4.3
Operational Semantics
the \p-th" operational interpretation is complete for [[ ]]p. We do not need an operational semantics corresponding to [[ ]]1.
De nition 3. For each basic type , we de ne a subset of the closed terms to be output terms, and for each output term M we de ne it's output o(M ) to be a value in B [[ ]]. For real, a term of the form joinaM is an output term, and o(joinaM ) := a. For nat, a term of the form n is an output term, and o(n) = n. For bool, a term of the form true or false is an output term, and o is de ned obviously. For , a term of the form hM; N i is an output term provided M and N are output terms, and o(hM; N i) = ho(M ); o(N )i.
Lemma 6. For an output term M and p > 0,
(o(M )) v [[M ]]p v[ f (x) j o(M ) v
(x)g :
Proof. [
We de ne !p to be the least relation that includes single-step reduction rules
for PCF [
N !p N 0 M N !p M N 0
if M is joina, rrconsa, rtestl;r, if, pri, let.
De nition 4. We de ne the operational meaning of a closed term M of basic type in i steps of computation, written [M ]ip 2 [[ ]].
For a closed term of basic type , de ne [M ]i as follows: [M ]ip = [ f (o(M 0)) j 9M 09k k i; M 0 is an output term and M !p M 0 g; k where an empty formal join is ?, and !p denotes the k-fold composition of the relation !p.
Finally, [M ]p = Fi[M ]ip: which is justi ed by the obvious fact that [M ]ip v [M ]ip+1.
k such that M !p M 0 can only hold for nitely many output terms M 0. This can be established easily by induction on the operational rules.
Lemma 7. [[M ]]p = S f [[N ]]p j M !p N g (this is a nite union).
Proof. [
Proof. [
Lemma 8. For all closed terms M of ground type, [M ]p v [[M ]]p. De nition 5. A closed term is said to be p-computable as follows: 1. A closed term M of basic type is p-computable whenever [[M ]]p v [M ]p,
for every closed p-computable term Q of type , An open term M : with free variables x1; : : : ; xn of type 1; : : : ; n is pcomputable whenever [N1=x1] [Nn=xn]M is p-computable for every family Ni : i of closed p-computable terms. Lemma 9. Every term of LRTp is p-computable.
Theorem 2. [M ]p = [[M ]]p, for all closed LRTp terms M and all positive reals p.
Remark 41 We are interested in those continuos functions F : PH (X) ! PH (Y ) for which u(F ( (x))) is a singleton. As we observed previously, this property can be veri ed using the denotational semantics. Although ? cannot be distinguised from any other element of the Hoare powerdomain, u allows to get those maximal elements of a given element of the Hoare powerdomain, hence, we just have to veri ed that the image of u is a singleton, which can be done denotationally. By adequacy there is a program which denotes such continuous function. Notice that LRTp is more expressive because we can de ne relations, however, in this paper, we are not concerned about the full expressivity of LRTp, we only care about the de nability of rst order computable functions. 5
De nition 6. For basic LRTp types, we de ne a set-theoretic interpretation as follows: R [[nat]] = N;
R [[bool]] = T;
R [[real]] = R;
Theorem 1 establishes that composition in LRTp corresponds to -composition. That is, if F and G are closed terms of type 1 ! 2 and 2 ! 3, both are strongly disciplined and f [[F ]] and g [[G]], then g f [[ x:let y = F (x) in G(y)]]p.
De nition 7. De ne the following closed term of LRTp:
Lim[F ](x) := aux lim F (x; 0) id where aux lim0 F (x; n) G := let r = G(F (x; n)) in if rtest 5=16;5=16(r) then if rtest 5=16; 4=16(r) then consL(aux lim F (x; (+1)(n)) (tailL else consC (aux lim F (x; (+1)(n)) (tailC else if rtest4=16;5=16(r) then consC (aux lim F (x; (+1)(n)) (tailC else consR(aux lim F (x; (+1)(n)) (tailR G)) G)) G)) G)) consa := joinA rrconsa A := [ 1; 1] L := [ 1=2; 0] taila := joinA rrconsa 1
C := [ 1=4; 1=4] R := [0; 1=2]
In these de nitions we understand Lim, for example, to be a second-order term, where F is an argument. We set them apart for readability using square brackets.
Theorem 3. For any p < 1=4, in the semantics [[ ]]p, the term Lim preserves
disciplined. Moreover, if f F and g G for single-valued f and g and these
\type check" in the obvious way, then lim f [[Lim]]pF . In other words if the
input of Lim is a single-valued function F then Lim[F ] convergences to a
singlevalued output
Proof. The assumption p < 1=4 is needed to ensure that the limit of the strong
Cauchy sequence in which ri appears as the i-th term is bounded within a
distance of 2 (i+2) from ri. In fact, this is the only point at when the assumption
that p is small is required. Plume [
By allowing a reasonable de nition of strongly convergence for relations, we get a
characterization of single-valued relations (e.g. functions). This characterization
di ers from the one presented in [