- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

Date: Tue, 05 Jan 2010 01:42:52 +0100

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

Date: Tue, 05 Jan 2010 01:42:52 +0100

On Jan 4, 2010, at 10:53 PM, Sergio Antoy wrote:

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.

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/curryReceived on Di Jan 05 2010 - 09:51:27 CET

*
This archive was generated by hypermail 2.3.0
: Do Jan 20 2022 - 07:15:04 CET
*