# call-time choice and extensionality

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Wed, 24 Aug 2011 13:48:59 +0900

Dear all,

I am currently pondering extensionality in FLP and am interested in

According to Wikipedia  extensionality refers to "principles that
judge objects to be equal if they have the same external properties".

For example, in mathematics, functions f and g are said to be
extensionally equal iff f and g have the same domain and

f(x) = g(x)

for all x in the domain. Another way to put it is that the extensions
(sets of input-output pairs) are equal and this definition generalizes
to relations. This is in contrast to intensional equality which
compares definitions. For example, the function f defined as f(x) =
x+x is intesionally different from g defined as g(x) = 2*x.

In purely functional languages, I think extensionality of functions is
the same as in mathematics because the semantics of a function in a
purely functional language is a mathematical function.

In "Rewriting and Call-Time Choice: The HO Case" , Paco, Juan, and
Jaime give the familiar "fcoin" example

g _ = 0
h _ = 1

f = g ? h

f' x = f x

that demonstrates that functional logic languages with call-time
choice do not allow eta-expansion (nor reduction). They further state
that f and f' are "by definition" extensionally equivalent which would
imply that FLP with call-time choice does not satisfy extensionality
because f and f' are observably different. For example `fdouble f' 0`
can yield 1 but `fdouble f 0` cannot where

fdouble f = fadd f f
fadd f g x = f x + g x

However, I find the claim that f and f' are "by definition"
extensionally equivalent questionable because f and f' are not
mathematical functions (not even relations) and so the definitions of
extensionality for mathematical functions or relations do not apply.

I think we need a different notion of extensionality for (possibly
higher-order) expressions. A possible candidate that is in the spirit
of Wikipedia's high-level description is observable equivalence itself
because it judges objects based on their external properties. However,
observational equivalence is of little use to decide if a language
satisfies extensionality because it is defined in terms of all
contexts the language provides. If there is, for example, a comparison
operator that can distinguish expressions based on their definition,
observational equivalence degrades to intensional equality.

Personally, I have a feeling that FLP with call-time choice *does*
satisfy extensionality in some sense but I'm not sure in which sense.

I think there should be some equivalence relation that includes the
defining rules of an FLP program. For example, if

a = b

is a program rule (and the only defining rule for the root symbol of
a), then a and b should be equivalent in some sense. In Curry (as
specified in the report) I think such a rule implies that a and b are
observably equal. Note that from

f' x = f x

we cannot conclude that f and f' are equivalent, only that `f x` and
`f' x` are equivalent for all x.

PAKCS supports comparison of functions based on their definition. If we define

id' = id

PAKCS can distinguish the two:

pakcs> id == id'
False

This means that `id` and `id'` are observably different although `id'
= id` is the only program rule defining id'. This property breaks
extensionality in my (intuitive, vague) sense but this behaviour of
PAKCS is, I think, undocumented, not specified in the Curry report,
and not generally part of FLP languages with call-time choice.
Similarly, higher-order patterns in Toy break extensionality.

I believe that without such intensional features it is not possible to
distinguish a from b defined as `a = b` and in this sense I think FLP
with call-time choice satisfies extensionality.

Sorry for being vague. Maybe your thoughts can help me to become more clear.

Cheers,
Sebastian

: http://en.wikipedia.org/wiki/Extensionality
: http://gpd.sip.ucm.es/fraguas/papers/FLOPS08-Springer.pdf
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Aug 24 2011 - 09:04:22 CEST

This archive was generated by hypermail 2.3.0 : So Jan 26 2020 - 07:15:11 CET