Re: residuation for compositional search?

From: Sebastian Fischer <>
Date: Wed, 15 Jun 2011 10:23:23 +0200

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..


curry mailing list
Received on Mi Jun 15 2011 - 18:09:47 CEST

This archive was generated by hypermail 2.3.0 : Sa Dez 09 2023 - 07:15:12 CET