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

From: Wolfgang Lux <lux_at_wi.uni-muenster.de>

Date: Wed, 24 Oct 2001 13:21:46 +0200

Hello Mario,

*> I agree with Wolgang that a less strict lifting algorithm would be better,
*

*> in order to achieve succesful computations in those cases where Haskell does
*

*> so. However, I have a comment about the alternative translation which
*

*> Wolgang proposes to eliminate local pattern declarations. It seems to me
*

*> that the translation does not work in the case of recursive local definitions
*

*> .
*

*> Consider for example the definition
*

*>
*

*> f x = let {xs = x:xs} in head (tail xs)
*

*>
*

*> In Haskell, (f 0) evaluates to 0, while the translation proposed by Wolgang
*

*> cannot be applied because free (x:xs) is not a subset of free (f x).
*

*>
*

*> Maybe the translation is not meant to be used for recursive local definitions
*

*> .
*

you are right. The proposal does not work for recursive definitions.

However, this is the same as in the current report (for the reason

Micheal already noted). In principal one could try to extend the

proposal to transform local recursive bindings into mutually recursive

functions, e.g. your example could be lifted into the following set of

equations:

f x = f'' x (f_1 x)

f'' xs = head (tail xs)

f_1 x = x : f_1 x

But it is not clear to me whether the result preserves the intended

semantics. Consider the example

coin = 0

coin = 1

coins = coin : coins

The value of coins is an infinite list where each element is

instantiated independently to 0 or 1. However, what about the

declaration

f = let coins = coin : coins in coins

Should the result still be an infinite list where each element is

instantiated independently or should be an infinite list where

either all elements are 0 or all elements are 1?

The former case can be handled be modified translation rules but I

do not see how to translate the definition of f into a set mutually

recursive (top-level) equations with the same semantics for the second

case.

Regards

Wolfgang

Date: Wed, 24 Oct 2001 13:21:46 +0200

Hello Mario,

you are right. The proposal does not work for recursive definitions.

However, this is the same as in the current report (for the reason

Micheal already noted). In principal one could try to extend the

proposal to transform local recursive bindings into mutually recursive

functions, e.g. your example could be lifted into the following set of

equations:

f x = f'' x (f_1 x)

f'' xs = head (tail xs)

f_1 x = x : f_1 x

But it is not clear to me whether the result preserves the intended

semantics. Consider the example

coin = 0

coin = 1

coins = coin : coins

The value of coins is an infinite list where each element is

instantiated independently to 0 or 1. However, what about the

declaration

f = let coins = coin : coins in coins

Should the result still be an infinite list where each element is

instantiated independently or should be an infinite list where

either all elements are 0 or all elements are 1?

The former case can be handled be modified translation rules but I

do not see how to translate the definition of f into a set mutually

recursive (top-level) equations with the same semantics for the second

case.

Regards

Wolfgang

-- Wolfgang Lux Phone: +49-251-83-38263 Institut fuer Wirtschaftinformatik FAX: +49-251-83-38259 Universitaet Muenster Email: wlux_at_uni-muenster.de _______________________________________________ curry mailing list curry_at_lists.RWTH-Aachen.DE http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curryReceived on Mi Okt 24 2001 - 13:36:22 CEST

*
This archive was generated by hypermail 2.3.0
: Do Jan 21 2021 - 07:15:03 CET
*