# Nominal Anti-Unification

This is a Java implementation of the anti-unification algorithm for nominal terms described in:

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.
 Anti-unification problem:(Use the semicolon to separate the equations of the system.) f(a,b) =^= f(b,c) Freshness context: e.g. a#X, b#Y Extra atoms: (Atoms from the problem set / freshness context are automatically carried over.) Justify computed generalization: (An error will occure if the justification fails.) Output format: SimpleVerboseProgress

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}

 Author: Alexander Baumgartner Project: SToUT - Symbolic Computation Techniques for Unranked Terms