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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Wed, 15 Jun 2011 09:34:35 +0200

Sebastian Fischer wrote:

*> Hello Wolfgang,
*

*>
*

*> thanks for clarifying.
*

*>
*

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

*>
*

*> I would expect that MCC terminates in both examples, then.
*

Okay then let's have a closer look. The definition

partition1 l | concat p =:= l & all (not . null) p =:= True = p

where p free

terminates for MCC when computing all solutions. The other definition

partition2 l | all (not . null) p =:= True & concat p =:= l = p

where p free

therefore is more interesting. Since this definition terminates when

partition2 is applied to the empty list, the first interesting case

therefore is partition [_]. So, looking at the constraint alone we have

all (not . null) p1 =:= True & concat p1 =:= [_]

where p1 is a fresh variable. Both arguments of the conjunction can

only proceed with a non-deterministic reduction step and MCC will

choose the left one. (Since both constraints will instantiate p1 the

choice does not matter.) The first solution is p1=[], which trivially

fails in the right argument. The second solution instantiates p1 to

p2:p3. Reducing the all application then yields

(not (null p2) && all (not . null) p3) =:= True & concat (p2:p3)

=:= [_]

At this point the left constraint can only proceed with a non-

deterministic instantiation of p2, so now the concat application is

reduced and we arrive at

(not (null p2) && all (not . null) p3) =:= True & p2 ++ concat p3

=:= [_]

Now both threads can proceed only with a non-deterministic

instantiation of p2. Again the left one is chosen. (And again it

doesn't matter.) The first solution is p2=[] and you can trivially

check that this leads to a failure in the left constraint. The other

solution is p2=(q1:q2) which gives

(not (null (q1:q2)) && all (not . null) p3) =:= True & (q1:q2) ++

concat p3 =:= [_]

~> (not False && all (not . null) p3) =:= True & (q1:q2) ++ concat

p3 =:= [_]

~> (True && all (not . null) p3) =:= True & (q1:q2) ++ concat p3 =:=

[_]

~> all (not . null) p3 =:= True & (q1:q2) ++ concat p3 =:= [_]

~> all (not . null) p3 =:= True & q1 : q2 ++ concat p3 =:= [_]

~> all (not . null) p3 =:= True & q1 =:= _ & q2 ++ concat p3 =:=

[] (*)

At this point the free variables q1 and _ are unified and the two

remaining constraints can once again only proceed with a non-

deterministic instantiation. MCC once again chooses the left argument,

and this time the choice matters since the arguments are going to

instantiate different arguments (p3 vs. q2). If p3 is instantiated

with the empty list [] reduction succeeds after a few more reduction

steps and we have computed the (only) solution partition [_] = [[_]].

If p3 is instantiated with a non-empty list (p4:p5) reduction proceeds

as follows

all (not . null) (p4:p5) =:= True & q2 ++ concat (p4:p5) =:= []

~> (not (null p4) && all (not . null) p5) =:= True & q2 ++ concat

(p4:p5) =:= []

Once again both constraints can proceed only with a non-deterministic

reduction step and again the left one is chosen. The solution

p4=(q3:q4) yields after a few more reduction steps yields

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.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Wed Jun 15 2011 - 18:09:42 CEST

Date: Wed, 15 Jun 2011 09:34:35 +0200

Sebastian Fischer wrote:

Okay then let's have a closer look. The definition

partition1 l | concat p =:= l & all (not . null) p =:= True = p

where p free

terminates for MCC when computing all solutions. The other definition

partition2 l | all (not . null) p =:= True & concat p =:= l = p

where p free

therefore is more interesting. Since this definition terminates when

partition2 is applied to the empty list, the first interesting case

therefore is partition [_]. So, looking at the constraint alone we have

all (not . null) p1 =:= True & concat p1 =:= [_]

where p1 is a fresh variable. Both arguments of the conjunction can

only proceed with a non-deterministic reduction step and MCC will

choose the left one. (Since both constraints will instantiate p1 the

choice does not matter.) The first solution is p1=[], which trivially

fails in the right argument. The second solution instantiates p1 to

p2:p3. Reducing the all application then yields

(not (null p2) && all (not . null) p3) =:= True & concat (p2:p3)

=:= [_]

At this point the left constraint can only proceed with a non-

deterministic instantiation of p2, so now the concat application is

reduced and we arrive at

(not (null p2) && all (not . null) p3) =:= True & p2 ++ concat p3

=:= [_]

Now both threads can proceed only with a non-deterministic

instantiation of p2. Again the left one is chosen. (And again it

doesn't matter.) The first solution is p2=[] and you can trivially

check that this leads to a failure in the left constraint. The other

solution is p2=(q1:q2) which gives

(not (null (q1:q2)) && all (not . null) p3) =:= True & (q1:q2) ++

concat p3 =:= [_]

~> (not False && all (not . null) p3) =:= True & (q1:q2) ++ concat

p3 =:= [_]

~> (True && all (not . null) p3) =:= True & (q1:q2) ++ concat p3 =:=

[_]

~> all (not . null) p3 =:= True & (q1:q2) ++ concat p3 =:= [_]

~> all (not . null) p3 =:= True & q1 : q2 ++ concat p3 =:= [_]

~> all (not . null) p3 =:= True & q1 =:= _ & q2 ++ concat p3 =:=

[] (*)

At this point the free variables q1 and _ are unified and the two

remaining constraints can once again only proceed with a non-

deterministic instantiation. MCC once again chooses the left argument,

and this time the choice matters since the arguments are going to

instantiate different arguments (p3 vs. q2). If p3 is instantiated

with the empty list [] reduction succeeds after a few more reduction

steps and we have computed the (only) solution partition [_] = [[_]].

If p3 is instantiated with a non-empty list (p4:p5) reduction proceeds

as follows

all (not . null) (p4:p5) =:= True & q2 ++ concat (p4:p5) =:= []

~> (not (null p4) && all (not . null) p5) =:= True & q2 ++ concat

(p4:p5) =:= []

Once again both constraints can proceed only with a non-deterministic

reduction step and again the left one is chosen. The solution

p4=(q3:q4) yields after a few more reduction steps yields

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.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Wed Jun 15 2011 - 18:09:42 CEST

*
This archive was generated by hypermail 2.3.0
: Mon Nov 18 2019 - 07:15:08 CET
*