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 So Aug 28 2011 - 18:08:26 CEST