What is a unification algorithm?

Question

Well I know it might sound a bit strange but yes my question is: "What is a unification algorithm". Well, I am trying to develop an application in F# to act like Prolog. It should take a series of facts and process them when making queries.

I was suggested to get started in implementing a good unification algorithm but did not have a clue about this.

Please refer to this question if you want to get a bit deeper to what I want to do.

Thank you very much and Merry Christmas.

Answer 1

If you have two expressions with variables, then unification algorithm tries to match the two expressions and gives you assignment for the variables to make the two expressions the same.

For example, if you represented expressions in F#:

type Expr = 
  | Var of string              // Represents a variable
  | Call of string * Expr list // Call named function with arguments

And had two expressions like this:

Call("foo", [ Var("x"),                 Call("bar", []) ])
Call("foo", [ Call("woo", [ Var("z") ], Call("bar", []) ])

Then the unification algorithm should give you an assignment:

"x" -> Call("woo", [ Var("z") ]

This means that if you replace all occurrences of the "x" variable in the two expressions, the results of the two replacements will be the same expression. If you had expressions calling different functions (e.g. Call("foo", ...) and Call("bar", ...)) then the algorithm will tell you that they are not unifiable.

There is also some explanation in WikiPedia and if you search the internet, you'll surely find some useful description (and perhaps even an implementation in some functional language similar to F#).

Answer 2

I found Baader and Snyder's work to be most informative. In particular, they describe several unification algorithms (including Martelli and Montanari's near-linear algorithm using union-find), and describe both syntactic unification and various kinds of semantic unification.

Once you have unification, you'll also need backtracking. Kiselyov/Shan/Friedman's LogicT framework will help here.

Answer 3

Obviously, destructive unification would be much more efficient than a pure functional one, but much less F-sharpish as well. If it's a performance you're after, probably you will end up implementing a subset of WAM any way:

http://en.wikipedia.org/wiki/Warren_Abstract_Machine

And probably this could help:

http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.3203