- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Wolfgang Lux <wlux_at_uni-muenster.de>

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.

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

Date: Tue, 14 Jun 2011 11:37:32 +0200

Sebastian Fischer wrote:

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

*
This archive was generated by hypermail 2.3.0
: Mon Sep 23 2019 - 07:15:08 CEST
*