Sorry Wolfgang, I think I missed your point in the previous mail.
Now I think your point was that preferring unshared variables (if
there are infinitely many) may result in never guessing shared
variables and, hence, divergence.
Let's try your example step by step.
leftPath t =:= [1,2,3] & tree t where t free
Here we need to guess t. The binding t=Empty leads to a failure
immediately, so let's bind t to Node l1 x1 r1
leftPath (Node l1 x1 r1) =:= [1,2,3] & tree (Node l1 x1 r1) where
l1,x1,r1 free
Now both constraints can proceed deterministically, so let's
(arbitrarily) take the left one:
(x1 : leftPath l1) =:= [1,2,3] & tree (Node l1 x1 r1) where ... free
The left constraint can proceed further and binds x1 to 1.
leftPath l1 =:= [2,3] & tree (Node l1 x1 r1)
Now only the right branch can proceed deterministically:
leftPath l1 =:= [2,3] & tree l1 & tree r1
As l1 is shared, the heuristics would prefer to bin r1 in the third
constraint. Let's first try r1=Empty.
leftPath l1 =:= [2,3] & tree l1 & tree Empty
Now the third constraint succeeds and l1 is guessed because there is
no unshared variable left. l1=Empty fails immediately, so let's use a
node.
left (Node l2 x2 r2) =:= [2,3] & tree (Node l2 x2 r2)
This step is very similar to the second step. Eventually, the first solution
Node (Node (Node Empty 3 Empty) 2 Empty) 1 Empty
will be found using similar steps. Let's see what happens if we try
l1=Node l3 x3 r3 instead:
leftPath l1 =:= [2,3] & tree l1 & tree (Node l3 x3 r3)
leftPath l1 =:= [2,3] & tree l1 & tree l3 & tree r3
Again, l3 and r3 will be guessed first, because (unlike l1) they are
not shared. In the branches where both are Empty, l1 will be bound and
results will be found.
So, at least in this example, the heuristics seems to work fine.
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Jun 16 2011 - 18:28:35 CEST