Nominal Equivariance
This is a Java implementation of the equivariance
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: |
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.
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}
|
|
