Nominal Anti-Unification
This is a Java implementation of the anti-unification
algorithm for nominal terms described in:
-
Alexander Baumgartner,
Temur Kutsia,
Jordi Levy,
Mateu Villaret.
Nominal Anti-Unification.
In: M. Fernández, editor, Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA 2015. June 29–July 3, 2015, Warsaw, Poland. Vol. 36 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2015, 57–73.
Part of the Library of Unification and Anti-Unification Algorithms.
The algorithm solves the following problem:
| GIVEN: |
Nominal terms t and s of the same sort, a freshness context ∇ and a finite set of atoms A such that t, s, and ∇ are based on A. |
| FIND: |
A term r and a freshness context Γ, such that the term-in-context <Γ, r> is an A-based least general generalization of the terms-in-context <∇, t> and <∇, s>. |
The anti-unification algorithm relies on
a subalgorithm that constructively decides equivariance between
two terms-in-context. This subalgorithm can also be
accessed separately.
Input Syntax:
-
The symbols A-Z, a-z, 1-9 are allowed for atom names,
function names, variable names and sort names. Names can be of any length.
- If the first letter of the name is within [a,e] or [A,E], then it
is an atom.
- If the first letter of the name is within [u,z] or [U,Z], then it
is a variable.
- Otherwise it is a function symbol. The application of a function with arity zero f() may be written as just f.
- The dot "." is used for abstraction.
- The colon ":" is used to declare the sorts.
- If a sort name starts with a capital letter, then it is of sort data.
- The dash "-" is used as type constructor.
- The sharp "#" is used for freshness constrains.
- Mixed mode of typed and untyped calculus is allowed.
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):
- f(a,b) =^= f(a,b)
- f(a,a) =^= f(b,b)
- f(a,a) =^= f(b,c)
- f(a,b) =^= f(b,c)
- f(a:i,a:i):o =^= f:i-i-o(b,b)
- a.a =^= b.c
- a.b =^= b.a
- a.b =^= b.a with extra atom c
- f(a,b) =^= f(Y,(a b)Y) with nabla {b#Y}
- f(b,a) =^= f(Y,(a b)Y) with nabla {b#Y}
- h(a.a, b.b) =^= h(c.Y, c.Y) with nabla {a#Y}
- h(f(X1), c.f(X1)) =^= h(g(X2), c.g(X2)) with nabla {c#X1, c#X2}
- h(f(X1), a.f((a c)X1)) =^= h(g(X2), b.g((b c)X2)) with nabla {a#X1,b#X1,c#X1,a#X2,b#X2,c#X2}
- h(f(X1), a.f(X2)) =^= h(g(X1), a.g(X2)) with nabla {a#X1}
- a.b.c =^= c.a.b
- a.b.b =^= b.b.a
- f(a.b, X) =^= f(b.a, Y) with nabla {c#X}
|
|
