🚀 go-pugleaf

In article <5455@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
>
>But how can one speak of strict or lazy constructors?
>Consider for example, the ordered pair constructor,
>which uses elements X1 and X2 of domains D1 and D2,
>to create the element <X1,X2> of domain D1xD2.
>The standard selector functions will choose
>the appropriate piece of <X1,X2> regardless
>of whether the other side happens to be the bottom.

Well, the above constructor you described is not strict. But consider
the following constructor: StrictPair: it takes X1 from D1 and X2 from
D2 and creates an element of D1 * D2. If either of X1 or X2 is bottom
the pair constructed is bottom.

Now the complete definition of D1 * D2:

Let U be the Universal domain and D1 and D2 be the arbitrary
computable subspaces of the Universal domain U characterized  by the
projection maps R1 and R2. Using the cartesian map "pair" : U -> (U ->
U X U) we can build several simple composite spaces, one of them is
the "coalesced product" ( because the product operation described is
strict, it is customary to describe that operation as "strict")

D1 * D2 = { <x,y> | x in D1 and y in D2 and x != bot and y != bot}
	  U { bottom}

The corresponding functions are:

StrictPair: D1 -> (D2 -> D1 * D2) =
	\ x. \y. if  defined(x) and defined(y) pair(x y) else bottom
fst z =  left z
snd z = left z
R_strict : U -> (D1 * D2) = \x. if defined(x) then 
		StrictPair( (R1 o fst (x) (R2 o snd(x))))

>Of course, the language designer may choose to deny the programmer
>direct access to the standard selector functions,
>and instead provide selector functions which,
>before selecting an element, verify that both sides
>are strictly above bottom.  In any case,
>the elements <X1,bot>, <bot,X2> and <bot,bot> are
>distinct elements of D1xD2, regardless of whether
>any particular language lets the programmer make use of this fact.
>
>So, when we speak of strict constructors, are we not _really_
>describing a property of the _selector_ functions, and not the constructor?
>Or, is there another version of domain theory I am not aware of?
>
>	Frank Silbermann	fs@cs.tulane.edu
>	Tulane University	New Orleans, Louisianna  USA


In the above version of the coalesced product we formed there are no
elements such as <X1, bot>.  For an excellent discussion of all the
different semantics of lazy data constructors you can read the
following paper:

[Lazy]  {Cartwright, R. and J. Donahue}.
The semantics of lazy (and industrious) evaluation.  In {\it Proc.
1982 ACM Symposium on Lisp and Functional Programming\/}, 1982,
253--264. Also available as Xerox Parc Technical Report CSL-83-9,
1984.


Regards
Rama Rao (rama@rice.edu)