call-time choice and extensionality

From: Sebastian Fischer <>
Date: Wed, 24 Aug 2011 13:48:59 +0900

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'

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.


curry mailing list
Received on Mi Aug 24 2011 - 09:04:22 CEST

This archive was generated by hypermail 2.3.0 : Mi Aug 17 2022 - 07:15:14 CEST