Re: call-time choice and extensionality

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

Hi Juan and others,

> Sebastian, for what you say here maybe what you need is a fully abstract
> semantics (http://en.wikipedia.org/wiki/Denotational_semantics#Abstraction),
> in which equality of denotations is equivalent to observable equivalence in
> any context. Then you could say that two expressions are extensionaly
> equivalent iff they have the same denotation in that semantics.

Yes, this is probably what I was thinking of.

> We made some
> advances regarding a fully abstract semantics for higher order FLP in
> http://arxiv.org/abs/1002.1833, but it only works for programs without extra
> variables.

Thank you for the pointer. While I agree that mathematical functions
(and the associated notion of extensionality) do not fit FLP with
call-time choice, I am not convinced that an intensional view of
functions is necessary to achieve full abstraction and
compositionality. I think there is a notion of extensionality that is
suitable for FLP with call-time choice.

More specifically, I wonder about the consequences of your observation
- that a functional style semantics based on something like set-valued
functions is necessarily unsound - for the denotational semantics for
typed FlatCurry (without recursive let):
http://www.iai.uni-bonn.de/~jv/IAI-TR-2011-1.pdf

Do f and f' defined below have the same semantics w.r.t. this semantics?

    f' x = f x
    f = (\_ -> 0) ? (\_ -> 1)

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:08:26 CEST

This archive was generated by hypermail 2.3.0 : Thu Sep 19 2019 - 07:15:08 CEST