A KnuthBendixLike Ordering for Orienting Combinator Equations
 2 Citations
 185 Downloads
Abstract
We extend the graceful higherorder basic KnuthBendix order (KBO) of Becker et al. to an ordering that orients combinator equations lefttoright. The resultant ordering is highly suited to parameterising the firstorder superposition calculus when dealing with the theory of higherorder logic, as it prevents inferences between the combinator axioms. We prove a number of desirable properties about the ordering including it having the subterm property for ground terms, being transitive and being wellfounded. The ordering fails to be a reduction ordering as it lacks compatibility with certain contexts. We provide an intuition of why this need not be an obstacle when using it to parameterise superposition.
1 Introduction
There exists a wide range of methods for automated theorem proving in higherorder logic. Some provers such as AgsyHOL [17], Satallax [10] and LeoII [4] implement dedicated higherorder proof calculi. A common approach, followed by the LeoIII prover [21], is to use a cooperative architecture with a dedicated higherorder prover working in conjunction with a firstorder prover. It has long been part of theorem proving folklore that sound and complete translations from higherorder to firstorder logic exist. Kerber [15] proves this result for a higherorder logic that does not assume comprehension axioms (otherwise known as applicative firstorder logic). Thus, translating higherorder problems to firstorder logic and running firstorder provers on the translations is another method of automated higherorder theorem proving. Variations of this method are widely utilised by interactive theorem provers and their hammers such as Sledgehammer [18] and the CoqHammer [11].
Almost all translations to firstorder logic translate \(\lambda \)expressions using combinators. It is well known that the set of combinators \(\varvec{\mathsf {S}}, \varvec{\mathsf {K}}\) and \(\varvec{\mathsf {I}}\) is sufficient to translate any \(\lambda \)expression. For purposes of completeness, these combinators must be axiomatised: \(\varvec{\mathsf {S}}{\langle \tau _1, \tau _2, \tau _3\rangle } \, x\, y\, z = x\, z\, (y\, z)\), \(\varvec{\mathsf {K}}{\langle \tau _1, \tau _2\rangle } \, x \, y = x\) and \(\varvec{\mathsf {I}}{\langle \tau \rangle } \, x = x\). If translating to a monomorphic logic a finite set of axioms cannot achieve completeness.
However, till now, translation based methods have proven disappointing and only achieved decent results with interactive theorem provers when the problems are firstorder or nearly firstorder [22]. One major reason for this is that inferences between combinator axioms can be hugely explosive. A common firstorder proof calculus is superposition [19]. Consider a superposition inference from the \(\varvec{\mathsf {K}}\) axiom onto the righthand of the \(\varvec{\mathsf {S}}\) axiom. The result is \(\varvec{\mathsf {S}}\, \varvec{\mathsf {K}}\, y \, z = z\). There is little to restrict such inferences.
Superposition is parameterised by a simplification ordering and inferences are only carried out on the larger side of literals with respect to this ordering. Inferences are not carried out at variables. Consider the \(\varvec{\mathsf {S}}\), \(\varvec{\mathsf {K}}\) and \(\varvec{\mathsf {I}}\)axioms given above. There can clearly be no unifiers between a subterm of the left side of one axiom and the left side of another except at a variable. Thus, if a simplification ordering exists that orients the axioms lefttoright, inferences amongst the axioms would be impossible.
Currently, no such simplification ordering is known to exist and the authors suspect that no such ordering can exist. Whilst there is a large body of work on higherorder orderings, all either lack some property required for them to be simplification orderings or are unsuitable for orienting the combinator axioms. Jouannaud and Rubio introduced a higherorder version of the recursive path order called HORPO [14]. HORPO is compatible with \(\beta \)reduction which suggests that without much difficulty it could be modified to be compatible with weak reduction. However, the ordering does not enjoy the subterm property, nor is it transitive. Likewise, is the case for orderings based on HORPO such as the computability path ordering [8] and the iterative HOIPO of Kop and Van Raamsdonk [16]. More recently, a pair of orderings for \(\lambda \)free higherorder terms have been developed [2, 7]. These orderings lack a specific monotonicity property, but this does not prevent their use in superposition [3]. However, neither ordering orients combinator axioms directly.
We investigate an extension of the graceful higherorder basic KBO \(>_{\mathsf {hb}}\) introduced by Becker et al. [2]. Our new ordering, \(>_{\mathsf {ski}}\), orients combinator equations lefttoright. Thus, if it is used to parameterise a superposition calculus, there can be no inferences among the axioms. The \(>_{\mathsf {ski}}\) ordering lacks full compatibility with contexts which is normally a requirement for an ordering to parameterise superposition. In particular, the ordering is not compatible with the socalled unstable contexts. In separate work we show that this is not an obstacle to achieving completeness [5].
A complete superposition calculus for HOL already exists [3]. This calculus has the \(\lambda \)calculus rather than combinatory logic as its underlying logic. It also employs higherorder unification. There appear to be two potential benefits to using a slightly modified firstorder superposition calculus parameterised by our new ordering \(>_{\mathsf {ski}}\) over lambda superposition as developed in [3].

A superposition calculus parameterised by \(>_{\mathsf {ski}}\) is far closer to standard firstorder superposition than lambda superposition. Unification is firstorder and there is no need to deal with binders and bound variables. This allows the reuse of the wellstudied datastructures and algorithms used in firstorder superposition [12, 20].

As discussed further in the conclusion (Sect. 6), the \(>_{\mathsf {ski}}\) ordering allows the comparison of a larger class of nonground terms than the ordering used in [3]. This results in fewer superposition inferences.
Two approaches extending the \(>_{\mathsf {hb}}\) ordering by first comparing terms by the length of the longest weak reduction from them. The approaches differ in the manner in which they compare nonground terms. A useful trait for an ordering that parameterises superposition is to be able to compare a large class of nonground terms since this reduces the number of inferences carried out. The most powerful method of defining a nonground ordering \(\succ \) is to semantically lift a ground ordering, i.e., to define \(t \succ s\) to hold iff \(t\theta \succ s\theta \) for all grounding substitutions \(\theta \). Such an ordering in noncomputable and both our methods attempt to approximate it (Sect. 3).
A set of proofs that the introduced \(>_{\mathsf {ski}}\) ordering enjoys the necessary properties required for its use within the superposition calculus (Sect. 4) and a set of examples demonstrating how the ordering applies to certain terms (Sect. 5).
2 Preliminaries
The type of the term \(\mathsf {f}{\langle \, \overline{\tau _n} \,\rangle }\) is \(\sigma \{\, \overline{\alpha _n} \, \rightarrow \, \overline{\tau _n} \,\}\). Following [2], terms of the form \(t_1 \, t_2\) are called applications. Nonapplication terms are called heads. A term can uniquely be decomposed into a head and n arguments. Let \(t = \zeta \, \, \overline{t'_n} \,\). Then \(head(t) = \zeta \) where \(\zeta \) could be a variable or constant applied to possibly zero type arguments. The symbol \(\varvec{\mathcal {C_{\mathsf {any}}}}\) denotes a member of \(\{\varvec{\mathsf {S}}, \varvec{\mathsf {C}}, \varvec{\mathsf {B}}, \varvec{\mathsf {K}}, \varvec{\mathsf {I}}\}\), whilst \(\varvec{\mathcal {C_\mathsf {3}}}\) denotes a member of \(\{\varvec{\mathsf {S}}, \varvec{\mathsf {C}}, \varvec{\mathsf {B}}\}\). These symbols are only used when the combinator is assumed to have a full complement of arguments. Thus, in \(\varvec{\mathcal {C_\mathsf {3}}}\, \, \overline{t_n} \,\), \(n \ge 3\) is assumed. The symbols \(x,y,z \ldots \) are reserved for variables, \(\mathsf {c}, \mathsf {d}, \mathsf {f} \ldots \) for noncombinator constants and \(\zeta , \xi \) range over arbitrary symbols and, by an abuse of notation, at times even terms. A term is ground if it contains no variables and term ground if it contains no term variables.
Positions over Terms: For a term t, if Open image in new window or \(t = \mathsf {f}{\langle \, \overline{\tau } \,\rangle }\), then \(pos(t) = \{\epsilon \}\) (type arguments have no position). If \(t = t_1t_2\) then \(pos(t) = \{\epsilon \} \cup \{i.p \; \vert \; 1 \le i \le 2, \; p \in pos(t_i)\}\). Subterms at positions of the form p.1 are called prefix subterms and subterms at positions of the form p.2 are known as firstorder subterms. A position p is strictly above a position \(p'\) (denoted \(p < p'\)) if \(\exists p''. p'' \ne \epsilon \; \wedge \; p' = p.p''\). Positions p and \(p'\) are incomparable (denoted \(p \, \Vert \, p'\)) if neither \(p < p'\) nor \(p' < p\), nor \(p = p'\). By \(\vert t \vert \), the number of symbols occurring in t is denoted. By \(vars_{\#}(t)\) the multiset of variables in t is denoted. The expression \(A \subseteq B\) means that either A is a subset of B or A is a submultiset of B depending on whether A and B are sets or multisets.
Stable Subterms: We define a subset of firstorder subterms called stable subterms. Let \(\mathsf {LPP}(t, p)\) (LPP stands for Longest Proper Prefix) be a partial function that takes a term t and a position p and returns the longest proper prefix \(p'\) of p such that \(head(t \vert _{p'})\) is not a partially applied combinator if such a position exists. For a position \(p \in pos(t)\), p is a stable position in t if \(\mathsf {LPP}(t, p)\) is not defined or \(head(t \vert _{\mathsf {LPP}(t, p)})\) is not a combinator. A stable subterm is a subterm occurring at a stable position and is denoted \(t \langle \! \langle u \rangle \! \rangle _p\). We call \(t \langle \! \langle \rangle \! \rangle _p\) a stable context and drop the position where it is not relevant. For example, the subterm \(\mathsf {a}\) is not stable in \(\mathsf {f} \, (\varvec{\mathsf {S}}\, \mathsf {a} \, \mathsf {b} \, \mathsf {c})\), \(\varvec{\mathsf {S}}\, (\varvec{\mathsf {S}}\, \mathsf {a}) \, \mathsf {b} \, \mathsf {c}\) (in both cases, \(head(t\vert _{\mathsf {LPP}(t, p)}) = \varvec{\mathsf {S}}\)) and \(\mathsf {a} \, \mathsf {c}\) (\(\mathsf {a}\) is not a firstorder subterm), but is in \(\mathsf {g} \, \mathsf {a} \, \mathsf {b}\) and \(\mathsf {f} \, (\varvec{\mathsf {S}}\, \mathsf {a}) \, \mathsf {b}\). A subterm that is not stable is known as an unstable subterm.
The notation \(t [ u ]_p\) denotes an arbitrary subterm u of t that occurs at position p and may be unstable. The notation \(t [ u_1, \ldots , u_n ]\) (or \(t [ \, \overline{u_n} \, ]\)) denotes the term t containing n nonoverlapping subterms \(u_1\) to \(u_n\). By \(u [ ]_n\), we refer to a context with n nonoverlapping holes. Whilst this resembles the notation for a term at position n, ambiguity is avoided by never using n to denote a position or p to denote a natural number.
Weak Reduction: Each combinator is defined by its characteristic equation; \(\varvec{\mathsf {S}}\, x \, y \, z = x \, z \, (y \, z)\), \(\varvec{\mathsf {C}}\, x \, y \, z\) \( = x \, z \, y\), \(\varvec{\mathsf {B}}\, x \, y \, z = x \, (y \, z)\), \(\varvec{\mathsf {K}}\, x \, y = x\) and \(\varvec{\mathsf {I}}\, x = x\). A term t weakreduces to a term \(t'\) in one step (denoted \(t \longrightarrow _wt'\)) if \(t = u [ s ]_p\) and there exists a combinator axiom \(l = r\) and substitution \(\sigma \) such that \(l\sigma = s\) and \(t' = u [ r\sigma ]_p\). The term \(l\sigma \) in t is called a weak redex or just redex. By \(\longrightarrow _w^*\), the reflexive transitive closure of \(\longrightarrow _w\) is denoted. If term t weakreduces to term \(t'\) in n steps, we write \(t \longrightarrow _w^n t'\). Further, if there exists a weakreduction path from a term t of length n, we say that \(t \in n_w\). Weakreduction is terminating and confluent as proved in [13]. By \((t)\! \downarrow ^w\), we denote the term formed from t by contracting its leftmost redex.
The length of the longest weak reduction from a term t is denoted \(\Vert t \Vert \). This measure is one of the crucial features of the ordering investigated in this paper.
2.1 A Maximal WeakReduction Strategy
To show that the measure \(\Vert \Vert \) is computable we provide a maximal weakreduction strategy and prove its maximality. The strategy is used in a number of proofs later in the paper. It is in a sense equivalent to Barendregt’s ‘perpetual strategy’ in the \(\lambda \)calculus [1]. Our proof of its maximality follows the style of Van Raamsdonk et al. [23] in their proof of the maximality of a particular \(\beta \)reduction strategy. We begin by proving the fundamental lemma of maximality for combinatory terms.
Lemma 1 (Fundamental Lemma of Maximality)
\(\Vert \varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{t_n} \, \Vert = \Vert (\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{t_n} \,) \downarrow ^w\Vert + 1 + isK(\varvec{\mathcal {C_{\mathsf {any}}}}) \times \Vert t_2 \Vert \) where \(isK(\varvec{\mathcal {C_{\mathsf {any}}}}) = 1\) if \(\varvec{\mathcal {C_{\mathsf {any}}}}= \varvec{\mathsf {K}}\) and is 0 otherwise. The lemma holds for \(n \ge 3\) if \(\varvec{\mathcal {C_{\mathsf {any}}}}\in \{\varvec{\mathsf {S}}, \varvec{\mathsf {C}}, \varvec{\mathsf {B}}\}\), \(n \ge 2\) if \(\varvec{\mathcal {C_{\mathsf {any}}}}= \varvec{\mathsf {K}}\) and \(n \ge 1 \) otherwise.
Proof
Lemma 2
The reduction strategy \(F_\infty \) is maximal.
Proof
As the Lemma is not of direct relevance to the paper, its proof is relegated to the accompanying technical report [6].
3 Term Order
First, Becker et al.’s [2] graceful higherorder basic KBO is presented as it is utilised within our ordering. The presentation here differs slightly from that in [2] because we do not allow ordinal weightings and all function symbols have finite arities. Furthermore, we do not allow the use of different operators for the comparison of tuples, but rather restrict the comparison of tuples to use only the lengthlexicographic extension of the base order. This is denoted \(\gg _{\mathsf { hb}}^{\mathsf {length\_lex}}\). The lengthlexicographic extension first compares the lengths of tuples and if these are equal, carries out a lexicographic comparison. For this section, terms are assumed to be untyped following the original presentation.
3.1 Graceful HigherOrder Basic KBO
Standard firstorder KBO first compares the weights of terms, then compares their headsymbols and finally compares arguments recursively. When working with higherorder terms, the head symbol may be a variable. To allow the comparison of variable heads, a mapping ghd is introduced that maps variable heads to members of \(\varSigma \) that could possibly instantiate the head. This mapping respects arities if for any variable x, all members of ghd(x) have arities greater or equal to that of x. The mapping can be extended to constant heads by taking \(ghd(\mathsf {f}) = \{\mathsf {f}\}\). A substitution \(\sigma \) respects the mapping ghd, if for all variables x, \(ghd(x\sigma ) \subseteq ghd(x)\).
 Z1
 Z2
Open image in new window and \(\zeta \succ \xi \)
 Z3
Open image in new window and \(\, \overline{t} \, \gg _{\mathsf { hb}}^{\mathsf {length\_lex}} \, \overline{s} \,\)
3.2 Combinator Orienting KBO
The combinator orienting KBO is the focus of this paper. It has the property that all ground instances of combinator axioms are oriented by it lefttoright. This is achieved by first comparing terms by the length of the longest weak reduction from the term and then using \(>_{\mathsf {hb}}\). This simple approach runs into problems with regards to stability under substitution, a crucial feature for any ordering used in superposition.
Consider the terms \(t = \mathsf {f} \, x \, \mathsf {a}\) and \(s = x \, \mathsf {b}\). As the length of the maximum reduction from both terms is 0, the terms would be compared using \(>_{\mathsf {hb}}\) resulting in \(t \succ s\) as Open image in new window. Now, consider the substitution \(\theta = \{x \rightarrow \varvec{\mathsf {I}}\}\). Then, \(\Vert s\theta \Vert = 1\) whilst \(\Vert t\theta \Vert = 0\) resulting in \(s\theta \succ t\theta \).
The easiest and most general way of obtaining an order which is stable under substitution would be to restrict the definition of the combinator orienting KBO to ground terms and then semantically lift it to nonground terms as mentioned in the introduction. However, the semantic lifting of the ground order is noncomputable and therefore useless for practical purposes. We therefore provide two approaches to achieving an ordering that can compare nonground terms and is stable under substitution both of which approximate the semantic lifting. Both require some conditions on the forms of terms that can be compared. The first is simpler, but more conservative than the second.
First, in the spirit of Bentkamp et al. [3], we provide a translation that replaces “problematic” subterms of the terms to be compared with fresh variables. With this approach, the simple variable condition of the standard KBO, \(vars_{\#}(s) \subseteq vars_{\#}(t)\), ensures stability. However, this approach is overconstrained and prevents the comparison of terms such as \(t = x \, \mathsf {a}\) and \(s = x \, \mathsf {b}\) despite the fact that for all substitutions \(\theta \), \(\Vert t\theta \Vert = \Vert s\theta \Vert \). Therefore, we present a second approach wherein no replacement of subterms occurs. This comes at the expense of a far more complex variable condition. Roughly, the condition stipulates that two terms are comparable if and only if the variables and relevant combinators are in identical positions in each.
Approach 1. Because the \(>_{\mathsf {hb}}\) ordering is not defined over typed terms, type arguments are replaced by equivalent term arguments before comparison. The translation \( ( \! [ ]\!) \) from Open image in new window to untyped terms is given below. First we define precisely the subterms that require replacing by variables.
Definition 1 (Type1 term)
Consider a term t of the form \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{t_n} \,\). If there exists a position p such \(t \vert _p\) is a variable, then t is a type1 term.
Definition 2 (Type2 term)
A term \(x \, \, \overline{t_n} \,\) where \(n > 0\) is a type2 term.
The translation to untyped terms is defined as follows. If t is a type variable \(\tau \), then \( ( \! [ t ]\!) = \tau \). If \(t = \kappa (\, \overline{\sigma _n} \,)\), then \( ( \! [ t ]\!) = \kappa \, ( \! [ \, \overline{\sigma _n} \, ]\!) \). If t is a term variable x, then \( ( \! [ t ]\!) = x\). If t is a type1 or type2 term, then \( ( \! [ t ]\!) \) is a fresh variable \(x_t\). If \(t = \mathsf {f} {\langle \, \overline{\tau _n} \,\rangle }\), then \( ( \! [ t ]\!) = \mathsf {f} \, ( \! [ \, \overline{\tau _n} \, ]\!) \). Finally, if \(t = t_1 \, t_2\), then \( ( \! [ t ]\!) = ( \! [ t_1 ]\!) ( \! [ t_2 ]\!) \).
An untyped term t weak reduces to an untyped term \(t'\) in one step if \(t = u [ s ]_p\) and there exists a combinator axiom \(l = r\) and substitution \(\sigma \) such that \( ( \! [ l ]\!) \sigma = s\) and \(t' = u [ ( \! [ r ]\!) \sigma ]_p\). The aim of the ordering presented here is to parametrise the superposition calculus. For this purpose, the property that for terms t and \(t'\), \(t \longrightarrow _wt' \implies t \succ t'\), is desired. To this end, the following lemma is proved.
Lemma 3
For all term ground polymorphic terms t and \(t'\), it is the case that \(t \longrightarrow _wt' \iff ( \! [ t ]\!) \longrightarrow _w ( \! [ t' ]\!) \).
Proof
The \(\implies \) direction can be proved by a straightforward induction on the t. The opposite direction is proved by an induction on \( ( \! [ t ]\!) \).
Corollary 1
A straightforward corollary of the above lemma is that for all termground polymorphic terms t, \(\Vert t \Vert = \Vert ( \! [ t ]\!) \Vert \).
 R1
\(\Vert t' \Vert > \Vert s' \Vert \) or,
 R2
\(\Vert t' \Vert = \Vert s' \Vert \) and \(t' >_{\mathsf {hb}}s'\).
Approach 2. Using approach 1, terms \(t = y \, \mathsf {a}\) and \(s = y \, \mathsf {b}\) are incomparable. Both are type2 terms and therefore \( ( \! [ t ]\!) = x_t\) and \( ( \! [ s ]\!) = x_s\). The variable condition obviously fails to hold between \(x_t\) and \(x_s\). Therefore, we consider another approach which does not replace subterms with fresh variables. We introduce a new translation \(\llbracket \rrbracket \) from Open image in new window to untyped terms that merely replaces type arguments with equivalent term arguments and does not affect term arguments at all. The simpler translation comes at the cost of a more complex variable condition. Before the revised variable definition can be provided, some further terminology requires introduction.
Definition 3 (Safe Combinator)
Let \(\varvec{\mathcal {C_{\mathsf {any}}}}\) occur in t at position p and let \(p'\) be the shortest prefix of p such that \(head(t \vert _{p'})\) is a combinator and for all positions \(p''\) between p and \(p'\), \(head(t \vert _{p''})\) is a combinator. Let \(p''\) be a prefix of p of length one shorter than \(p'\) if such a position exists and \(\epsilon \) otherwise. Then \(\varvec{\mathcal {C_{\mathsf {any}}}}\) is safe in t if \(t \vert _{p'}\) is ground and Open image in new window and unsafe otherwise.
Intuitively, unsafe combinators are those that could affect a variable on a longest reduction path or could become applied to a subterm of a substitution. For example, all combinators in the term \(\varvec{\mathsf {S}}\, (\varvec{\mathsf {K}}\, \varvec{\mathsf {I}}) \, \mathsf {a} \, x\) are unsafe because they affect x, whilst the combinator in \(\mathsf {f} \, (\varvec{\mathsf {I}}\, \mathsf {b}) \, y\) is safe. The combinators in \(x \, (\varvec{\mathsf {S}}\, \varvec{\mathsf {I}}) \, \mathsf {a}\) are unsafe because they could potentially interact with a term substituted for x.
Definition 4
We say a subterm is toplevel in a term t if it doesn’t appear beneath an applied variable or fully applied combinator head in t.
Definition 5 (Safe)
Let \(t_1\) and \(t_2\) be untyped terms. The predicate \(safe(t_1, t_2)\) holds if for every position p in \(t_2\) such that \(t_2 \vert _p = \varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{t_n} \,\) and \(\varvec{\mathcal {C_{\mathsf {any}}}}\) (not necessarily fully applied) is unsafe, then \(t_{1} \vert _p = \varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{s_n} \,\) and for \(1 \le i \le n\), \(\Vert s_i \Vert \ge \Vert t_i \Vert \). Further, for all p in \(pos(t_2)\) such that \(t_2 \vert _p = x \, \, \overline{t_n} \,\), then \(t_{1} \vert _p = x \, \, \overline{s_n} \,\) and for \(1 \le i \le n\), \(\Vert s_i \Vert \ge \Vert t_i \Vert \).
The definition of safe ensures that if safe(t, s) and \(\Vert t \Vert \ge \Vert s \Vert \), then \(\Vert t\sigma \Vert \ge \Vert s\sigma \Vert \) for any substitution \(\sigma \) a result we prove in Lemma 13. Consider terms \(t = x \, (\varvec{\mathsf {I}}(\varvec{\mathsf {I}}\, (\varvec{\mathsf {I}}\, \mathsf {a}))) \, \mathsf {b}\) and \(s = x \, \mathsf {a} \, (\varvec{\mathsf {I}}\, (\varvec{\mathsf {I}}\, \mathsf {b}))\). We have that \(\Vert t \Vert = 3 > \Vert s \Vert = 2\). However, it is not the case that safe(t, s) because the condition that \(\Vert t_i \Vert \ge \Vert s_i \Vert \) for all i is not met. \(\Vert t_2 \Vert = \Vert b \Vert = 0 < 2 = \Vert \varvec{\mathsf {I}}\, (\varvec{\mathsf {I}}\, \mathsf {b}) \Vert = \Vert s_2 \Vert \). Now consider the substitution \(\sigma = \{x \rightarrow \varvec{\mathsf {S}}\, \mathsf {c} \}\). Because this substitution duplicates the second argument in s and t, \(\Vert t\sigma \Vert = 4 < \Vert s\sigma \Vert = 5\) showing the importance of the safe predicate in ensuring stability.
We draw out some obvious consequences of the definition of safety. Firstly, the predicate enjoys the subterm property in the following sense. If p is a position defined in terms \(t_1\) and \(t_2\), then \(safe(t_1, t_2) \implies safe(t_1\vert _p, t_2\vert _p)\). Secondly, the predicate is transitive; \(safe(t_1, t_2) \wedge safe(t_2, t_3) \implies safe(t_1, t_3)\).
There is a useful property that holds for nonground terms t and s such that safe(t, s).
Definition 6 (Semisafe)
Let t and s be untyped terms. Let \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{s_n} \,\) be a term that occurs in s at p such that all head symbols above \(\varvec{\mathcal {C_{\mathsf {any}}}}\) in s are combinators. Then semisafe(t, s) if \(t \vert _p = \varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{t_n} \,\) and for \(1 \le i \le n\), \(\Vert t_i \Vert \ge \Vert s_i \Vert \).
For example \(var\_cond(t, s)\) holds where \(t = \mathsf {f} \, y \, (x \, \mathsf {a})\) and \(s = \mathsf {g} \, (x \, b)\). In this case \(A = \{x \, \mathsf {b}\}\) and \(B = \{y, x \, \mathsf {a}\}\). There exists and injective total function from A to B that matches the requirements by relating \( x \, \mathsf {b}\) to \(x \, \mathsf {a}\). However, the variable condition does not hold in either direction if \(t = \mathsf {f} \, y \, (x \, \mathsf {a})\) and \(s = \mathsf {g} \, (x \, (\varvec{\mathsf {I}}\, \mathsf {b}))\). In this case, \(x \, (\varvec{\mathsf {I}}\, \mathsf {b})\) cannot be related to \(x \, a\) since the condition that \(\Vert a \Vert \ge \Vert \varvec{\mathsf {I}}\, \mathsf {b} \Vert \) is not fulfilled.
 R1
\(\Vert t' \Vert > \Vert s' \Vert \) or,
 R2
\(\Vert t' \Vert = \Vert s' \Vert \) and \(t' >_{\mathsf {hb}}s'\).
Lemma 4
For all ground instances of combinator axioms \(l \approx r\), we have \(l >_{\mathsf {ski}}r\).
Proof
Since for all ground instances of the axioms \(l \approx r\), we have \(\Vert l \Vert > \Vert r \Vert \), the theorem follows by an application of R1.
It should be noted that for nonground instances of an axiom \(l \approx r\), we do not necessarily have \(l >_{\mathsf {ski}}r\) since l and r may be incomparable. This is no problem since the definition of \(>_{\mathsf {ski}}\) could easily be amended to have \(l >_{\mathsf {ski}}r\) by definition if \(l \approx r\) is an instance of an axiom. Lemma 4 ensures that stability under substitution would not be affected by such an amendment.
4 Properties
Various properties of the order \(>_{\mathsf {ski}}\) are proved here. The proofs provided here lack detail, the full proofs can be found in our report [6]. The proofs can easily be modified to hold for the less powerful \(>_{\mathsf {ski1}}\) ordering. In general, for an ordering to parameterise a superposition calculus, it needs to be a simplification ordering [19]. That is, superposition is parameterised by an irreflexive, transitive, total on groundterms, compatible with contexts, stable under substitution and wellfounded binary relation. Compatibility with contexts can be relaxed at the cost of extra inferences [3, 5, 9]. A desirable property to have in our case is coincidence with firstorder KBO, since without this, the calculus would not behave on firstorder problems as standard firstorder superposition would.
Theorem 1 (Irreflexivity)
For all terms s, it is not the case that \(s >_{\mathsf {ski}}s\).
Proof
Let \(s' = \llbracket s \rrbracket \). It is obvious that \(\Vert s' \Vert = \Vert s' \Vert \). Therefore \(s >_{\mathsf {ski}}s\) can only be derived by rule R2. However, this is precluded by the irreflexivity of \(>_{\mathsf {hb}}\).
Theorem 2 (Transitivity)
For terms s, t and u, if \(s >_{\mathsf {ski}}t\) and \(t >_{\mathsf {ski}}u\) then \(s >_{\mathsf {ski}}u\).
Proof
Let \(s' = \llbracket s \rrbracket \), \(t' = \llbracket t \rrbracket \) and \(u' = \llbracket u \rrbracket \). From \(var\_cond(s',t')\) and \(var\_cond(t',u')\), \(var\_cond(s',u')\) by the definition of \(var\_cond\) and the application of the transitivity of safe. If \(\Vert s' \Vert > \Vert t' \Vert \) or \(\Vert t' \Vert > \Vert u' \Vert \) then \(\Vert s' \Vert > \Vert u' \Vert \) and \(s >_{\mathsf {ski}}u\) follows by an application of rule R1. Therefore, suppose that \(\Vert s' \Vert = \Vert t' \Vert = \Vert u' \Vert \). Then it must be the case that \(s' >_{\mathsf {hb}}t'\) and \(t' >_{\mathsf {hb}}u'\). It follows from the transitivity of \(>_{\mathsf {hb}}\) that \(s' >_{\mathsf {hb}}u'\) and thus \(s >_{\mathsf {ski}}u\).
Theorem 3 (Ground Totality)
Let s and t be ground terms that are not syntactically equal. Then either \(s >_{\mathsf {ski}}t\) or \(t >_{\mathsf {ski}}s\).
Proof
Let \(s' = \llbracket s \rrbracket \) and \(t' = \llbracket t \rrbracket \). If \(\Vert s' \Vert \ne \Vert t' \Vert \) then by R1 either \(s >_{\mathsf {ski}}t\) or \(t >_{\mathsf {ski}}s\). Otherwise, \(s'\) and \(t'\) are compared using \(>_{\mathsf {hb}}\) and either \(t' >_{\mathsf {hb}}s'\) or \(s' >_{\mathsf {hb}}t'\) holds by the ground totality of \(>_{\mathsf {hb}}\) and the injectivity of \(\llbracket \rrbracket \).
Theorem 4 (Subterm Property for Ground Terms)
If t and s are ground and t is a proper subterm of s then \(s >_{\mathsf {ski}}t\).
Proof
Let \(s' = \llbracket s \rrbracket \) and \(t' = \llbracket t \rrbracket \). Since t is a subterm of s, \(t'\) is a subterm of \(s'\) and \(\Vert s' \Vert \ge \Vert t' \Vert \) because any weak reduction in \(t'\) is also a weak reduction in \(s'\). If \(\Vert s' \Vert > \Vert t' \Vert \), the theorem follows by an application of R1. Otherwise \(s'\) and \(t'\) are compared using \(>_{\mathsf {hb}}\) and \(s' >_{\mathsf {hb}}t'\) holds by the subterm property of \(>_{\mathsf {hb}}\). Thus \(s >_{\mathsf {ski}}t\).
Next, a series of lemmas are proved that are utilised in the proof of the ordering’s compatibility with contexts and stability under substitution. We prove two monotonicity properties Theorems 5 and 6. Both hold for nonground terms, but to show this, it is required to show that the variable condition holds between terms \(u [ t ]\) and \(u [ s ]\) for t and s such that \(t >_{\mathsf {ski}}s\). To avoid this complication, we prove the Lemmas for ground terms which suffices for our purposes. To avoid clutter, assume that terms mentioned in the statement of Lemmas 5–16 are all untyped, formed by translating polymorphic terms.
Lemma 5
\(\Vert \zeta \, \overline{t_n} \, \Vert = \sum _{i=1}^{n} \Vert t_i \Vert \) if \(\zeta \) is not a fully applied combinator.
Lemma 6
Let \(t = \zeta \, \overline{t_n} \,\). Then \(\Vert t \Vert \!>\! \sum _{i=1}^{n} \Vert t_i \Vert \) if \(\zeta \) is a fully applied combinator.
Lemma 7
Let \(\, \overline{t_n} \,\) be terms such that for each \(t_i\), \(head(t_i) \notin \{\varvec{\mathsf {I}}, \varvec{\mathsf {K}}, \varvec{\mathsf {B}}, \varvec{\mathsf {C}}, \varvec{\mathsf {S}}\}\). Let \(\, \overline{t'_n} \,\) be terms with the same property. Moreover, let \(\Vert t_i \Vert \ge \Vert t'_i \Vert \) for \(1 \le i \le n\). Let \(s = u [ \, \overline{t_n} \, ]\) and \(s' = u [ \, \overline{t'_n} \, ]\) where each \(t_i\) and \(t'_i\) is at position \(p_i\) in s and \(s'\). If the \(F_\infty \) redex in s is within \(t_i\) for some i, then the \(F_\infty \) redex in \(s'\) is within \(t'_i\) unless \(t'_i\) is in normal form.
Proof
Proof is by induction on \(\vert s \vert + \vert s' \vert \). If u has a hole at head position, then \(s = \mathsf {f} \, \, \overline{r_m} \, \, \, \overline{s_{m''}} \,\) and \(s' = \mathsf {g} \, \, \overline{v_{m'}} \, \, \, \overline{s'_{m''}} \,\) where \(t_1 = \mathsf {f} \, \, \overline{r_m} \,\) and \(t'_1 = \mathsf {g} \, \, \overline{v_{m'}} \,\). Assume that the \(F_\infty \) redex of s is in \(t_1\). Further, assume that \(\Vert t'_1 \Vert > 0\). Then, for some i in \(\{1 \ldots m'\}\), it must be the case that \(\Vert v_i \Vert > 0\). Let j be the smallest index such that \(\Vert v_j \Vert > 0\). Then by the definition of \(F_\infty \), \(F_\infty (s') = \mathsf {g} \, v_1 \ldots v_{j1} \, F_\infty (v_j) \, v_{j+1} \ldots v_{m'} \, \, \overline{s'_{m''}} \,\) and the \(F_\infty \) redex of \(s'\) is in \(t'_1\).
Suppose that the \(F_\infty \) redex of s is not in \(t_1\). This can only be the case if \(\Vert t_1 \Vert = 0\) in which case \(\Vert t'_1 \Vert = 0 \) as well. In this case, by the definition of \(F_\infty \), \(F_\infty (s) = \mathsf {f} \, \, \overline{r_m} \, \, s_1 \ldots s_{i1} \, F_\infty (s_i) \, s_{i+1} \ldots s_m''\) where \(\Vert s_j \Vert = 0\) for \(1 \le j < i\). Without loss of generality, assume that the \(F_\infty \) redex of \(s_i\) occurs inside \(t_i\). Then \(t'_i\) must be a subterm of \(s'_i\). Assume that \(\Vert t'_i \Vert > 0\) and thus \(\Vert s'_i \Vert > 0\). Since for all i, \(s_i\) and \(s'_i\) only differ at positions where one contains a \(t_j\) and the other contains a \(t'_j\) and \(\Vert t_i \Vert \ge \Vert t'_i \Vert \) for \(1 \le i \le m''\), we have that \(\Vert s_j \Vert = 0\) implies \(\Vert s_j' \Vert = 0\). Thus, using the definition of \(F_\infty \), \(F_\infty (s') = \mathsf {g} \, \, \overline{v_{m'}} \, \, s'_1 \ldots s'_{i1} \, F_\infty (s'_i) \, s'_{i+1} \ldots s'_{m''}\). The induction hypothesis can be applied to \(s_i\) and \(s'_i\) to conclude that the \(F_\infty \) redex of \(s'_i\) occurs inside \(t'_i\). The lemma follows immediately.
If u does not have a hole at its head, then \(s = \mathsf {\zeta } \, \, \overline{s_n} \,\) and \(s' = \mathsf {\zeta } \, \, \overline{s'_n} \,\) where \(\zeta \) is not a fully applied combinator other than \(\varvec{\mathsf {K}}\) (if it was, the \(F_\infty \) redex would be at the head).
If \(\zeta \) is not a combinator, the proof follows by a similar induction to above. Therefore, assume that \(\zeta = \varvec{\mathsf {K}}\). It must be the case that \(\Vert s_2 \Vert > 0\) otherwise the \(F_\infty \) redex in s would be at the head and not within a \(t_i\). By the definition of \(F_\infty \), \(F_\infty (s) = \varvec{\mathsf {K}}\, s_1 \, F_\infty (s_2) \, s_3 \ldots s_n\). Let the \(F_\infty \) redex of \(s_2\) occur inside \(t_j\). Then \(t'_j\) is a subterm of \(s'_2\). If \(\Vert t'_j \Vert > 0\) then \(\Vert s'_2 \Vert > 0\) and \(F_\infty (s') = \varvec{\mathsf {K}}\, s'_1 \, F_\infty (s'_2) \, s'_3 \ldots s'_n\). By the induction hypothesis, the \(F_\infty \) redex of \(s'_2\) occurs in \(t'_j\).
Lemma 8
 1.
\(\exists i. u' = u [ t_1, \ldots , \hat{t_i}, \ldots , t_n ] \) where \(t_i \longrightarrow _w\hat{t_i}\) or
 2.
\(u' = \hat{u}\{x_1 \rightarrow t_1, \ldots , x_n \rightarrow t_n \}\) where \(u [ x_1, \ldots , x_n ] \longrightarrow _w\hat{u}\)
Proof
Let \(s = u [ \, \overline{t_n} \, ]\) and let \(p_1, \ldots p_n\) be the positions of \(\, \overline{t_n} \,\) in s. Since s is reducible, there must exist a p such that \(s\vert _p\) is a redex.
If \(p > p_i\) for some i, there exists a \(p' \ne \epsilon \) such that \(p = p_ip'\). Then, \(u [ t_1, \ldots , t_i,\) \(\ldots , t_n ]\vert _{p_i} = t_i [ \varvec{\mathcal {C_{\mathsf {any}}}}\, \overline{r_n} \, ]_{p'} \longrightarrow _wt_i [ (\varvec{\mathcal {C_{\mathsf {any}}}}\, \overline{r_n} \,)\! \downarrow ^w ]_{p'} \). Let \(\hat{t_i} = t_i [ (\varvec{\mathcal {C_{\mathsf {any}}}}\, \overline{r_n} \,)\! \downarrow ^w ]_{p'}\). We thus have that \(t_i \longrightarrow _w\hat{t_i}\) and thus \(u [ t_1, \ldots , t_i, \ldots , t_n ] \longrightarrow _wu [ t_1, \ldots , \hat{t_i}, \ldots , t_n ]\).
It cannot be the case that \(p = p_i\) for any i because \(head(t_i)\) is not a combinator for any \(t_i\). In the case where \(p < p_i\) or \(p \, \Vert \, p_i\) for all i, we have that \(u [ \, \overline{t_n} \, ] = (u [ \, \overline{x_n} \, ])\sigma \) and \(u [ \, \overline{x_n} \, ] \vert _p\) is a redex where \(\sigma = \{\, \overline{x_n} \, \rightarrow \, \overline{t_n} \,\}\). Let \(\hat{u}\) be formed from \(u [ \, \overline{x_n} \, ]\) by reducing its redex at p. Then , \(s = u [ \, \overline{t_n} \, ] = (u [ \, \overline{x_n} \, ])\sigma \longrightarrow _w{\hat{u}}\sigma = \hat{u}\{x_1 \rightarrow t_1 \ldots x_n \rightarrow t_n \}\)
Lemma 9
 1.
If \(\Vert t_i \Vert = \Vert t'_i \Vert \) for all i in \(\{1, \ldots , n\}\), then \(\Vert u [ \, \overline{t_n} \, ] \Vert = \Vert u [ \, \overline{t'_n} \, ] \Vert \) for all n holed contexts u.
 2.
If \(\Vert t_j \Vert > \Vert t'_j \Vert \) for some \(j \in \{1, \ldots , n\}\) and \(\Vert t_i \Vert \ge \Vert t'_i \Vert \) for \(i \ne j\), then \(\Vert u [ \, \overline{t_n} \, ] \Vert > \Vert u [ \, \overline{t'_n} \, ] \Vert \) for all n holed contexts u.
Proof
Let \(p_1, \ldots , p_n\) be the positions of the holes in u and let \(s = u [ \, \overline{t_n} \, ]\) and \(s' = u [ \, \overline{t'_n} \, ]\). Proof is by induction on \(\Vert s \Vert + \Vert s' \Vert \). We prove part (1) first:
Assume that \(\Vert u [ \, \overline{t_n} \, ] \Vert = 0\). Then \(\Vert t_i \Vert = 0\) for \(1 \le i \le n\). Now assume that \(\Vert u [ \, \overline{t'_n} \, ] \Vert \ne 0\). Then there must exist some position p such that \(s'\vert _p\) is a redex. We have that \(p \ne p_i\) for all \(p_i\) as \(head(t'_i) \notin \{\varvec{\mathsf {I}}, \varvec{\mathsf {K}}, \varvec{\mathsf {B}}, \varvec{\mathsf {C}}, \varvec{\mathsf {S}}\}\). Assume \(p > p_i\) for some \(p_i\). But then, \(\Vert t'_i \Vert > 0\) which contradicts the fact that \(\Vert t_i \Vert = \Vert t'_i \Vert \) for all i. Therefore, for all \(p_i\) either \(p < p_i\) or \(p \, \Vert \, p_i\). But then, if \(s'\vert _p\) is a redex, so must \(s \vert _p\) be, contradicting the fact that \(\Vert u [ \, \overline{t_n} \, ] \Vert = 0\). Thus, we conclude that \(\Vert u [ \, \overline{t'_n} \, ] \Vert = 0\).
Assume that \(\Vert u [ \, \overline{t_n} \, ] \Vert > 0\). Let \(u' = F_\infty (s)\). By Lemma 8 either \(u' = u [ t_1, \ldots , \hat{t_i},\) \( \ldots , t_n ]\) where \(t_i \longrightarrow _w\hat{t_i}\) for \(1 \le i \le n\) or \(u' = \hat{u}\{\, \overline{x_n} \, \rightarrow \, \overline{t_n} \,\}\) where \(u [ \, \overline{x_n} \, ] \longrightarrow _w\hat{u}\). In the first case, by Lemma 7 and \(\Vert t_i \Vert = \Vert t'_i \Vert \) we have \(F_\infty (s') = u'' = u [ t'_1, \ldots , \hat{t'_i},\) \( \ldots , t'_n ]\) where \(t'_i \longrightarrow _w\hat{t'_i}\). By the induction hypothesis \(\Vert u' \Vert = \Vert u'' \Vert \) and thus \(\Vert s \Vert = \Vert s' \Vert \). In the second case, \(F_\infty (s') = u'' = \hat{u}\{\, \overline{x_n} \, \rightarrow \, \overline{t'_n} \,\}\) where \(u [ \, \overline{x_n} \, ] \longrightarrow _w\hat{u}\). Again, the induction hypothesis can be used to show \(\Vert u' \Vert = \Vert u'' \Vert \) and the theorem follows.
We now prove part (2); \(\Vert u [ \, \overline{t_n} \, ] \Vert \) must be greater than 0. Again, let \(u' = F_\infty (s)\) and \(u'' = F_\infty (s')\). If \(u' = u [ t_1, \ldots , \hat{t_i},\) \(\ldots , t_n ]\) and \(\Vert t'_i \Vert \ne 0\), then by Lemma 7 \(u'' = u [ t'_1, \ldots , \hat{t'_i},\) \(\ldots , t'_n ]\) where \(t'_i \longrightarrow _w\hat{t'_i}\) unless \(\Vert t'_i \Vert = 0\) and the lemma follows by the induction hypothesis.
If \(\Vert t'_i \Vert = 0\), consider terms \(u'\) and \(s'\). If \(\Vert \hat{t_i} \Vert > 0\) or \(\Vert t_{j} \Vert > \Vert t'_j \Vert \) for some \(j \ne i\), then the induction hypothesis can be used to show \(\Vert u' \Vert > \Vert s' \Vert \) and therefore \(\Vert s \Vert = \Vert u' \Vert + 1 > \Vert s' \Vert \). Otherwise, \(\Vert t_j \Vert = \Vert t'_j \Vert \) for all \(j \ne i\) and \(\Vert \hat{t_i} \Vert = 0 = \Vert t'_i \Vert \). Part 1 of this lemma can be used to show that \(\Vert u' \Vert = \Vert s' \Vert \) and thus \(\Vert s \Vert = \Vert u' \Vert + 1 > \Vert s' \Vert \). If \(u' = \hat{u}\{\, \overline{x_n} \, \rightarrow \, \overline{t_n} \,\}\), then \(u'' = \hat{u}\{\, \overline{x_n} \, \rightarrow \, \overline{t'_n} \,\}\) and the lemma follows by the induction hypothesis.
Theorem 5 (Compatibility with Contexts)
For ground terms s and t, such that head(s), head(t) \(\notin \{\varvec{\mathsf {I}}, \varvec{\mathsf {K}}, \varvec{\mathsf {B}}, \varvec{\mathsf {C}}, \varvec{\mathsf {S}}\}\), and \(s >_{\mathsf {ski}}t\), then \(u [ s ] >_{\mathsf {ski}}u [ t ]\) for all ground contexts \(u [ ]\).
Proof
Let \(s' = \llbracket s \rrbracket \), \(t' = \llbracket t \rrbracket \) and \(u' = \llbracket u \rrbracket \). By Lemma 9 Part 2, we have that if \(\Vert s' \Vert > \Vert t' \Vert \), then \(\Vert u' [ s' ] \Vert > \Vert u' [ t' ] \Vert \). Thus, if \(s >_{\mathsf {ski}}t\) was derived by R1, \(u [ s ] >_{\mathsf {ski}}u [ t ]\) follows by R1. Otherwise, \(s >_{\mathsf {ski}}t\) is derived by R2 and \(\Vert s' \Vert = \Vert t' \Vert \). By Lemma 9 Part 1, \(\Vert u' [ s' ] \Vert = \Vert u' [ t' ] \Vert \) follows. Thus, \(u' [ s' ]\) is compared with \(u' [ t' ]\) by R2 and \(u [ s ] >_{\mathsf {ski}}u [ t ]\) by the compatibility with contexts of \(>_{\mathsf {hb}}\).
Lemma 10
\(\Vert s \Vert> \Vert t \Vert \implies \Vert u \langle \! \langle s \rangle \! \rangle \Vert > \Vert u \langle \! \langle t \rangle \! \rangle \Vert \) and \(\Vert s \Vert = \Vert t \Vert \implies \Vert u \langle \! \langle s \rangle \! \rangle \Vert = \Vert u \langle \! \langle t \rangle \! \rangle \Vert \).
Proof
Proceed by induction on the size of the context u. If u is the empty context, both parts of the theorem hold trivially.
The inductive case is proved for the first implication of the lemma first. If u is not the empty context, \(u \langle \! \langle s \rangle \! \rangle \) is of the form \(u' \langle \! \langle \zeta \, t_1 \ldots t_{i1}, s, t_{i+1} \ldots t_n \rangle \! \rangle \) . By the definition of a stable subterm \(\zeta \) cannot be a fully applied combinator and thus by Lemma 5 we have that \(\Vert \zeta \, t_1 \ldots t_{i1}, s, t_{i+1} \ldots t_n \Vert = \sum \nolimits _{j=1 \wedge j\ne i}^{n} \Vert t_j \Vert + \Vert s \Vert > \sum \nolimits _{j=1 \wedge j\ne i}^{n} \Vert t_j \Vert + \Vert t \Vert = \Vert \zeta \, t_1 \ldots t_{i1}, t, t_{i+1} \ldots t_n \Vert \). If \(\zeta \) is not a combinator, then \(\Vert u' \langle \! \langle \zeta \, t_1 \ldots t_{i1}, s, t_{i+1} \ldots \) \(t_n \rangle \! \rangle \Vert > \Vert u' \langle \! \langle \zeta \) \(\, t_1 \ldots t_{i1}, t,\) \(t_{i+1} \ldots t_n \rangle \! \rangle \Vert \) follows from Lemma 9 Part 2. Otherwise, \(\zeta \) is a partially applied combinator and \(u'\) is a smaller stable context than u. The induction hypothesis can be used to conclude that \(\Vert u' \langle \! \langle \zeta \, t_1 \) \(\ldots t_{i1}, s, t_{i+1}\) \(\ldots t_n \rangle \! \rangle \Vert > \Vert u' \langle \! \langle \zeta \, t_1 \ldots \) \( t_{i1}, t, t_{i+1} \ldots t_n \rangle \! \rangle \Vert \) and thus that \(\Vert u \langle \! \langle s \rangle \! \rangle \Vert > \Vert u \langle \! \langle t \rangle \! \rangle \Vert \). The proof of the inductive case for the second implication of the lemma is almost identical.
Theorem 6 (Compatibility with Stable Contexts)
For all stable ground contexts \(u \langle \! \langle \rangle \! \rangle \) and ground terms s and t, if \(s >_{\mathsf {ski}}t\) then \(u \langle \! \langle s \rangle \! \rangle >_{\mathsf {ski}}u \langle \! \langle t \rangle \! \rangle \).
Proof
If \(\Vert s \Vert > \Vert t \Vert \) then by Lemma 10, \(\Vert u \langle \! \langle s \rangle \! \rangle \Vert > \Vert u \langle \! \langle t \rangle \! \rangle \Vert \) holds and then by an application of R1 we have \(u \langle \! \langle s \rangle \! \rangle >_{\mathsf {ski}}u \langle \! \langle t \rangle \! \rangle \). Otherwise, if \(\Vert s \Vert = \Vert t \Vert \), then by Lemma 10 we have that \(\Vert u \langle \! \langle s \rangle \! \rangle \Vert = \Vert u \langle \! \langle t \rangle \! \rangle \Vert \). Thus \(u \langle \! \langle s \rangle \! \rangle \) and \(u \langle \! \langle t \rangle \! \rangle \) are compared using \(>_{\mathsf {hb}}\). By the compatibility with contexts of \(>_{\mathsf {hb}}\), \(\llbracket u \langle \! \langle s \rangle \! \rangle \rrbracket >_{\mathsf {hb}}\llbracket u \langle \! \langle t \rangle \! \rangle \rrbracket \) holds and then by ofan application of R2 \(u \langle \! \langle s \rangle \! \rangle >_{\mathsf {ski}}u \langle \! \langle t \rangle \! \rangle \) is true.
 1.
\(var\_cond(s,t)\) implies \(var\_cond(s\sigma , t\sigma )\).
 2.
\(var\_cond(s,t)\) and \(\Vert s \Vert \ge \Vert t \Vert \) imply \(\Vert s\sigma \Vert \ge \Vert t\sigma \Vert \)
The first is proved in Lemma 15. A slightly generalised version of (2) is proved in Lemma 14. Lemmas 11–13 are helper lemmas used in the proof of the above two properties.
Lemma 11
For a single hole context \(u \langle \! \langle \rangle \! \rangle \) such that the hole does not occur below a fully applied combinator and any term t, \(\Vert u \langle \! \langle t \rangle \! \rangle \Vert = \Vert u \langle \! \langle \rangle \! \rangle \Vert + \Vert t \Vert \).
Proof
Proof to be found in report.
Lemma 12
Let \(\, \overline{t_n} \,\) and \(\, \overline{s_n} \,\) be terms such that for \(n_1 \ldots n_n \in \mathbb {N}\) and for \(1 \le i \le n\), \(\Vert t_i \Vert \ge \Vert s_i \Vert + n_i\). Further, let \(t = t_1 \, t_2 \ldots t_n\) and \(s = s_1 \, s_2 \ldots s_n\). Assume that semisafe(t, s) holds. Then \(\Vert t \Vert \ge \Vert s \Vert + \sum _{i=1}^{n} n_i\).
Proof
Proof to be found in report.
Lemma 13
Let t and s be nonground terms such that \(\Vert t \Vert \ge \Vert s \Vert + m\) for some \(m \in \mathbb {N}\) and safe(t, s). Then, for any substitution \(\sigma \), \(\Vert t\sigma \Vert \ge \Vert s\sigma \Vert + m\) and \(safe(t\sigma , s\sigma )\).
Proof
Proof to be found in report.
Lemma 14
For terms t and s such that \(var\_cond(t,s)\) holds and \(\Vert t \Vert \ge \Vert s \Vert + n\) for some \(n \in \mathbb {N}\), for all substitutions \(\sigma \), \(\Vert t\sigma \Vert \ge \Vert s\sigma \Vert + n\).
Proof
If s and t are ground, the theorem is trivial. If s is ground, then \(\Vert t\sigma \Vert \ge \Vert t \Vert \ge \Vert s \Vert + n\). If s is not ground, then \(var\_cond(t,s)\) implies that t is not ground. Therefore, assume that neither is ground. If head(s) (and therefore head(t) by the variable condition) are fully applied combinators or variables, then \(var\_cond(t,s)\) implies safe(t, s) and Lemma 13 can be invoked to prove the lemma. Therefore, assume that both have nonvariable, nonfully applied combinator heads.
Let \(t = u \langle \! \langle \, \overline{t_m} \, \rangle \! \rangle \) and \(s = u' \langle \! \langle \, \overline{s_m} \, \rangle \! \rangle \) where \(\, \overline{s_m} \,\) are all the nonground, toplevel, firstorder subterms of the form \(x \, \, \overline{args} \,\) or \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{args} \,\) in s. By the variable condition, we have that there exists a total injective function respecting the given conditions from the \(s_i\) to nonground, toplevel, firstorder subterms of t of the form \(x \, \, \overline{args} \,\) or \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{args} \,\). Let \(\, \overline{t_m} \,\) be the terms related to \(\, \overline{s_m} \,\) by this function. Without loss of generality, assume that this function relates \(s_1\) to \(t_1\), \(s_2\) to \(t_2\) and so on. For \(1 \le i \le m\), \(\Vert t_i \Vert = \Vert s_i \Vert + m_i\) for \(m_i \in \mathbb {N}\). This follows from the fact that since \(t_i\) and \(s_i\) are both nonground and \(safe(t_i, s_i)\), we have \(semisafe(t_i, s_i)\) and can therefore invoke Lemma 12.
Lemma 15
For terms t and s such that \(var\_cond(t,s)\) holds and for all substitutions \(\sigma \), \(var\_cond(t\sigma , s\sigma )\).
Proof
Let \(t = u \langle \! \langle \, \overline{t_m} \, \rangle \! \rangle \) and \(s = u' \langle \! \langle \, \overline{s_m} \, \rangle \! \rangle \) where \(\, \overline{s_m} \,\) are all the nonground, toplevel, firstorder subterms of the form \(x \, \, \overline{args} \,\) or \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{args} \,\) in s. By the variable condition, we have that there exists a total injective function respecting the given conditions from the \(s_i\) to nonground, toplevel, firstorder subterms of t of the form \(x \, \, \overline{args} \,\) or \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{args} \,\). Let \(\, \overline{t_m} \,\) be the terms related to \(\, \overline{s_m} \,\) by this function. Without loss of generality, assume that this function relates \(s_1\) to \(t_1\), \(s_2\) to \(t_2\) and so on. By the definition of the variable condition, we have that \(u'\) must be ground. This implies that any nonground subterms of \(s\sigma \) must be subterms of some \(s_i\sigma \) for \(1 \le i \le m\).
Assume that for some i and \(p \in pos(s_i\sigma )\), \(s_i\sigma \vert _p\) is a nonground, toplevel, firstorder subterm of the form \(x \, \, \overline{args} \,\) or \(\varvec{\mathcal {C_{\mathsf {any}}}}\, \, \overline{args} \,\). We show that \(t_i\sigma \vert _p\) is a nonground, toplevel, firstorder subterm of \(t\sigma \) and \(safe(t_i\vert _p, s_i\vert _p)\). This implies the existence of a total, injective function from the multiset of nonground, toplevel firstorder subterms in \(s\sigma \) to the like multiset of \(t\sigma \) in turn proving \(var\_cond(t\sigma ,s\sigma )\).
From Lemma 13, it can be shown that for \(1 \le i \le m\), \(safe(t_i\sigma , s_i\sigma )\). By the subterm property of safety, this implies that \(safe(t_i\sigma \vert _p, s_i\sigma \vert _p)\).
To show that \(t_i\sigma \vert _p\) must be a nonground, toplevel, firstorder subterm in \(t\sigma \), it can be assumed that this not the case. This easily leads to a contradiction with \(safe(t_i\sigma , s_i\sigma )\).
Lemma 16
Let t be a polymorphic term and \(\sigma \) be a substitution. We define a new substitution \(\rho \) such that the domain of \(\rho \) is \(dom(\sigma )\). Define \(y\rho = \llbracket y\sigma \rrbracket \). For all terms t, \(\llbracket t\sigma \rrbracket = \llbracket t \rrbracket \rho \).
Proof
Via a straightforward induction on t.
Theorem 7 (Stability under Substitution)
If \(s >_{\mathsf {ski}}t\) then \(s\sigma >_{\mathsf {ski}}t\sigma \) for all substitutions \(\sigma \) that respect the ghd mapping.
Proof
Let \(s' = \llbracket s \rrbracket \) and \(t' = \llbracket t \rrbracket \). Let \(\rho \) be defined as per Lemma 16. First, we show that if R1 was used to derive \(s >_{\mathsf {ski}}t\) and thus \(\Vert s' \Vert > \Vert t' \Vert \) then \(\Vert s'\rho \Vert > \Vert t'\rho \Vert \) and thus \(s\sigma >_{\mathsf {ski}}t\sigma \) because \(\llbracket s\sigma \rrbracket = s'\rho \) and \(\llbracket t\sigma \rrbracket = t'\rho \).
From Lemma 15 and \(var\_cond(s',t')\), \(var\_cond(s'\rho ,t'\rho )\) holds. Furthermore, if \(\Vert s' \Vert > \Vert t' \Vert \), then by Lemma 14 \(\Vert s'\rho \Vert > \Vert t'\rho \Vert \) and \(s\sigma >_{\mathsf {ski}}t\sigma \) by an application of R1.
On the other hand, if \(\Vert s' \Vert = \Vert t' \Vert \), then R2 was used to derive \(s >_{\mathsf {ski}}t\). By Lemma 14 \(\Vert s'\rho \Vert \ge \Vert t'\rho \Vert \). If \(\Vert s'\rho \Vert > \Vert t'\rho \Vert \), then this is the same as the former case. Otherwise \(\Vert s'\rho \Vert = \Vert t'\rho \Vert \) and \(s'\rho \) and \(t\rho \) are compared using R2. From the stability under substitution of \(>_{\mathsf {hb}}\), \(s'\rho >_{\mathsf {hb}}t'\rho \) follows and \(s\sigma >_{\mathsf {ski}}t\sigma \) can be concluded.
Theorem 8 (Wellfoundedness)
There exists no infinite descending chain of comparisons \(s_1>_{\mathsf {ski}}s_2 >_{\mathsf {ski}}s_3 \cdots \).
Proof
Assume that such a chain exists. For each \(s_i >_{\mathsf {ski}}s_{i+1}\) derived by R1, we have that \(\Vert s_i \Vert > \Vert s_{i+1} \Vert \). For each \(s_i >_{\mathsf {ski}}s_{i+1}\) derived by R2, we have that \(\Vert s_i \Vert = \Vert s_{i+1} \Vert \). Therefore the number of times \(s_i >_{\mathsf {ski}}s_{i+1}\) by R1 in the infinite chain must be finite and there must exist some m such that for all \(n > m\), \(s_n >_{\mathsf {ski}}s_{n+1}\) by R2. Therefore, there exists an infinite sequence of \(>_{\mathsf {hb}}\) comparisons \(\llbracket s_m \rrbracket>_{\mathsf {hb}}\llbracket s_{m+1} \rrbracket >_{\mathsf {hb}}\llbracket s_{m+2} \rrbracket \cdots \). This contradicts the wellfoundedness of \(>_{\mathsf {hb}}\).
Theorem 9 (Coincidence with FirstOrder KBO)
Let \(>_{\mathsf {fo}}\) be the firstorder KBO as described by Becker et al. in [2]. Assume that \(>_{\mathsf {ski}}\) and \(>_{\mathsf {fo}}\) are parameterised by the same precedence \(\succ \) and that \(>_{\mathsf {fo}}\) always compares tuples using the lexicographic extension operator. Then \(>_{\mathsf {ski}}\) and \(>_{\mathsf {fo}}\) always agree on firstorder terms.
Proof
Let \(t' = \llbracket t \rrbracket \) and \(s' = \llbracket s \rrbracket \). Since s and t are firstorder, \(\Vert s' \Vert = 0\) and \(\Vert t' \Vert = 0\). Thus, \(s'\) and \(t'\) will always be compared by \(>_{\mathsf {hb}}\). Since \(>_{\mathsf {hb}}\) coincides with \(>_{\mathsf {fo}}\) on firstorder terms, so does \(>_{\mathsf {ski}}\).
5 Examples
To give a flavour of how the ordering behaves, we provide a number of examples.
Example 1
Consider the terms (ignoring type arguments) \(t = \varvec{\mathsf {S}}\, (\varvec{\mathsf {K}}\, \mathsf {a}) \, \mathsf {b} \, \mathsf {c}\) and \(s = \mathsf {f} \, \mathsf {c} \, \mathsf {e}\). From the definition of the translation \(\llbracket \rrbracket \), we have that \(\llbracket t \rrbracket = \varvec{\mathsf {S}}\, (\varvec{\mathsf {K}}\, \mathsf {a}) \, \mathsf {b} \, \mathsf {c}\) and \(\llbracket s \rrbracket = \mathsf {f} \, \mathsf {c} \, \mathsf {e}\). Since \(\Vert \varvec{\mathsf {S}}\, (\varvec{\mathsf {K}}\, \mathsf {a}) \, \mathsf {b} \, \mathsf {c} \Vert = 2\) and \(\Vert \mathsf {f} \, \mathsf {c} \, \mathsf {e} \Vert = 0\), we have that \(t >_{\mathsf {ski}}s\).
Example 2
Consider the terms \(t = \mathsf {f} \, (\mathsf {g} \, \mathsf {b}) \, \mathsf {e} \, \mathsf {d}\) and \(s = \varvec{\mathsf {I}}\, \mathsf {a}\). Here \(s >_{\mathsf {ski}}t\) despite the fact that s is syntactically smaller than t because s has a maximum reduction of 1 as opposed to 0 of t.
Example 3
Consider terms \(t = \mathsf {f} \, (\varvec{\mathsf {I}}\, \mathsf {d}) \, (\varvec{\mathsf {S}}\, x \, \mathsf {a \, b})\) and \(s = \mathsf {g} \, (\varvec{\mathsf {S}}\, x \, \mathsf {(h \, d) \, b}) \). The two terms are comparable as the variable condition relates subterm \(\varvec{\mathsf {S}}\, x \, \mathsf {(h \, d) \, b}\) in s to subterm \(\varvec{\mathsf {S}}\, x \, \mathsf {a \, b}\) in t. The unsafe combinator \(\varvec{\mathsf {S}}\) and variable x are in the same position in each subterm. As \(\Vert t \Vert > \Vert s \Vert \), \(t >_{\mathsf {ski}}s\).
Example 4
Consider terms \(t = \mathsf {f} \, (\varvec{\mathsf {I}}\, \mathsf {d}) \, (\varvec{\mathsf {S}}\, x \, \mathsf {a} \, y)\) and \(s = \mathsf {g} \, (\varvec{\mathsf {S}}\, x \, (\mathsf {h} \, y) \, \mathsf {b}) \). This is very similar to the previous example, but in this case the terms are incomparable. Let \(s'\) be a name for the subterm \((\varvec{\mathsf {S}}\, x \, (\mathsf {h} \, y) \, \mathsf {b})\) in s and \(t'\) a name for the subterm \((\varvec{\mathsf {S}}\, x \, \mathsf {a} \, y)\). The variable y occurs in different positions in \(s'\) and \(t'\). Therefore, \(s'\) cannot be related to t by the variable condition and the two terms are incomparable.
Example 5
Consider terms \(t = \mathsf {f} \, (x \, (\mathsf {g} \, (\varvec{\mathsf {K}}\, \varvec{\mathsf {I}}\, \mathsf {a} \, \mathsf {b})))\) and \(s = \mathsf {h} \, (\varvec{\mathsf {I}}\, \mathsf {a}) \, (x \, \mathsf {c})\). The variable condition holds between t and s by relating \((x \, (\mathsf {g} \, (\varvec{\mathsf {K}}\, \varvec{\mathsf {I}}\, \mathsf {a} \, \mathsf {b})))\) to \((x \, \mathsf {c})\). The combinator \(\varvec{\mathsf {I}}\) in s is not unsafe and therefore does not need to be related to a combinator in t.
Since \(\Vert t \Vert = 2 > \Vert s \Vert = 1\), \(t >_{\mathsf {ski}}s\). Intuitively, this is safe because a substitution for x in t can duplicate \((\mathsf {g} \, (\varvec{\mathsf {K}}\, \varvec{\mathsf {I}}\, \mathsf {a} \, \mathsf {b}))\) whose maximum reduction length is 2 whilst a substitution for x in s can only duplicate \(\mathsf {c}\) whose maximum reduction length is 0.
6 Conclusion and Discussion
We have presented an ordering that orients all ground instances of \(\varvec{\mathsf {S}}\), \(\varvec{\mathsf {C}}\), \(\varvec{\mathsf {B}}\), \(\varvec{\mathsf {K}}\) and \(\varvec{\mathsf {I}}\) axioms lefttoright. The ordering enjoys many other useful properties such as stability under substitution, compatibility with stable contexts, ground totality and transitivity. In as yet unpublished work, we have used this ordering to parameterise a complete superposition calculus for HOL [5]. Lack of full compatibility with context has not been an obstacle. In the standard firstorder proof of the completeness of superposition, compatibility with contexts is used in model construction to rule out the need for superposition inferences beneath variables [19]. Thus, by utilising \(>_{\mathsf {ski}}\), some superposition is required beneath variables. However, because terms with functional heads are compatible with all contexts, such inference are quite restricted.
The \(>_{\mathsf {ski}}\) ordering presented here is able to compare nonground terms that cannot be compared by any ordering used to parameterise Bentkamp et al.’s lambda superposition calculus [3]. They define terms to be \(\beta \)equivalence classes. Nonground terms are compared using a quasiorder, \(\succsim \), such that \(t \succsim s\) iff for all grounding substitutions \(\theta \), \(t\theta \succeq s\theta \). Consider terms \(t = x \, \mathsf {a} \, \mathsf {b}\) and \(s = x \, \mathsf {b} \, \mathsf {a}\) and grounding substitutions \(\theta _1 = {x \rightarrow \lambda x \> y \>. \mathsf {f} \> y \> x}\) and \(\theta _2 = {x \rightarrow \lambda x \> y \>. \mathsf {f} \> x \> y}\). By ground totality of \(\succ \) it must be the case that either \(\mathsf {f \> a \> b} \succ \mathsf {f \> b \> a}\) or \(\mathsf {f \> b \> a} \succ \mathsf {f \> a \> b}\). Without loss of generality assume the first. Then, neither \(t \succsim s\) nor \(s \succsim t\) since \(t\theta _1 = \mathsf {f \> b \> a} \prec \mathsf {f \> a \> b} = s\theta _1\) and \(t\theta _2 = \mathsf {f \> a \> b} \succ \mathsf {f \> b \> a} = s\theta _2\).
The \(>_{\mathsf {ski}}\) ordering allows weak reduction (or \(\beta \)reduction) to be treated as part of the superposition calculus. This allows terms t and \(t'\) such that \(t \longrightarrow _w^+ t'\) (or \(t \longrightarrow _\beta ^+ t'\)) to be considered separate terms resulting in terms such as t and s given above being comparable. Since \(\Vert t \Vert = \Vert s \Vert \), t and s are compared using \(>_{\mathsf {hb}}\) with stability under substitution ensured by the stability under substitution of \(>_{\mathsf {hb}}\).
Many of the definitions that have been provided here are conservative and can be tightened to allow the comparison of a far larger class of nonground terms without losing stability under substitution. We provide an example of how the definition of stable subterm could be refined in our report [6]. In further work, we hope to thoroughly explore such refinements.
Notes
Acknowledgements
Thanks to Jasmin Blanchette, Alexander Bentkamp and Petar Vukmirović for many discussions on aspects of this research. We would also like to thank reviewers of this paper, whose comments have done much to shape this paper. The first author thanks the family of James Elson for funding his research.
References
 1.Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, 2nd edn. Elsevier Science Publishers B.V., Amsterdam (1984)zbMATHGoogle Scholar
 2.Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth–Bendix order for lambdafree higherorder terms. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 432–453. Springer, Cham (2017). https://doi.org/10.1007/9783319630465_27CrossRefGoogle Scholar
 3.Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 55–73. Springer, Cham (2019). https://doi.org/10.1007/9783030294366_4CrossRefGoogle Scholar
 4.Benzmüller, C., Sultana, N., Paulson, L.C., Theiß, F.: The higherorder prover LeoII. J. Autom. Reasoning 55(4), 389–404 (2015). https://doi.org/10.1007/s108170159348yMathSciNetCrossRefzbMATHGoogle Scholar
 5.Bhayat, A., Reger, G.: A combinatorbased superposition calculus for higherorder logic. In: The 10th International Joint Conference on Automated Reasoning (IJCAR) (2020)Google Scholar
 6.Bhayat, A., Reger, G.: A KnuthBendixlike ordering for orienting combinator equations (technical report). Technical report, University of Mancester (2020). https://easychair.org/publications/preprint_open/rXSk
 7.Blanchette, J.C., Waldmann, U., Wand, D.: A lambdafree higherorder recursive path order. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 461–479. Springer, Heidelberg (2017). https://doi.org/10.1007/9783662544587_27CrossRefGoogle Scholar
 8.Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering: the end of a quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 1–14. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540875314_1CrossRefGoogle Scholar
 9.Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation with nonmonotonic orderings. In: Proceedings  Symposium on Logic in Computer Science, August 1999Google Scholar
 10.Brown, C.E.: Satallax: an automatic higherorder prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111–117. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642313653_11CrossRefGoogle Scholar
 11.Czajka, Ł., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reasoning 61(1), 423–453 (2018)MathSciNetCrossRefGoogle Scholar
 12.Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117–131. Springer, Heidelberg (1995). https://doi.org/10.1007/3540592008_52CrossRefGoogle Scholar
 13.Hindley, J.R., Seldin, J.P.: LambdaCalculus and Combinators: An Introduction, 2nd edn. Cambridge University Press, New York (2008)CrossRefGoogle Scholar
 14.Jouannaud, J.P., Rubio, A.: Polymorphic higherorder recursive path orderings. J. ACM 54(1) (2007). https://doi.org/10.1145/1206035.1206037
 15.Kerber, M.: How to prove higher order theorems in first order logic. In: IJCAI, pp. 137–142, January 1991Google Scholar
 16.Kop, C., van Raamsdonk, F.: A higherorder iterative path ordering. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 697–711. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540894391_48CrossRefGoogle Scholar
 17.Lindblad, F.: https://github.com/frelindb/agsyHOL. Accessed 25 Sept 2019
 18.Meng, J., Paulson, L.C.: Translating higherorder clauses to firstorder clauses. J. Autom. Reasoning 40(1), 35–60 (2008). https://doi.org/10.1007/s108170079085yMathSciNetCrossRefzbMATHGoogle Scholar
 19.Nieuwenhuis, R., Rubio, A.: Paramodulationbased theorem proving. In: Handbook of Automated Reasoning, vol. 1, pp. 371–443. Elsevier Press and MIT press, August 2001. https://doi.org/10.1016/B9780444508133/500096
 20.Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing, chap. 26. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 1853–1964. Elsevier Science (2001)Google Scholar
 21.Steen, A.: Extensional paramodulation for higherorder logic and its effective implementation LeoIII. Ph.D. thesis, Freie Universität Berlin (2018)Google Scholar
 22.Sultana, N., Blanchette, J.C., Paulson, L.C.: LeoII and Satallax on the Sledgehammer test bench. J. Appl. Logic 11(1), 91–102 (2013). https://doi.org/10.1016/j.jal.2012.12.002MathSciNetCrossRefzbMATHGoogle Scholar
 23.van Raamsdonk, F., Severi, P., Sørensen, M., Xi, H.: Perpetual reductions in lambda calculus. Inf. Comput. 149(2), 173–225 (1999). https://doi.org/10.1006/inco.1998.2750CrossRefzbMATHGoogle Scholar