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