RISC RISC Research Institute for Symbolic Computation  

Nominal Equivariance

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

Part of the Library of Unification and Anti-Unification Algorithms.

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:
Equivariance problem set:
(Use the semicolon to separate
the equations of the system.)
Freshness context: e.g. a#X, b#Y
Justify computed permutation: (An error will occure if the justification fails.)
Output format:


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 FWF Der Wissenschaftsfond
Project: SToUT - Symbolic Computation Techniques for Unranked Terms