Hello Wolfgang,
thank you for your careful analysis. It shows clearly why MCC fails to
terminate and how this failure to fail in finite time relates to MCC's
strategy of solving concurrent constraints:
> all (not . null) p5 =:= True & q2 ++ concat ((q3:q4):p5) =:= []
>
> This is just a variation of the goal marked with (*) above, so reduction
> will never terminate with a finite failure.
If MCC would guess q2 here, both branches would fail, but because MCC
continues with the left constraint repeatedly, it will never recognize
that the right constraint is unsatisfiable.
With partition1, the left-biased interleaving seems to reach finite
failure coincidentally.
This come as a surprise to me because I have an implementation of
residuation in Haskell that terminates for (variants of) both
partition1 and partition2. I have no idea yet, whether this is by
coincidence. I shall eventually check..
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 15 2011 - 18:09:47 CEST