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