Sergio Antoy wrote:
> But the key problem is not the details of the operational
> semantics, but the independence of the order of evaluation. What
> does that mean in non-confluent programs? A formal definition is
> in Antoy and Brassel PPDP07. Informally, the order in which
> non-overlapping narrexes are reduced does not affect the result.
> Now consider:
>
> 1+x ? zero x
>
> where x is free and zero 0 = 0. There are only to narrexes: the
> whole term and zero x. They are non-overlapping. These are two
> complete computations.
>
> 1+x ? zero x -> 1+x
> 1+x ? zero x -> 1+0 ? 0 -> 1+0 -> 1
>
> In this program, the choice of the initial narrex affect the
> result of the computation. How can we fix this? Abolish
> residuation (thanks Bernd). Share variables always (thanks Curry
> Report). Claim the independence of the order of evaluation except
> for (?) (less desirable).
I'm sorry, but your reduction is wrong. The first and only redex of
1+x ? zero x is the operator (?) itself. Its definition is a
non-deterministic choice between (\x y -> x) and (\x y -> y). So
the two alternative reductions for 1+x ? zero x are
1+x ? zero x ~~> (\x y -> x) (1+x) (zero x) ~~> 1+x ~~> suspend
and
1+x ? zero x ~~> (\x y -> y) (1+x) (zero x) ~~> zero x ~~> {x=0} 0
> ------------------------------------------------------------------
>
> Here are other replies:
>
> Paco's example:
>
> f 0 = 0
> g 1 = 1
> f x ? g x where x free
>
> The results are 0 and 1 independently of the order of evaluation
> whether or not x is shared, since there is no residuation (easy
> to verify all the possibilities).
>
> ------------------------------------------------------------------
>
> Wolfgang question:
>
> Why in
>
> positive :: Int -> Bool
> positive(p ? q)
>
> the redex p?q should not be reduced first? Several reasons: if
> neither p nor q evaluate to a normal form, the reduction of p?q is
> useless.
Looks like I was particularly dense when asking my question. Of course
one must reduce positive first in a language with outermost reduction.
And it is no surprise that you can end up with doing redundant work or
even with complete failure when evaluating an inner node like (p?q)
first. This is just the well known advantage of outermost reduction that
it can avoid non-termination and redundant computations, including
non-deterministic choices in the functional-logic setting. So an
optimization that would evaluate (p?q) first would be correct only
when positive demands its argument.
> Furthermore, if p (resp. q) fails, p?q can be reduced to
> q (resp. p) without ever creating a choice point, or cloning the
> context, or performing whatever other typically expensive
> operation is required by non-deterministic choices.
Yet, how do you want to find out that p or q fails without performing
the reduction? If this is known at compile time (stupid example:
failed ? 0), then you should replace the expression by the other
non-failing expression. But if it is not known at compile time I
do not see any chance to avoid the non-deterministic choice.
Regards
Wolfgang
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Nov 02 2007 - 11:06:47 CET