Legend has it that a million years ago Plotkin was talking to his professor Popplestone, who said that unification (finding the most general unifier or the MGU) might have an interesting dual, and that Plotkin should find it. It turns out that the dual *is* interesting and it is known as the Least General Generalisation (LGG). Plotkin apparently described both the LGG for terms, and for clauses. I say apparently because I can't find his paper on-line.
The LGG for clauses is more complicated so we'll get back to it after we look at the LGG of terms. We can see how the MGU is related to the LGG by looking at a couple of examples and the above image. We use the prolog convention that function symbols start with lower case, and variables start with uppercase. The image above is organised as a DAG (Directed Acyclic Graph). DAGs are a very important structure in mathematics since DAGs are lattices.
Essentially what we have done is drawn an (incomplete) Hasse diagram for the lattice defined. Each of the arrows in our diagram represents a possible substitution. For instance 'p(X)' can have X substituted for either 's' or 'g(r,Y)'. Anything that can be reached from a series of downward traversals is "unifiable" and the substitution of the unification is the aggregate composition of substitutions we encountered on the path. So for instance 'p(X)' will unify with 'p(g(r,s))' under the substitution X=g(r,Y) and Y=s. Any two terms which are not connected by a path are not unifiable.
The least general generalisation is also apparent in our picture. Any two terms will have a common parent in the Hasse diagram. The least, (in the sense of distance from the top) parent of any two terms in our diagram is the LGG. So actually the connection between the two is fairly straightforward (using 20/20 hindsight).
Essentially what we have done is drawn an (incomplete) Hasse diagram for the lattice defined. Each of the arrows in our diagram represents a possible substitution. For instance 'p(X)' can have X substituted for either 's' or 'g(r,Y)'. Anything that can be reached from a series of downward traversals is "unifiable" and the substitution of the unification is the aggregate composition of substitutions we encountered on the path. So for instance 'p(X)' will unify with 'p(g(r,s))' under the substitution X=g(r,Y) and Y=s. Any two terms which are not connected by a path are not unifiable.
The least general generalisation is also apparent in our picture. Any two terms will have a common parent in the Hasse diagram. The least, (in the sense of distance from the top) parent of any two terms in our diagram is the LGG. So actually the connection between the two is fairly straightforward (using 20/20 hindsight).
Comments
Post a Comment