I'm working through my AI textbook I got and I've come to the last homework problem for my section:
"Implement the Unification Algorithm outlined on page 69 in any language of your choice."
On page 69, you have the following pseudo-code for the unification algorithm:
function unify(E1, E2);
begin
case
both E1 and E2 are constants or the empty list:
if E1 = E2 then return {}
else return FAIL;
E1 is a variable:
if E1 occurs in E2 then return FAIL
else return {E2/E1}
E2 is a variable
if E2 occurs in E1 then FAIL
else return {E1/E2}
either E1 or E2 are empty then return FAIL
otherwise:
begin
HE1 := first element of E1;
HE2 := first element of E2;
SUBS1 := unify(HE1, HE2);
if SUBS1 := FAIL then return FAIL;
TE1 := apply(SUBS1, rest of E1);
TE2 := apply(SUBS1, rest of E2);
SUBS2 := unify(TE1, TE2);
if SUBS2 = FAIL then return FAIL;
else return composition(SUBS1, SUBS2)
end
end
end
Now, I understand the general concept of unification but I have absolutely no idea how I would even begin to implement this in a language like Java or C#.
I'm not even sure what the method signature would look like. What type of variables would it take? I'm fairly certain I need to return lists to represent predicate calculus constructs but that is a guess.
For example, when it says "E1 is a variable", well, if I'm passing it into the Unify method, how could it be anything but? I could check for null but would that be different than "empty list"?
Can anyone help me or point me in the right direction for implementing the Unificaiton algorithm in C# or Java?
Syntactical first-order unification is used in logic programming and programming language type system implementation, especially in Hindley–Milner based type inference algorithms. Semantic unification is used in SMT solvers, term rewriting algorithms and cryptographic protocol analysis.
Unification is used in logical programming where the aim is to make expressions look identical to each other, and in order to make them identical, we generally use substitution. Substitution means replacing one variable with another term.
Unification: It is the act of unifying the different laws valid for different phenomena in to a single theory that explains all the different phenomena. Eg. Electricity, magnetism and light are different phenomena and have different laws of physics for each of them.
For anyone interested I found the same algorithm at http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html with a bit more context.
Lets look at the first line:
function unify(E1, E2)
E1 and E2 are expressions: either lists, variables, or constants. In traditional OOP style typically we would create an abstract base class Expression
and derive other classes from it like List
, Variable
, or Constant
. However in my opinion this is overkill. I implemented this in C# using the dynamic
keyword.
The next question is what does it return? A list of bindings which can be implemented as a Dictionary<string, Object>
.
Below is a snippet from the C# implementation of an implementation from a library called Jigsaw that I am developing for teaching how to implement languages C#.
public static Dictionary<string, object> Unify(dynamic e1, dynamic e2)
{
if ((IsConstant(e1) && IsConstant(e2)))
{
if (e1 == e2)
return new Dictionary<string,object>();
throw new Exception("Unification failed");
}
if (e1 is string)
{
if (e2 is List && Occurs(e1, e2))
throw new Exception("Cyclical binding");
return new Dictionary<string, object>() { { e1, e2 } };
}
if (e2 is string)
{
if (e1 is List && Occurs(e2, e1))
throw new Exception("Cyclical binding");
return new Dictionary<string, object>() { { e2, e1 } };
}
if (!(e1 is List) || !(e2 is List))
throw new Exception("Expected either list, string, or constant arguments");
if (e1.IsEmpty || e2.IsEmpty)
{
if (!e1.IsEmpty || !e2.IsEmpty)
throw new Exception("Lists are not the same length");
return new Dictionary<string, object>();
}
var b1 = Unify(e1.Head, e2.Head);
var b2 = Unify(Substitute(b1, e1.Tail), Substitute(b1, e2.Tail));
foreach (var kv in b2)
b1.Add(kv.Key, kv.Value);
return b1;
}
You can find the rest of the algorithm code online at http://code.google.com/p/jigsaw-library/source/browse/trunk/Unifier.cs. Not that in this example the List
class is actually a Lisp-style list that I implemented for the library.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With