Bernd Brassel schrieb:
> Sergio Antoy schrieb:
> > It looks like we have different
> > notions of what can or needs to be evaluated to obtains all the
> > results of a computation. This can be partly due to the semantics
> > or models we have in mind. E.g., Wolfgang thinks functions
> > whereas I think rewrite rules. With a different model, maybe some
> > steps that I would like to perform are not justified.
>
> Could it be that the semantic model you have in mind is that of
> _confluent_ rewriting? That you want to embed the non-confluence of
> non-deterministic functions into a confluent system with special
> treatment of the non-deterministic choice?
Not exactly. The semantics of non-determinism we intend in Curry
is such that computations are confluent (except for the order and
timing in which non-deterministic alternatives are produced), but
here I see the problem as an interaction between order of
evaluation, sharing and non-deterministic choices. The meaning of
(f x ? g x where x free)
as
(f x where x free) ? (g x where x free)
makes sense. Unfortunately, the language syntactically allows the
first form and I am afraid one cannot catch all the variations of
this problem at compile time. Giving the intended semantics
statically might be quite difficult.
> This would enlighten your comment:
>
> > When a variable is shared, a narrowing step must instantiate the
> > variable with a generator, not only with the cases of the function
> > that is narrowing the variable.
>
> and also your reply, to Michael's example:
>
> > Michael's example is another case in point.
> >
> >> f True _ = True
> >> g False = False
> >>
> >> and the expression (f x (g x)). If you reduce the narrex (g x),
> >> you cannot obtain the normal form True.
> >
> > Since x is shared it should be narrowed to (True ? False).
In my opinion, this is mostly or only related to the order of
evaluation. I am thinking about the opportunities that massively
parallel computations would offer. Hence I do not want to count
too much on any specific order.
> Making such non-standard narrowing steps is implemented in kics, since
> mapping to functional programs means that you have to map to a confluent
> system. And, unfortunately, we couldn't add the additional constraint
> "since x is shared" which would make many computations in kics much more
> efficient.
Well... 10 years ago (in my ALP 1997 paper), I defined a narrowing
step as a two-part process in which part 1 is just an
instantiation and part 2 is plain rewriting. The most general
instantiation is a generator. I think this is a simple and
general way to look at narrowing that is useful for both theory
and implementations.
Why you could not add the constraint that x is shared? I
discussed this a bit with Sebastian, when he was here, but it was
not detailed enough. I understand that you map kics to
haskell. If the mapping of kics expressions into haskell
expressions is the identity (or close to it), then controlling
sharing might be difficult or impossible. But I would guess that
there are other mappings that satisfactorily abstract sharing.
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Nov 06 2007 - 08:34:51 CET