Re: residuation for compositional search?

From: Sebastian Fischer <>
Date: Wed, 15 Jun 2011 11:07:42 +0200

> 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

> 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.

curry mailing list
Received on Mi Jun 15 2011 - 18:09:49 CEST

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:11 CEST