## Wednesday, November 30, 2011

### Term unification in C#

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.