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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Fri, 09 Nov 2007 12:55:40 +0100

Hi Sergio!

*> My fault. I should have explained it better. Sorry if this
*

*> message is long. First I change a bit your program to work only
*

*> with algebraic types, the usual integers are not defined by a
*

*> finite data declaration (but Brassel et al. showed that they could
*

*> be "declared").
*

*>
*

*> t = let x free in (f x ? g x)
*

*> f True = success
*

*> g False = success
*

*>
*

*> I also assume that both f and g are flexible or narrow their
*

*> argument.
*

*>
*

*> Let (a/x) denote the substitution that maps x to a. t(True/x)
*

*> evaluates to success and so t(False/x). A complete strategy
*

*> evaluates t to success with computer answer (True/x) and likewise
*

*> (False/x).
*

*>
*

*> t has 3 narrexes (4 steps). I think you disagreed with this
*

*> statement in the past, but I insist.
*

I disagreed with that statement only because I was presupposing

an outermost reduction strategy.

*> 1. t -> let x free in f x
*

*> 2. t -> let x free in g x
*

*> 3. t -> success ? g (True ? False)
*

*> 4. t -> f (True ? False) ? success
*

*>
*

*> In the narrowing step, I bound the free variable x to (True ?
*

*> False) rather than only True or only False, because variables may
*

*> be shared (indeed x is shared in this case).
*

And this is the point I do not understand. In 3. you have chosen

to narrow the narrex (f x), which means that x is instantiated to

True. So if x is shared (as you admit), then the only possible

reduction is

3. t -> success ? g True

and likewise for 4. By using an independent and unconstrained

generator (True ? False) for the variable x in (g x) you break

the sharing.

*> [...]
*

*> Now, here comes the twist.
*

*>
*

*>
*

*> Suppose that g is rigid or residuates on its argument. What are
*

*> the intended results of t? If t is equal to
*

*>
*

*> (let x free in f x) ? (let x free in g x)
*

*>
*

*> the the only result is success with (True/x). Then the
*

*> independence of the order of evaluation argued above is lost. The
*

*> derivations starting with steps 1 and 2 give the intended meaning,
*

*> step 4 is never computed, which is OK, but step 3 gives a wrong
*

*> result.
*

But this can happen only if you break the sharing in 3. But then

you should not replace the variable by a generator in the first

place (after all, g is rigid in this variant).

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Fr Nov 09 2007 - 13:59:06 CET

Date: Fri, 09 Nov 2007 12:55:40 +0100

Hi Sergio!

I disagreed with that statement only because I was presupposing

an outermost reduction strategy.

And this is the point I do not understand. In 3. you have chosen

to narrow the narrex (f x), which means that x is instantiated to

True. So if x is shared (as you admit), then the only possible

reduction is

3. t -> success ? g True

and likewise for 4. By using an independent and unconstrained

generator (True ? False) for the variable x in (g x) you break

the sharing.

But this can happen only if you break the sharing in 3. But then

you should not replace the variable by a generator in the first

place (after all, g is rigid in this variant).

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Fr Nov 09 2007 - 13:59:06 CET

*
This archive was generated by hypermail 2.3.0
: Mi Aug 05 2020 - 07:15:03 CEST
*