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

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>

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

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 Thu Jun 16 2011 - 18:28:35 CEST

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

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 Thu Jun 16 2011 - 18:28:35 CEST

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