Re: call-time choice and extensionality

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

On Sat, Aug 27, 2011 at 5:34 PM, Janis Voigtländer
<jv_at_informatik.uni-bonn.de> wrote:
>>
>>     |[ f  ]| = {\_ ->  {0}, \_ ->  {1}}
>>     |[ f' ]| = {\_ ->  {0,1}}
>>
>> Is this correct?
>
> Yes, that's the idea.

Then, I think elements in your semantic domain provide a suitable
notion of "extension" for expressions in a FLP language with call-time
choice. FLP languages (without PAKCS's == operator that can compare
functions or TOY's HO patterns that can match partial applications)
can then be considered as extensional in the sense that

    |[a]| = |[b]|

implies that a and b are observably equivalent. I think HO patterns
and PAKCS's == operator destroy extensionality in this sense.

Best regards,
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

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:10 CET