Functions-as-Constructors Higher-Order Unification

Abstract

Unification is a central operation in the construction of a range of
computational logic systems based on first-order and higher-order
logics.  First-order unification has a number of properties that
dominates the way it is incorporated within such systems.  In
particular, first-order unification is decidable, unary, and can be
performed on untyped term structures.  None of these three properties
hold for full higher-order unification: unification is undecidable,
unifiers can be incomparable, and term-level typing can dominate the
search for unifiers.  The so-called pattern subset of
higher-order unification was designed to be a small extension to
first-order unification that respected the basic laws governing
lambda-binding (the equalities of alpha, beta, and
eta-conversion) but which also satisfied those three properties.
While the pattern fragment of higher-order unification has been
popular in various implemented systems and in various theoretical
considerations, it is too weak for a number of applications.  In this
paper, we define an extension of pattern unification that is motivated
by some existing applications and which satisfies these three
properties.  The main idea behind this extension is that the arguments
to a higher-order, free variable can be more than just distinct bound
variables: they can also be terms constructed from (sufficient numbers
of) such variables using term constructors and where no argument is a
subterm of any other argument.  We show that this extension to pattern
unification satisfies the three properties mentioned above.