Term Graph Anti-Unification
This is a Java implementation of the algorithm described in:
See also
Part of the Library of Unification and Anti-Unification Algorithms.
Input Syntax:
-
Term graphs are collections of recursion equations with a well defined root. I.e., they are mappings from variables to terms. The first variable in the input field is taken as the root of the graph. Term graphs have the following form:
{x0 = t0, ..., xn = tn, X0 = Y0, ..., Xm = Ym}
where x0,...,xn are term recursion variables, t0,...,tn are terms, X0,...,Xm are hedge recursion variables, and Y0,...,Ym are hedge variables.
-
The symbols [a-zA-Z1-9_] are allowed for variable names and
function names. Names can be of any length.
- If the first letter of the name is within [u-zU-Z], then it is a variable.
- If the first letter is an upper case letter then it is a hedge variable.
- Otherwise, it is a term variable.
- Otherwise, it is a function symbol.
- The free variables of the two input graphs have to be disjoint.
This software is released under the
GNU Lesser General Public License ("LGPL").
For presentation purpose, the Java source code has been translated into JavaScript by the
GWT compiler.
Some examples (click on them to prepared the input form):
-
x=f(x,y), y=a;
y=f(x,y), x=a
-
x=f(x,y), y=f(x,y);
y=f(x,y), x=f(x,y)
-
x0 = f(x1,x2,x3,x0,x3,x2,x3), x1 = g(x1,x2), x2 = b, x3 = a;
y0 = f(y1,y0,y3), y1 = g(y1,y2), y2 = b, y3 = a
|
|
