🚀 go-pugleaf

In article <5455@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
>I understand what it means to say that a _function_ is strict:
>it maps the bottom element of the input domain
>to the bottom element of the output domain.
>I also understand that this property can justify
>evaluation orders which otherwise might not always work.
>
>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.
>
>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?

Yes, somewhat. A "constructor" is an *uninterpreted* function, which
can be thought of as forming a "record" of appropriate type and arity, that
allows the recovery of components by *implicit* selector functions. The 
notion of "strict constructor" is a slight abuse of terminology, since the
so-called constructor is not wholly uninterpreted. Actually what we are
doing is pretend we are working with the product domains (e.g. D1xD2), 
but are actually working with variants of them (possibly embeddable in the
product domain), where elements such as <X,bottom> are identified with 
<bottom,bottom>, which might be bottom of the product domain (i.e. of D1xD2). 
Therefore, the selector (deconstructor) functions do not let us recover the 
components but only approximations of them. The so-called constructor symbol
is weakly interpreted (under approximation ordering), but otherwise behaves as
a true constructor would (for all non-bottom/ bottomless elements). 

So for example:
true pairing written (_,_) : D1xD2 -> D1xD2, pi_1, pi_2 are true 
                                                           deconstructors.
strict_pairing written <_,_> : D1 x D2 -> strict_pseudo-product(D1,D2)  
                                                   [resembles D1xD2]
first: strict_pseudo-product(D1,D2) -> D1
second: strict_pseudo-product(D1,D2) -> D2

first <X,bottom> = bottom		whereas pi_1 (x,y) = x
first <X,Y> = X  (if Y =/= bottom)
second < bottom, Y> = bottom		whereas pi_2 (x, y) = y
second <X,Y> = Y (if X =/= bottom)

Note that given any a,b in D1, D2: 
      first <a,b> <=_(in D1) a,      second <a,b> <=_(in D2) b.
strict_pseudo-product(D1,D2) is embeddable in D1xD2 but not isomorphic to it.
Other quasi-constructors for pairing are possible -- e.g. first-strict,
second-strict, depending on the kind of projection [an idempotent 
approximation of identity] desired.

>Or, is there another version of domain theory I am not aware of?
No, I don't think so.

Regards,
Sanjiva Prasad
ORA, Ithaca NY 14850		sanjiva@oracorp.com

PS: Frank, did you see my posting re: recursion in languages based on the 
typed lambda calculus?