A Variant of Higher-Order Anti-Unification

This is a Java implementation of the higher-order anti-unification algorithm described in:

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

The algorithm solves the following problem:

GIVEN: Higher-order terms t and s.
FIND: A higher-order pattern least general generalization of t and s.

The anti-unification algorithm relies on a subalgorithm that constructively decides about the existence of a variable renaming such that two lambda terms become alpha-equivalent. This subalgorithm can also be accessed separately.
The algorithm works both for untyped and simply-typed λ-terms. For untyped terms, the input should not contain β-redexes. For simply typed terms, the input should be in the η-long β-normal form.

Input Syntax:
Anti-unification problem:
(Use the semicolon to separate
the equations of the system.)
Maximum reduction recursion:
Justify computed generalization: (An error will occure if the justification fails.)
Output format: User friendly:


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):

  • \x.f(x,x) =^= \x.f(a,x)
  • \x.f(b,x) =^= \x.f(a,x)
  • \x,y.f(f(g(x),y),f(g(y),x)) =^= \x,y.f(h(y,g(x)),h(x,g(y)))
  • \x,y.f(x,y) =^= \x,y.f(y,x)
  • \y:i2.\z:i3. f:i2-i3-i1(y,z) =^= \y:i2.\z:i3. x:i3-i2-i1(z,y)
  • \x,y,z.g(f(x,z),f(y,z),f(y,x)) =^= \x,y,z.g(h(y,x),h(x,y),h(z,y))
  • \x,y.f(\z.g(z,y),g(x,y)) =^= \x,y.f(\z.h(y,z),h(y,x))
  • \x.f(\y.g(x,y),\y.g(y,x)) =^= \x.f(\y.h(x,y,x),\y.h(y,x,y))

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