Java – implementing unification algorithm

javaunification

I worked the last 5 days to understand how unification algorithm works in Prolog .
Now ,I want to implement such algorithm in Java ..

I thought maybe best way is to manipulate the string and decompose its parts using some datastructure such as Stacks ..

to make it clear :

suppose user inputs is:
a(X,c(d,X)) = a(2,c(d,Y)).

I already take it as one string and split it into two strings (Expression1 and 2 ).
now, how can I know if the next char(s) is Variable or constants or etc.. ,
I can do it by nested if but it seems to me not good solution ..
I tried to use inheritance but the problem still ( how can I know the type of chars being read ?)

Best Answer

First you need to parse the inputs and build expression trees. Then apply Milner's unification algorithm (or some other unification algorithm) to figure out the mapping of variables to constants and expressions.

A really good description of Milner's algorithm may be found in the Dragon Book: "Compilers: Principles, Techniques and Tools" by Aho, Sethi and Ullman. (Milners algorithm can also cope with unification of cyclic graphs, and the Dragon Book presents it as a way to do type inference). By the sounds of it, you could benefit from learning a bit about parsing ... which is also covered by the Dragon Book.

EDIT: Other answers have suggested using a parser generator; e.g. ANTLR. That's good advice, but (judging from your example) your grammar is so simple that you could also get by with using StringTokenizer and a hand-written recursive descent parser. In fact, if you've got the time (and inclination) it is worth implementing the parser both ways as a learning exercise.

Related Solutions

C# – Simplest example of need for “unification” in type inference

public Type inferType(ITypeEnvironment typeEnvironment)
{
    return typeEnvironment.getType(name);
}

What if you just don't know the type of the variable? That's the whole point of type inference, right? Something very simple like this (in some pseudocode language):

function foo(x) { return x + 5; }

You don't know the type of x, until you infer the addition, and realize that it must be an integer because it's added to an integer, or something like that.

What if you have another function like this:

function bar(x) { return foo(x); }

You can't figure out the type of x until you have figured out the type of foo, and so on.

So when you first see a variable, you have to just assign some placeholder type for a variable, and then later, when that variable is passed to some kind of function or something, you have to "unify" it with the argument type of the function.

R – Higher-order unification

State of the art — yes, so far as I know all algorithms more or less take the same shape as Huet's (I follow theory of logic programming, although my expertise is tangential) provided you need full higher-order matching: subproblems such as higher-order matching (unification where one term is closed), and Dale Miller's pattern calculus, are decidable.

Note that Huet's algorithm is the best in the following sense — it is like a semi-decision algorithm, in that it will find the unifiers if they exist, but it is not guaranteed to terminate if they do not. Since we know that higher-order unification (indeed, second-order unification) is undecidable, you can't do better than that.

Explanations: The first four chapters of Conal Elliott's PhD thesis, Extensions and Applications of Higher-Order Unification should fit the bill. That part weighs almost 80 pages, with some dense type theory, but its well motivated, and is the most readable account I've seen.

Examples: Huet's algorithm will come up with the goods for this example: [X(o), Y(succ(0))]; which of necessity will perplex a first-order unification algorithm.

Best Answer

Related Solutions

C# – Simplest example of need for “unification” in type inference

R – Higher-order unification

Related Topic