Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How can I implement the unification algorithm in a language like Java or C#?

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?

like image 517
Mithrax Avatar asked Sep 08 '09 22:09

Mithrax


People also ask

What are the applications of the unification algorithm?

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.

What is unification Why is it important in logic programming?

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.

What is unification give an example?

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.


1 Answers

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.

like image 51
cdiggins Avatar answered Nov 23 '22 08:11

cdiggins