Re: call-time choice and extensionality

From: Sebastian Fischer <>
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 (,
> 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
>, 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):

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

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

curry mailing list
Received on So Aug 28 2011 - 18:08:26 CEST

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:11 CEST