- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

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 Wed Aug 24 2011 - 09:04:22 CEST

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'

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 Wed Aug 24 2011 - 09:04:22 CEST

*
This archive was generated by hypermail 2.3.0
: Wed Sep 18 2019 - 07:15:08 CEST
*