Advertisement

A Knuth-Bendix-Like Ordering for Orienting Combinator Equations

  • Ahmed Bhayat
  • Giles RegerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12166)

Abstract

We extend the graceful higher-order basic Knuth-Bendix order (KBO) of Becker et al. to an ordering that orients combinator equations left-to-right. The resultant ordering is highly suited to parameterising the first-order superposition calculus when dealing with the theory of higher-order 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 well-founded. 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 higher-order logic. Some provers such as AgsyHOL [17], Satallax [10] and Leo-II [4] implement dedicated higher-order proof calculi. A common approach, followed by the Leo-III prover [21], is to use a co-operative architecture with a dedicated higher-order prover working in conjunction with a first-order prover. It has long been part of theorem proving folklore that sound and complete translations from higher-order to first-order logic exist. Kerber [15] proves this result for a higher-order logic that does not assume comprehension axioms (otherwise known as applicative first-order logic). Thus, translating higher-order problems to first-order logic and running first-order provers on the translations is another method of automated higher-order 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 first-order 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 first-order or nearly first-order [22]. One major reason for this is that inferences between combinator axioms can be hugely explosive. A common first-order proof calculus is superposition [19]. Consider a superposition inference from the \(\varvec{\mathsf {K}}\) axiom onto the right-hand 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 left-to-right, 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 higher-order 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 higher-order 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 higher-order 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 higher-order basic KBO \(>_{\mathsf {hb}}\) introduced by Becker et al. [2]. Our new ordering, \(>_{\mathsf {ski}}\), orients combinator equations left-to-right. 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 so-called 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 higher-order unification. There appear to be two potential benefits to using a slightly modified first-order 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 first-order superposition than lambda superposition. Unification is first-order and there is no need to deal with binders and bound variables. This allows the re-use of the well-studied data-structures and algorithms used in first-order superposition [12, 20].

  • As discussed further in the conclusion (Sect. 6), the \(>_{\mathsf {ski}}\) ordering allows the comparison of a larger class of non-ground terms than the ordering used in [3]. This results in fewer superposition inferences.

In Sect. 2, we provide the necessary preliminaries and then move on to the main contributions of this paper which are:
  • 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 non-ground terms. A useful trait for an ordering that parameterises superposition is to be able to compare a large class of non-ground terms since this reduces the number of inferences carried out. The most powerful method of defining a non-ground 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 non-computable 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

Syntax of Types and Terms: We work in a polymorphic applicative first-order logic. Let Open image in new window be a set of type variables and \(\varSigma _\mathsf {ty}\) be a set of type constructors with fixed arities. It is assumed that a binary type constructor \(\rightarrow \) is present in \(\varSigma _\mathsf {ty}\) which is written infix. The set of types is defined:
The notation \(\, \overline{t_n} \,\) is used to denote a tuple or list of types or terms depending on the context. A type declaration is of the form \(\varPi \, \overline{\alpha } \,.\sigma \) where \(\sigma \) is a type and all type variables in \(\sigma \) appear in \(\, \overline{\alpha } \,\). Let \(\varSigma \) be a set of typed function symbols and Open image in new window a set of variables with associated types. It is assumed that \(\varSigma \) contains the following function symbols, known as basic combinators:
$$ \begin{array}{ll} \varvec{\mathsf {S}}: \varPi \alpha \tau \gamma . (\alpha \rightarrow \tau \rightarrow \gamma ) \rightarrow (\alpha \rightarrow \tau ) \rightarrow \alpha \rightarrow \gamma &{} \quad \varvec{\mathsf {I}}: \varPi \alpha . \alpha \rightarrow \alpha \\ \varvec{\mathsf {C}}: \varPi \alpha \tau \gamma . (\alpha \rightarrow \tau \rightarrow \gamma ) \rightarrow \tau \rightarrow \alpha \rightarrow \gamma &{} \quad \varvec{\mathsf {K}}: \varPi \alpha \gamma . \alpha \rightarrow \gamma \rightarrow \alpha \\ \varvec{\mathsf {B}}: \varPi \alpha \tau \gamma . (\alpha \rightarrow \gamma ) \rightarrow (\tau \rightarrow \alpha ) \rightarrow \tau \rightarrow \gamma \end{array} $$
The set of terms over \(\varSigma \) and Open image in new window is defined below. In what follows, type subscripts, and at times even type arguments, are omitted.

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. Non-application 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 non-combinator 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 first-order 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 first-order 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 first-order 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 non-overlapping subterms \(u_1\) to \(u_n\). By \(u [ ]_n\), we refer to a context with n non-overlapping 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 weak-reduces 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 weak-reduces to term \(t'\) in n steps, we write \(t \longrightarrow _w^n t'\). Further, if there exists a weak-reduction path from a term t of length n, we say that \(t \in n_w\). Weak-reduction 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 Weak-Reduction Strategy

To show that the measure \(\Vert \Vert \) is computable we provide a maximal weak-reduction 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

Assume that \(\varvec{\mathcal {C_{\mathsf {any}}}}= \varvec{\mathsf {K}}\). Then any maximal reduction from \(\varvec{\mathsf {K}}\, \, \overline{t_n} \,\) is of the form: \( \varvec{\mathsf {K}}\, t_1 \, t_2 \ldots t_n \longrightarrow _w^m \varvec{\mathsf {K}}\, t_1' \, t_2' \ldots t_n' \longrightarrow _wt_1' \, t_3' \ldots t_n' \longrightarrow _w^{m'} s\) where \(\Vert s \Vert = 0\), \(t_1 \longrightarrow _w^{m_1} t_1' \, \ldots \, t_n \longrightarrow _w^{m_n} t_n'\), \(\Vert t_2 \Vert = m_2\) and \(m = m_1 + \cdots + m_n\). Thus, \(\Vert \varvec{\mathsf {K}}\, \, \overline{t_n} \, \Vert = \sum _{i = 1}^n m_i + 1 + m'\). There is another method of reducing \(\varvec{\mathsf {K}}\, \, \overline{t_n} \,\) to s:
$$\begin{aligned} \varvec{\mathsf {K}}\, t_1 \, t_2 \ldots t_n&\longrightarrow _w^{m_2}&\varvec{\mathsf {K}}\, t_1 \, t_2' \ldots t_n \qquad&\longrightarrow _w&t_1 \, t_3 \ldots t_n \\&\longrightarrow _w^{m - m_2}&t_1' \, t_3' \ldots t_n' \qquad&\longrightarrow _w^{m'}&s \end{aligned}$$
As the length of this reduction is the same as the previous reduction, it must be a maximal reduction as well. Therefore we have that: \(\Vert \varvec{\mathsf {K}}\, t_1 \, t_2 \ldots t_n \Vert = m + m' + 1 = (m - m_2 + m') + m_2 + 1 = \Vert t_1 \, t_3 \ldots t_n \Vert + \Vert t_2 \Vert + 1\)
Conversely, assume that \(\varvec{\mathcal {C_{\mathsf {any}}}}\) is not \(\varvec{\mathsf {K}}\). We prove that the formula holds if \(\varvec{\mathcal {C_{\mathsf {any}}}}= \varvec{\mathsf {S}}\). The other cases are similar. If \(\varvec{\mathcal {C_{\mathsf {any}}}}= \varvec{\mathsf {S}}\), any maximal reduction from \(\varvec{\mathsf {S}}\, \, \overline{t_n} \,\) must be of the form: \(\varvec{\mathsf {S}}\, t_1 \ldots t_n \longrightarrow _w^m \varvec{\mathsf {S}}\, t_1' \ldots t_n' \longrightarrow _wt_1' \, t_3' \, (t_2' \, t_3') \, t_4' \ldots t_n' \longrightarrow _w^{m'} s\) where \(\Vert s \Vert = 0\), \(t_1 \longrightarrow _w^{m_1} t_1' \, \ldots \, t_n \longrightarrow _w^{m_n} t_n'\) and \(m = m_1 + \cdots + m_n\). There is another method of reducing \(\varvec{\mathsf {S}}\, \, \overline{t_n} \,\) to s:
$$\begin{aligned} \varvec{\mathsf {S}}\, t_1 \ldots t_n&\longrightarrow _w&t_1 \, t_3 \, (t_2 \, t_3) \, t_4 \ldots t_n \\&\longrightarrow _w^{m + m_3}&t_1' \, t_3' \, (t_2' \, t_3') \, t_4' \ldots t_n \\&\longrightarrow _w^{m'}&s \end{aligned}$$
Thus, we have that \(\Vert \varvec{\mathsf {S}}\, \, \overline{t_n} \, \Vert = m + m' + 1 \le m + m_3 + m' + 1 = \Vert (\varvec{\mathsf {S}}\, \, \overline{t_n} \,)\! \downarrow ^w \Vert + 1\). Since \(m + m' + 1\) is the length of the maximal reduction, equality must hold.

Lemma 2

Define a map \(F_\infty \) from Open image in new window to Open image in new window as follows:

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 higher-order 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 length-lexicographic extension of the base order. This is denoted \(\gg _{\mathsf { hb}}^{\mathsf {length\_lex}}\). The length-lexicographic 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 Higher-Order Basic KBO

Standard first-order KBO first compares the weights of terms, then compares their head-symbols and finally compares arguments recursively. When working with higher-order 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)\).

Let \(\succ \) be a total well-founded ordering or precedence on \(\varSigma \). The precedence \(\succ \) is extended to arbitrary heads by defining \(\zeta \succ \xi \) iff \(\forall f \in ghd(\zeta )\) and \(\forall g \in ghd(\xi ), f \succ g\). Let Open image in new window be a function from \(\varSigma \) to \(\mathbb {N}\) that denotes the weight of a function symbol and Open image in new window a function from Open image in new window to \(\mathbb {N}\) denoting the weight of a term. Let \(\varepsilon \in \mathbb {N}_{>0}\). For all constants \(\mathsf {c}\), Open image in new window. The weight of a term is defined recursively:The graceful higher-order basic Knuth-Bendix order \(>_{\mathsf {hb}}\) is defined inductively as follows. Let \(t = \zeta \, \, \overline{t} \,\) and \(s = \xi \, \, \overline{s} \,\). Then \(t >_{\mathsf {hb}}s\) if \(vars_{\#}(s) \subseteq vars_{\#}(t)\) and any of the following are satisfied:
Z1

Open image in new window

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 left-to-right. 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 non-ground terms as mentioned in the introduction. However, the semantic lifting of the ground order is non-computable and therefore useless for practical purposes. We therefore provide two approaches to achieving an ordering that can compare non-ground 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 over-constrained 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 (Type-1 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 type-1 term.

Definition 2 (Type-2 term)

A term \(x \, \, \overline{t_n} \,\) where \(n > 0\) is a type-2 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 type-1 or type-2 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 term-ground polymorphic terms t, \(\Vert t \Vert = \Vert ( \! [ t ]\!) \Vert \).

The combinator orienting Knuth-Bendix order (approach 1) \(>_{\mathsf {ski1}}\) is defined as follows. For terms t and s, let \(t' = ( \! [ t ]\!) \) and \(s' = ( \! [ s ]\!) \). Then \(t >_{\mathsf {ski1}}s\) if \(vars_{\#}(s') \subseteq vars_{\#}(t')\) and:
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 type-2 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 top-level 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(ts) 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(ts) 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 non-ground terms t and s such that safe(ts).

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(ts) 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 \).

It is clearly the case that \((t \text { not ground }) \wedge (s \text { not ground }) \wedge safe(t, s) \;\; \implies semisafe(t, s)\). The implication does not hold in the other direction. A useful property of semisafe is that it is stable under head reduction. If for terms t and s that reduce at their heads to \(t'\) and \(s'\) respective, we have semisafe(ts), then we have \(semisafe(t', s')\).

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.

We now define the combinator orienting Knuth-Bendix order (approach 2) \(>_{\mathsf {ski}}\). For terms t and s, let \(t' = \llbracket t \rrbracket \) and \(s' = \llbracket s' \rrbracket \). Then \(t >_{\mathsf {ski}}s\) if \(var\_cond(t', s')\) and:
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 non-ground 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 ground-terms, compatible with contexts, stable under substitution and well-founded 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 first-order KBO, since without this, the calculus would not behave on first-order problems as standard first-order 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 non-ground 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 516 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_{j-1} \, 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_{i-1} \, 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'_{i-1} \, 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

Let \(\, \overline{t_n} \,\) be terms such that for \(1 \le i \le n\), \(head(t_i) \notin \{\varvec{\mathsf {I}}, \varvec{\mathsf {K}}, \varvec{\mathsf {B}}, \varvec{\mathsf {C}}, \varvec{\mathsf {S}}\}\). Then for all contexts \(u [ ]_n\), if \(u [ \, \overline{t_n} \, ]\) \(\longrightarrow _wu'\) then either:
  1. 1.

    \(\exists i. u' = u [ t_1, \ldots , \hat{t_i}, \ldots , t_n ] \) where \(t_i \longrightarrow _w\hat{t_i}\) or

     
  2. 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

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. Then:
  1. 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. 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_{i-1}, 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_{i-1}, 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_{i-1}, t, t_{i+1} \ldots t_n \Vert \). If \(\zeta \) is not a combinator, then \(\Vert u' \langle \! \langle \zeta \, t_1 \ldots t_{i-1}, s, t_{i+1} \ldots \) \(t_n \rangle \! \rangle \Vert > \Vert u' \langle \! \langle \zeta \) \(\, t_1 \ldots t_{i-1}, 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_{i-1}, s, t_{i+1}\) \(\ldots t_n \rangle \! \rangle \Vert > \Vert u' \langle \! \langle \zeta \, t_1 \ldots \) \( t_{i-1}, 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.

We next prove stability under substitution. In order to prove this, it needs to be shown that for untyped terms s and t and all substitutions \(\sigma \):
  1. 1.

    \(var\_cond(s,t)\) implies \(var\_cond(s\sigma , t\sigma )\).

     
  2. 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 1113 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(ts) 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 non-ground terms such that \(\Vert t \Vert \ge \Vert s \Vert + m\) for some \(m \in \mathbb {N}\) and safe(ts). 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(ts) and Lemma 13 can be invoked to prove the lemma. Therefore, assume that both have non-variable, non-fully 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 non-ground, top-level, first-order 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 non-ground, top-level, first-order 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 non-ground and \(safe(t_i, s_i)\), we have \(semisafe(t_i, s_i)\) and can therefore invoke Lemma 12.

Let \(m' = \Vert u \langle \! \langle \rangle \! \rangle \Vert - \Vert u' \langle \! \langle \rangle \! \rangle \Vert \). Note that \(m'\) could be negative. By Lemma 11, \(\Vert t \Vert = \Vert u \langle \! \langle \rangle \! \rangle \Vert + \sum _{i=1}^{m} \Vert t_i \Vert \) and \(\Vert s \Vert = \Vert u' \langle \! \langle \rangle \! \rangle \Vert + \sum _{i=1}^{m} \Vert s_i \Vert \). Thus, \(\Vert t \Vert = \Vert s \Vert + m' + \sum _{i=1}^{m} m_i\). Therefore, \(m' + \sum _{i=1}^{m} m_i \ge n\). Lemma 13 can be used to show that for all i, \(\Vert t_i\sigma \Vert \ge \Vert s_i\sigma \Vert + m_i\). Because \(u' \langle \! \langle \rangle \! \rangle \) is ground, it follows \(\Vert u\sigma \langle \! \langle \rangle \! \rangle \Vert -\Vert u'\sigma \langle \! \langle \rangle \! \rangle \Vert \ge m'\). To conclude the proof:

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 non-ground, top-level, first-order 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 non-ground, top-level, first-order 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 non-ground 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 non-ground, top-level, first-order 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 non-ground, top-level, first-order 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 non-ground, top-level first-order 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 non-ground, top-level, first-order 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 (Well-foundedness)

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 well-foundedness of \(>_{\mathsf {hb}}\).

Theorem 9 (Coincidence with First-Order KBO)

Let \(>_{\mathsf {fo}}\) be the first-order 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 first-order terms.

Proof

Let \(t' = \llbracket t \rrbracket \) and \(s' = \llbracket s \rrbracket \). Since s and t are first-order, \(\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 first-order 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 left-to-right. 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 first-order 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 non-ground 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. Non-ground 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 non-ground 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. 1.
    Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, 2nd edn. Elsevier Science Publishers B.V., Amsterdam (1984)zbMATHGoogle Scholar
  2. 2.
    Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth–Bendix order for lambda-free higher-order terms. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 432–453. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63046-5_27CrossRefGoogle Scholar
  3. 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/978-3-030-29436-6_4CrossRefGoogle Scholar
  4. 4.
    Benzmüller, C., Sultana, N., Paulson, L.C., Theiß, F.: The higher-order prover Leo-II. J. Autom. Reasoning 55(4), 389–404 (2015).  https://doi.org/10.1007/s10817-015-9348-yMathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: The 10th International Joint Conference on Automated Reasoning (IJCAR) (2020)Google Scholar
  6. 6.
    Bhayat, A., Reger, G.: A Knuth-Bendix-like ordering for orienting combinator equations (technical report). Technical report, University of Mancester (2020). https://easychair.org/publications/preprint_open/rXSk
  7. 7.
    Blanchette, J.C., Waldmann, U., Wand, D.: A lambda-free higher-order 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/978-3-662-54458-7_27CrossRefGoogle Scholar
  8. 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/978-3-540-87531-4_1CrossRefGoogle Scholar
  9. 9.
    Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation with non-monotonic orderings. In: Proceedings - Symposium on Logic in Computer Science, August 1999Google Scholar
  10. 10.
    Brown, C.E.: Satallax: an automatic higher-order 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/978-3-642-31365-3_11CrossRefGoogle Scholar
  11. 11.
    Czajka, Ł., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reasoning 61(1), 423–453 (2018)MathSciNetCrossRefGoogle Scholar
  12. 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/3-540-59200-8_52CrossRefGoogle Scholar
  13. 13.
    Hindley, J.R., Seldin, J.P.: Lambda-Calculus and Combinators: An Introduction, 2nd edn. Cambridge University Press, New York (2008)CrossRefGoogle Scholar
  14. 14.
    Jouannaud, J.P., Rubio, A.: Polymorphic higher-order recursive path orderings. J. ACM 54(1) (2007).  https://doi.org/10.1145/1206035.1206037
  15. 15.
    Kerber, M.: How to prove higher order theorems in first order logic. In: IJCAI, pp. 137–142, January 1991Google Scholar
  16. 16.
    Kop, C., van Raamsdonk, F.: A higher-order 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/978-3-540-89439-1_48CrossRefGoogle Scholar
  17. 17.
    Lindblad, F.: https://github.com/frelindb/agsyHOL. Accessed 25 Sept 2019
  18. 18.
    Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008).  https://doi.org/10.1007/s10817-007-9085-yMathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, vol. 1, pp. 371–443. Elsevier Press and MIT press, August 2001.  https://doi.org/10.1016/B978-044450813-3/50009-6
  20. 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. 21.
    Steen, A.: Extensional paramodulation for higher-order logic and its effective implementation Leo-III. Ph.D. thesis, Freie Universität Berlin (2018)Google Scholar
  22. 22.
    Sultana, N., Blanchette, J.C., Paulson, L.C.: Leo-II 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. 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

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.University of ManchesterManchesterUK

Personalised recommendations