Re: residuation for compositional search?

From: Wolfgang Lux <>
Date: Tue, 14 Jun 2011 11:37:32 +0200

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.


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.

  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
Received on Di Jun 14 2011 - 17:39:56 CEST

This archive was generated by hypermail 2.3.0 : Mo Okt 26 2020 - 07:15:05 CET