Michael Hanus wrote:
> Wolfgang Lux wrote:
> > I think sharing of variables across different branches of a
> > non-deterministic choice should only be a matter of optimization.
> > An implementation *may* choose to share variables across
> > non-deterministic branches if it can prove that this does not affect
> > the results computed (though eventually the order in which they are
> > computed). On the other hand, within a particular branch of a
>
> I fully agree to this. I think that sharing is heavily related
> to the details of the operational semantics. For instance,
> sharing is important to obtain optimal evaluation in
> demand-driven strategies. It is required for non-confluent
> programs evaluated by a demand-driven strategy if the declarative
> semantics is based on CRWL. Thus, if the declarative semantics
> of a language like Curry or Toy is based on CRWL,
> sharing between non-deterministic branches can be an important
> optimization (in particular contexts) but is not strictly required.
> If one wants to have more, it should be justified by a
> declarative semantics in order to make it comprehensible
> without any reference to a complex strategy.
Sorry for stirring this up. I think it is of marginal importance
for the large majority of program.
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).
------------------------------------------------------------------
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. 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.
Note that this optimization is possible only if the semantics
guarantee the independence of the order of evaluation.
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Nov 01 2007 - 23:50:33 CET