Re: call-time choice and extensionality

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Sat, 27 Aug 2011 17:04:40 +0900

(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 Sun Aug 28 2011 - 18:05:04 CEST

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:08 CEST