Restricted Combinatory Unification

Abstract

First-order theorem provers are commonly utilised as backends to proof assistants. In order to improve efficiency, it is desirable that such provers can carry out some higher-order reasoning. In his 1991 paper, Dougherty proposed a combinatory unification algorithm for higher-order logic. The algorithm removes the need to deal with $\lambda$-binders and $\alpha$-renaming, making it attractive to implement in first-order provers. However, since publication it has garnered little interest due to a number of characteristics that make it unsuitable for a practical implementation. It fails to terminate on many trivial instances and requires polymorphism. We present a restricted version of Dougherty’s algorithm that is incomplete, terminating and does not require polymorphism. Further, we describe its implementation in the Vampire theorem prover, including a novel use of a substitution tree as a filtering index for higher-order unification. Finally, we analyse the performance of the algorithm on two benchmark sets and show that it is competitive.

A Restricted Combinatory Unification Is Terminating

We prove the termination of an algorithm identical to RCU, except that reductions can be performed at all positions. That RCU is terminating follows immediately. A straight-forward corollary of this is that RCU is incomplete.

Lemma 6

For any (finite) system $\mathcal {S}$, if there exists an infinite RCU computation path on $\mathcal {S}$, then there exists a system $\mathcal {S}'$ such that $\mathcal {S} \Longrightarrow ^* \mathcal {S}'$ and there exists an infinite computation path on $\mathcal {S}'$ that does not include the Eliminate or Split transforms.

Proof

Both Eliminate and Split reduce the number of unsolved variables in $\mathcal {S}$. As $\mathcal {S}$ is finite, it can only contain a finite number of unsolved variables. A case analysis of the other rules shows that either they reduce the number of unsolved variables or leave it unchanged. Thus Split and Eliminate can only be carried out a finite number of times.    $\square$

Based on Lemma 6, to prove that RCU is terminating, it suffices to prove that RCU without the eliminate and split transforms is terminating. Call the resulting set of transformation rules RCU−. Next a result analogous to Lemma 6 is proved with respect to the HeadNarrow transformation.

Definition 4

(Size). The size of a type $\sigma$ is defined inductively as follows:

• $\sigma$ is atomic, the $size(\sigma ) = 0$

• $\sigma = \alpha \rightarrow \beta$, then $size(\sigma ) = size(\alpha ) + size(\beta ) + 1$

For a term t, its type is denoted by $\tau (t)$

Intuitively, $size(\sigma )$ is the number of ‘$\rightarrow$’s in $\sigma$.

Lemma 7

For any (finite) system $\mathcal {S}$, if there exists an infinite RCU− computation path on $\mathcal {S}$, then there exists a system $\mathcal {S}'$ such that $\mathcal {S} \Longrightarrow ^* \mathcal {S}'$ and there exists an infinite computation path on $\mathcal {S}'$ that does not include the head narrow transform.

Proof

Consider the following measure on systems:

$$\begin{aligned} (\sum _{v \in vars(\mathcal {S})} size(\tau (v)), \# \mathcal {S} ) \end{aligned}$$

Where the pairs are compared lexicographically and $\# \mathcal {S}$ denotes the number of variables in $\mathcal {S}$ or equivalently, the cardinality of . The transformation rules of RCU−, other than head narrow, keep this measure constant or reduce it. HeadNarrow reduces the measure, so there can only be a finite number of applications of head narrow. The former claim is demonstrated for a number of HeadNarrow steps:

• 1. KX-narrow. For a variable X to be eligible for a KX-narrow step, it must have type $\alpha \rightarrow \beta$. It is replaced by a term $\varvec{\mathsf {K}}_{\beta \rightarrow \alpha \rightarrow \beta } X'_{\beta }$. Clearly $size(\tau (X')) < size(\tau (X))$ and so the first item of the measure is reduced.

• 2. BX-narrow. For a variable X to be eligible for a BX-narrow step, it must have type $(\alpha \rightarrow \beta ) \rightarrow \alpha \rightarrow \gamma$. It is replaced by a term $\varvec{\mathsf {B}}_{(\beta \rightarrow \gamma ) \rightarrow (\alpha \rightarrow \beta ) \rightarrow \alpha \rightarrow \gamma } X'_{\beta \rightarrow \gamma }$. Again $size(\tau (X')) < size(\tau (X))$ and so the first item of the measure is reduced.

• 3. CX-narrow. In this case, the size of the type of the variable being narrowed is not reduced. For a variable X to be eligible for a CX-narrow step, it must have type $\alpha \rightarrow \beta \rightarrow \gamma$. It is replaced by a term $\varvec{\mathsf {C}}_{(\beta \rightarrow \alpha \rightarrow \gamma ) \rightarrow \alpha \rightarrow \beta \rightarrow \gamma } X'_{\beta \rightarrow \alpha \rightarrow \gamma }$. Here $size(\tau (X')) = size(\tau (X))$. However, each CX-narrow step replaces a variable with a variable and therefore the second item of the measure is reduced.    $\square$

Based on Lemma 7 to prove that RCU− is terminating, it suffices to prove that RCU− without the HeadNarrow transformation is terminating. This is precisely Dougherty’s VT transformations which he has proven to be terminating in [11]. Therefore we have:

Theorem 2

Every sequence of RCU transformations terminates.