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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Wed, 25 Nov 2009 16:29:36 +0100

Sebastian Fischer wrote:

*> Hello,
*

*>
*

*> it is well known that eta-expansion is not valid in functional-
*

*> logic programs [1]. To my surprise, this has the consequence that
*

*> the same is true for applications of lambda abstractions (due to
*

*> the way they are eliminated using lambda lifting). Here is an
*

*> example session using the Münster Curry Compiler, but PACKS behaves
*

*> similarly (but does not allow lambda abstractions in its prompt):
*

*>
*

*> cyi> let twice f x = f (f x) in twice ((1?2)+) 10
*

*> 12
*

*> More solutions? [Y(es)/n(o)/a(ll)]
*

*> 14
*

*> cyi> let twice f x = f (f x) in twice ((\x -> \y -> x+y) (1?2)) 10
*

*> 12
*

*> More solutions? [Y(es)/n(o)/a(ll)]
*

*> 14
*

*> cyi> let twice f x = f (f x) in twice (\y -> (1?2)+y) 10
*

*> 12
*

*> More solutions? [Y(es)/n(o)/a(ll)]
*

*> 13
*

*> More solutions? [Y(es)/n(o)/a(ll)]
*

*> 13
*

*> More solutions? [Y(es)/n(o)/a(ll)]
*

*> 14
*

*>
*

*> The second call is a (semantically valid, I think) translation of
*

*> the first partial application into lambda abstractions, the third
*

*> call results from the second by application which is - for me,
*

*> surprisingly - an invalid transformation.
*

Sorry for nitpicking. The transformation from the partial application

((+) (1?2)) to (\x y -> x + y) (1?2) happens to be valid only by

virtue of the fact that (+) is a binary function. If you replace (+)

by the following, contrived function

addOrSub x = (x +) ? (x -)

the introduction of the lambda abstraction would be an invalid eta-

expansion, i.e., (addOrSub (1?2)) and (\x y -> x `addOrSub` y) (1?2)

are no longer equivalent.

Lambda abstractions just define anonymous local functions. Giving

names to them your examples read

twice ((let lambda1 x y = x + y in lambda1) (1?2)) 10

and

twice (let lambda2 y = (1?2) + y in lambda2) 10

where both local functions are supercombinators, i.e., functions with

no (syntactically) free variables. Therefore the different semantics

of the expressions has nothing to do with lambda lifting, which is a

transformation to transform lambda abstractions (or more generally

local function declarations) with free variables into

supercombinators, but rather just another case that shows that beta-

reduction is also not valid in general in a functional-logic language

with compile-time choice.

Cheers

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Nov 25 2009 - 18:21:42 CET

Date: Wed, 25 Nov 2009 16:29:36 +0100

Sebastian Fischer wrote:

Sorry for nitpicking. The transformation from the partial application

((+) (1?2)) to (\x y -> x + y) (1?2) happens to be valid only by

virtue of the fact that (+) is a binary function. If you replace (+)

by the following, contrived function

addOrSub x = (x +) ? (x -)

the introduction of the lambda abstraction would be an invalid eta-

expansion, i.e., (addOrSub (1?2)) and (\x y -> x `addOrSub` y) (1?2)

are no longer equivalent.

Lambda abstractions just define anonymous local functions. Giving

names to them your examples read

twice ((let lambda1 x y = x + y in lambda1) (1?2)) 10

and

twice (let lambda2 y = (1?2) + y in lambda2) 10

where both local functions are supercombinators, i.e., functions with

no (syntactically) free variables. Therefore the different semantics

of the expressions has nothing to do with lambda lifting, which is a

transformation to transform lambda abstractions (or more generally

local function declarations) with free variables into

supercombinators, but rather just another case that shows that beta-

reduction is also not valid in general in a functional-logic language

with compile-time choice.

Cheers

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Nov 25 2009 - 18:21:42 CET

*
This archive was generated by hypermail 2.3.0
: Sa Jan 25 2020 - 07:15:09 CET
*