Re: residuation for compositional search?

From: Sebastian Fischer <>
Date: Thu, 16 Jun 2011 14:19:23 +0200

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

    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.

curry mailing list
Received on Do Jun 16 2011 - 18:28:35 CEST

This archive was generated by hypermail 2.3.0 : Fr Okt 07 2022 - 07:15:24 CEST