On Jan 4, 2010, at 10:53 PM, Sergio Antoy wrote:
> The proposed derivations, such as the above one, make steps that
> do not appear to be needed at the time in which they are made.
That's true. In fact, let rewriting does not fix the strategy and
would even allow innermost derivations. Non-strictness is introduced
using an explicit bottom value, such that
ones = 1 : ones
can be reduced to "1 : _|_" to model non-strictness. You need to guess
when to introduce bottom.
> E.g., the following derivation is lazier. Loosely speaking, the
> lazier you are, the more results you get. This might change the
> claims on the number of results.
>
> test1
> (Fapp)
> twice f1 10
> (Fapp)
> f1 (f1 10)
> ...
The second step is no valid application of the (Fapp) rule as defined
in the HO-let-rewriting calculus cited in my previous message. The
arguments of rewritten functions must be patterns, i.e., terms made
from variables and constructors (or bottoms) but f1 (the first
argument of twice) is a defined operation (without arguments).
HO-let-rewriting only allows derivations that yield results which can
be deduced using CRWL and hence reflects call-time choice semantics.
That also fixes the number of possible results.
Sorry, that I did not state clearly that the derivations are in the HO-
let-rewriting calculus. I could have used a different calculus but it
occurred to me as the most intuitive calculus with Curry (i.e. call-
time choice) semantics.
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 Di Jan 05 2010 - 09:51:27 CET