Unranked Second-Order Anti-Unification — Extended Version

This is a Java implementation of an extended version of the algorithm described in:

Alexander Baumgartner, Temur Kutsia. Unranked Second-Order Anti-Unification.
Information and Computation, 255:262-286, 2017.

We provide an additional rule called "Eleminate siblings of context-holes" which makes the resulting generalizations less general than those described in the paper. In addidion this extended version also allows the user to specify commutative function symbols.

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

Input Syntax:

The symbols [a-zA-Z1-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-zU-Z], then it is a variable.
- If the variable is applied to a hedge then it is a context variable (e.g. X(a, b)).
- Otherwise, it is a hedge variable (e.g. f(x, a)).
Otherwise, it is a function symbol.
The input hedges have to be variable disjoint.

Anti-unification problem: (Use the semicolon to separate the equations of the system. Hedge equations are allowed.)	f(g(c,a),b) =^= f(b,f(a,a,a,c))
Alignment computation:	Compute longest admissible alignments.	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.
Alignment computation:	Input an alignment by hand.	e.g. a<1.1, 2.2> f<2, 3> a<2.1.2, 3.1>
Commutative function symbols:	e.g. f,g,...	Commutative root hedge:
Upper bound for iterating commutative arrangements:	e.g. 5000000	Minimum alignment length:
Filter equal results:	This is a simple equality filter, respecting commutativity.
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:		EXPERIMENTAL! Eleminate siblings of context-holes:

Your web browser must have JavaScript enabled in order for this application to work.

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(h(g(b)),a,a)
f(c), f(f(g(a, a)), a, a) =^= f(g(b, b, b), b, b, b),c
f(a, h(a,a,c,c), a) =^= f(g(c,b,c,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))))

if(eq(n,0), 1,
    if(eq(n,1), times(1,1),
           if(eq(n,2), times(2,times(1,1)),
                  if(eq(n,3), times(3,times(2,times(1,1))))
           )
    )
)
=^=
if(eq(n,0), 0,
    if(eq(n,1), subtract(0,1),
           if(eq(n,2), subtract(subtract(0,1),2),
                  if(eq(n,3), subtract(subtract(subtract(0,1),2),3))
           )
    )
)

a, a, b, f, f, f(a, a, b) =^= f, f(a, c, a), f, c, a, a
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(a(a())))))))))))

Authors:	Alexander Baumgartner and David Cerna
Project:	SToUT - Symbolic Computation Techniques for Unranked Terms GALA - Generalization Algorithms and Applications