Computation of Permuting Matcher for Lambda Terms
This is a Java implementation of the permuting matcher computation for lambda terms described in:
-
Alexander Baumgartner,
Temur Kutsia,
Jordi Levy,
Mateu Villaret.
A Variant of Higher-Order Anti-Unification.
In: F. van Raamsdonk, editor, Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013. June 24-26, 2013, Eindhoven, The Netherlands. Vol. 21 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2013, 113-127.
Part of the Library of Unification and Anti-Unification Algorithms.
The algorithm solves the following problem:
| GIVEN: |
A set of equations of the form t ≈ s where t and s are lambda terms, and two sets of variables, the Domain and the Range. |
| FIND: |
A variable renaming ρ:Domain --> Range, such that ρ(t) is alpha equivalent to s for all equations t ≈ s. |
The equivariance algorithm is a part of an algorithm which solves the higher-order 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 variable names and
function names. Names can be of any length.
- If the first letter of the name is within [u,z] or [U,Z], then it
is a variable.
- The backslash "\" is used for the lambda symbol.
- The colon ":" is used to declare the type.
- The dash "-" is used as type constructor.
- 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):
- \y.f(x,y) = \x.f(y,x)
- x(y,z) = y(z,x)
- x:i-o(y:i-o,z:i) = y:i-o(z:i,x:i-o)
- \u.u(f(x,z),u(y,z),f(y,v)) = \v.v(f(y,x),v(z,x),f(z,u))
|
|
