Sebastian Fischer wrote:
> 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.
Actually, it is not that coincidental. If you look carefully at the
goal that you have cited, you will notice that the variable p5, which
is instantiated by the left argument, also appears in the right
constraint. If one swaps the two constraints (or if one were using a
right-biased selection strategy), all variables that appear as
arguments of the all function will be instantiated by the other
argument and the all (not . null) constraint effectively acts as a
passive constraint.
Regards
Wolfgang
_______________________________________________
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