Hello Sebastian,
> My Haskell implementation uses the following heuristics that might
> explain why it works better: guessing unshared variables is better
> than guessing shared variables (but binding shared variables to a
> constructor using =:= is ok). In the goal
>
> all (not . null) p5 =:= True & q2 ++ concat ((q3:q4):p5) =:= []
>
> guessing q2 would be preferred over guessing p5 because q2 is not
> shared but p5 is.
>
> (Actually, my implementation still might terminate by coincidence,
> because even q2 originates from the shared p1 and I'm not sure whether
> my implementation recognizes that q2 is not shared anymore.)
let me check if I'm understanding your heuristics correctly. Given the
definitions
data Tree a = Empty | Node (Tree a) a (Tree a)
tree Empty = success
tree (Node l _ r) = tree l & tree r
leftPath Empty = []
leftPath (Node l x _) = x : leftPath l
and the goal
leftPath t =:= [1,2,3] & tree t where t free
wouldn't your heuristics mean that you are going to instantiate only
the right branches of the tree t, since the variable r in the
definition of tree is not shared, whereas guessing of the left nodes
of the tree would be suspended since they are shared between the tree
constraint and the left path constraint, would it?
If so, you would be unable to compute even one solution (the goal of
course has infinitely many solutions).
Wolfgang
_______________________________________________
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:26 CEST