(cc'ing those not on the list)
On Sat, Aug 27, 2011 at 4:03 PM, Janis Voigtländer
<jv_at_informatik.uni-bonn.de> wrote:
>> Do f and f' defined below have the same semantics w.r.t. this semantics?
>>
>> f' x = f x
>> f = (\_ -> 0) ? (\_ -> 1)
>
> I think they don't. (And they shouldn't, in a semantics that is sound
> for call-time choice, right?)
Yes, because
twice f = (f (), f ())
can distinguish them.
It is a bit difficult for me to derive the semantics of f and f' after
a brief look at the denotational semantics. From Figure 3 I guess they
are something like this (possibly eliding partial values):
|[ f ]| = {\_ -> {0}, \_ -> {1}}
|[ f' ]| = {\_ -> {0,1}}
Is this correct?
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on So Aug 28 2011 - 18:05:04 CEST