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 Mi Jun 15 2011 - 18:09:42 CEST