# Efficient Full Higher-Order Unification

Petar Vukmirović  Vrije Universiteit Amsterdam, De Boelelaan 1111, 1081 HV
Amsterdam, The Netherlands<EMAIL_ADDRESS>,  Alexander Bentkamp  Vrije
Universiteit Amsterdam, De Boelelaan 1111, 1081 HV Amsterdam, The Netherlands
<EMAIL_ADDRESS>and  Visa Nummelin  Vrije Universiteit Amsterdam, De
Boelelaan 1111, 1081 HV Amsterdam, The Netherlands<EMAIL_ADDRESS>
###### Abstract.

We developed a procedure to enumerate complete sets of higher-order unifiers
based on work by Jensen and Pietrzykowski. Our procedure removes many
redundant unifiers by carefully restricting the search space and tightly
integrating decision procedures for fragments that admit a finite complete set
of unifiers. We identify a new such fragment and describe a procedure for
computing its unifiers. Our unification procedure, together with new higher-
order term indexing data structures, is implemented in the Zipperposition
theorem prover. Experimental evaluation shows a clear advantage over Jensen
and Pietrzykowski’s procedure.

###### Key words and phrases:

unification, higher-order logic, theorem proving, term rewriting, indexing
data structures

##  1\. Introduction

Unification is concerned with finding a substitution that makes two terms
equal, for some notion of syntactic equality. Since the invention of
Robinson’s first-order unification algorithm [22], it has become an
indispensable tool in theorem proving, logic programming, natural language
processing, programming language compilation and other areas of computer
science.

Many of these applications are based on higher-order formalisms and require
higher-order unification. Due to its undecidability and explosiveness, the
higher-order unification problem is considered one of the main obstacles on
the road to efficient higher-order tools.

One of the reasons for higher-order unification’s explosiveness lies in _flex-
flex pairs_ , which consist of two variable-headed terms, e.g.,
$F\,X\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{a}$, where $F$, $G$,
and $X$ are variables and $\mathsf{a}$ is a constant. Even this seemingly
simple problem has infinitely many incomparable unifiers. One of the first
methods designed to combat this explosion is Huet’s preunification [12]. Huet
noticed that some logical calculi would remain complete if flex-flex pairs are
not eagerly solved but postponed as constraints. If only flex-flex constraints
remain, we know that a unifier must exist and we do not need to solve them.
Huet’s preunification has been used in many reasoning tools including Isabelle
[20], Leo-III [25], and Satallax [4]. However, recent developments in higher-
order theorem proving [2, 3] require full unification—i.e., enumeration of
unifiers even for flex-flex pairs, which is the focus of this article.

Jensen and Pietrzykowski’s (JP) procedure [13] is the best known procedure for
this purpose (Section 2). Given two terms to unify, it first identifies a
position where the terms disagree. Then, in parallel branches of the search
tree, it applies suitable substitutions, involving a variable either at the
position of disagreement or above, and repeats this process on the resulting
terms until they are equal or trivially nonunifiable.

Building on the JP procedure, we designed a new procedure (Section 3) with the
same completeness guarantees (Section 4). The new procedure addresses many of
the issues that are detrimental to the performance of the JP procedure. First,
the JP procedure does not terminate in many cases of obvious nonunifiability,
e.g., for $X\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}\,X$, where $X$ is a
non-functional variable and $\mathsf{f}$ is a function constant. This example
also shows that the JP procedure does not generalize Robinson’s first-order
procedure gracefully. To address this issue, our procedure detects whether a
unification problem belongs to a fragment for which unification is decidable
and finite complete sets of unifiers (CSUs) exist. We call algorithms that
enumerate elements of the CSU for such fragments _oracles_. Noteworthy
fragments with oracles are first-order terms, patterns [19], functions-as-
constructors [16], and a new fragment we present in Section 5. The unification
procedures of Isabelle and Leo-III check whether the unification problem
belongs to a decidable fragment, but we take this idea a step further by
checking this more efficiently and for every subproblem arising during
unification.

Second, the JP procedure computes many redundant unifiers. Consider the
example $F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b}$, where it
produces, in addition to the desired unifiers $\\{F\mapsto\lambda x.\,H\\}$
and $\\{G\mapsto\lambda x.\,\mathsf{b}\\}$, the redundant unifier
$\\{F\mapsto\lambda x.\,H,\;G\mapsto\lambda x.\,x\\}$. The design of our
procedure avoids computing many redundant unifiers, including this one.
Additionally, as oracles usually return a small CSU, their integration reduces
the number of redundant unifiers.

Third, the JP procedure applies more explosive rules than Huet’s
preunification procedure to flex-rigid pairs. To gracefully generalize Huet’s
procedure, we show that his rules for flex-rigid pairs suffice to enumerate
CSUs if combined with appropriate rules for flex-flex pairs.

Fourth, the JP procedure repeatedly traverses the parts of the unification
problem that have already been unified. Consider the problem
$\mathsf{f}^{100}\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}^{100}\,(H\,\mathsf{b})$,
where the exponents denote repeated application. It is easy to see that this
problem can be reduced to
$G\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}H\,\mathsf{b}$. However, the JP
procedure will wastefully retraverse the common context $\mathsf{f}^{100}[\;]$
after applying each new substitution. Since the JP procedure must apply
substitutions to the variables occurring in the common context above the
disagreement pair, it cannot be easily adapted to eagerly decompose
unification pairs. By contrast, our procedure is designed to decompose the
pairs eagerly, never traversing a common context twice.

Last, the JP procedure does not allow to apply substitutions and
$\beta$-reduce lazily. The rules of simpler procedures (e.g., first-order [11]
and pattern unification [19]) depend only on the heads of the unification
pair. Thus, to determine the next step, implementations of these procedures
need to substitute and $\beta$-reduce only until the heads of the current
unification pair are not mapped by the substitution and are not
$\lambda$-abstractions. Since the JP procedure is not based on the
decomposition of unification pairs, it is unfit for optimizations of this
kind. We designed our procedure to allow for this optimization.

To more efficiently find terms (in a large term set) that are unifiable with a
given query term, we developed a higher-order extension of fingerprint
indexing [23] (Section 6). We implemented our procedure, several oracles, and
the fingerprint index in the Zipperposition prover (Section 7). Since a
straightforward implementation of the JP procedure already existed in
Zipperposition, we used it as a baseline to evaluate the performance of our
procedure (Section 8). The results show substantial performance improvements.

This invited article is an extended version of our FSCD-2020 paper [30]. Most
notable extension is the Section 4, which gives the detailed proof of
completeness of our new procedure. In addition, we give proofs for all the
unproved statements from the paper, expand the examples and provide more
detailed explanations.

##  2\. Background

Our setting is the simply typed $\lambda$-calculus. Types
$\alpha,\beta,\gamma$ are either base types or functional types
$\alpha\rightarrow\beta$. By convention, when we write
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$, we assume
$\beta$ to be a base type. Basic terms are free variables (denoted
$F,G,H,\dots$), bound variables ($x,y,z$), and constants
($\mathsf{f},\mathsf{g},\mathsf{h}$). Complex terms are applications of one
term to another ($s\,t$) or $\lambda$-abstractions ($\lambda x.\,s$).
Following Nipkow [19], we use these syntactic conventions to distinguish free
from bound variables. Bound variables with no enclosing binder, such as $x$ in
$\lambda y.\,x$, are called _loose bound variables_. We say that a term
without loose bound variables is _closed_ and a term without free variables is
_ground_. Iterated $\lambda$-abstraction $\lambda x_{1}\ldots\lambda
x_{n}.\,s$ is abbreviated as $\lambda\overline{x}_{n}.\,s$ and iterated
application $(s\,t_{1})\,\ldots\,t_{n}$ as $s\,\overline{t}_{n}$, where $n\geq
0$. Similarly, we denote a sequence of terms $t_{1},\ldots,t_{n}$ by
$\overline{t}_{n}$, omitting its length $n\geq 0$ where it can be inferred or
is irrelevant. Parameters and body for any term $\lambda\overline{x}.\,s$ are
defined to be $\overline{x}$ and $s$ respectively, where $s$ is not a
$\lambda$-abstraction. The _size_ of a term is inductively defined as
$\text{size}(F)=1$; $\text{size}(x)=1$; $\text{size}(\mathsf{f})=1$;
$\text{size}(s\,t)=\text{size}(s)+\text{size}(t)$; $\text{size}(\lambda
x.\,s)=\text{size}(s)+1$.

We assume the standard notions of $\alpha$-, $\beta$-, $\eta$-conversions. A
term is in _head normal form_ (hnf) if it is of the form
$\lambda\overline{x}.\,a\,\overline{t}$, where $a$ is a free variable, bound
variable, or a constant. In this case, $a$ is called the _head_ of the term.
By convention, $a$ and $b$ denote heads. If $a$ is a free variable, we call it
a _flex_ head; otherwise, we call it a _rigid_ head. A term is called flex or
rigid if its head is flex or rigid, respectively. By
${s}_{\downarrow{\textsf{h}}}$ we denote the term obtained from a term $s$ by
repeated $\beta$-reduction of the leftmost outermost redex until it is in hnf.
Unless stated otherwise, we view terms syntactically, as opposed to
$\alpha\beta\eta$-equivalence classes. We write
$s\leftrightarrow^{*}_{\alpha\beta\eta}t$ if $s$ and $t$ are
$\alpha\beta\eta$-equivalent. Substitutions ($\sigma,\varrho,\theta$) are
functions from free and bound variables to terms; $\sigma t$ denotes
application of $\sigma$ to $t$, which $\alpha$-renames $t$ to avoid variable
capture. The composition $\varrho\sigma$ of substitutions is defined by
$\mathopen{}\mathclose{{}\left(\varrho\sigma}\right)t=\varrho\mathopen{}\mathclose{{}\left(\sigma
t}\right)$. A variable $F$ is mapped by $\sigma$ if $\sigma
F\not\leftrightarrow^{*}_{\alpha\beta\eta}F$. Given a substitution $\varrho$,
which maps $F$ to $s$, we write $\varrho\setminus\\{F\mapsto s\\}$ to denote a
substitution that does not map $F$ and otherwise coincides with $\varrho$.
Given substitutions $\varrho$ and $\sigma$, which map disjoint sets of
variables, we write $\varrho\cup\sigma$ to denote $\varrho\sigma$.

Deviating from the standard notion of higher-order subterm, we define subterms
on $\beta$-reduced terms as follows: a term $t$ is a subterm of $t$ at
position $\varepsilon$. If $s$ is a subterm of $u_{i}$ at position $p$, then
$s$ is a subterm of $a\;\overline{u}_{n}$ at position $i.p$. If $s$ is a
subterm of $t$ at position $p$, then $s$ is a subterm of $\lambda x.\,t$ at
position $1.p$. Our definition of subterm gracefully generalizes the
corresponding first-order notion: $\mathsf{a}$ is a subterm of
$\mathsf{f}\,\mathsf{a}\,\mathsf{b}$ at position 1, but $\mathsf{f}$ and
$\mathsf{f}\,\mathsf{a}$ are not subterms of
$\mathsf{f}\,\mathsf{a}\,\mathsf{b}$. A context is a term with zero or more
subterms replaced by a hole $\square$. We write $C[\overline{u}_{n}]$ for the
term resulting from filling in the holes of a context $C$ with the terms
$\overline{u}_{n}$ from left to right. The common context $\mathcal{C}(s,t)$
of two $\eta$-long $\beta$-reduced terms $s$ and $t$ of the same type is
defined inductively as follows, assuming that $a\not=b$: $\mathcal{C}(\lambda
x.\,s,\lambda y.\,t)=\lambda x.\,\mathcal{C}(s,\\{y\mapsto x\\}t)$;
$\mathcal{C}(a\,\overline{s}_{m},b\,\overline{t}_{n})=\square$;
$\mathcal{C}(a\,\overline{s}_{m},a\,\overline{t}_{m})=a\,\mathcal{C}(s_{1},t_{1})\,\ldots\,\mathcal{C}(s_{m},t_{m})$.

A _unification constraint_ $s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ is an unordered pair of two
terms of the same type. A _unifier_ of a multiset of unification constraints
$E$ is a substitution $\sigma$, such that $\sigma
s\leftrightarrow^{*}_{\alpha\beta\eta}\sigma t$, for all
$s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\in E$. A _complete set of
unifiers_ (_CSU_) of $E$ is defined as a set $U$ of $E$’s unifiers along with
a set $V$ of _auxiliary variables_ such that no
$s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\in E$ contains variables from
$V$ and for every unifier $\varrho$ of $E$, there exists a $\sigma\in U$ and a
substitution $\theta$ such that for all $X\not\in V,$ $\varrho X=\theta\sigma
X$. A _most general unifier_ (_MGU_) is a one-element CSU. A unifier of terms
$s$ and $t$ is a unifier of the singleton multiset
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$.

######  Remark 1.

We use this definition of a CSU because JP’s definition of a CSU, which we
have adopted in our FSCD-2020 paper, is flawed. JP’s definition does not
employ the notion of auxiliary variables, but instead requires $\varrho
X=\theta\sigma X$ for all variables mapped by $\varrho$. This is problematic
because nothing prevents $\varrho$ from mapping the auxiliary variables. For
example, $\sigma=\\{F\mapsto\lambda xy.\>G\>y\\}$ is supposed to be an MGU for
$F\>\mathsf{a}\>\mathsf{c}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\>\mathsf{b}\>\mathsf{c}$. But
for the unifier $\varrho=\\{F\mapsto\lambda xy.\>y,\>G\mapsto\lambda
x.\>\mathsf{d}\\}$, without the notion of auxiliary variables, there exists no
appropriate substitution $\theta$ because $\varrho G=\theta\sigma G$ requires
$\theta G=\lambda x.\>\mathsf{d}$ and $\varrho F=\theta\sigma F$ requires
$\theta G=\lambda x.\>x$.

##  3\. The Unification Procedure

To unify two terms $s$ and $t$, our procedure builds a tree as follows. The
nodes of the tree have the form $(E,\sigma)$, where $E$ is a multiset of
unification constraints
$\\{(s_{1}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{1}),\ldots,(s_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{n})\\}$ and $\sigma$ is the
substitution constructed up to that point. The root node of the tree is
$(\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\},\operatorname{id})$, where
$\operatorname{id}$ is the identity substitution. The tree is then constructed
applying the transitions listed below. The leaves of the tree are either
failure nodes $\bot$ or substitutions $\sigma$. Ignoring failure nodes, the
set of all substitutions in the leaves forms a complete set of unifiers for
$s$ and $t$. More generally, our procedure can be used to unify a multiset $E$
of constraints by making the root of the unification tree
$(E,\operatorname{id})$.

The procedure requires an infinite supply of fresh free variables. These fresh
variables must be disjoint from the variables occurring in the initial
multiset $E$. Whenever a transition
$(E,\sigma)\longrightarrow(E^{\prime},\sigma^{\prime})$ is made, all fresh
variables used in $\sigma^{\prime}$ are removed from the supply and cannot be
used again as fresh variables.

The transitions are parametrized by a mapping $\mathcal{P}$ that assigns a set
of substitutions to a unification pair; this mapping abstracts the concept of
unification rules present in other unification procedures. Moreover, the
transitions are parametrized by a selection function $S$ mapping a multiset
$E$ of unification constraints to one of those constraints $S(E)\in E$, the
_selected_ constraint in $E$. The transitions, defined as follows, are only
applied if the grayed constraint is selected.

Succeed:

$(\varnothing,\sigma)\longrightarrow\sigma$

Normalizeαη:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}_{m}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{y}_{n}.\,t}$}}\\}\uplus
E,\sigma)\longrightarrow(\\{\lambda\overline{x}_{m}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}_{m}.\,t^{\prime}\,x_{n+1}\ldots
x_{m}\\}\uplus E,\sigma)$
where $m\geq n$, $\overline{x}_{m}\not=\overline{y}_{n}$, and
$t^{\prime}=\\{y_{1}\mapsto x_{1},\ldots,y_{n}\mapsto x_{n}\\}t$

Normalizeβ:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t}$}}\\}\uplus
E,\sigma)\longrightarrow(\\{\lambda\overline{x}.\,{s}_{\downarrow{\textsf{h}}}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,{t}_{\downarrow{\textsf{h}}}\\}\uplus
E,\sigma)$
where $s$ or $t$ is not in hnf

Dereference:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t}$}}\\}\uplus
E,\sigma)\longrightarrow(\\{\lambda\overline{x}.\,(\sigma
F)\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t\\}\uplus
E,\sigma)$
where none of the previous transitions apply and $F$ is mapped by $\sigma$

Fail:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,a\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,b\,\overline{t}_{n}}$}}\\}\uplus
E,\sigma)\longrightarrow\bot$
where none of the previous transitions apply, and $a$ and $b$ are different
rigid heads

Delete:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}s}$}}\\}\uplus
E,\sigma)\longrightarrow(E,\sigma)$
where none of the previous transitions apply

OracleSucc:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t}$}}\\}\uplus
E,\sigma)\longrightarrow(E,\varrho\sigma)$
where none of the previous transitions apply, some oracle found a finite CSU
$U$ for $\sigma s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\sigma t$ using fresh auxiliary
variables, and $\varrho\in U$; if multiple oracles found a CSU, only one of
them is considered

OracleFail:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t}$}}\\}\uplus
E,\sigma)\longrightarrow\bot$
where none of the previous transitions apply, and some oracle determined
$\sigma s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\sigma t$ has no solutions

Decompose:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,a\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t}_{m}}$}}\\}\uplus
E,\sigma)\longrightarrow(\\{s_{1}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{1},\ldots,s_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{m}\\}\uplus E,\sigma)$
where none of the transitions Succeed to OracleFail apply

Bind:

$(\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t}$}}\\}\uplus
E,\sigma)\longrightarrow(\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}\uplus E,\varrho\sigma)$
where none of the transitions Succeed to OracleFail apply, and
$\varrho\in\mathcal{P}(s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t)$.

The transitions are designed so that only OracleSucc, Decompose, and Bind can
introduce parallel branches in the constructed tree. OracleSucc can introduce
branches using different unifiers of the CSU, Bind can introduce branches
using different substitutions in $\mathcal{P}$, and Decompose can be applied
in parallel with Bind.

Our approach is to apply substitutions and $\alpha\beta\eta$-normalize terms
lazily. In particular, the transitions that modify the constructed
substitution, OracleSucc and Bind, do not apply that substitution to the
unification pairs directly. Instead, the transitions Normalizeαη, Normalizeβ,
and Dereference partially normalize and partially apply the constructed
substitution just enough to ensure that the heads are the ones we would get if
the substitution was fully applied and the term was fully normalized. To
support lazy dereferencing, OracleSucc and Bind must maintain the invariant
that all substitutions are idempotent. The invariant is easily preserved if
the substitution $\varrho$ from the definition of OracleSucc and Bind is
itself idempotent and no variable mapped by $\sigma$ occurs in $\varrho F$,
for any variable $F$ mapped by $\varrho$.

The OracleSucc and OracleFail transitions invoke oracles, such as pattern
unification, to compute a CSU faster, produce fewer redundant unifiers, and
discover nonunifiability earlier. In some cases, addition of oracles lets the
procedure terminate more often.

In the literature, oracles are usually stated under the assumption that their
input belongs to the appropriate fragment. To check whether a unification
constraint is inside the fragment, we need to fully apply the substitution and
$\beta$-normalize the constraint. To avoid these expensive operations and
enable efficient oracle integration, oracles must be redesigned to lazily
discover whether the terms belong to their fragment. Most oracles contain a
decomposition operation which requires only a partial application of the
substitution and only partial $\beta$-normalization. If one of the constraints
resulting from decomposition is not in the fragment, the original problem is
not in the fragment. This allows us to detect that the problem is not in the
fragment without fully applying the substitution and $\beta$-normalizing.

The core of the procedure lies in the Bind step, parameterized by the mapping
$\mathcal{P}$ that determines which substitutions (called _bindings_) to
create. The bindings are defined as follows:

JP-style projection for $F$:

Let $F$ be a free variable of type
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$, where some
$\alpha_{i}$ is equal to $\beta$ and $n>0$. Then the JP-style projection
binding is

$F\mapsto\lambda\overline{x}_{n}.\,x_{i}$

Huet-style projection for $F$:

Let $F$ be a free variable of type
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$, where some
$\alpha_{i}=\gamma_{1}\rightarrow\cdots\rightarrow\gamma_{m}\rightarrow\beta$,
$n>0$ and $m\geq 0$. Huet-style projection is

$F\mapsto\lambda\overline{x}_{n}.\,x_{i}\,(F_{1}\,\overline{x}_{n})\,\ldots\,(F_{m}\,\overline{x}_{n})$

where the fresh free variables $\overline{F}_{m}$ and bound variables
$\overline{x}_{n}$ are of appropriate types.

Imitation of $\mathsf{g}$ for $F$:

Let $F$ be a free variable of type
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$ and let
$\mathsf{g}$ be a constant of type
$\gamma_{1}\rightarrow\cdots\rightarrow\gamma_{m}\rightarrow\beta$ where
$n,m\geq 0$. The imitation binding is

$F\mapsto\lambda\overline{x}_{n}.\,\mathsf{g}\,(F_{1}\,\overline{x}_{n})\ldots(F_{m}\,\overline{x}_{n})$

where the fresh free variables $\overline{F}_{m}$ and bound variables
$\overline{x}_{n}$ are of appropriate types.

Elimination for $F$:

Let $F$ be a free variable of type
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$, where
$n>0$. In addition, let $1\leq j_{1}<\cdots<j_{i}\leq n$ and $i<n$.
Elimination for the sequence $(j_{k})_{k=1}^{i}$ is

$F\mapsto\lambda\overline{x}_{n}.\,G\,x_{j_{1}}\,\ldots\,x_{j_{i}}$

where the fresh free variable $G$ as well as all $x_{j_{k}}$ are of
appropriate type. We call fresh variables emerging from this binding in the
role of $G$ _elimination variables_.

Identification for $F$ and $G$:

Let $F$ and $G$ be different free variables. Furthermore, let the type of $F$
be $\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta$ and the
type of $G$ be
$\gamma_{1}\rightarrow\cdots\rightarrow\gamma_{m}\rightarrow\beta$, where
$n,m\geq 0$. Then, the identification binding binds $F$ and $G$ with

$F\mapsto\lambda\overline{x}_{n}.\,H\,\overline{x}_{n}\,(F_{1}\,\overline{x}_{n})\ldots(F_{m}\,\overline{x}_{n})\quad
G\mapsto\lambda\overline{y}_{m}.\,H\,(G_{1}\,\overline{y}_{m})\ldots(G_{n}\,\overline{y}_{m})\,\overline{y}_{m}$

where the fresh free variables $H,\overline{F}_{m},\overline{G}_{n}$ and bound
variables $\overline{x}_{n}$,$\overline{y}_{m}$ are of appropriate types. We
call fresh variables emerging from this binding in the role of $H$
_identification variables_.

Iteration for $F$:

Let $F$ be a free variable of the type
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{n}\rightarrow\beta_{1}$ and let
some $\alpha_{i}$ be the type
$\gamma_{1}\rightarrow\cdots\rightarrow\gamma_{m}\rightarrow\beta_{2}$, where
$n>0$ and $m\geq 0$. Iteration for $F$ at $i$ is

$F\mapsto\lambda\overline{x}_{n}.\,H\,\overline{x}_{n}\,(\lambda\overline{y}.\,x_{i}\,(G_{1}\,\overline{x}_{n}\,\overline{y})\ldots(G_{m}\,\overline{x}_{n}\,\overline{y}))$

The free variables $H$ and $G_{1},\ldots,G_{m}$ are fresh, and $\overline{y}$
is an arbitrary-length sequence of bound variables of arbitrary types. All new
variables are of appropriate type. Due to indeterminacy of $\overline{y}$,
this step is infinitely branching.

The following mapping
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t)$ is used
as the parameter $\mathcal{P}$ of the procedure:

  * •

If the constraint is rigid-rigid,
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t)=\varnothing$.

  * •

If the constraint is flex-rigid, let
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t})$
be

    * –

an imitation of $a$ for $F$, if $a$ is a constant, and

    * –

all Huet-style projections for $F$, if $F$ is not an identification variable.

  * •

If the constraint is flex-flex and the heads are different, let
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,G\,\overline{t})$
be

    * –

all identifications and iterations for both $F$ and $G$, and

    * –

all JP-style projections for non-identification variables among $F$ and $G$.

  * •

If the constraint is flex-flex and the heads are identical, we distinguish two
cases:

    * –

if the head is an elimination variable,
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t)=\varnothing$;

    * –

otherwise, let
$\mathcal{P}_{\mathsf{c}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F\,\overline{t})$
be all iterations for $F$ at arguments of functional type and all eliminations
for $F$.

### Comparison with the JP Procedure

In contrast to our procedure, the JP procedure constructs a tree with only one
unification constraint per node and does not have a Decompose rule. Instead,
at each node $(s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t,\sigma)$, the JP procedure
computes the common context $C$ of $s$ and $t$, yielding term pairs
$(s_{1},t_{1}),\ldots,(s_{n},t_{n})$, called _disagreement pairs_ , such that
$s=C[s_{1},\ldots,s_{n}]$ and $t=C[t_{1},\ldots,t_{n}]$. The procedure
heuristically chooses one of the disagreement pairs $(s_{i},t_{i})$ and
applies a binding to the heads of $s_{i}$ and $t_{i}$ or to a free variable
occurring above the disagreement pair in the common context $C$. Due to this
application of bindings above the disagreement pair, lazy normalization and
dereferencing cannot easily be integrated into the JP procedure.

The mapping $\mathcal{P}$ uses many binding rules of the JP procedure, but our
procedure explores the search space differently. In particular, the JP
procedure allows iteration or elimination to be applied at a free variable in
the common context of the unification constraint, even if bindings were
already applied below that free variable. In contrast, our procedure forces
the eliminations and iterations to be applied as soon as it observes a flex-
flex pair with identical heads. After applying the Decompose transition, this
flex-flex pair will be reduced to pairs representing the arguments of the
identical heads. Therefore, unlike the JP algorithm, it will not apply
bindings to the flex-flex pair after bindings have been applied to its
arguments.

The JP procedure can be modified to solve the preunification problem by making
it choose only flex-rigid disagreement pairs and terminate with a preunifier
when no flex-rigid pair remains. However, such a procedure would be less
efficient than Huet’s procedure because it would use the iteration binding
instead of Huet-style projection to solve flex-rigid pairs. Our procedure
applies Huet-style projections on flex-rigid pairs, which results in two
important improvements over the JP procedure. First, our procedure terminates
more often than the JP procedure because Huet-style projections cause only a
finite branching, whereas iteration causes an infinite branching. Second, when
our procedure is modified to solve the preunification problem by never
selecting flex-flex pairs and stopping when only flex-flex pairs are left, it
becomes an optimized variant of Huet’s procedure that supports oracles as well
as lazy substitution and $\beta$-reduction.

The bindings of our procedure contain further optimizations that are absent in
the JP procedure: The JP procedure applies eliminations for only one parameter
at a time, yielding multiple paths to the same unifier. It applies imitations
to flex-flex pairs, which we found to be unnecessary. Moreover, it does not
keep track of which rules introduced which variables: iterations and
eliminations are applied on elimination variables, and projections are applied
on identification variables.

### Examples

We present some illustrative derivations. The displayed branches of the
constructed trees are not necessarily exhaustive. We abbreviate JP-style
projection as JP Proj, imitation as Imit, identification as Id, Decompose as
Dc, Dereference as Dr, $\sf{Normalize_{\beta}}$ as $\sf{N_{\beta}}$, and Bind
of a binding $x$ as ${\sf B(}x{\sf)}$. Transitions of the JP procedure are
denoted by $\Longrightarrow$. For the JP transitions we implicitly apply the
generated bindings and fully normalize terms, which significantly shortens JP
derivations.

The JP procedure does not terminate on the problem
$G\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}\,G$:

$(G\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}\,G,\operatorname{id})\overset{\sf{Imit}}{\Longrightarrow}(\mathsf{f}\,G^{\prime}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}^{2}\,G^{\prime},\sigma_{1})\overset{\sf{Imit}}{\Longrightarrow}(\mathsf{f}^{2}\,G^{\prime\prime}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}^{3}\,G^{\prime\prime},\sigma_{2})\overset{\sf{Imit}}{\Longrightarrow}\cdots$

where $\sigma_{1}=\\{G\mapsto\lambda x.\,\mathsf{f}\,G^{\prime}\\}$ and
$\sigma_{2}=\\{G^{\prime}\mapsto\lambda
x.\,\mathsf{f}\,G^{\prime\prime}\\}\sigma_{1}$. By including any oracle that
supports the first-order occurs check, such as the pattern oracle or the
fixpoint oracle described in Section 7, our procedure gracefully generalizes
first-order unification:

$(\\{G\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}\,G\\},\operatorname{id})\overset{\sf{OracleFail}}{\longrightarrow}\bot$

The following derivation illustrates the advantage of the Decompose rule.

$\displaystyle(\\{\mathsf{h}^{100}\,(F\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{h}^{100}\,(G\,\mathsf{b})\\},\operatorname{id})\overset{\sf{Dc^{100}}}{\longrightarrow}(\\{F\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{b}\\},\operatorname{id})\overset{\sf{B(Id)}}{\longrightarrow}(\\{F\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{b}\\},\sigma_{1})$
$\displaystyle\overset{\sf{Dr+N_{\beta}}}{\longrightarrow}(\\{H\,\mathsf{a}\,(F^{\prime}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}H\,(G^{\prime}\,\mathsf{b})\,\mathsf{b}\\},\sigma_{1})\overset{\sf{Dc}}{\longrightarrow}(\\{\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G^{\prime}\,\mathsf{b},F^{\prime}\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{1})$
$\displaystyle\overset{\sf{B(Imit)}}{\longrightarrow}(\\{\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G^{\prime}\,\mathsf{b},F^{\prime}\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{2})\overset{\sf{Dr+N_{\beta}}}{\longrightarrow}(\\{\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{a},F^{\prime}\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{2})\overset{\sf{Delete}}{\longrightarrow}(\\{F^{\prime}\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{2})$
$\displaystyle\overset{\sf{B(Imit)}}{\longrightarrow}(\\{F^{\prime}\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{3})\overset{\sf{Dr+N_{\beta}}}{\longrightarrow}(\\{\mathsf{b}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\sigma_{3})\overset{\sf{Delete}}{\longrightarrow}(\varnothing,\sigma_{3})\overset{\sf{Succeed}}{\longrightarrow}\sigma_{3}$

where $\sigma_{1}=\\{F\mapsto\lambda x.\,H\,x\,(F^{\prime}\,x),G\mapsto\lambda
y.\,H\,(G^{\prime}\,y)\,y\\}$; $\sigma_{2}=\\{G^{\prime}\mapsto\lambda
x.\,\mathsf{a}\\}\sigma_{1}$; and $\sigma_{3}=\\{F^{\prime}\mapsto\lambda
x.\,\mathsf{b}\\}\sigma_{2}$. The JP procedure produces the same intermediate
substitutions $\sigma_{1}$ to $\sigma_{3}$, but since it does not decompose
the terms, it retraverses the common context $\mathsf{h}^{100}\,[\;]$ at every
step to identify the contained disagreement pair:

$\displaystyle(\mathsf{h}^{100}\,(F\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{h}^{100}\,(G\,\mathsf{b}),\operatorname{id})\overset{\sf{Id}}{\Longrightarrow}(\mathsf{h}^{100}\,(H\,\mathsf{a}\,(F^{\prime}\,\mathsf{a}))\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{h}^{100}\,(H\,(G^{\prime}\,\mathsf{b})\,\mathsf{b}),\sigma_{1})$
$\displaystyle\overset{\sf{Imit}}{\Longrightarrow}(\mathsf{h}^{100}\,(H\,\mathsf{a}\,(F^{\prime}\,\mathsf{a}))\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{h}^{100}\,(H\,\mathsf{a}\,\mathsf{b}),\sigma_{2})\overset{\sf{Imit}}{\Longrightarrow}(\mathsf{h}^{100}\,(H\,\mathsf{a}\,\mathsf{b})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{h}^{100}\,(H\,\mathsf{a}\,\mathsf{b}),\sigma_{3})\overset{\sf{Succeed}}{\Longrightarrow}\sigma_{3}$

The search space restrictions also allow us to prune some redundant unifiers.
Consider the problem
$F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b}$, where
$\mathsf{a}$ and $\mathsf{b}$ are of base type. Our procedure produces only
one failing branch and the following two successful branches:

$\displaystyle(\\{F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b}\\},\operatorname{id})\overset{\sf{Dc}}{\longrightarrow}(\\{G\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\operatorname{id})\overset{\sf{B(Imit)}}{\longrightarrow}(\\{G\,\mathsf{a}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\\{G\mapsto\lambda
x.\,\mathsf{b}\\})$
$\displaystyle\overset{\sf{Dr+N_{\beta}}}{\longrightarrow}(\\{\mathsf{b}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{b}\\},\\{G\mapsto\lambda
x.\,\mathsf{b}\\})\overset{\sf{Delete}}{\longrightarrow}(\varnothing,\\{G\mapsto\lambda
x.\,\mathsf{b}\\})\overset{\sf{Succeed}}{\longrightarrow}\\{G\mapsto\lambda
x.\,\mathsf{b}\\}$
$\displaystyle(\\{F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b}\\},\operatorname{id})\overset{\sf{B(Elim)}}{\longrightarrow}(\\{F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b}\\},\\{F\mapsto\lambda
x.\,F^{\prime}\\})$
$\displaystyle\overset{\sf{Dr+N_{\beta}}}{\longrightarrow}(\\{F^{\prime}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F^{\prime}\\},\\{F\mapsto\lambda
x.\,F^{\prime}\\})\overset{\sf{Delete}}{\longrightarrow}(\varnothing,\\{F\mapsto\lambda
x.\,F^{\prime}\\})\overset{\sf{Succeed}}{\longrightarrow}\\{F\mapsto\lambda
x.\,F^{\prime}\\}$

The JP procedure additionally produces the following redundant unifier:

$\displaystyle(F\,(G\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F\,\mathsf{b},\operatorname{id})\overset{\sf{JP\,Proj}}{\Longrightarrow}(F\,\mathsf{a}=F\,\mathsf{b},\\{G\mapsto\lambda
x.\,x\\})$
$\displaystyle\overset{\sf{Elim}}{\Longrightarrow}(F^{\prime}=F^{\prime},\\{G\mapsto\lambda
x.\,x,F\mapsto\lambda
x.\,F^{\prime}\\})\overset{\sf{Succeed}}{\Longrightarrow}\\{G\mapsto\lambda
x.\,x,F\mapsto\lambda x.\,F^{\prime}\\}$

Moreover, the JP procedure does not terminate because an infinite number of
iterations is applicable at the root. Our procedure terminates in this case
since we only apply iteration binding for non base-type arguments, which $F$
does not have.

### Pragmatic Variant

We structured our procedure so that most of the unification machinery is
contained in the Bind step. Modifying $\mathcal{P}$, we can sacrifice
completeness and obtain a pragmatic variant of the procedure that often
performs better in practice. Our preliminary experiments showed that using
mapping $\mathcal{P}_{\mathsf{p}}$ defined as follows is a reasonable
compromise between completeness and performance:

  * •

If the constraint is rigid-rigid,
$\mathcal{P}_{\mathsf{p}}(\lambda\overline{x}.\,s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t)=\varnothing$.

  * •

If the constraint is flex-rigid, let
$\mathcal{P}_{\mathsf{p}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t})$
be

    * –

an imitation of $a$ for $F$, if $a$ is a constant, and

    * –

all Huet-style projections for $F$ if $F$ is not an identification variable.

  * •

If the constraint is flex-flex and the heads are different, let
$\mathcal{P}_{\mathsf{p}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,G\,\overline{t})$
be

    * –

an identification binding for $F$ and $G$, and

    * –

all Huet-style projections for $F$ if $F$ is not an identification variable

  * •

If the constraint is flex-flex and the heads are identical, we distinguish two
cases:

    * –

if the head is an elimination variable,
$\mathcal{P}_{\mathsf{p}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F\,\overline{t})=\varnothing$;

    * –

otherwise, let
$\mathcal{P}_{\mathsf{p}}(\lambda\overline{x}.\,F\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F\,\overline{t})$
be the set of all eliminations bindings for $F$.

The pragmatic variant of our procedure removes all iteration bindings to
enforce finite branching. Moreover, it imposes limits on the number of
bindings applied, counting the applications of bindings locally, per
constraint. It is useful to distinguish the Huet-style projection cases where
$\alpha_{i}$ is a base type (called _simple projection_), which always reduces
the problem size, and the cases where $\alpha_{i}$ is a functional type
(called _functional projection_). We limit the number applications of the
following bindings: functional projections, eliminations, imitations and
identifications. In addition, a limit on the total number of applied bindings
can be set. An elimination binding that removes $k$ arguments counts as $k$
elimination steps. Due to these limits, the pragmatic variant terminates.

To fail as soon as any of the limits is reached, the pragmatic variant employs
an additional oracle. If this oracle determines that the limits are reached
and the constraint is of the form
$\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,G\,\overline{t}_{n}$,
it returns a _trivial unifier_ – a substitution
$\\{F\mapsto\lambda\overline{x}_{m}.\,H,G\mapsto\lambda\overline{x}_{n}.\,H\\}$,
where $H$ is a fresh variable; if the limits are reached and the constraint is
flex-rigid, the oracle fails; if the limits are not reached, it reports that
terms are outside its fragment. The trivial unifier prevents the procedure
from failing on easily unifiable flex-flex pairs.

Careful tuning of each limit optimizes the procedure for a specific class of
problems. For problems originating from proof assistants, shallow unification
depth usually suffices. However, hard hand-crafted problems often need deeper
unification.

##  4\. Proof of Completeness

Like the JP procedure, our procedure misses no unifiers:

######  Theorem 2.

The procedure described in Section 3 parametrized by
$\mathcal{P}_{\mathsf{c}}$ is complete, meaning that the substitutions on the
leaves of the constructed tree form a CSU. More precisely, let $E$ be a
multiset of constraints and let $V$ be the supply of fresh variables provided
to the procedure. Then for any unifier $\varrho$ of $E$ there exists a
derivation
$\mathopen{}\mathclose{{}\left(E,\operatorname{id}}\right)\longrightarrow^{*}\sigma$
and a substitution $\theta$ such that for all free variables $X\not\in V$, we
have $\varrho X=\theta\sigma X$.

Taking a high-level view, this theorem is proved by incrementally defining
states $\mathopen{}\mathclose{{}\left(E_{j},\sigma_{j}}\right)$ and
_remainder_ _substitutions_ $\varrho_{j}$ starting with
$\mathopen{}\mathclose{{}\left(E_{0},\sigma_{0}}\right)=\mathopen{}\mathclose{{}\left(E,\operatorname{id}}\right)$
and $\varrho_{0}=\varrho$. The substitution $\varrho_{j}$ is what remains to
be added to $\sigma_{j}$ to reach $\varrho_{0}$. States are defined so that
the shape of the selected constraint from $E_{j}$ and the remainder
substitution guide the choice of applicable transition rule of our procedure.
We employ a measure based on values of $E_{j}$ and $\varrho_{j}$ that
decreases with each application of the rules. Therefore, eventually, we will
reach the target substitution $\sigma$.

In the remaining of this section, we view terms as
$\alpha\beta\eta$-equivalence classes, with the $\eta$-long $\beta$-normal
form as their canonical representative. Moreover, we consider all
substitutions to be fully applied. These assumptions are justified because all
bindings depend only on the head of terms and hence replacing the lazy
transitions $\textsf{Normalize}_{\alpha\eta}$, $\textsf{Normalize}_{\beta}$,
and Dereference by eager counterparts only affects the efficiency but not the
overall behavior of our procedure.

We now give the detailed completeness proof of Theorem 2. Our proof is an
adaptation of the proof given by Jensen and Pietrzykowski [13]. Definitions
and lemmas are reused, but are combined together differently to suit our
procedure. We start by listing all reused definitions and lemmas from the
original JP proof. The “JP” labels in their statements refer to the
corresponding lemmas and definitions from the original proof.

[JP D1.6] Given two terms $t$ and $s$ and their common context $C$, we can
write $t$ as $C[\overline{t}]$ and $s$ as $C[\overline{s}]$ for some
$\overline{t}$ and $\overline{s}$. The pairs $(s_{j},t_{j})$ are called
_disagreement pairs._ [JP D3.1] Given two terms $t$ and $s$, let
$\lambda\overline{x}.\,t^{\prime}$ and $\lambda\overline{y}.\,s^{\prime}$ be
respective $\alpha$-equivalent terms such that their parameters $\overline{x}$
and $\overline{y}$ are disjoint. Then the disagreement pairs of $t^{\prime}$
and $s^{\prime}$ are called _opponent pairs_ in $t$ and $s$.

######  Lemma 3 (JP L3.3 (1)).

Let $\varrho$ be a substitution and $X$, $Y$ be free variables such that
$\varrho\mathopen{}\mathclose{{}\left(X\,\overline{s}}\right)=\varrho\mathopen{}\mathclose{{}\left(Y\,\overline{t}}\right)$
for some term tuples $\overline{s}$ and $\overline{t}$. Then for every
opponent pair $u$, $v$ in $\varrho X$ and $\varrho Y$ (Definition 2), the head
of $u$ or $v$ is a parameter of $\varrho X$ or $\varrho Y$.

In contrast to applied constants, applied variables should not be eagerly
decomposed. For a constant $\mathsf{f}$, if
$\mathsf{f}\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{f}\,\overline{t}$ has a
unifier, that unifier must clearly also unify
$s_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{i}$ for each $i$. For a free
variable $X$, a unifier of
$X\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}X\,\overline{t}$ does not
necessarily unify $s_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{i}$. The concept of
$\omega$-simplicity is a criterion on unifiers that captures some of the cases
where eager decomposition is possible. Non-$\omega$-simplicity on the other
hand is the main trigger of Iteration—the most explosive binding of our
procedure.

[JP D3.2]An occurrence of a parameter $x$ of term $t$ in the body of $t$ is
$\omega$_-simple_ if both

  1. (1)

the arguments of $x$ are distinct and are exactly (the $\eta$-long forms of)
all of the variables bound in the body of $t$, and

  2. (2)

this occurrence of $x$ is not in an argument of any parameter of $t$.

This definition is slightly too restrictive for our purposes. It is
unfortunate that condition 1 requires $x$ to be applied to _all_ instead of
just some of the bound variables. The JP proof would probably work with such a
relaxation, and the definition would then cover all cases where eager
decomposition is possible. However, to reuse the JP lemmas, we stick to the
original notion of $\omega$-simplicity and introduce the following relaxation:
An occurrence of a parameter $x$ of term $t$ in the body of $t$ is _base-
simple_ if it is $\omega$-simple or both

  1. (1)

$x$ is of base type, and

  2. (2)

this occurrence of $x$ is not in an argument of any parameter of $t$.

######  Lemma 4.

Let $s$ have parameters $\overline{x}$ and a subterm $x_{j}\,\overline{v}$
where this occurrence of $x_{j}$ is base-simple. Then for any sequence
$\overline{t}$ of (at least $j$) terms, the body of $t_{j}$ is a subterm of
$s\,\overline{t}$ (after normalization) at the position of
$x_{j}\,\overline{v}$ up to renaming of the parameters of $t_{j}$. To compare
positions of $s$ and $s\,\overline{t}$, ignore the parameter count mismatch.

######  Proof 4.1.

Consider the process of $\beta$-normalizing $s\,\overline{t}$. After
substituting terms $\overline{t}$ into the body of $s$, a further reduction
can only take place when some $t_{k}$ is an abstraction that gets arguments in
$s$. The arguments $\overline{v}$ to the $x_{j}$ are distinct variables bound
in the body of $s$. This follows easily from either case of the definition of
base-simplicity. So $t_{j}$ is applied to the unmodified $\overline{v}$ after
substituting terms $\overline{t}$ into the body of $s$. Base-simplicity also
implies that $t_{j}\,\overline{v}$ does not occur in an argument to another
$t_{k}$. Hence only the reduction of $t_{j}\,\overline{v}$ itself affects this
subterm. The variables $\overline{v}$ match the parameter count of $t_{j}$
because we consider the $\eta$-long form of $t_{j}$; so $t_{j}\,\overline{v}$
reduces to the body of $t_{j}$ (modulo renaming). The position is obviously
that of $x_{j}\,\overline{v}$.

######  Lemma 5 (JP C3.4 strengthened).

Let $\varrho$ be a substitution and $X$ a free variable. If
$\varrho\mathopen{}\mathclose{{}\left(\lambda\overline{x}.\,X\,\overline{s}}\right)=\varrho\mathopen{}\mathclose{{}\left(\lambda\overline{x}.\,X\,\overline{t}}\right)$
and some occurrence of the $i^{\text{th}}$ parameter of $\varrho X$ is base-
simple, then $\varrho s_{i}=\varrho t_{i}$.

######  Proof 4.2.

By Lemma 4, $\varrho s_{i}$ occurs in $\varrho
X\mathopen{}\mathclose{{}\left(\varrho\overline{s}}\right)$ at certain
position that depends only on $\varrho X$. Similarly $\varrho t_{i}$ occurs in
$\varrho X\mathopen{}\mathclose{{}\left(\varrho\overline{t}}\right)=\varrho
X\mathopen{}\mathclose{{}\left(\varrho\overline{s}}\right)$ at the same
position, and hence $\varrho s_{i}=\varrho t_{i}$.

We define more properties to determine which binding to apply to a given
constraint. Roughly speaking, the simple comparison form will trigger
identification bindings, projectivity will trigger Huet-style projections, and
simple projectivity will trigger JP-style projections. [JP D3.4] We say that
$s$ and $t$ are in _simple comparison form_ if all $\omega$-simple heads of
opponent pairs in $s$ and $t$ are distinct, and each opponent pair has an
$\omega$-simple head. [JP D3.5] A term $t$ is called _projective_ if the head
of $t$ is a parameter of $t$. If the whole body is just the parameter, then
$t$ is called _simply projective._ A central part of the proof is to find a
suitable measure for the remaining problem size. Showing that the measure is
strictly decreasing and well-founded guarantees that the procedure finds a
suitable substitution in finitely many steps. We reuse the measure for
remainder substitutions from JP [13], but embed it into a lexicographic
measure to handle the decomposition steps and oracles of our procedure. [JP
D3.7] The _free weight_ of a term $t$ is the total number of occurrences of
free variables and constants in $t$. The _bound weight_ of $t$ is the total
number of occurrences (excluding occurrences $\lambda x$) of bound variables
in $t$, but with the particular exemption: if a prefix variable $u$ has one or
more $\omega$-simple occurrences in the body, then one such occurrence and its
arguments are not counted. It does not matter which occurrence is not counted
because in $\eta$-long form the bound weight of the arguments of an
$\omega$-simple variable is the same for all occurrences of that variable. [JP
D3.8] For multisets $E$ of unification constraints and substitutions
$\varrho$, our measure on pairs $(E,\varrho)$ is the lexicographic comparison
of

A:

the sum of the sizes of the terms in $E$

B:

the sum over the free weight of $\varrho F$, for all variables $F$ mapped by
$\varrho$

C:

the sum over the bound weight of $\varrho F$, for all variables $F$ mapped by
$\varrho$

D:

the sum over the number of parameters of $\varrho F$, for all variables $F$
mapped by $\varrho$

We denote the quadruple containing these numbers as
$\operatorname{ord}(E,\varrho)$. We denote the triple containing only the last
three components of $\operatorname{ord}(E,\varrho)$ as
$\operatorname{ord}\varrho$. We write $<$ for the lexicographic comparison of
these tuples. The next six lemmas correspond to the bindings of our procedure
and sufficient conditions for the binding to bring us closer to a given
solution. This is expressed as a decrease of the $\operatorname{ord}$ measure
of the remainder. In each of these lemmas, let $u$ be a term with a variable
head $a$ and $v$ a term with an arbitrary head $b$. Let $\varrho$ be a unifier
of $u$ and $v$. The conclusion, let us call it _C_ , is always the same: there
exists a binding $\delta$ applicable to the problem
$u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v$, and there exists a
substitution $\varrho^{\prime}$ such that
$\operatorname{ord}\varrho^{\prime}<\operatorname{ord}\varrho$ and for all
variables $X$ except the fresh variables introduced by the binding $\varrho
X=\varrho^{\prime}\,\delta X$. For most of these lemmas, we refer to JP [13]
for proofs. Although JP only claim $\varrho X=\varrho^{\prime}\,\delta X$ for
variables $X$ mapped by $\varrho$, inspection of their proofs shows that the
equality holds for all $X$ except the fresh variables introduced by the
binding. Moreover, some of our bindings have more preconditions, yielding
additional orthogonal hypotheses in our lemmas, which we address below.

######  Lemma 6 (JP L3.9).

If $a=b$ is not an elimination variable and $\varrho a$ discards any of its
parameters, then C by elimination. Moreover, for the elimination variable $G$
introduced by this elimination, $\varrho^{\prime}G$ discards none of its
parameters and has the body of $\varrho a$.

######  Proof 4.3.

Let $\varrho a=\lambda\overline{x}.\,t$ and let
$\mathopen{}\mathclose{{}\left(x_{j_{k}}}\right)_{k=1}^{i}$ be the subsequence
of $\overline{x}$ consisting of those variables which occur in the body $t$.
It is a strict subsequence,__ since $\varrho a$ is assumed to discard some
parameter. Since the equal heads $a=b$ of the constraint
$u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v$ are not elimination variables,
elimination for $\mathopen{}\mathclose{{}\left(j_{k}}\right)_{k=1}^{i}$ can be
applied. Let
$\delta=\mathopen{}\mathclose{{}\left\\{a\mapsto\lambda\overline{x}.\,G\,x_{j_{1}}\,\ldots\,x_{j_{i}}}\right\\}$
be the corresponding binding. Define $\varrho^{\prime}$ to be like $\varrho$
except

$\varrho^{\prime}a=a\quad\text{and}\quad\varrho^{\prime}G=\lambda
x_{j_{1}}...x_{j_{i}}.\,t.$

Obviously $\varrho^{\prime}G$ is a closed term and $\varrho
X=\varrho^{\prime}\,\delta X$ holds for all $X\not=G$. Moreover
$\operatorname{ord}\varrho^{\prime}<\operatorname{ord}\varrho$, because free
and bound weights stay the same ($\varrho a$ and $\varrho^{\prime}G$ have the
same body $t$) whereas the number of parameters strictly decreases. The
definition of $\mathopen{}\mathclose{{}\left(j_{k}}\right)_{k=1}^{i}$ implies
that $\varrho^{\prime}G$ discards none of its parameters.

######  Lemma 7 (JP L3.10).

Assume that there exists a parameter $x$ of $\varrho a$ such that $x$ has a
non-$\omega$-simple (Definition 3) occurrence in $\varrho a$, which is not
below another parameter, or such that $x$ has at least two $\omega$-simple
occurrences in $\varrho a$. Moreover, if $a=b$, to make iteration applicable,
$a$ must not be an elimination variable, and $x$ must be of functional type.
Then C is achieved by iteration.

######  Lemma 8 (JP L3.11).

Assume that $a$ and $b$ are different free variables. If $\varrho a$ is simply
projective (Definition 4.2) and $a$ is not an identification variable, then C
by JP-style projection.

######  Lemma 9 (JP L3.12).

If $\varrho a$ is not projective and $b$ is rigid, then C by imitation.

######  Lemma 10 (JP L3.13).

Let $a\not=b$. Assume that $\varrho a\not=a$ and $\varrho b\not=b$ are in
simple comparison form (Definition 4.2) and neither is projective. Then C by
identification. Moreover, $\varrho^{\prime}H$ is not projective, where $H$ is
the identification variable introduced by this application of the
identification binding.

######  Proof 4.4.

This is JP’s Lemma 3.13, plus the claim that $\varrho^{\prime}H$ is not
projective. Inspecting the proof of that lemma, it is obvious that
$\varrho^{\prime}H$ cannot be projective because $\varrho a$ and $\varrho b$
are not projective.

######  Lemma 11.

Assume that $\varrho a$ is projective (Definition 4.2), $a$ is not an
identification variable, and $b$ is rigid. Then C by Huet-style projection.

######  Proof 4.5.

Since $\varrho a$ is projective, we have $\varrho
a=\lambda\overline{x}_{n}.\,x_{k}\,\overline{t}_{m}$ for some $k$ and some
terms $\overline{t}_{m}$. If $\varrho a$ is also simply projective, then
$x_{k}$ must be non-functional and since Huet-style projection and JP-style
projection coincide in that case, Lemma 8 applies. Hence, in the following we
may assume that $\varrho a$ is not simply projective, i.e., that $m>0$.

Let $\delta$ be the Huet-style projection binding:

$\delta=\\{a\mapsto\lambda\overline{x}_{n}.\,x_{i}\,(F_{1}\,\overline{x}_{n})\,\ldots\,(F_{m}\,\overline{x}_{n})\\}$

for fresh variables $F_{1},\dots,F_{m}$. This binding is applicable because
$b$ is rigid. Let $\varrho^{\prime}$ be the same as $\varrho$ except that we
set $\varrho^{\prime}a=a$ and for each $1\leq j\leq m$ we set

$\varrho^{\prime}F_{j}=\lambda\overline{x}_{n}.\,t_{j}$

It remains to show that
$\operatorname{ord}\varrho^{\prime}<\operatorname{ord}\varrho$. The free
weight of $\varrho a$ is the same as the sum of the free weights of
$\varrho^{\prime}F_{j}$ for $1\leq j\leq m$. Thus, the free weight is the same
for $\varrho$ and $\varrho^{\prime}$. The bound weight of $\varrho a$ however
is exactly $1$ larger than the sum of the bound weights of
$\varrho^{\prime}F_{j}$ for $1\leq j\leq m$ because of the additional
occurrence of $x_{k}$ in $\varrho a$. The exemption for $\omega$-simple
occurrences in the definition of the bound weight cannot be triggered by this
occurrence of $x_{k}$ because $m>0$ and thus $x_{k}$ is not $\omega$-simple.
It follows that
$\operatorname{ord}\varrho^{\prime}<\operatorname{ord}\varrho$.

We are now ready to prove the completeness theorem (Theorem 2).

######  Proof 4.6.

Let $E$ be a multiset of constraints and let $V$ be the supply of fresh
variables provided to our procedure. Let $\varrho$ be a unifier of $E$. We
must show that there exists a derivation
$\mathopen{}\mathclose{{}\left(E,\operatorname{id}}\right)\longrightarrow^{*}\sigma$
and a substitution $\theta$ such that for all free variables $X\not\in V$, we
have $\varrho X=\theta\sigma X$.

Let $E_{0}=E$ and $\sigma_{0}=\operatorname{id}$. Let
$\varrho_{0}=\tau\varrho$ for some renaming $\tau$, such that every free
variable occurring in $\varrho_{0}E_{0}$ does not occur in $E_{0}$ and is not
contained in $V$. Then $\varrho_{0}$ unifies $E_{0}$ because $\varrho$ unifies
$E$ by assumption. Moreover, $\varrho_{0}=\varrho_{0}\sigma_{0}$. We proceed
to inductively define $E_{j}$, $\sigma_{j}$ and $\varrho_{j}$ until we reach
some $j$ such that $E_{j}=\varnothing$. To guarantee well-foundedness, we
ensure that the measure
$\operatorname{ord}\mathopen{}\mathclose{{}\left(\varrho_{j},E_{j}}\right)$
decreases with each step. We maintain the following invariants for all $j$:

  * •

$\mathopen{}\mathclose{{}\left(E_{j},\sigma_{j}}\right)\longrightarrow\mathopen{}\mathclose{{}\left(E_{j+1},\sigma_{j+1}}\right)$;

  * •

$\operatorname{ord}\mathopen{}\mathclose{{}\left(\varrho_{j},E_{j}}\right)>\operatorname{ord}\mathopen{}\mathclose{{}\left(\varrho_{j+1},E_{j+1}}\right)$;

  * •

$\varrho_{j}$ unifies $E_{j}$;

  * •

$\varrho_{0}X=\varrho_{j}\sigma_{j}X$ for all free variables $X\not\in V$;

  * •

every free variable occurring in $\varrho_{j}E_{j}$ does not occur in $E_{j}$
and is not contained in $V$;

  * •

for every identification variable $X$, $\varrho_{j}X$ is not projective; and

  * •

for every elimination variable $X$, each parameter of $\varrho_{j}X$ has
occurrences in $\varrho_{j}X$, all of which are base-simple.

If $E_{j}\not=\varnothing$, let
$u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v$ be the selected constraint
$S(E_{j})$ in $E_{j}$.

First assume that an oracle is able to find a CSU for the constraint
$u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v$. Since $\varrho_{j}$ unifies
$u$ and $v$, by the definition of a CSU, the CSU discovered by the oracle
contains a unifier $\delta$ of $u$ and $v$ such that there exists
$\varrho_{j+1}$ and for all free variables $X$ except for the auxiliary
variables of the CSU we have $\varrho_{j}X=\varrho_{j+1}\,\delta X$. Thus, an
OracleSucc transition is applicable and yields the node
$\mathopen{}\mathclose{{}\left(E_{j+1},\sigma_{j+1}}\right)=\mathopen{}\mathclose{{}\left(\delta\mathopen{}\mathclose{{}\left(E_{j}\setminus\mathopen{}\mathclose{{}\left\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v}\right\\}}\right),\delta\,\sigma_{j}}\right)$.
Since the auxiliary variables introduced by OracleSucc are fresh, they cannot
occur in $E_{j}$. Therefore we have a strict containment
$\varrho_{j+1}E_{j+1}\subset\varrho_{j+1}\,\delta\,E_{j}=\varrho_{j}E_{j}$.
This implies
$\operatorname{ord}\mathopen{}\mathclose{{}\left(E_{j+1},\varrho_{j+1}}\right)<\operatorname{ord}\mathopen{}\mathclose{{}\left(E_{j},\varrho_{j}}\right)$.
It also shows that the constraints $\varrho_{j+1}E_{j+1}$ are unified when
$\varrho_{j}E_{j}$ are. Since the auxiliary variables introduced by OracleSucc
are fresh, they cannot occur in $\sigma_{j}X$ for any $X\not\in V$ either.
Hence, we have
$\varrho_{0}X=\varrho_{j}\sigma_{j}X=\varrho_{j+1}\,\delta\,\sigma_{j}X=\varrho_{j+1}\sigma_{j+1}X$
for all free variables $X\not\in V$. Any free variable occurring in
$\varrho_{j+1}E_{j+1}$ cannot not occur in $E_{j+1}$ and is not contained in
$V$ because $\varrho_{j+1}E_{j+1}\subset\varrho_{j}E_{j}$ and the variables
the variables in
$E_{j+1}=\delta\mathopen{}\mathclose{{}\left(E_{j}\setminus\mathopen{}\mathclose{{}\left\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v}\right\\}}\right)$ are either
variables already present in $E_{j}$ or fresh variables introduced by
OracleSucc. New identification or elimination variables are not introduced; so
their properties are preserved. Hence all invariants are preserved.

Otherwise we proceed by a case distinction on the form of
$u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v$. Typically, one of the Lemmas
6–11 is going to apply. Any one of them gives substitutions $\varrho^{\prime}$
and $\delta$ with properties that let us define $E_{j+1}=\delta E_{j}$,
$\sigma_{j+1}=\delta\,\sigma_{j}$ and $\varrho_{j+1}=\varrho^{\prime}$. The
problem size always strictly decreases, because these lemmas imply
$\varrho_{j+1}E_{j+1}=\varrho_{j+1}\delta E_{j}=\varrho_{j}E_{j}$ and
$\operatorname{ord}\varrho_{j+1}=\operatorname{ord}\varrho^{\prime}<\operatorname{ord}\varrho_{j}$.
Regarding the other invariants, the former equation guarantees that
$\varrho_{j+1}$ unifies $E_{j+1}$, and
$\varrho_{0}X=\varrho_{j}\,\sigma_{j}X=\varrho_{j+1}\,\delta\,\sigma_{j}X=\varrho_{j+1}\,\sigma_{j+1}X$
for all $X\not\in V$ because the fresh variables introduced by the binding
cannot occur in $\sigma_{j}X$ for any $X\not\in V$. The conditions on
variables must be checked separately when new ones are introduced. Let $a$ be
the head of $u=\lambda\overline{x}.\,a\,\overline{u}$ and $b$ be the head of
$v=\lambda\overline{x}.\,b\,\overline{v}$. Consider the following cases:

$u$ and $v$ have the same head symbol $a=b$:

  1. (1):

Suppose that $\varrho_{j}a$ has a parameter with non-base-simple occurrence.
By one of the induction invariants, $a$ is not an elimination variable. Among
all non-base-simple occurrences of parameters in $\varrho_{j}a$, choose the
leftmost one, which we call $x$. This occurrence of $x$ cannot be below
another parameter, because having $x$ occur in one of its arguments would make
that other parameter non-base-simple, contradicting the occurrence of $x$
being leftmost. Thus $x$ is neither base-simple nor below another parameter;
so $x$ is of functional type. Moreover, non-base-simplicity implies
non-$\omega$-simplicity. Hence, we can apply Lemma 7 (iteration).

  2. (2):

Otherwise suppose that $\varrho_{j}a$ discards some of its parameters. By one
of the induction invariants, $\varrho_{j}a$ is not an elimination variable.
Hence Lemma 6 (elimination) applies. The newly introduced elimination variable
$G$ satisfies the required invariants, because Lemma 6 guarantees that
$\varrho_{j+1}G$ uses its parameters and shares the body with $\varrho_{j}a$
which by assumption of this case contains only base-simple occurrences.

  3. (3):

Otherwise every parameter of $\varrho_{j}a$ has occurrences and all of them
are base-simple. We are going to show that Decompose is a valid transition and
decreases $\varrho_{j}E_{j}$. By Lemma 5 we conclude from
$\varrho_{j}u=\varrho_{j}v$ that $\varrho_{j}u_{i}=\varrho_{j}v_{i}$ for every
$i$. Hence the new constraints
$E_{j+1}=E_{j}\setminus\mathopen{}\mathclose{{}\left\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v}\right\\}\cup\mathopen{}\mathclose{{}\left\\{u_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v_{i}\,\middle|\,\text{for all
}i}\right\\}$ after Decompose are unified by $\varrho_{j}$. This allows us to
define $\varrho_{j+1}=\varrho_{j}$ and $\sigma_{j+1}=\sigma_{j}$. To check
that $\varrho_{j+1}E_{j+1}=\varrho_{j}E_{j+1}$ is smaller than
$\varrho_{j}E_{j}$ it suffices to check that constraints
$\varrho_{j}u_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\varrho_{j}v_{i}$ together are
smaller than $\varrho_{j}u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\varrho_{j}v$. Since all
parameters of $\varrho_{j}a$ have base-simple occurrences, $\varrho_{j}u_{i}$
is a subterm of
$\varrho_{j}u=\lambda\overline{x}.\,\varrho_{j}a\,\mathopen{}\mathclose{{}\left(\varrho_{j}\overline{u}}\right)$
by Lemma 4. Similarly for $\varrho_{j}v$. It follows that
$\varrho_{j+1}E_{j+1}$ is smaller than $\varrho_{j}E_{j}$. Since
$\varrho_{j+1}=\varrho_{j}$ and $\sigma_{j+1}=\sigma_{j}$, the other
invariants are obviously preserved.

$u$ and $v$ is a flex-flex pair with different heads:

  1. (5):

First, suppose that $\varrho_{j}a$ or $\varrho_{j}b$ is simply projective
(Definition 4.2). By the induction hypothesis, the simply projective head
cannot be an identification variable. Thus Lemma 8 (JP-style projection)
applies.

  2. (6):

Otherwise suppose that $\varrho_{j}a$ is projective but not simply. Then the
head of $\varrho_{j}a$ is some parameter $x_{k}$. But this occurrence cannot
be $\omega$-simple because it has arguments which cannot be bound above the
head $x_{k}$. Thus Lemma 7 (iteration) applies. If $\varrho_{j}b$ is
projective but not simply, the same argument applies.

  3. (7):

Otherwise suppose that $\varrho_{j}a$, $\varrho_{j}b$ are in simple comparison
form (Definition 4.2). By one of the the induction invariants, the free
variables occurring in $\varrho_{j}E_{j}$ do not occur in $E_{j}$. Thus
$\varrho_{j}a\not=a$ and $\varrho_{j}b\not=b$. Then Lemma 10 (identification)
applies.

  4. (8):

Otherwise $\varrho_{j}a$, $\varrho_{j}b$ are not in simple comparison form. By
Lemma 3 and by the definition of simple comparison form, there is some
opponent pair $x_{k}\,\overline{r}$, $b$ in $\varrho_{j}a$ and $\varrho_{j}b$
(after possibly swapping $u$ and $v$) where either the occurrence of $x_{k}$
is not $\omega$-simple (Definition 3) or else $x_{k}$ has another
$\omega$-simple occurrence in the body of $\varrho_{j}a$. Then Lemma 7
(iteration) applies.

$u$ and $v$ is a flex-rigid pair:

Without loss of generality, assume that $a$ is flex and $b$ is rigid.

  1. (9):

Suppose first that $\varrho_{j}a$ is projective. By one of the induction
invariants, $a$ cannot be an identification variable. Thus Lemma 11 (Huet-
style projection) applies.

  2. (10):

Otherwise $\varrho_{j}a$ is not projective. The head of $\varrho_{j}a$ must be
$b$ because $b$ is rigid, and $\varrho_{j}$ unifies $u$ and $v$. Since
$\varrho_{j}a$ is not projective, that means that $b$ is not a bound variable.
Therefore, $b$ must be a constant. Then Lemma 9 (imitation) applies.

We have now constructed a run
$\mathopen{}\mathclose{{}\left(E_{0},\sigma_{0}}\right)\longrightarrow\mathopen{}\mathclose{{}\left(E_{1},\sigma_{1}}\right)\longrightarrow\mathopen{}\mathclose{{}\left(E_{2},\sigma_{2}}\right)\longrightarrow\cdots$
of the procedure. This run cannot be infinite because because the measure
$\operatorname{ord}\mathopen{}\mathclose{{}\left(E_{j},\varrho_{j}}\right)$
strictly decreases as $j$ increases. Hence, at some point we reach a $j$ such
that $E_{j}=\varnothing$ and $\varrho_{0}X=\varrho_{j}\,\sigma_{j}X$ for all
$X\not\in V$. Therefore,
$\mathopen{}\mathclose{{}\left(E,\operatorname{id}}\right)\longrightarrow^{*}\mathopen{}\mathclose{{}\left(\varnothing,\sigma_{j}}\right)\longrightarrow\sigma_{j}$,
and $\varrho X=\tau^{-1}\,\varrho_{j}\,\sigma_{j}X$ for all $X\not\in V$,
completing the proof.

##  5\. A New Decidable Fragment

We discovered a new fragment that admits a finite CSU and a simple oracle. The
oracle is based on work by Prehofer and the PT procedure [21], a modification
of Huet’s procedure. PT transforms an initial multiset of constraints $E_{0}$
by applying bindings $\varrho$. If there is a sequence
$E_{0}\;\Longrightarrow^{\varrho_{1}}\;\cdots\;\Longrightarrow^{\varrho_{n}}\;E_{n}$
such that $E_{n}$ has only flex-flex constraints, we say that PT produces a
preunifier $\sigma=\varrho_{n}\ldots\varrho_{1}$ with constraints $E_{n}$. A
sequence fails if $E_{n}=\bot$. As in the previous section, we consider all
terms to be $\alpha\beta\eta$-equivalence classes with the $\eta$-long
$\beta$-reduced form as their canonical representative. Unlike previously, in
this section we view unification constraints
$s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ as ordered pairs.

The following rules, however, are stated modulo orientation. The PT transition
rules, adapted for our presentation style, are as follows:

Deletion:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}s}$}}\\}\uplus
E\;\Longrightarrow^{\text{id}}\;E$

Decomposition:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,a\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t}_{m}}$}}\\}\uplus\allowbreak
E\;\Longrightarrow^{\text{id}}\;\\{s_{1}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{1},\ldots,s_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{m}\\}\uplus E$
where $a$ is rigid

Failure:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,a\,\overline{s}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,b\,\overline{t}}$}}\\}\uplus\allowbreak
E\;\Longrightarrow^{\text{id}}\;\bot$
where $a$ and $b$ are different rigid heads

Solution:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,F\,\overline{x}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t}$}}\\}\uplus
E\;\Longrightarrow^{\varrho}\;\varrho E$
where $F$ does not occur in $t$, $t$ does not have a flex head, and
$\varrho=\\{F\mapsto\lambda\overline{x}.\,t\\}$

Imitation:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,\mathsf{f}\,\overline{t}_{n}}$}}\\}\uplus
E\;\Longrightarrow^{\varrho}\;\varrho(\\{G_{1}\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{1},\ldots,G_{n}\,\overline{s}_{m}\allowbreak\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{n}\\}\uplus E)$
where
$\varrho=\\{F\mapsto\lambda\overline{x}_{m}.\,\mathsf{f}\,(G_{1}\,\overline{x}_{m})\ldots(G_{n}\,\overline{x}_{m})\\}$,
$\overline{G}_{n}$ are fresh variables of appropriate types

Projection:

$\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t}}$}}\\}\uplus
E\;\Longrightarrow^{\varrho}\;\varrho(\\{s_{i}\,(G_{1}\,\overline{s}_{m})\ldots(G_{j}\,\overline{s}_{m})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}a\,\overline{t}\\}\uplus E)$
where
$\varrho=\\{F\mapsto\lambda\overline{x}_{m}.\,x_{i}\,(G_{1}\,\overline{x}_{m})\ldots(G_{j}\,\overline{x}_{m})\\}$,
$\overline{G}_{j}$ are fresh variables of appropriate types

The grayed constraints are required to be selected by a given selection
function $S$. We call $S$ _admissible_ if it prioritizes selection of
constraints applicable for Failure and Decomposition, and of descendant
constraints of Projection transitions with $j=0$ (i.e., for $x_{i}$ of base
type), in that order of priority. In the remainder of this section we consider
only admissible selection functions, an assumption that Prehofer also makes
implicitly in his thesis. Additionally, whenever we compare multisets, we use
the multiset ordering defined by Dershowitz and Manna [8]. As above, we assume
that the fresh variables are taken from an infinite supply $V$ of fresh
variables that are different from the variables in the initial problem and
never reused.

The following Lemma states that PT is _complete for preunification_ :

######  Lemma 12.

Let $\varrho$ be a unifier of a multiset of constraints $E_{0}$. Then PT
produces a preunifier $\sigma$ with constraints $E_{n}$, and there exists a
unifier $\theta$ of $E_{n}$ such that $\varrho X=\theta\sigma X$ for all $X$
that are not contained in the supply $V$ of fresh variables.

######  Proof 5.1.

This lemma is a refinement of Lemma 4.1.7 from Prehofer’s PhD thesis [21], and
this proof closely follows the proof of that lemma.

We prove the lemma by induction using a well-founded measure on
$(\varrho,E_{0})$. The ordering is the lexicographic comparison of the
following properties:

A:

sum of the abstraction-free sizes of the terms $\varrho F$ for each variable
$F$ mapped by $\varrho$

B:

multiset of the sizes of constraints in $E_{0}$

Here, the _abstraction-free size_ is inductively defined by
$\text{afsize}(F)=1$; $\text{afsize}(x)=1$; $\text{afsize}(\mathsf{f})=1$;
$\text{afsize}(s\,t)=\text{afsize}(s)+\text{afsize}(t)$;
$\text{afsize}(\lambda x.\,s)=\text{afsize}(s)$.

If $E_{0}$ consists only of flex-flex constraints, then we can take an empty
transition sequence (i.e., $\sigma=\text{id}$) and $\theta=\varrho$.
Otherwise, there exists a constraint that is selected by an admissible
selection function. We show that for each such constraint, there is going to
be a PT transition bringing us closer to the desired preunifier.

Let $E_{0}=\\{\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t}$}}\\}\uplus E^{\prime}_{0}$.
Since $s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ is selected, at least one of
$s$ and $t$ must have a rigid head. We distinguish several cases based on the
form of $s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ (modulo the constraint order):

  * •

$s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}s$: in this case, Deletion
applies. This transition does not alter $\varrho$, but removes an equation
obtaining $E_{1}$ which is smaller than $E_{0}$ and still unifiable by
$\varrho$. By induction hypothesis, the preunifier is reachable.

  * •

$\lambda\overline{x}.\,a\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,b\,\overline{t}_{n}$,
where $a$ and $b$ are rigid: since $\varrho$ is a unifier, then $a=b$ and
$n=m$. Therefore, Decomposition applies. Similarly to the above case, we
conclude that the preunifier is reachable.

  * •

$\lambda\overline{x}.\,F\,\overline{x}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t$ where
$t$ has a rigid head and $F$ does not occur in $t$: Solution applies. Huet
showed [12, proof of L5.1] that in this case $\varrho=\varrho\sigma_{1}$,
where $\sigma_{1}=\\{F\mapsto\lambda\overline{x}.\,t\\}$. Let
$\varrho_{1}=\varrho\setminus\\{F\mapsto\varrho F\\}$. Then
$\varrho=\varrho_{1}\sigma_{1}$. Since $\varrho$ unifies $E^{\prime}_{0}$,
$\varrho_{1}$ unifies $E_{1}=\sigma_{1}E^{\prime}_{0}$. Clearly, $\varrho_{1}$
is smaller than $\varrho$. Now we can apply induction hypothesis on
$\varrho_{1}$ and $E_{1}$, from which we obtain a sequence
$E_{1}\;\Longrightarrow^{\sigma_{2}}\;\cdots\;\Longrightarrow^{\sigma_{n}}\;E_{n}$,
$\theta$ which unifies $E_{n}$ and
$\sigma^{\prime}=\sigma_{n}\ldots\sigma_{2}$, such that
$\varrho_{1}X=\theta\sigma^{\prime}X$ for all $X\not\in V$. Finally, it is
clear that sequence
$E_{0}\;\Longrightarrow^{\sigma_{1}}\;E_{1}\;\Longrightarrow^{\sigma_{2}}\;\cdots\;\Longrightarrow^{\sigma_{n}}\;E_{n}$,
$\theta$, and $\sigma=\sigma^{\prime}\sigma_{1}$ are as wanted in the lemma
statement.

  * •

$\lambda\overline{x}.\,F\,\overline{s}_{m}~{}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}~{}\lambda\overline{x}.\,a\,\overline{t}$
where $a$ is rigid: depending on the value of $\varrho$, we can either take an
Imitation or Projection step. In either case, we show that the measure
reduces. Let $\varrho F=\lambda\overline{x}_{m}.\,b\,\overline{u}_{n}$ where
$b$ is either a constant or a bound variable. If $b$ is a constant, we choose
the Imitation step; otherwise we choose the Projection step. In either case,
$\sigma_{1}=\\{F\mapsto\lambda\overline{x}_{m}.\,b\,(G_{1}\,\overline{x}_{m})\ldots(G_{n}\,\overline{x}_{m})\\}$.
Then it is easy to check that
$\varrho_{1}=\varrho\setminus\\{F\mapsto\lambda\overline{x}_{m}.\,b\,\overline{u}_{n}\\}\cup\\{G_{1}~{}\mapsto~{}\lambda\overline{x}_{m}.\,u_{1},\allowbreak\ldots,G_{n}\mapsto\lambda\overline{x}_{m}.\,u_{n}\\}$
unifies $E_{1}$ created as the result of imitation or projection. Clearly,
$\varrho_{1}$ has smaller abstraction-free size than $\varrho$. Therefore, by
the induction hypothesis we obtain the transitions
$E_{1}\;\Longrightarrow^{\sigma_{2}}\;\cdots\;\Longrightarrow^{\sigma_{n}}\;E_{n}$
and substitutions $\theta$ and $\sigma^{\prime}=\sigma_{n}\ldots\sigma_{2}$,
where $\varrho_{1}X=\theta\sigma^{\prime}X$ for all $X\not\in
V\setminus\\{G_{1},\dots,G_{n}\\}$ and $\theta$ is a unifier of $E_{n}$. Our
goal is to prove $\varrho X=\theta\sigma^{\prime}\sigma_{1}X$ for all
$X\not\in V$. For variables $X\not\in V$ that are not $F$, we have
$\sigma_{1}X=X$ and $\varrho X=\varrho_{1}X$, which implies $\varrho
X=\theta\sigma^{\prime}\sigma_{1}X$. For $X=F$, since $\varrho_{1}$ and
$\theta\sigma^{\prime}$ agree on $G_{1},\ldots,G_{n}$, we conclude that
$\varrho F=\theta\sigma^{\prime}\sigma_{1}F$. Therefore, by taking
$\sigma=\sigma^{\prime}\sigma_{1}$, and prepending $E_{0}$ to the sequence
from the induction hypothesis, we show that the preunifier is reachable.

Prehofer showed that PT terminates for some classes of constraints. We call a
term _linear_ if no free variable has repeated occurrences in it. We call a
term _solid_ if the arguments of its free variables are either bound variables
or ground base-type terms. We call it _strictly solid_ 111In Prehofer’s
thesis, strictly solid terms are called weakly second-order. if the arguments
of its free variables are either bound variables or second-order ground base-
type terms. For example, if $G$, $\mathsf{a}$, and $x$ are of base type, and
$F$, $H$, $\mathsf{g}$, and $y$ are binary, the terms $F\,G\,\mathsf{a}$, and
$H\,(\lambda x.\,x)\,\mathsf{a}$ are not solid; $\lambda x.\,F\,x\,x$ is
strictly solid; $F\,\mathsf{a}\,(\mathsf{g}\,(\lambda
y.\,y\,\mathsf{a}\,\mathsf{a})\,\mathsf{a})$ is solid, but not strictly.
Prehofer’s thesis states that PT terminates on
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$ if $s$ is linear, $s$
shares no free variables with $t$, $s$ is strictly solid, and $t$ is second-
order.

We extend this result in Theorem 18 along two axes: we create an oracle for
the full unification problem (rather than the preunification problem), and we
lift the second-order constraints by requiring $s$ and $t$ to be solid.

As a first step, we consider the matching problem. A _matching problem_ is a
unification problem $\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$ where $t$ is ground. In
what follows, we establish some useful properties of matching problems in
which both $s$ and $t$ are solid (_solid matching problems_). We call the
unifier of a matching problem a _matcher_.

######  Lemma 13.

PT terminates on a solid matching problem
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$.

######  Proof 5.2.

We show termination by designing a measure on a matching problem $E$ that
decreases with each application of a PT transition (possibly followed by
Decomposition or Failure steps). Our measure function compares the following
properties lexicographically:

A:

multiset of the sizes of right-hand sides of the constraints in $E$

B:

number of free variables in $E$

Clearly, when applying PT transitions, the problem stays a matching problem
because the applied bindings do not introduce free variables on the right-hand
sides. It is also easy to check that each applied binding keeps the terms in
the solid fragment. Namely, bindings for both Imitation and Projection
transitions are patterns, which means that, after applying the binding, fresh
free variables are applied only to bound variables or ground base-type terms.
The Solution transition effectively replaces the variable with a ground term,
which is obviously solid. We show each transition either trivially terminates
or reduces the measure:

Deletion:

A decreases.

Decomposition:

A decreases.

Failure:

Trivial – represents a terminal node.

Solution:

This transition applies on constraints of the form
$F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$. This reduces A, since the
constraint $F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ is removed and $F$ cannot
appear on the right-hand side.

Imitation:

The rule is applicable only on
$\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,\mathsf{f}\,\overline{t}_{n}$.
The Imitation transition replaces the constraint with
$\\{H_{i}\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\overline{t}_{i}\mid 1\leq i\leq
n\\}$. This reduces A, as $F$ does not appear on any right-hand side.

Projection:

The rule is applicable only on
$\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{t}_{n}$.
If $a$ is a bound variable, and we project $F$ to argument $s_{i}$ different
than $a$, Failure applies and PT trivially terminates. If we project $F$ to
$a$, we apply Decomposition, which reduces $A$. If $a$ is a constant, for
Failure not to apply, we have to project to a base-type ground term $s_{i}$.
This does not increase A, since no variables appear on right-hand sides, but
removes the variable $F$ from $E$, reducing B by one.

We say $\sigma$ is a grounding substitution if for every variable $F$ mapped
by $\sigma$, $\sigma F$ is ground.

######  Lemma 14.

All unifiers produced by PT for the solid matching problem
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$ are grounding
substitutions.

######  Proof 5.3.

Closely following the proof of Lemma 5.2.5 in Prehofer’s PhD thesis [21], we
prove our claim by induction on the length of the PT transition sequence that
leads to the unifier. We know this sequence is finite by Lemma 13. The base
case of induction, for the empty sequence, is trivial. The induction step is
made using one of the following transitions:

Deletion:

Trivial.

Decomposition:

Trivial.

Failure:

This rule is not relevant, since it will not lead to the unifier.

Solution:

This rule applies the substitution $\\{F\mapsto t\\}$, which is grounding
since $t$ is ground.

Imitation:

This transition applies on constraints of the form

$\lambda\overline{x}.\,F\,\overline{s}_{k}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,\mathsf{f}\,\overline{t}_{l}$

The binding for Imitation is
$\varrho=\\{F\mapsto\lambda\overline{x}_{k}.\,\mathsf{f}\,(G_{1}\,\overline{s}_{k})\ldots(G_{l}\,\overline{s}_{k})\\}$,
and reduces the problem to
$\\{G_{i}\,\overline{s}_{k}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t_{i}\mid 1\leq i\leq l\\}$.
Since the right-hand sides are ground, any unifier $\sigma$ produced by PT
must map all of the variables $G_{1},\ldots,G_{l}$. By induction hypothesis,
$\sigma G_{i}$ is ground. Therefore, $\sigma\varrho$ must map $F$ to a ground
term.

Projection:

This transition applies on constraints of the form

$\lambda\overline{x}.\,F\,\overline{s}_{k}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,t$

The binding for Projection is
$\varrho=\\{F\mapsto\lambda\overline{x}_{k}.\,x_{i}\,(G_{1}\,\overline{x}_{k})\ldots(G_{j}\,\overline{x}_{k})\\}$,
and reduces the problem to
$\\{s_{i}\,(G_{1}\,\overline{s}_{k})\ldots(G_{j}\,\overline{s}_{k})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}a\,\overline{t}_{l}\\}$. Since
the right-hand side is ground, any unifier $\sigma$ produced by PT must map
all of the variables $G_{1},\ldots,G_{j}$. By induction hypothesis, $\sigma
G_{i}$ is ground. Therefore, $\sigma\varrho$ must map $F$ to a ground term.

######  Lemma 15.

If $s$ and $t$ are solid, $s$ is linear and shares no free variables with $t$,
PT terminates for the preunification problem
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$, and all remaining flex-
flex constraints are solid.

######  Proof 5.4.

This lemma is a modification of Lemma 5.2.1 and Theorem 5.2.6 from Prehofer’s
PhD thesis [21]. Correspondingly, the following proof closely follows the
proofs for these two lemmas. We also adopt the notion of an _isolated_
variable from Prehofer’s thesis: a variable is isolated in a multiset $E$ of
constraints if it appears exactly once in $E$.

First, similarly to the proof of previous lemma we conclude each transition
maintains the condition that the terms remain solid. Second, we have to show
that variables on left-hand sides remain isolated. For Imitation and
Projection rules, the preservation of this invariant is obvious. Later, we
also show that Solution preserves it. Third, since $s$ and $t$ share no
variables, and $s$ is linear, no rule can introduce a variable from the right-
hand side to the left-hand side.

To prove termination of PT, we devise a measure that decreases with each
application of a PT transition. The measure lexicographically compares the
following properties:

A:

number of occurrences of constant symbols and bound variables that are not
below free variables on left-hand sides

B:

number of free variables on right-hand sides

C:

multiset of the sizes of right-hand sides

We show that each transition either trivially terminates or reduces the
measure:

Deletion:

A does not increase and at least one of A or B reduces.

Decomposition:

A reduces.

Failure:

Trivial.

Solution:

This rule applies in two cases:

  * •:

$F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$: since $F$ is isolated, A is
unchanged, B is not increased, and C reduces. All variables on left-hand sides
remain isolated since they are unaffected by this substitution.

  * •:

$t\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F$: since $F$ does not occur on
any left-hand side and the head of $t$ must be a constant or bound variable
(otherwise the rule would not be applicable), $A$ reduces. Even though $t$
might contain some free variables and $F$ can have multiple occurrences on
right-hand sides, all free variables on left-hand sides remain isolated.
Namely, all free variables in $t$ occur exactly once in the multiset, and
since $t\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}F$ is removed, all of them either
disappear or end up on right-hand sides.

Imitation:

We distinguish the following two forms of the selected constraint:

  * •:

$\lambda\overline{x}.\,F\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,\mathsf{f}\,\overline{u}_{m}$:
We replace this constraint by
$\\{H_{i}\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}u_{i}\mid 1\leq i\leq m\\}$ and
apply the Imitation binding
$F\mapsto\lambda\overline{x}_{n}.\,\mathsf{f}\,(H_{1}\,\overline{x}_{n})\allowbreak\ldots(H_{m}\,\overline{x}_{n})$.
As $F$ is isolated, A and B do not increase. Since $F$ is isolated, it does
not occur on any right-hand side, and hence C decreases.

  * •:

$\lambda\overline{x}.\,\mathsf{f}\,\overline{u}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F\,\overline{v}_{n}$:
applying the Imitation transition as above will reduce A since $F$ cannot
appear on any left-hand side.

Projection:

Similarly to the previous transition rule, we have two cases:

  * •:

$\lambda\overline{x}.\,F\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{u}_{m}$:
if $a$ is a bound variable, then for Failure not to be applicable afterwards,
we have to project $F$ onto argument $v_{i}$ equal to $a$. Then we proceed
like for Imitation. If $a$ is not a bound variable, then we have to project to
some base-type term $v_{j}$ (otherwise Failure would be applicable
afterwards). This reduces the problem to
$\lambda\overline{x}.\,v_{j}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{u}_{m}$.
This is a solid matching problem, whose solutions computed by PT are grounding
substitutions (see Lemma 14). Applying one of those solutions will eliminate
all the free variables in $\lambda\overline{x}.\,a\,\overline{u}_{m}$. Since
PT is parametrized by an admissible selection function, we know that there are
no constraints descending from a simple projection in $E$ since the constraint
$\lambda\overline{x}.\,F\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{u}_{m}$
was chosen, which, due to solidity restrictions, cannot be such a descendant.
Therefore, we know that PT will transform the descendants of the matching
problem
$\lambda\overline{x}.\,v_{j}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{u}_{m}$
until either Failure is observed (making PT trivially terminating) or until no
descendant exists and the grounding matcher is computed (see Lemmas 14 and
13). This results in removal of the original constraint
$\lambda\overline{x}.\,F\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,a\,\overline{u}_{m}$
and application of the computed grounding matcher which will either remove all
the free variables in the right-hand side of the constraint (not increasing A
and reducing B) or not increasing A and B, reduce C if no free variables occur
in the right-hand side.

  * •:

$\lambda\overline{x}.\,a\,\overline{v}_{n}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F\,\overline{u}_{m}$:
if $a$ is a bound variable, projecting $F$ onto argument $u_{i}$ will either
enable application of Decomposition as the next step reducing A, or it will
result in Failure, trivially terminating. If $a$ is a constant, then
projecting $F$ onto some $u_{j}$ will either yield Failure or enable
Decomposition, reducing A.

Enumerating a CSU for a solid flex-flex pair may seem as hard as for any other
flex-flex pair; however, the following two lemmas show that solid pairs admit
an MGU:

######  Lemma 16.

The unification problem
$\\{\lambda\overline{z}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{z}.\,F\,\overline{s}^{\prime}_{m}\\}$,
where both terms are solid, has an MGU of the form
$\sigma=\\{F\mapsto\lambda\overline{x}_{m}.\,G\,x_{j_{1}}\ldots x_{j_{r}}\\}$
where $G$ is a auxiliary variable, and $1\leq j_{1}<\cdots<j_{r}\leq m$ are
exactly those indices $j_{i}$ for which $s_{j_{i}}=s^{\prime}_{j_{i}}$.

######  Proof 5.5.

Let $\varrho$ be a unifier for the given unification problem. Let
$\lambda\overline{x}.\,u=\varrho F$. Take an arbitrary subterm of $u$ whose
head is a bound variable $x_{i}$. If $x_{i}$ is of function type, it
corresponds to either $s_{i}$ or $s^{\prime}_{i}$ which, due to solidity
restrictions, has to be a bound variable. Furthermore, since $\varrho$ is a
unifier, $s_{i}$ and $s^{\prime}_{i}$ have to be the syntactically equal.
Similarly, if $x_{i}$ is of base type, it corresponds to two ground terms
$s_{i}$ and $s^{\prime}_{i}$ which have to be syntactically equal. We conclude
that $\varrho$ can use variables from $\overline{x}_{n}$ only if they
correspond to syntactically equal terms. Therefore, there is a substitution
$\theta$ such that $\varrho X=\theta\sigma X$ for all $X\not=G$. Due to
arbitrary choice of $\varrho$, we conclude that $\sigma$ is an MGU.

######  Lemma 17.

Let
$\\{\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F^{\prime}\,\overline{s}^{\prime}_{m^{\prime}}\\}$
be a solid unification problem where $F\neq F^{\prime}$. By Lemma 13, there
exists a finite CSU $\\{\sigma_{i}^{1},\dots,\sigma_{i}^{k_{i}}\\}$ of the
problem $\\{s_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}H_{i}\,\overline{s}^{\prime}_{m^{\prime}}\\}$,
where $H_{i}$ is a fresh free variable. Let
$\lambda\overline{y}_{m^{\prime}}.\,s_{i}^{j}=\lambda\overline{y}_{m^{\prime}}.\,\sigma_{i}^{j}(H_{i})\,\overline{y}_{m^{\prime}}$.
Similarly, also by Lemma 13, there exists a finite CSU
$\\{\tilde{\sigma}_{i}^{1},\dots,\tilde{\sigma}_{i}^{l_{i}}\\}$ of the problem
$\\{s^{\prime}_{i}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\tilde{H}_{i}\,\overline{s}_{m}\\}$,
where $\tilde{H}_{i}$ is a fresh free variable. Let
$\lambda\overline{x}_{m}.\,{s^{\prime}}_{i}^{j}=\lambda\overline{x}_{m}.\,\tilde{\sigma}_{i}^{j}(\tilde{H}_{i})\,\overline{x}_{m}$.
Let $Z$ be a fresh free variable. An MGU $\sigma$ for the given problem is

$\displaystyle F$
$\displaystyle\mapsto\lambda\overline{x}_{m}.\,Z\,\underbrace{x_{1}\,\ldots\,x_{1}}_{k_{1}\text{
times}}\,\ldots\,\underbrace{x_{m}\,\ldots\,x_{m}}_{k_{m}\text{
times}}\,{s^{\prime}}_{1}^{1}\ldots{s^{\prime}}_{1}^{l_{1}}\,\ldots\,{s^{\prime}}_{m^{\prime}}^{1}\ldots{s^{\prime}}_{m^{\prime}}^{l_{m^{\prime}}}\,$
$\displaystyle F^{\prime}$
$\displaystyle\mapsto\lambda\overline{y}_{m^{\prime}}.\,Z\,s_{1}^{1}\ldots
s_{1}^{k_{1}}\ldots s_{m}^{1}\ldots s_{m}^{k_{m}}\,\underbrace{y_{1}\,\ldots
y_{1}}_{l_{1}\text{ times}}\,\ldots\,\underbrace{y_{m^{\prime}}\,\ldots
y_{m^{\prime}}}_{l_{m^{\prime}}\text{ times}}$

where the auxiliary variables are $H_{1},\dots,H_{m}$,
$\tilde{H}_{1},\dots\tilde{H}_{m^{\prime}}$, $Z$ and all auxiliary variables
associated with the above CSUs.

######  Proof 5.6.

Let $\varrho$ be an arbitrary unifier for the problem
$\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F^{\prime}\,\overline{s}^{\prime}_{m^{\prime}}$.
We prove $\sigma$ is an MGU by showing that there exists a substitution
$\theta$ such that $\varrho X=\theta\sigma X$ for all non-auxiliary variables
$X$. We can focus only on $X\in\\{F,F^{\prime}\\}$ because all other non-
auxiliary variables do neither appear in the original problem nor in $\sigma
F$ or $\sigma F^{\prime}$; so we can simply define $\theta X=\varrho X$.

Let $\lambda\overline{x}_{m}.\,u=\varrho F$ and
$\lambda\overline{y}_{m^{\prime}}.\,u^{\prime}=\varrho{F^{\prime}}$, where the
bound variables $\overline{x}_{m}$ and $\overline{y}_{m^{\prime}}$ have been
$\alpha$-renamed apart. We also assume that the names of variables bound
inside $u$ and $u^{\prime}$ are $\alpha$-renamed so that they are different
from $\overline{x}_{m}$ and $\overline{y}_{m^{\prime}}$. Finally, bound
variables from the definition of $\sigma$ have been $\alpha$-renamed to match
$\overline{x}_{m}$ and $\overline{y}_{m^{\prime}}$. We define $\theta$ to be
the substitution

$\theta=\\{Z\mapsto\lambda z_{1}^{1}\ldots z_{1}^{k_{1}}\ldots z_{m}^{1}\ldots
z_{m}^{k_{m}}\,w_{1}^{1}\ldots w_{1}^{l_{1}}\ldots w_{m^{\prime}}^{1}\ldots
w_{m^{\prime}}^{l_{m^{\prime}}}.\,\textsf{diff}(u,u^{\prime})\\}$

where diff$(v,v^{\prime})$ is defined recursively as

$\displaystyle\textsf{diff}(\lambda x.\,v,\lambda y.\,v^{\prime})$
$\displaystyle{}={}$ $\displaystyle\lambda x.\,\textsf{diff}(v,\\{y\mapsto
x\\}v^{\prime})$ (1)
$\displaystyle\textsf{diff}(a\,\overline{v}_{n},a\,\overline{v}^{\prime}_{n})$
$\displaystyle=$ $\displaystyle
a\,\textsf{diff}(v_{1},v^{\prime}_{1})\ldots\textsf{diff}(v_{n},v^{\prime}_{n})$
(2) $\displaystyle\textsf{diff}(x_{i},v^{\prime})$ $\displaystyle=$
$\displaystyle z_{i}^{k}\text{, if $v^{\prime}={s}_{i}^{k}$ }$ (3)
$\displaystyle\textsf{diff}(v,y_{i})$ $\displaystyle=$ $\displaystyle
w_{i}^{l}\text{, if $v={s^{\prime}}_{i}^{l}$ }$ (4)
$\displaystyle\textsf{diff}(x_{i}\,\overline{v}_{n},y_{j}\,\overline{v}^{\prime}_{n})$
$\displaystyle=$ $\displaystyle
z_{i}^{k}\,\textsf{diff}(v_{1},v^{\prime}_{1})\ldots\textsf{diff}(v_{n},v^{\prime}_{n})\text{,
if $y_{j}=s_{i}^{k}$ }$ (5)

From diff’s definition it is clear that there are terms $v,v^{\prime}$ for
which it is undefined. However, we will show that for each $u$ and
$u^{\prime}$ which are bodies of bindings from a unifier $\varrho$, diff is
defined and has the desired property. In equations 3, 4, and 5, if there are
multiple numbers $k$ or $l$ that fulfill the condition, choose an arbitrary
one. We need to show that $\varrho F=\theta\sigma F$ and $\varrho
F^{\prime}=\theta\sigma F^{\prime}$. By the definitions of $u$, $u^{\prime}$,
$\theta$ and $\sigma$ and $\beta$-reduction, this is equivalent to

$\displaystyle\lambda\overline{x}_{m}.\,u$
$\displaystyle=\lambda\overline{x}_{m}.\,\\{z_{i}^{k}\mapsto
x_{i},w_{i}^{l}\mapsto{s^{\prime}}_{i}^{l}\text{ for all
}k,l,i\\}\,\textsf{diff}(u,u^{\prime})$
$\displaystyle\lambda\overline{y}_{m^{\prime}}.\,u^{\prime}$
$\displaystyle=\lambda\overline{y}_{m^{\prime}}.\,\\{z_{i}^{k}\mapsto
s_{i}^{k},w_{i}^{l}\mapsto y_{i}\text{ for all
}k,l,i\\}\,\textsf{diff}(u,u^{\prime})$

We will show by induction that for any $\lambda\overline{x}_{m}.\,v$,
$\lambda\overline{y}_{m}.\,v^{\prime}$ such that

$\\{x_{1}\mapsto s_{1},\ldots,x_{m}\mapsto s_{m}\\}v=\\{y_{1}\mapsto
s^{\prime}_{1},\ldots,y_{m^{\prime}}\mapsto
s^{\prime}_{m^{\prime}}\\}v^{\prime}$

we have

$\displaystyle\begin{array}[]{c@{\qquad}l}v&=\\{z_{i}^{k}\mapsto
x_{i},w_{i}^{l}\mapsto{s^{\prime}}_{i}^{l}\text{ for all
}k,l,i\\}\,\textsf{diff}(v,v^{\prime})\\\ v^{\prime}&=\\{z_{i}^{k}\mapsto
s_{i}^{k},w_{i}^{l}\mapsto y_{i}\text{ for all
}k,l,i\\}\,\textsf{diff}(v,v^{\prime})\end{array}$

The equation ($\star$) holds for $v=u$ and $v^{\prime}=u^{\prime}$ because
$\varrho$ is a unifier of
$\lambda\overline{x}.\,F\,\overline{s}_{m}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda\overline{x}.\,F^{\prime}\,\overline{s}^{\prime}_{m^{\prime}}$.
Therefore, once we have shown that ($\star$) implies ($\dagger$), we know that
($\dagger$) holds for $v=u$ and $v^{\prime}=u^{\prime}$ and we are done.

We prove that ($\star$) implies ($\dagger$) by induction on the size of $v$
and $v^{\prime}$. We consider the following cases:

$v=\lambda x.\,v_{1}$:

For ($\star$) to hold $v$ and $v^{\prime}$ must be of the same type.
Therefore, the $\lambda$-prefixes of their $\eta$-long representatives must
have the same length and we can apply equation 1. By the induction hypothesis,
($\dagger$) holds.

$v=x_{i}$:

In this case, $\\{x_{1}\mapsto s_{1},\ldots,x_{m}\mapsto s_{m}\\}v=s_{i}$.
Since ($\star$) holds, $v^{\prime}$ must be an instance of a unifier from the
CSU of $s_{i}=H_{i}\,\overline{s}^{\prime}_{m^{\prime}}$. However, since
$s_{i}$ and all terms in $\overline{s}^{\prime}_{m^{\prime}}$ are ground,
$\lambda\overline{y}_{m}.\,v^{\prime}=\sigma_{i}^{k}(H_{i})$, for some $k$.
Then, $\textsf{diff}(x_{i},v^{\prime})=z_{i}^{k}$, and it is easy to check
that ($\dagger$) holds.

$v=x_{i}\,\overline{v}_{n},n>0$:

In this case, $x_{i}$ is mapped to $s_{i}$ which, due to solidity
restrictions, has to be a functional bound variable. Since ($\star$) holds, we
conclude that the head of $\\{y_{1}\mapsto
s^{\prime}_{1},\ldots,y_{m^{\prime}}\mapsto
s^{\prime}_{m^{\prime}}\\}v^{\prime}$ must be $s^{\prime}_{j}$, such that
$s^{\prime}_{j}=s_{i}$; this also means that
$v^{\prime}=y_{j}\,\overline{v^{\prime}}_{n}$. Therefore, it is easy to check
that some $\tau=\\{H_{i}\mapsto\lambda\overline{y}_{m^{\prime}}.\,y_{j}\\}$ is
a matcher for the problem $s_{i}=H_{i}\,\overline{s}^{\prime}_{m^{\prime}}$.
For some $k$, $\sigma_{i}^{k}=\tau$, i.e.,
$\textsf{diff}(v,v^{\prime})=z_{i}^{k}\,\textsf{diff}(v_{1},v^{\prime}_{1})\ldots\textsf{diff}(v_{n},v^{\prime}_{n})$.
By induction hypothesis, we get that $(\dagger)$ holds.

$v=a\,\overline{v}_{n}$:

In the remaining cases $a$ is either a free variable, a loose bound variable
different than $x_{1},\ldots,x_{m}$, or a constant. If $a$ is a free variable
or a loose bound variable different than $x_{1},\ldots,x_{m}$, then
$v^{\prime}=a\,\overline{v^{\prime}}_{n}$, since ($\star$) holds, all of
$\overline{s}^{\prime}_{m^{\prime}}$ are ground, and bound variables different
than $x_{1},\ldots,x_{m}$ and $y_{1},\ldots,y_{m^{\prime}}$ are renamed to
match by equation 1. By the induction hypothesis and by equation 2, we obtain
$(\dagger)$. If $a$ is a constant, we consider two cases: either
$v^{\prime}=a\,\overline{v^{\prime}}_{n}$ which allows us to apply the
induction hypothesis and obtain $(\dagger)$ as above, or
$v^{\prime}=y_{j}\,\overline{v^{\prime}}_{m}$. Since $a$ is a constant,
$y_{j}$ cannot be a functional bound variable, since then it would be mapped
to $s^{\prime}_{j}$, which due to solidity restrictions also has to be a
functional bound variable and $(\star)$ would not hold. Therefore
$v^{\prime}=y_{j}$. In this case, we proceed as in the case $v=x_{i}$ with the
roles of $v$ and $v^{\prime}$ swapped.

######  Theorem 18.

Let $s$ and $t$ be solid terms that share no free variables, and let $s$ be
linear. Then the unification problem
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$ has a finite CSU.

######  Proof 5.7.

By Lemma 15, PT terminates on
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$ with a finite set of
preunifiers $\sigma$, each associated with a multiset $E$ of solid flex-flex
pairs.

An MGU $\delta_{E}$ of the remaining multiset $E$ of solid flex-flex
constraints can be found as follows. Choose one constraint
$(u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v)\in E$ and determine an MGU
$\varrho$ for it using Lemma 16 or 17. Then the set
$\varrho(E\setminus\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v\\})$ also contains only solid
flex-flex constraints, and we iterate this process by choosing a constraint
from $\varrho(E\setminus\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v\\})$ next until there are no
constraints left, eventually yielding an MGU $\varrho^{\prime}$ of
$\varrho(E\setminus\\{u\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}v\\})$. Finally, we obtain the
MGU $\delta_{E}=\varrho^{\prime}\varrho$ of $E$.

Let $U=\\{\delta_{E}\sigma\mid\text{PT produces preunifier $\sigma$ with
constraints }E\\}$. By termination of PT, $U$ is finite. We show that $U$ is a
CSU. Let $\varrho$ be an arbitrary unifier for
$\\{s\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$. By Lemma 12, PT produces a
preunifier $\sigma$ with flex-flex constraints $E$ such that there is a
unifier $\theta$ of $E$ and $\varrho X=\theta\sigma X$ for all $X$ not
contained in the supply of fresh variables $V$. Since $\delta_{E}$ is an MGU
of $E$, assuming that we use variables from $V$ in the role of the auxiliary
variables, there exists a substitution $\theta^{\prime}$ such that $\theta
X=\theta^{\prime}\delta_{E}X$ for all $X\not\in V$. If we make sure that we
never reuse fresh variables and that the supply $V$ does not contain any
variables from the initial problem, it follows that $\varrho
X=\theta^{\prime}\delta_{E}\sigma X$ for all $X\not\in V$. Therefore, $U$ is a
CSU.

The proof of Theorem 18 provides an effective way to calculate a CSU using PT
and the results of Lemmas 16 and 17.

Let
$\\{F\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{g}\,\mathsf{a}\,(G\,\mathsf{a})\\}$
be the unification problem to solve. Projecting $F$ onto the first argument
will lead to a nonunifiable problem, so we perform imitation of $\mathsf{g}$
building a binding $\sigma_{1}=\\{F\mapsto\lambda
x.\,\mathsf{g}\,(F_{1}\,x)\,(F_{2}\,x)\\}$. This yields the problem
$\\{F_{1}\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{a},\allowbreak
F_{2}\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{a}\\}$. Again, we can
only imitate $\mathsf{a}$ for $F_{1}$ – building a new binding
$\sigma_{2}=\\{F_{1}\mapsto\lambda x.\,\mathsf{a}\\}$. Finally, this yields
the problem
$\\{F_{2}\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{a}\\}$. According to
Lemma 17, we find CSUs for the problems
$J_{1}\,\mathsf{a}=\mathsf{f}\,\mathsf{a}$ and
$I_{1}\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\mathsf{a}$ using PT. The latter
problem has a singleton CSU $\\{I_{1}\mapsto\lambda x.\,\mathsf{a}\\}$,
whereas the former has a CSU containing $\\{J_{1}\mapsto\lambda
x.\,\mathsf{f}\,x\\}$ and $\\{J_{1}\mapsto\lambda
x.\,\mathsf{f}\,\mathsf{a}\\}$. Combining these solutions, we obtain an MGU
$\sigma_{3}=\\{F_{2}\mapsto\lambda x.\,H\,x\,x\,\mathsf{a},\,G\mapsto\lambda
x.\,H\,(\mathsf{f}\,\mathsf{a})\,(\mathsf{f}\,x)\,x\\}$ for
$F_{2}\,(\mathsf{f}\,\mathsf{a})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{a}$. Finally, we get
the MGU $\sigma=\sigma_{3}\sigma_{2}\sigma_{1}=\\{F\mapsto\lambda
x.\,\mathsf{g}\,\mathsf{a}\,(H\,x\,x\,\mathsf{a}),\,G\mapsto\lambda
x.\,H\,(\mathsf{f}\,\mathsf{a})\,(\mathsf{f}\,x)\,x\\}$ of the original
problem. For brevity, we omitted the intermediate bindings of auxiliary
variables in $\sigma$.

Small examples that violate conditions of Theorem 18 and admit only infinite
CSUs can be found easily. The problem $\\{\lambda
x.\,F\,(\mathsf{f}\,x)\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda
x.\,\mathsf{f}\,(F\,x)\\}$ violates variable distinctness and is a well-known
example of a problem with only infinite CSUs. Similarly, $\lambda
x.\,\mathsf{g}\,(F\,(\mathsf{f}\,x))\,F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda
x.\,\mathsf{g}\,(\mathsf{f}\,(G\,x))\,G$, which violates linearity, reduces to
the previous problem. Only ground arguments to free variables are allowed
because $\\{F\,X\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}G\,\mathsf{a}\\}$ has only
infinite CSUs. Finally, it is crucial that functional arguments to free
variables are only bound variables: the problem $\\{\lambda y.\,X(\lambda
x.\,x)\,y\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}\lambda y.\,y\\}$ has only
infinite CSUs.

##  6\. An Extension of Fingerprint Indexing

A fundamental building block for almost all automated reasoning tools is the
operation of retrieving term pairs that satisfy certain conditions, e.g.,
unifiable terms, instances or generalizations. Indexing data structures are
used to implement this operation efficiently. If the data structure retrieves
precisely the terms that satisfy the condition, it is called _perfect_.

Higher-order indexing has received little attention compared to its first-
order counterpart. However, recent research in higher-order theorem proving
increased the interest in higher-order indexing [17, 3]. A _fingerprint index_
[23, 31] is an imperfect index based on the idea that the skeleton of the term
consisting of all non-variable positions is not affected by substitutions.
Therefore, we can easily determine that the terms are not unifiable (or
matchable) if they disagree on a fixed set of sample positions.

More formally, when we sample an untyped first-order term $t$ on a sample
position $p$, the _generic fingerprinting function_ gfpf distinguishes four
possibilities:

$\kern 50.00008pt\text{gfpf}(t,p)=\begin{cases}\mathsf{f}&\text{if $t|_{p}$
has a symbol head $\mathsf{f}$}\\\\[-3.0pt] {\textsf{A}}&\text{if $t|_{p}$ is
a variable}\\\\[-3.0pt] {\textsf{B}}&\text{if $t|_{q}$ is a variable for some
proper prefix $q$ of $p$}\\\\[-3.0pt]
{\textsf{N}}&\text{otherwise}\end{cases}\kern 50.00008pt$

We define the _fingerprinting function_
$\text{fp}(t)=(\text{gfpf}(t,p_{1}),\ldots,\text{gfpf}(t,p_{n}))$, based on a
fixed tuple of positions $\overline{p}_{n}$. Determining whether two terms are
compatible for a given retrieval operation reduces to checking their
fingerprints’ componentwise compatibility. The following matrices determine
the compatibility for retrieval operations:

$\mathsf{f}_{1}$ $\mathsf{f}_{2}$ A B N $\mathsf{f}_{1}\vphantom{{}^{()}}$ ✗ ✗
A ✗ B N ✗ ✗ ✗ $\mathsf{f}_{1}$ $\mathsf{f}_{2}$ A B N
$\mathsf{f}_{1}\vphantom{{}^{()}}$ ✗ ✗ ✗ ✗ A ✗ ✗ B N ✗ ✗ ✗ ✗

The left matrix determines unification compatibility, while the right matrix
determines compatibility for matching term $s$ (rows) onto term $t$ (columns).
Symbols $\mathsf{f}_{1}$ and $\mathsf{f}_{2}$ stand for arbitrary distinct
constants. Incompatible features are marked with ✗. For example, given a tuple
of term positions $(1,1.1.1,2)$, and terms
$\mathsf{f}(\mathsf{g}(X),\mathsf{b})$ and
$\mathsf{f}(\mathsf{f}(\mathsf{a},\mathsf{a}),\mathsf{b})$, their fingerprints
are $(\mathsf{g},{\textsf{B}},\mathsf{b})$ and
$(\mathsf{f},{\textsf{N}},\mathsf{b})$, respectively. Since the first
fingerprint component is incompatible, terms are not unifiable.

Fingerprints for the terms in the index are stored in a trie data structure.
This allows us to efficiently filter out terms that are not compatible with a
given retrieval condition. For the remaining terms, a unification or matching
procedure must be invoked to determine whether they satisfy the condition or
not.

The fundamental idea of first-order fingerprint indexing carries over to
higher-order terms – application of a substitution does not change the rigid
skeleton of a term. However, to extend fingerprint indexing to higher-order
terms, we must address the issues of $\alpha\beta\eta$-normalization and
figure how to cope with $\lambda$-abstractions and bound variables. To that
end, we define a function $\lfloor t\rfloor$, defined on $\beta$-reduced
$\eta$-long terms in De Bruijn [5] notation:

$\displaystyle\lfloor F\,\overline{s}\rfloor=F$ $\displaystyle\lfloor
x_{i}\,\overline{s}_{n}\rfloor=\textsf{db}_{i}^{\alpha}(\lfloor
s_{1}\rfloor,\ldots,\lfloor s_{n}\rfloor)$
$\displaystyle\lfloor\mathsf{f}\,\overline{s}_{n}\rfloor=\mathsf{f}(\lfloor
s_{1}\rfloor,\ldots,\lfloor s_{n}\rfloor)$
$\displaystyle\lfloor\lambda\overline{x}.\,s\rfloor=\lfloor s\rfloor$

We let $x_{i}$ be a bound variable of type $\alpha$ with De Bruijn index $i$,
and $\textsf{db}_{i}^{\alpha}$ be a fresh constant corresponding to this
variable. All constants $\textsf{db}_{i}^{\alpha}$ must be fresh. Effectively,
$\lfloor\;\rfloor$ transforms a $\eta$-long $\beta$-reduced higher-order term
to an untyped first-order term. Let ${t}_{\downarrow{\beta\eta}}$ be the
$\eta$-long $\beta$-reduced form of $t$; the higher-order generic
fingerprinting function $\text{gfpf}_{\textsf{ho}}$, which relies on
conversion $\langle t\rangle_{\textsf{db}}$ from named to De Bruijn
representation, is defined as

$\text{gfpf}_{\textsf{ho}}(t,p)=\text{gfpf}(\lfloor\langle{t}_{\downarrow{\beta\eta}}\rangle_{\textsf{db}}\rfloor,p)$

If we define
$\text{fp}_{\textsf{ho}}(t)=\text{fp}(\lfloor\langle{t}_{\downarrow{\beta\eta}}\rangle_{\textsf{db}}\rfloor)$,
we can support fingerprint indexing for higher-order terms with no changes to
the compatibility matrices. For example, consider the terms $s=(\lambda
xy.\,x\,y)\,\textsf{g}$ and $t=\mathsf{f}$, where $\mathsf{g}$ has the type
$\alpha\rightarrow\beta$ and $\mathsf{f}$ has the type
$\alpha\rightarrow\alpha\rightarrow\beta$. For the tuple of positions
$(1,1.1.1,2)$ we get

$\displaystyle\text{fp}_{\textsf{ho}}(s)=\text{fp}(\lfloor\langle{s}_{\downarrow{\beta\eta}}\rangle_{\textsf{db}}\rfloor)=\text{fp}(\mathsf{g}(\textsf{db}_{0}^{\alpha}))=(\textsf{db}_{0}^{\alpha},{\textsf{N}},{\textsf{N}})$
$\displaystyle\text{fp}_{\textsf{ho}}(t)=\text{fp}(\lfloor\langle{t}_{\downarrow{\beta\eta}}\rangle_{\textsf{db}}\rfloor)=\text{fp}(\mathsf{f}(\textsf{db}_{1}^{\alpha},\textsf{db}_{0}^{\alpha}))=(\textsf{db}_{1}^{\alpha},{\textsf{N}},\textsf{db}_{0}^{\alpha})$

Since the first and third fingerprint component are incompatible, the terms
are not unifiable.

Other first-order indexing techniques such as feature vector indexing and
substitution trees can probably be extended to higher-order terms using the
method described here as well.

##  7\. Implementation

Zipperposition [6, 7] is an open-
source222https://github.com/sneeuwballen/zipperposition theorem prover written
in OCaml. It is a versatile testbed for prototyping extensions to
superposition-based theorem provers. It was initially designed as a prover for
polymorphic first-order logic and then extended to higher-order logic. A
recent addition is a complete mode for Boolean-free higher-order logic [2],
which depends on a unification procedure that can enumerate a CSU. We
implemented our procedure in Zipperposition.

We used OCaml’s functors to create a modular implementation. The core of our
procedure is implemented in a module which is parametrized by another module
providing oracles and implementing the Bind step. In this way we can obtain
the complete or pragmatic procedure and seamlessly integrate oracles while
reusing as much common code as possible.

To enumerate all elements of a possibly infinite CSU, we rely on lazy lists
whose elements are subsingletons of unifiers (either one-element sets
containing a unifier or empty sets). The search space must be explored in a
fair manner, meaning that no branch of the constructed tree is indefinitely
postponed.

Each Bind step will give rise to new unification problems $E_{1},E_{2},\ldots$
to be solved. Solutions to each of those problems are lazy lists
$p_{1},p_{2},\ldots$ containing subsingletons of unifiers. To avoid postponing
some unifier indefinitely, we use the dovetailing technique: we first take one
subsingleton from $p_{1}$, then one from each of $p_{1}$ and $p_{2}$. We
continue with one subsingleton from each of $p_{1},p_{2}$ and $p_{3}$, and so
on. Empty lazy lists are ignored in the traversal. To ensure we do not remain
stuck waiting for a unifier from a particular lazy list, the procedure will
periodically return an empty set, indicating that the next lazy list should be
probed.

The implemented selection function for our procedure prioritizes selection of
rigid-rigid over flex-rigid pairs, and flex-rigid over flex-flex pairs.
However, since the constructed substitution $\sigma$ is not applied eagerly,
heads can appear to be flex, even if they become rigid after dereferencing and
normalization. To mitigate this issue to some degree, we dereference the heads
with $\sigma$, but do not normalize, and use the resulting heads for
prioritization.

We implemented oracles for the pattern, solid, and fixpoint fragment. Fixpoint
unification [12] is concerned with problems of the form
$\\{F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t\\}$. If $F$ does not occur in
$t$, $\\{F\mapsto t\\}$ is an MGU for the problem. If there is a position $p$
in $t$ such that $t|_{p}=F\,\overline{u}_{m}$ and for each prefix $q\neq p$ of
$p$, $t|_{q}$ has a rigid head and either $m=0$ or $t$ is not a
$\lambda$-abstraction, then we can conclude that
$F\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}t$ has no solutions. Otherwise,
the fixpoint oracle is not applicable.

##  8\. Evaluation

We evaluated the implementation of our unification procedure in
Zipperposition, assessing the complete variant and the pragmatic variant, the
latter with several different combinations of limits for number of bindings.
As part of the implementation of the complete mode for Boolean-free higher-
order logic in Zipperposition [2], Bentkamp implemented a straightforward
version of JP procedure. This version is faithful to the original description,
with a check as to whether a (sub)problem can be solved using a first-order
oracle as the only optimization. Our evaluations were performed on StarExec
Miami [26] servers with Intel Xeon E5-2620 v4 CPUs clocked at 2.10 GHz with 60
s CPU limit.

Contrary to first-order unification, there is no widely available corpus of
benchmarks dedicated solely to evaluating performance of higher-order
unification algorithms. Thus, we used all 2606 monomorphic higher-order
theorems from the TPTP library [28] and 832 monomorphic higher-order
Sledgehammer (SH) generated problems [27] as our benchmarks333An archive with
raw results, all used problems, and scripts for running each configuration is
available at http://doi.org/10.5281/zenodo.4269591. Many TPTP problems require
synthesis of complicated unifiers, whereas Sledgehammer problems are only
mildly higher-order – many of them are solved with first-order unifiers.

We used the naive implementation of the JP procedure (jp) as a baseline to
evaluate the performance of our procedure. We compare it with the complete
variant of our procedure (cv) and pragmatic variants (pv) with several
different configurations of limits for applied bindings. All other
Zipperposition parameters have been fixed to the values of a variant of a
well-performing configuration we used for the CASC-27 theorem proving
competition [29]. The cv configuration and all of the pv configurations use
only pattern unification as an underlying oracle. To test the effect of oracle
choice, we evaluated the complete variant in 8 combinations: with no oracles
(n), with only fixpoint (f), pattern (p), or solid (s) oracle, and with their
combinations: fp, fs, ps, fps.

Figure 1 compares different variants of the procedure with the naive JP
implementation. Each pv configuration is denoted by pv${}^{a}_{bcde}$ where
$a$ is the limit on the total number of applied bindings, and $b$, $c$, $d$,
and $e$ are the limits of functional projections, eliminations, imitations,
and identifications, respectively. Figure 2 summarizes the effects of using
different oracles.

The configuration of our procedure with no oracles outperforms the JP
procedure with the first-order oracle. This suggests that the design of the
procedure, in particular lazy normalization and lazy application of the
substitution, already reduces the effects of the JP procedure’s main
bottlenecks. Raw evaluation data shows that on TPTP benchmarks, complete and
pragmatic configurations differ in the set of problems they solve – cv solves
19 problems not solved by pv${}^{4}_{2222}$, whereas pv${}^{4}_{2222}$ solves
34 problems cv does not solve. Similarly, comparing the pragmatic
configurations with each other, pv${}^{6}_{3333}$ and pv${}^{4}_{2222}$ each
solve 13 problems that the other one does not. The overall higher success rate
of pv${}^{2}_{1020}$ compared to pv${}^{2}_{1222}$ suggests that solving flex-
flex pairs by trivial unifiers often suffices for superposition-based theorem
proving.

jp cv pv${}^{12}_{6666}$ pv${}^{6}_{3333}$ pv${}^{4}_{2222}$ pv${}^{2}_{1222}$
pv${}^{2}_{1121}$ pv${}^{2}_{1020}$ TPTP [jp][r]1551 [nc][r]1717 [np6][r]1722
[np3][r]1732 [np2][r]1732 [np1][r]1715 [np10][r]1712 [np0][r]1719 SH
[jp][r]242 [nc][r]260 [np6][r]253 [np3][r]255 [np2][r]255 [np1][r]254
[np10][r]259 [np0][r]257

Figure 1. Proved problems, per configuration

n f p s fp fs ps fps TPTP [n][r]1658 [s][r]1717 [p][r]1717 [sp][r]1720
[n][r]1719 [s][r]1724 [p][r]1720 [sp][r]1723 SH [n][r]245 [s][r]255 [p][r]260
[sp][r]259 [n][r]255 [s][r]254 [p][r]258 [sp][r]254

Figure 2. Proved problems, per used oracle

Counterintuitively, in some cases, using oracles can hurt the performance of
Zipperposition. Using oracles typically results in generating smaller CSUs,
whose elements are more general substitutions than the ones we obtain without
oracles. These more general substitutions usually contain more applied
variables, which Zipperposition’s heuristics avoid due to their explosive
nature. This can make Zipperposition postpone necessary inferences for too
long. Configuration n benefits from this effect and therefore solves 18 TPTP
problems that no other configuration in Figure 2 solves. The same effect also
gives configurations with only one oracle an advantage over configurations
with multiple oracles on some problems.

The evaluation sheds some light on how often solid unification problems appear
in practice. The raw data show that configuration s solves 5 TPTP problems
that neither f nor p solve. Configuration f solves 8 TPTP problems that
neither s nor p solve, while p solves 9 TPTP problems that two other
configurations do not. This suggests that the solid oracle is slightly less
beneficial than the fixpoint or pattern oracles, but still presents a useful
addition the set of available oracles.

A subset of TPTP benchmarks, concerning operations on Church numerals, is
designed to test the efficiency of higher-order unification. Our procedure
performs exceptionally well on these problems – it solves all of them, usually
faster than other competitive higher-order provers. There are 11 benchmarks in
NUM category of TPTP that contain conjectures about Church numerals: NUM020^1,
NUM021^1, NUM415^1, NUM416^1, NUM417^1, NUM418^1, NUM419^1, NUM798^1,