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