A Unification Algorithm for Second-Order Monadic Terms

William M. Farmer

1988

Abstract

This paper present an algorithm that, given a finite set E of pairs of
second-order monadic terms, returns a finite set U(E) of "substitution
schemata" such that a substitution unifies E iff it is an instance of
some member of U(E).  Moreover, E is unifiable precisely if U(E) is
not empty.  The algorithm terminates on all inputs, unlike the
unification algorithms for second-order monadic terms developed by
G. Huet and G. Winterstein.

The substitution schemata in U(E) use expressions (called "parametric
terms") which represent sets of terms that differ only in how many
times designated strings of (monadic) function constants follow
themselves.  The substitution schemata may contain unresolved
"identity restrictions"; consequently the members of U(E) generally do
not characterize all the unifiers of E in a completely explicit way.

The algorithm is particularly useful for investigating the complexity
of formal proofs.