Sebastian Fischer wrote:
> Wolfgang, can you clarify MCC's strategy of solving concurrent
> constraints?
Sure :-)
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).
So using the well known example of subtraction on natural numbers
(using a rigid addition function for the sake of the example)
nat n = fcase n of { Z -> success; S n' -> nat n' }
add m n = case m of { Z -> n; S m' -> S (add m' n) }
it doesn't matter (for MCC) whether you define your subtraction
function as
sub m n | nat d & add n d =:= m = d where d free
or as
sub m n | add n d =:= m & nat d = d where d free
However, if you look at an example where you have two generator
threads for independent variables, the order of constraints becomes
relevant. Say you are enumerating points in a two dimensional plane of
natural numbers (N*N) and
write the constraint
nat x & nat y where x,y free
then MCC will reliably enumerate points on the y-axis ({x=Z, y=Z},
{x=Z, y=S Z}, etc.). I somewhat dislike that this left-to-right bias
destroys the symmetry of (&), but it the end I was convinced that it
is necessary to provide a reliable and stable strategy for enumerating
solutions in multi-dimensional search spaces.
Regards
Wolfgang
PS I had a look at your example and tried to understand why (or why
not) particular implementations would terminate, but this is going to
become fairly complicated.
In
partition l | all (not . null) p =:= True & concat p =:= l & = p
where p free
you have quite a few generators with potentially infinite search spaces.
The constraint all (not . null) p is farily easy: It non-
deterministically generates an infinite number of solutions for p
(namely lists of the form [(a1:b1),...,(ai:bi)] for i >= 0).
The constraint concat p =:= l is a bit more complicated. On one hand,
this expression essentially is reduced into (length l) concurrent
constraints (one for each argument of the list l, as (=:=) on non-
empty lists is reduced via x:xs =:= y:ys = x=:=y & xs=:=ys). 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 []).
Maybe this helps to figure out yourself why particular solutions would
terminate (I gave up after a while :-).
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Jun 14 2011 - 17:39:56 CEST