> Actually, it is not that coincidental. If you look carefully at the goal
> that you have cited, you will notice that the variable p5, which is
> instantiated by the left argument, also appears in the right constraint.
So here a right-biased strategy would work better, by coincidence.
(By "concidentally" I mean that, in the terminating case, MCC's
strategy picks the better alternative without noticing that it is
better).
> If one swaps the two constraints (or if one were using a right-biased selection
> strategy), all variables that appear as arguments of the all function will
> be instantiated by the other argument and the all (not . null) constraint
> effectively acts as a passive constraint.
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.)
Anyway: my current impression is that implementations of residuation
can be improved by considering information about which variables are
shared. Maybe this would even allow an optimal implementation in the
sense that if a terminating interleaving exists then it will be found.
Sebastian
_______________________________________________
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:49 CEST