**Source Code:**unification_2.zip
Yesterday I completed an implementation of an algorithm
calculating the most general unifier of two terms. It took some time to come up
with a term representation that I was happy with, and also to implement it with
a proper parser, following compiler construction methods. I had no deadlines or
budget to worry about, so I took my time to create an easy to use C#
implementation.

I am not an expert in unification theory (it is an entire sub-field in computer
science) so I used the

*Handbook of Automated Reasoning*, Volume 1, as a reference. It contains a chapter by F. Baader and W. Snyder which explains unification very well, so if something in this posting is amiss, I would refer the reader to this resource.
My term representation was discussed in my previous blog
post: http://coffeesmudge.blogspot.com/2011/11/simple-term-parser-in-c.html

**The Unification Problem**

The unification problem is the problem of making two terms
the same by substituting their variables.
The variant of unification that I implemented is syntactic unification, meaning
that the terms are considered to be the equal when they are syntactically
identical. As an example, consider this unification problem: Let’s say that we
have two terms. Term 1 is:

Add(:x, 1)

And Term 2 is:

Add(:y, 1)

The solution to this unification problem is a substitution for the variables :x and :y. These substitutions are called a unifier. So an example of a unifier is

:x => 1 :y => 1

I.e. :x and :y are replaced by 1, making the two terms equal. Now you may point out that there are infinitely many possible unifiers. Some unifiers can be composed from other unifiers. Unifier 1 is more general than unifier 2 if unifier 1 can be composed with some other unifier in order to get unifier 2. The formal version of this definition is given in the Handbook of Automated Reasoning. In my example, the most general unifier is:

x: => :y

And:

y: => :x

As I understand it, these MGUs are equivilant in that they both lead to a unified term. In the unified term the variables may be renamed as long as there are some relation to the original variables in the input terms.

**My Implementation**
Sample output from the attached source code is
given here:

Terms are first parsed into an abstract syntax tree (AST)
using a recursive descent parser. Then the AST terms are conversed into
Entities that are plugged into the unification algorithm. The implementation creates
a copy of the input terms in order to preserve the original two terms.
It then calculates the MGU as explained in the reference, and prints it out on
the console. There are more
efficient algorithms for calculating a MGU, but I did not get around to
researching them, and I need to move forward with the implementation of my
programming language.

**Reference**

Unification Theory from Handbook of Automated Reasoning, Volume 1. Published by Elsivier Science Publishers. 2001. ISBN 0444508139.

## No comments:

## Post a Comment