algorithmf#functional-programmingprologunification

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.

Solution

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