Dear all,
I am currently pondering extensionality in FLP and am interested in
your opinions.
According to Wikipedia [1] 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" [2], 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
[1]:
http://en.wikipedia.org/wiki/Extensionality
[2]:
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