Re: lambda application destroys sharing

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Fri, 01 Jan 2010 23:47:15 +0100

Hello again,

On Nov 25, 2009, at 4:29 PM, Wolfgang Lux wrote:

> just another case that shows that beta-reduction is also not valid
> in general in a functional-logic language


Very true. I now realise that I was surprised by something else. Let
me nail down the observation differently.

I previously thought that `let x = a in b` can be replaced by b[a/x]
(meaning b where every free occurrence of x is replaced by a) if there
is at most one free occurrence of x in b. However, this is not true as
demonstrated by the following functions.

     f1 = let x = 1?2 in \y -> x+y
     f2 = \y -> (1?2) + y

Although f2 results from f1 by substituting the *unique* variable x,
f1 and f2 are not semantically equivalent. The context `twice _ 10`
(where _ denotes the hole) distinguishes them:

     twice f x = f (f x)

     test1 = twice f1 10
     test2 = twice f2 10

test1 has 2 results, test2 has 4.

Inlining nondeterministic expressions under lambdas is invalid even if
the replaced variable occurs at most once.

Cheers,
Sebastian

-- 
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Sa Jan 02 2010 - 12:31:42 CET

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:09 CET