RISC-Linz RISC-Linz Research Institute for Symbolic Computation  

Unranked Second-Order Anti-Unification

This is a Java implementation of the algorithm described in:

Input Syntax:
Anti-unification problem:
(Use the semicolon to separate
the equations of the system.
Hedge equations are allowed.)
Alignment computation: Longest admissible alignments are computed by computing common subsequences of the word representation of the input hedges. Therefore all the longest common subsequences (in form of alignments) with respect to a given upper bound are tested for admissibility. If none of them is admissible, then the upper bound is reduced.
e.g. a<1.1, 2.2> f<2, 3> a<2.1.2, 3.1>
Justify computed generalization: By obtaining substitutions from the store, instantiating the generalization and comparing the result with the input.
Iterate all possibilities: Compute generalizations for all admissible alignments, or only for the first one.
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):

  • f(a, g(h(a, h(b)))) =^= f(a, a, h(g(b)))
  • f(g(a,a), a, X, b) =^= f(g(b,b), g(Y), b)
  • f(h(c,a,c,a), a, a) =^= f(g(c,b,c,a), b, b)
  • f(x), f(f(g(a,a)), a, a) =^= x, f(g(b,b), b, b)
  • f(x), f(f(g(a,a)), a, a) =^= x, f(g(b,a), a, b)
  • f(x), f(h(f(c,a)), a, c) =^= x, f(g(b,a), a, b)
  • (f(a), f(a)) =^= (f(a), f)
  • if(geq(x1, x2), then(eq(x3, add(x4, x2)), eq(x4, add(x4, 1))), else(eq(x3, sub(x4, x1)))) =^=
    if(geq(y1, y2), then(eq(y3, add(y4, y2)), eq(y5, 1), eq(y4, add(y4, 5))), else(eq(y3, sub(y4, y1))))
  • a, a, b, f, f, f(a, a, b) =^= a, a, c, f, f, f(a, a, c)
  • a, a, b, b, f, f, f(a, a, b, b) =^= a, a, c, f, f, f(a, a, c)
  • f(g(a, X), a, X, b) =^= f(g(b), b))
  • a,a,a,a,a,a,a,a,a,a,a,a =^= a,a,a,a,a,a,a,a,a,a

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