Hello Wolfgang,
thanks for clarifying.
> MCC's strategy uses stability like AKL, i.e., it performs a
> non-deterministic reduction steps only when no thread can perform a
> deterministic reduction step (Andorra principle) and when only
> non-deterministic reduction steps are possible MCC systematically chooses
> the "left-most" thread (stability).
I would expect that MCC terminates in both examples, then.
> On the other hand, reduction of the
> concat application introduces fresh variables that are becoming subject to
> narrowing themselves by the second rule of concat:
> concat (xs:xss) = xs ++ concat xss
> So this constraint has an infinite search space as well (repeatedly
> instantiating xs in the above rule to the empty list []).
Whenever xs is bound to [] by this constraint, the branch can be
refused by the other constraint (which checks that xs is not null).
Then, I would expect that xs is bound to (y:ys) which allows concat to
produce a list headed by y. This is only possible a finite number of
times, afterwards even the binding of xs to a non-empty list will fail
because the result of concat should be empty.
Am I missing something?
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Jun 14 2011 - 18:30:07 CEST