Hello,
On Jan 4, 2010, at 10:07 AM, Juan Carlos González Moreno wrote:
> Hi, could you send he reduction steps for each goal ¿?
I can try. The problem is that lambda abstractions are part of the
Curry language but not of any formal specification of its semantics.
They are eliminated via lambda lifting in the formal specifications of
Curry semantics. I have obtained the results by running the
expressions in different Curry environments.
This does not mean, however, that one cannot explain the results on
formal basis. In fact, the results are perfectly reasonable and
although I was surprised in the first place that inlining under
lambdas is invalid even if the inlined variable is not directly
shared, I now find this observation obvious in retrospect. The
transformation becomes invalid if the lambda abstraction itself is
shared eventually.
In order to explain the results, we can eliminate the lambda as follows.
> f1 = let x = 1?2 in \y -> x+y
> f2 = \y -> (1?2) + y
f1 = let x = 1?2 in lambda1 x
lambda1 x y = x + y
f2 = lambda2
lambda2 y = (1?2) + y
Note that, in this representation, f2 no longer results from f1 via
inlining which usually does not inline arguments of partial
applications.
We can now use, e.g., higher-order let rewriting [1] to compute the
results of
> twice f x = f (f x)
>
> test1 = twice f1 10
> test2 = twice f2 10
Please correct me if the following derivations are incorrect as I'm no
expert in let rewriting.
There are two derivations for test1 (or possibly more which lead to
the same results):
test1
(Fapp)
twice f1 10
(Fapp)
twice (let x = 1?2 in lambda1 x) 10
(Fapp)
twice (let x = 1 in lambda1 x) 10
(Bind)
twice (lambda1 1) 10
(Fapp)
lambda1 1 (lambda1 1 10)
(Fapp)
lambda1 1 11
(Fapp)
12
test1
(Fapp)
twice f1 10
(Fapp)
twice (let x = 1?2 in lambda1 x) 10
(Fapp)
twice (let x = 2 in lambda1 x) 10
(Bind)
twice (lambda1 2) 10
(Fapp)
lambda1 2 (lambda1 2 10)
(Fapp)
lambda1 2 12
(Fapp)
14
And here are four derivations for test2 with three different results
(unlike claimed before, test2 does not have 4 results but 3. However,
the result 13 is computed twice by current Curry systems in distinct
derivations):
test2
(Fapp)
twice f2 10
(Fapp)
twice lambda2 10
(Fapp)
lambda2 (lambda2 10)
(Fapp)
lambda2 ((1?2) + 10)
(Fapp)
lambda2 (1 + 10)
(Fapp)
lambda2 11
(Fapp)
(1?2) + 11
(Fapp)
1 + 11
(Fapp)
12
test2
(Fapp)
twice f2 10
(Fapp)
twice lambda2 10
(Fapp)
lambda2 (lambda2 10)
(Fapp)
lambda2 ((1?2) + 10)
(Fapp)
lambda2 (1 + 10)
(Fapp)
lambda2 11
(Fapp)
(1?2) + 11
(Fapp)
2 + 11
(Fapp)
13
test2
(Fapp)
twice f2 10
(Fapp)
twice lambda2 10
(Fapp)
lambda2 (lambda2 10)
(Fapp)
lambda2 ((1?2) + 10)
(Fapp)
lambda2 (2 + 10)
(Fapp)
lambda2 12
(Fapp)
(1?2) + 12
(Fapp)
1 + 12
(Fapp)
13
test2
(Fapp)
twice f2 10
(Fapp)
twice lambda2 10
(Fapp)
lambda2 (lambda2 10)
(Fapp)
lambda2 ((1?2) + 10)
(Fapp)
lambda2 (2 + 10)
(Fapp)
lambda2 12
(Fapp)
(1?2) + 12
(Fapp)
2 + 12
(Fapp)
14
Cheers,
Sebastian
[1] Rewriting and Call-Time Choice: The HO Case
Francisco Javier López-Fraguas, Juan Rodríguez-Hortalá, and Jaime
Sánchez-Hernández
--
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 Di Jan 05 2010 - 09:51:22 CET