# Nominal Equivariance

This is a Java implementation of the equivariance algorithm for nominal terms described in:

The algorithm solves the following problem:

 GIVEN: A set of of atoms A, nominal equivariance equations of the form t ≈ s and a freshness context ∇, all based on A. FIND: An A-based permutation π, such that π(t) is alpha equivalent to s under ∇ for all equations.

The equivariance algorithm is a part of an algorithm which solves the nominal anti-unification problem. This anti-unification algorithm has also been implemented and is available online.

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.
 Equivariance problem set:(Use the semicolon to separate the equations of the system.) f(a,b) = f(b,c) Freshness context: e.g. a#X, b#Y Justify computed permutation: (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):

 c = a; g(c, b, a) = g(a, c, b) a = b; b = c) g(a, b, a) = g(a, c, b); c = a a.f(a,b) = b.f(b,a) a.f(a,c) = b.f(b,c); a = d a.f(a,a) = a.f(a,b); a = b a.b.f(a,b) = b.a.f(b,a) a.a.b.f(a,b) = a.b.b.f(a,b) a.a.b.f(a,b) = b.a.b.f(a,b) a.a.b.f(a,b) = c.b.a.f(b,a) a.X = b.X with nabla {a#X} a.(a b)X = b.X a.(a b)X = b.X with nabla {a#X} a.(a b)X = b.X; a = b with nabla {a#X} (a b)X = X with nabla {a#X, b#X} (a b)X = X a.(a b)(c d)X = b.X with nabla {a#X} a.f(b, X) = b.f(a, X) with nabla {a#X} a.f(b, (a b)X) = b.f(a, X) with nabla {a#X} (a b)X = (a b)X; b = c with nabla {a#X, c#X}

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