CODEWITHSUNDEEP
algorithmf#functional-programmingprologunification
Andry
Andry

Reputation: 16875

What is a unification algorithm?

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.

Upvotes: 5

Views: 2623

Answers (3)

SK-logic
SK-logic

Reputation: 9725

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:

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

And probably this could help: Andre Marien, Bart Demoen: A new Scheme for Unification in WAM.

Upvotes: 1

Frank Shearar
Frank Shearar

Reputation: 17142

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.

Upvotes: 2

Tomas Petricek
Tomas Petricek

Reputation: 243116

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

Upvotes: 5

Related Questions