%% %% \documentclass{article} \usepackage{IJFCS} % \documentstyle[IJFCS]{article} \usepackage{latexsym} \usepackage{amssymb} \usepackage{amsmath} \usepackage{url} \renewcommand{\today}{\number\day\ \ifcase\month\or January\or February\or March\or April\or May\or June\or July\or August\or September\or October\or November\or December\fi \ \number\year} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Preamble \newcommand{\SN}{\textit{SN}} \newcommand{\SNo}{{SN}^\circ} % needs math mode \newcommand{\SNSig}{\textit{SN}^\Sigma} \newcommand{\ISN}{\textit{ISN}} \newcommand{\btl}{\blacktriangleleft} \newcommand{\btr}{\blacktriangleright} \newcommand{\vtl}{\vartriangleleft} \newcommand{\vtr}{\vartriangleright} \newcommand{\vtlo}{\vartriangleleft^\circ} \newcommand{\vtro}{\vartriangleright^\circ} \newcommand{\vtluo}{\vtl \cup \vtlo} \newcommand{\gindy}{\textit{gindy}} \newcommand{\indy}{\textit{indy}} \newcommand{\gbars}{\textit{gbars}} \newcommand{\bars}{\textit{bars}} \newcommand{\wfp}{\textit{wfp}} \newcommand{\wruvo}{\wfp\ (\rho\ \cup \vtlo)} \newcommand{\subt}{\textit{subt}} \newcommand{\isubt}{\textit{isubt}} \newcommand{\psubt}{\textit{psubt}} \newcommand{\gpo}{\textit{gpo}} \newcommand{\lpo}{\textit{lpo}} \newcommand{\lex}{\textit{lex}} \newcommand{\fwf}{\textit{fwf}} \newcommand{\tyof}{\textit{tyof}} \newcommand{\ctxt}{\textit{ctxt}} \newcommand{\pctxt}{\textit{pctxt}} \newcommand{\ictxt}{\textit{ictxt}} \newcommand{\constrict}{\textit{constrict}} \newcommand{\cons}{\textit{cons}} \newcommand{\nil}{\textit{nil}} \newcommand{\nat}{\textit{nat}} \newcommand{\Zero}{\textit{Zero}} \newcommand{\Succ}{\textit{Succ}} %\newcommand\comment[1]{} % \pagestyle{myheadings} \renewcommand\theenumi{(\alph{enumi})} \renewcommand\labelenumi{\theenumi} \renewcommand\theenumii{(\roman{enumii})} \renewcommand\labelenumii{\theenumii} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 \newtheorem{condition}{Condition} \newtheorem{property}{Property} \newcommand\qed{\hfill$\Box$} % \pagestyle{plain} % IJFCS stuff \newcommand\hvcite[1]{[\refcite{#1}]} \begin{document} %% print out the publisher copyright heading \copyrightheading %% use symbolic footnote \symbolfootnote %% use normal text like skip (13pt) \textlineskip \begin{center} %% print out titles in IJFCS format \fcstitle{TERMINATION OF ABSTRACT REDUCTION SYSTEMS} \vspace{24pt} {\authorfont JEREMY E DAWSON} \vspace{2pt} %% use smaller line skip here \smalllineskip {\addressfont Logic and Computation Program, NICTA, Locked Bag 8001, Canberra ACT 2601, AUSTRALIA, RSISE (Bldg 115) Australian National University Canberra ACT 0200 AUSTRALIA } \vspace{10pt} and \vspace{10pt} {\authorfont RAJEEV GOR\'E} \vspace{2pt} \smalllineskip {\addressfont RSISE (Bldg 115) Australian National University Canberra ACT 0200 AUSTRALIA } \vspace{20pt} %% authors need not care about this \publisher{(received date)}{(revised date)}{Editor's name} \end{center} \alphfootnote \date{\today} \begin{abstract} We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL. \\ \keywords{rewriting, termination, well-founded ordering, strong normalisation} \end{abstract} \textlineskip \section{Introduction} \label{s-id} We address the general problem of termination of rewriting which can be informally posed as follows. Assume that we have a fixed set of ``objects'' defined in some way. Suppose we are given a binary relation $\rho$ on these objects, where $(t, s) \in \rho$ expresses that object $s$ may be transformed into object $t$. Let us call such a transformation a \emph{reduction}. Consider repeatedly reducing an object in any way possible. We are interested to know whether such repeated reduction necesarily terminates -- formally, whether or not there is an infinite sequence $t = t_0, t_1, \ldots$, where each $(t_{i+1}, t_i) \in \rho$. If there is not, we say that $t$ is strongly normalising: $t \in \SN$. The difficulty of the problem arises from the totally general notion of ``reduction''. In the common special case of a term rewriting system (TRS), an object is a term of some first-order language, and the reduction relation is described by a set of ``rewrite rules'' $l_i \to r_i$, where $l_i$ and $r_i$ are terms containing variables for which terms may be substituted. Here, rewriting is also usually \emph{monotonic} \cite{bfr}, or \emph{closed under context} \cite{hm-dpr}, in that if $C[\_]$, a term with a ``hole'', is the context, and $l$ reduces to $r$, then $C[l]$ reduces to $C[r]$. Several general methods capturing termination of such term rewriting systems exist \cite{dps00,nat-term,dggt}. For a detailed survey see \cite{dersh-har}. A discussion of methods for proving termination, including structural induction on terms, is found in \cite{jgl}. Term rewriting systems with specific rewriting strategies such as innermost, outermost (see, eg, \cite{fissore-gnaedig-kirchner-termination}, \cite{gnaedig-kirchner-properties}, and works cited therein) also are cases of this general problem. Jean Goubault-Larrecq \cite{jgl} has proved termination results for an abstract reduction system (ARS) where objects need not have a term structure and so there is no monotonicity assumption or subterm relation. Whereas proofs for TRSs involve the subterm relation, his proofs use an arbitrary well-founded relation $\vtl$ instead. His Theorem~1, call it JGL1, is the result of ``chasing generalizations and simplifications'' of earlier work and ``subsumes \ldots most path-orderings of the literature''. We first proved our Theorem~\ref{thm-csl} as \cite[Theorem~2]{dggt}. While Theorem~\ref{thm-csl} and JGL1 use remarkably similar ideas, neither JGL1 (even if restricted to TRSs) nor our Theorem~\ref{thm-csl} subsumed the other. Our new more general theorem subsumes both. We first present this more general theorem and its proof in \S\ref{s-tt}. In \S\ref{s-appl-ars}, we show that it generalises JGL1, % \cite[Theorem~1]{jgl}. and in \S\ref{s-gpo} we show directly how it implies the termination of the general path ordering of Dershowitz \& Hoot \cite{nat-term}. In \S\ref{s-snst}, we show how to use our new theorem to obtain two different proofs of strong normalisation for well-typed combinator terms. % and how our proof method can be adapted to show strong % normalisation for the simply-typed $\lambda$-calculus. In these cases, although the objects have a term structure, our proofs use the ARS setting and show the well-foundedness of larger, non-monotonic, relations. The combinator case suggests that our theorem properly generalises JGL1. Thus, our theorem handles most path-orderings in the literature and the reducibility method typically used for typed combinators. % But, for the simply-typed $\lambda$-calculus, % it requires modifications to reason indirectly about substitutions. % % We then show that the implication is proper by showing how our % theorem can be used to prove the termination of reduction of % well-typed combinator terms, % something which cannot be done using \cite{jgl} directly. % % Goubault-Larrecq's Theorem~2 is even more general than his Theorem~1, % extending the higher-order path ordering of % Jouannaud \& Rubio \cite{jr-horpo}. % In the longer version of this paper \cite{dgtars} we show how to % adapt and extend our proof to prove this result. % % and adapt our theorem to show strong % normalisation for the simply-typed $\lambda$-calculus. % We also use our techniques to give a different proof % of Goubault-Larrecq's much more complicated Theorem~2 \cite{jgl}. % His theorem generalises \cite[Theorem~1]{jgl}, handles the reducibility % argument, and encompasses explicit reasoning about substitutions % for handling the simply-typed $\lambda$-calculus. % In \S\ref{s-appl-rewr} we show how the main theorem implies a similar result for TRSs \cite[Theorem~2]{dggt}, and relate that result to work on constricting derivations. We consider applications of the theorem for TRSs, showing how it gives well-known results for the Knuth-Bendix Ordering, and results relating to dependency pairs. By an analogue of \S\ref{s-gpo} (see \cite[\S 3.7]{dggt}), the termination of the recursive path ordering \cite[Defn~4.22, 4.24]{dersh-har} follows. We also apply our theorem to numerous specific examples. Commonly, a rewrite system is defined by taking a base system, known to be terminating, and adding new function symbols and rules to it. In \S\ref{s-inc} we show how our theorem can be used to prove termination in certain such cases, for example, where the new symbols and rules are those of the examples in \S 3.3 to \S 3.5 of \cite{dggt}. A more complex variant of the result covers the example in \cite[\S 3.6]{dggt}. We then derive a path-ordering result in this context of incrementally defined systems. The history of our work is this. In \cite{dawson-gore-machine-checked-strong-normalisation} we described a proof of strong normalisation for a cut-elimination procedure in display logic. Since the procedure involved repeated transformation (or ``rewriting'') of a derivation tree, we realised that if we described a derivation tree as a term in a first-order language, we would get a proof of termination of a particular rewriting system. Finding the crucial properties of this rewriting system gave us \cite[Theorem~2]{dggt}. Tracing the similarities and differences between this result and JGL1 %, Goubault-Larrecq's \cite[Theorem~1]{jgl}, led us to our main result, Theorem~\ref{thm-allsn}. Our proofs were machine-checked in Isabelle/HOL: \cite{jdisa}, directories {\tt snabs,snlc}. % \comment{following replaced % We address the general problem of termination of rewriting % which can be informally posed as follows. % Assume that we have a fixed set of ``objects'' % defined according to some formal syntax. % Suppose we have a binary relation $\rho$ on these objects, % where $(t, s) \in \rho$ % expresses that object $s$ may be transformed into object $t$. % Let us call such a transformation a \emph{reduction}. % Consider repeatedly reducing an object in any way possible. % We are interested to know whether such repeated reduction necesarily % terminates -- formally, whether or not there is an infinite sequence % $t = t_0, t_1, \ldots$, where each $(t_{i+1}, t_i) \in \rho$. % If there is not, we say that $t$ is strongly normalising, $t \in \SN$. % The difficulty of the problem arises from the totally general notion % of ``reduction'', and there are several specialisations of this notion. % There are many different techniques in the literature for proving % termination of rewriting, but few general theorems which unify these % different proofs. % In the common special case of a term rewriting system (TRS), % an object is a term of some first-order language, and the % reduction relation is described by giving a set of ``rewrite rules'' % $l_i \to r_i$, where $l_i$ and $r_i$ are terms containing % (meta-)variables for which terms may be substituted. % Rewriting is also usually \emph{monotonic} \cite{bfr}, % or \emph{closed under context} \cite{hm-dpr}, % in that where $C[\_]$ is a context (a term with a ``hole''), % and $l$ reduces to $r$, then $C[l]$ reduces to $C[r]$. % % Such a relation is commonly called a \emph{reduction}, such as % % the ``$\beta$-reduction'' of the lambda calculus. % For example, if the ``objects'' are the terms of the simply-typed % $\lambda$-calculus, and the ``reductions'' are the usual % $\beta$- and $\eta$-reductions, % then the monotonicity assumption is valid and our question becomes the problem % of the strong normalisation of the simply-typed $\lambda$-calculus. % There are several quite general theorems about termination of rewriting in this % common special case where rewriting can be performed at any ``sub-object'': % that is, where the reduction relation % is assumed to be ``closed under contexts'' or monotonic. % More recently, various authors have investigated the problem of termination % of rewriting when this assumption does not hold. % The most common example is that of an abstruct reduction system (ARS) % where objects need not have a term structure. % Jean Goubault-Larrecq \cite{jgl} has proved termination results % which apply to the more general setting of an ARS. % He replaces the notion of subterm with an arbitrary well-founded relation. % His Theorem~1 is the result of % ``chasing generalizations and simplifications'' of earlier work % and ``subsumes \ldots most path-orderings of the literature'' (\cite{jgl}). % In \cite[Theorem~2]{dggt} we proved a theorem about the well-foundedness of % a monotonic relation on first-order terms, which applies to % the termination of systems of rewrite rules in a term rewriting system (TRS). % Our theorem has some similarity to Theorem~1 of \cite{jgl}, % but neither subsumes the other. % Motivated by his paper, % we reformulated our previous theorem and its proof, % in the setting of an ARS, % incorporating generalisations suggested by his work. % The result of this was to produce a theorem which subsumes % both our previous theorem and his Theorem~1. % We first present our generalised theorem. % We then give various applications of it to the % well-foundedness of abstract reduction relations on sets of objects % which need not have a term structure. % We show directly how our result implies the % termination of the general path ordering of Dershowitz \& Hoot % \cite{nat-term}, and relate our result to work on constricting derivations. % Goubault-Larrecq's Theorem~2 is even more general than his Theorem~1, % extending the higher-order path ordering of Jouannaud \& Rubio \cite{jr-horpo}. % In Section~\ref{jgl-ho} we show how to % adapt and extend our proof to prove this result. % Finally, we show how our theorem can be used to prove the termination % of reduction of well-typed combinator terms, % and how our proof method can be adapted to show % the strong normalisation of the simply-typed $\lambda$-calculus. % In these cases, although the objects have a term structure, % our proofs use the ARS setting in that they % show the well-foundedness of larger, non-monotonic, relations. % end of replaced part } \subsection{Notation, Terminology, Definitions and Basic Lemmas}\label{s-ntd} Assume we are given a set $\mathcal{U}$: in a TRS this would be the set of terms, but in the ARS setting we just call them ``objects''. For an irreflexive binary relation $\rho$, we write $(r, t) \in \rho$, $(r, t) \in\ <_\rho$, $r <_\rho t$ or $t >_\rho r$ interchangeably. We prefer $>_\rho$ over the more traditional $\to_\rho$ because the latter is typically used in TRSs, our setting is more abstract than TRSs, and when we deal with TRSs we need to carefully distinguish between a relation and its closure under contexts. For a symbol that suggests a direction such as $<$, $\vtl$, $\prec$, $\precsim$ or $\ll$ we will write $(r, t) \in\ \vtl$, $(t, r) \in\ \vtr$, $r \vtl t$ or $t \vtr r$ interchangeably. We say $r$ is \emph{strongly normalising}, or is $\in \SN$, (with respect to $\rho$) if there is no infinite descending sequence $r = r_0 >_\rho r_1 >_\rho r_2 >_\rho \ldots$ of objects, and $\rho$ is \emph{well-founded} (or \emph{Noetherian}) if every $r \in \SN$. We write $\leq_\rho$ or $\rho^=$, $<_\rho^+$ or $\rho^+$, and $<_\rho^*$ or $\rho^*$ for the reflexive closure, the transitive closure and the reflexive transitive closure, respectively, of $<_\rho$. We write $\sigma \circ \rho$ for relational composition: that is, $(r, s) \in \sigma \circ \rho$ if there exists $t$ such that $(r, t) \in \rho$ and $(t, s) \in \sigma$. In our formal treatment in Isabelle/HOL we used the following inductive definition (also used in the Isabelle libraries) for the set \SN\ of strongly normalising objects, and we proved, in the HOL logic, which is classical and contains the Axiom of Choice, that this definition is equivalent to the standard definition given above. \begin{definition}[Strongly Normalising -- HOL] \label{defn:SN} For a reduction relation $\rho$, the set \SN\ of strongly normalising objects is the (unique) smallest set of objects such that: if every object $t$ to which $s$ reduces is in \SN\ then $s \in \SN$. \end{definition} Our previous work \cite{dggt} on term rewriting was on the well-foundedness of the closure under context of a relation $\rho$. In contrast, we deal here with an abstract reduction system, usually calling the reduction relation $\rho$. So concepts like ``strongly normalising'', ``reduction'', etc, relate to $\rho$, and not, even when discussing structured terms, to the closure of $\rho$ under context. For structured terms, $\rho$ may be the closure under contexts of another relation $\sigma$, which may itself be the set of substitution instances of a set $R$ of rewriting rules. In the ARS setting, we use an arbitrary relation where we used the immediate subterm relation in the TRS setting. In \cite[\S 2.2]{dggt} we defined the set \ISN\ of ``inductively strongly normalising'' terms as the set of terms that are in \SN\ if their immediate subterms are in \SN. This is same idea as $\underline \SN$ of \cite{jgl}. Clearly, $\SN \subseteq \ISN$. We now define \gindy\ as a generalised notion of ``inductively'' for an arbitrary relation $\sigma$ in place of the immediate subterm relation, which we call \isubt. The concept ``\gindy'' enables us to express the principle of well-founded induction succinctly as: if every object is in $\gindy\ \sigma\ S$, and $\sigma$ is well-founded, then every object is in $S$. \begin{definition}[\gindy] \label{def-gindy} For a relation $\sigma$ and set $S$, an object $t \in \gindy\ \sigma\ S$ iff: \\ if $\forall u.\ (u, t) \in \sigma \Rightarrow u \in S$, then $t \in S$. \end{definition} The notion of well-foundedness is generalised to that of a particular object being \emph{accessible}, or in the \emph{well-founded part}, of a binary relation: the constructive definition is that $s$ is in the \emph{well-founded part} of a relation $<$ if there is no infinite downward chain ~$\ldots < s_2 < s_1 < s$~ starting from $s$. This is generalised to the notion that $s$ \emph{bars} $S$ in $<$ if every infinite downward chain, starting from $s$, contains a member of $S$. See \cite{jgl} for a detailed discussion of this. We now generalise \bars\ to a function \gbars\ where the members of a downward chain, until it meets $S$, must be in some set $Q$. The inductive definition of \gbars\ is: \begin{definition}[\gbars] \label{def-gbars-isa} For sets of objects $Q$ and $S$, and relation $\sigma$, $\gbars\ \sigma\ Q\ S$ is the (unique) smallest set such that: \begin{romanlist} \item \label{gbars-inI} $S \subseteq \gbars\ \sigma\ Q\ S$ \item \label{gbars-gbarsI} if $t \in Q$ and $\forall u.\ (u, t) \in \sigma \Rightarrow u \in \gbars\ \sigma\ Q\ S$, then $t \in \gbars\ \sigma\ Q\ S$. \end{romanlist} \end{definition} The next lemma gives another characterisation of \gbars\ which is provably equivalent in classical logic using the Axiom of Choice: $t \in \gbars\ \sigma\ Q\ S$ iff every downward $\sigma$-chain starting from $t$ is within $Q$ until it hits $S$ or it terminates. \begin{lemma}[\gbars -alternative] \label{def-gbars} For sets of objects $Q$ and $S$, and relation $\sigma$, object $t \in \gbars\ \sigma\ Q\ S$ iff: for every downward $\sigma$-chain $t = t_0 >_\sigma t_1 >_\sigma t_2 >_\sigma \ldots$, either the chain is finite and all $t_i \in Q$, or for some member $t_n$ of the chain, both $t_n \in S$ and $\{t_0, t_1, t_2, \ldots, t_{n-1}\} \subseteq Q$. \end{lemma} Definition \ref{def-wfp,bars} records how \gbars\ generalises the notions of ``$S$ \emph{bars} $s$ in $\sigma$'' and of ``$s$ is \emph{accessible} in $\sigma$, or $s$ is in the \emph{well-founded part} of $\sigma$'' as defined in \cite{jgl}. \begin{definition}[\wfp, \bars] \label{def-wfp,bars} ~ \begin{romanlist} \item \label{def-bars} $s \in \bars\ \sigma\ S$ iff $s \in \gbars\ \sigma\ \mathcal{U}\ S$ \hfill (``$S$ \emph{bars} $s$ in $\sigma$'') \item $s \in \wfp\ \sigma$ iff $s \in \bars\ \sigma\ \emptyset$ \hfill (``$s$ \emph{accessible} in $\sigma$ ''). \end{romanlist} \end{definition} Thus $\SN = \wfp\ \rho$ and $\ISN = \gindy\ \isubt\ \SN$. Lemma~\ref{def-gbars} gives the following characterisation of \bars, which was given in \cite{jgl}: $s \in \bars\ \sigma\ S$ if every infinite decreasing $\sigma$-sequence \mbox{$s_0 >_\sigma s_1 >_\sigma s_2 >_\sigma \ldots$ meets $S$}, ie, for some $k$, $s_k \in S$. The \gbars-induction principle is analogous to the principles of well-founded induction, and of Brouwer's \bars-induction (see \cite[Proposition~1]{jgl}). Like Lemma~\ref{def-gbars}, it follows easily from the inductive definition of \gbars\ in Isabelle's Higher Order Logic. In fact it is generated automatically by the Isabelle theorem prover from the inductive definition of \gbars\ above. However in weaker logics these do not necessarily hold: see \cite[Ch~1, \S 6]{kv} or \cite[Ch~3]{dummett} for discussions of this topic. We write $\mathcal P\ s$ to mean that $s$ satisfies property $\mathcal P$. \begin{proposition}[\gbars-induction]\label{gbars-ind} For sets $Q$ and $S$, and any property $\mathcal P$, if \begin{romanlist} \item \label{gi-in} for every $s \in S$, we have $\mathcal P\ s$, and \item \label{gi-rec} for every $s \in Q$, if $\forall t.\ (t, s) \in \sigma \Rightarrow \mathcal P\ t$, then $\mathcal P\ s$ \end{romanlist} then every $s \in \gbars\ \sigma\ Q\ S$ satisfies $\mathcal P$. \end{proposition} \begin{lemma}\label{gindy-gbars} ~ % to align parts \begin{romanlist} \item \label{2a}$S = \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S $ \item \label{2b}$Q \subseteq \gindy\ \sigma\ (\gbars\ \sigma\ Q\ S) $ \end{romanlist} \end{lemma} {\bf Proof.} \begin{romanlist} \item $\subseteq$: this is trivial, from Definition~\ref{def-gbars-isa}\ref{gbars-inI}, by letting $Q$ be $\gindy\ \sigma\ S$. $\supseteq$: Let $\mathcal P\ s = s \in S$. We use Proposition~\ref{gbars-ind} with $Q = \gindy\ \sigma\ S$. Condition~\ref{gi-in} of Proposition~\ref{gbars-ind} holds trivially, and condition~\ref{gi-rec} is given by Definition~\ref{def-gindy}. \item Follows directly from Definitions \ref{def-gindy} and \ref{def-gbars-isa}\ref{gbars-gbarsI}. \hfill$\Box$ \end{romanlist} \begin{lemma}\label{l2} ~ % to align parts \begin{romanlist} \item \label{gindy-bars} if all objects are in $\gindy\ \sigma\ S$, then $\bars\ \sigma\ S = S$, whence, if $\sigma$ is well-founded, then every object is in $S$, and \item \label{bars-wfp} $\bars\ \sigma\ (\wfp\ \sigma) = \wfp\ \sigma$ \end{romanlist} \end{lemma} {\bf Proof.} \begin{romanlist} \item As $\mathcal U = \gindy\ \sigma\ S$, this follows from Lemma~\ref{gindy-gbars}\ref{2a} and Definition~\ref{def-wfp,bars}\ref{def-bars}. If $\sigma$ is well-founded, then $\mathcal U = \wfp\ \sigma = \bars\ \sigma\ \emptyset \subseteq \bars\ \sigma\ S$. \item By Lemma~\ref{gindy-gbars}\ref{2b}, $\mathcal U \subseteq \gindy\ \sigma\ (\gbars\ \sigma\ \mathcal U\ \emptyset)$, that is (by Definition~\ref{def-wfp,bars}) every object is in $ \gindy\ \sigma\ (\wfp\ \sigma)$. The result now follows from part (i). \hfill$\Box$ \end{romanlist} \section{The Termination Theorem} \label{s-tt} Given a reduction relation $\rho$, our general termination result utilises two relations $\vtl$ and $\ll$, which, together with $\rho$, must satisfy a number of properties given below. These relations play a role similar to the relations $\vtl$ and $\ll$ in \cite{jgl}, and, where convenient, we express our conditions so as to enable easy comparisons with \cite{jgl}. Most commonly, the relation $\vtl$ is instantiated to the immediate subterm relation, and $\ll$ is often some sort of approximation to the rewrite relation itself. The most general version of the properties that $\vtl$ and $\ll$ must satisfy is Condition~\ref{conds-defs}\ref{rpc0} below, but in practice we often use the simpler and stronger conditions \ref{rpc} to \ref{rpc2}. (Even weaker conditions than \ref{conds-defs}\ref{rpc0} are possible, since we could for example suppose that $s$ also satisfies $\forall {u} \ll {s}.\ u \in \gindy \vtl \SN$: see the proof of Lemma~\ref{dth} below). \begin{condition}\label{conds-defs} ~ % to align parts \begin{romanlist} \item \label{rpc0} If $\forall s' \vtl s.\ s' \in \SN$, then $s \in \bars\ \rho\ (\gbars \vtl \{u\:|\ u \ll s\}\ \SN)$ \item \label{rpc} For all $(t, s) \in \rho$, if $\forall s' \vtl s.\ s' \in \SN$, then $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$ \item \label{rpca} For all $(t, s) \in \rho$, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \{v\:|\ (v, s) \in (\vtl \circ\ \rho)\}$ \item \label{rpc1} $\vtl$ is well-founded and, for all $(t, s) \in \rho$, if $\forall s' \vtl s.\ s' \in \SN$, then, \\ for all $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$ \item \label{rpc2} $\vtl$ is well-founded and, for all $(t, s) \in \rho$ and all $t' \vtl^* t$,\\ either $(t', s) \in (\vtl \circ\ \rho^*)$ or $t' \ll s$. \end{romanlist} \end{condition} \begin{lemma} \label{conds-lemma} Each of Conditions~\ref{conds-defs}\ref{rpc} to \ref{rpc2} implies Condition~\ref{conds-defs}\ref{rpc0} for all $s$. \end{lemma} \proof{ Clearly, for any set $X$, $\forall (t, s) \in \rho.\ t \in X$ implies $s \in \bars\ \rho\ X$. Thus it follows that Condition~\ref{conds-defs}\ref{rpc} implies that Condition~\ref{conds-defs}\ref{rpc0} holds for all $s$. To show that Condition~\ref{conds-defs}\ref{rpc1} implies Condition~\ref{conds-defs}\ref{rpc}, assume \ref{rpc1} holds. Then, as $\vtl$ is well-founded, there is no infinite descending $\vtl$-chain. Any descending $\vtl$-chain from $t$ is contained in \mbox{$\{t'\:|\ t' \ll s\} \cup \SN$}. A fortiori, members of such a chain are contained in $\{t'\:|\ t' \ll s\}$ until the chain reaches a member of \SN. That is, \mbox{$t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$}, and so \ref{rpc} holds. To show that Condition~\ref{conds-defs}\ref{rpc2} implies Condition~\ref{conds-defs}\ref{rpc1}, and likewise, that Condition~\ref{conds-defs}\ref{rpca} implies Condition~\ref{conds-defs}\ref{rpc}, assume that $\forall s' \vtl s.\ s' \in \SN$. Then, if $(t', s) \in (\vtl \circ\ \rho^*)$ because $t' <_\rho^* s' \vtl s$, then we have $s' \in \SN$ and so $t' \in \SN$. Note that in Condition~\ref{conds-defs}\ref{rpca} we could have $(\vtl \circ\ \rho^*)$ in place of $(\vtl \circ\ \rho)$. } Our key lemma is Lemma~\ref{dth}. We thank an unnamed referee for pointing out that our proof resembles the proof by Buchholz \cite{buchholz-pta} of the well-foundedness of the lexicographic path ordering, although it was obtained independently. \begin{lemma} \label{dth} If object $s$ satisfies Condition~\ref{conds-defs}\ref{rpc0}, then \mbox{$s \in \gindy \ll (\gindy \vtl \SN)$}. \end{lemma} \proof{ Given $s$, assume that $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0} and that (a) $\forall {u} \ll {s}.\ u \in \gindy \vtl \SN$. \noindent We then need to show $s \in \gindy \vtl \SN$, so we assume (b) $\forall {s'} \vtl {s}.\ s' \in \SN$ \noindent and we show that $s \in \SN$. By Lemma~\ref{l2}\ref{bars-wfp}, it suffices to show $s \in \bars\ \rho\ \SN$. The antecedent of Condition~\ref{conds-defs}\ref{rpc0} holds by assumption (b), and so \\ {$s \in \bars\ \rho\ (\gbars \vtl \{u\:|\ u \ll s\}\ \SN)$}. As \bars\ is monotonic in its second argument, it is enough to show $\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq \SN$. As $\{u\:|\ u \ll s\} \subseteq \gindy \vtl \SN$ by assumption (a), and as \gbars\ is monotonic in its second argument, \\ $\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq \gbars \vtl (\gindy \vtl \SN)\ \SN$. By Lemma~\ref{gindy-gbars}\ref{2a}, \\ $\gbars \vtl (\gindy \vtl \SN)\ \SN = \SN$. So we have $s \in \SN$. Thus, discharging assumptions (b) and then (a), we have $s \in \gindy \vtl \SN$, and then $s \in \gindy \ll (\gindy \vtl \SN)$. } We now identify the conditions % we need to deduce, from Lemma~\ref{dth}, that guarantee that every object is in \SN. \begin{theorem} \label{thm-allsn} Suppose that $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0} for all $s$ and \begin{romanlist} \item \label{ubg} every object is in $\bars \ll (\gindy \vtl \SN)$, and \item \label{vbs} every object is in $\bars \vtl \SN$. \end{romanlist} Then $\rho$ is well-founded. \end{theorem} \proof{ As $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, every $s \in \gindy \ll (\gindy \vtl \SN)$ by Lemma~\ref{dth}. Then, for any $u$, if $u \in \bars \ll (\gindy \vtl \SN)$ then Lemma~\ref{l2}\ref{gindy-bars} gives $u \in \gindy \vtl \SN$. Thus every $u \in \gindy \vtl \SN$. Then, for any $v$, if $v \in \bars \vtl \SN$ then Lemma~\ref{l2}\ref{gindy-bars} gives $v \in \SN$. Thus every $v \in \SN$: that is, $\rho$ is well-founded. } If Condition~\ref{conds-defs}\ref{rpc} holds, then it also holds if we augment $\rho$ to contain $\vtl$. Thus, for fixed $\vtl$, Theorem~\ref{thm-allsn} does \emph{not} provide a universal method of proving termination because it is possible that $\rho$ is well-founded but $\rho\ \cup \vtl$ is not. However, if $\rho$ is well-founded and we can choose $\vtl$ so that $\vtl\ \subseteq \rho$, then Theorem~\ref{thm-allsn} can be applied trivially. Let $\ll\ = \ \vtl\ = \rho^+$, which is well-founded. Then even Condition~\ref{conds-defs}\ref{rpc2} applies. Clearly also, conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn} apply as $\ll$ and $\vtl$ are well-founded. That is, Theorem~\ref{thm-allsn} is, trivially, a universal result for proving termination (as are several other orderings in the literature). Most commonly the conditions of Theorem~\ref{thm-allsn} will be satisfied by choosing $\ll$ and $\vtl$ to be well-founded relations. At this point we mention a lemma which we will use several times, for proving that a relation is well-founded. \begin{lemma} \label{wf-rs} Assume that $\phi$ and $\psi$ are well-founded relations. Then each of the following conditions is sufficient for $\phi \cup \psi$ to be well-founded: \begin{alphlist} \item \label{tco} $\phi \circ \psi \ \subseteq\ \psi^* \circ \phi$ \item \label{otc} $\phi \circ \psi \ \subseteq\ \psi \circ \phi^*$ \item \label{runs} $\phi \circ \psi \ \subseteq\ \phi \cup \psi$ \item \label{dvk} $\phi \circ \psi \ \subseteq\ (\psi \circ (\phi \cup \psi)^*) \cup \phi$. \end{alphlist} \end{lemma} Of these, the last is from Doornbos \& von Karger \cite{dvk}, and is implied by each of the others, which are in earlier results discussed and cited in \cite{dvk}. \section{Applications to Abstract Rewrite Systems} \label{s-appl-ars} \subsection{Generalising Goubault-Larrecq's General Theorem for ARSs} \label{s-jgl1} We show that JGL1, ie, Goubault-Larrecq's \cite[Theorem~1]{jgl}, which itself generalizes many results in the literature, is a special case of our Theorem~\ref{thm-allsn}. Note that \cite{jgl} uses $<$ where we use $\rho$, uses $T$ where we use $\mathcal U$ and uses $\underline{SN}$ where we use $\gindy\ \vtl\ \SN$. We reproduce JGL1, using our notation. \begin{property} \label{jgl-p1} For every $s, t \in \mathcal U$, if $s >_\rho t$ then either: \begin{romanlist} \item[(i)] for some $u \in \mathcal U$, $s \vtr u$ and $u \geq_\rho t$, or \item[(ii)] $s \gg t$ and for every $u \vtl t$, $s >_\rho u$ \end{romanlist} \end{property} \begin{theorem}[JGL1: \cite{jgl}, Theorem~1] \label{JGL1} Assume that Property~\ref{jgl-p1} holds, and \begin{romanlist} \item[(iii)] $\vtr$ is well-founded on $\mathcal U$, and \item[(iv)] for every $s \in \mathcal U$, if every $u \vtl s$ is in \SN, then $\gindy\ \vtl\ \SN$ bars $s$ in $\gg$. \end{romanlist} Then $>_\rho$ is well-founded on $\mathcal U$. \end{theorem} We first require two lemmas. \begin{lemma} \label{lemma-P2} Given set $S$ and object $s$, suppose that for all $t$, if $(t, s) \in \rho$, then \begin{romanlist} \item \label{P2a} $t \in S$, or \item \label{P2b} $s \gg t$ and, for every $u \vtl t$, either $(u, s) \in \rho$ or $u \in S$. \end{romanlist} Assume $\vtl$ is well-founded. Then $(t, s) \in \rho$ implies $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. \end{lemma} {\bf Proof.} Let $(t, s) \in \rho$. We prove this result for $t$ by well-founded induction on $\vtl$, so assume that, for all $v \vtl t$, if $(v, s) \in \rho$ then $v \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. We consider the two cases \ref{P2a} and \ref{P2b} as above. \begin{itemlist} \item First, if $t \in S$, then $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$ by Definition~\ref{def-gbars-isa}\ref{gbars-inI}. \item Second, if \ref{P2b} holds, we show that $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$ using Definition~\ref{def-gbars-isa}\ref{gbars-gbarsI}. We have $t \ll s$, and for any $u \vtl t$, there are two cases. \begin{itemlist} \item If $(u, s) \in \rho$ then by the inductive hypothesis, $u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. \item If $u \in S$ then \mbox{$u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$} by Definition~\ref{def-gbars-isa}\ref{gbars-inI}. \hfill $\Box$ \end{itemlist} \end{itemlist} \begin{lemma} \label{lemma-P1} Suppose that Property~\ref{jgl-p1} holds, and that $\vtl$ is well-founded. Then Condition~\ref{conds-defs}\ref{rpc} holds. \end{lemma} \proof{ We use Lemma~\ref{lemma-P2} with $S = $ \mbox{$\{v\:|\ \exists x.\ s \vtr x \mbox{ and } x \geq_\rho v\}$}. To show Condition~\ref{conds-defs}\ref{rpc}, let $(t, s) \in \rho$, and suppose that $\forall s' \vtl s.\ s' \in \SN$. By Lemma~\ref{lemma-P2}, $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. We show $S \subseteq \SN$. Let $v \in S$, say $s \vtr x $ and $ x \geq_\rho v$. Then $x \in \SN = \wfp\ \rho$ and so $v \in \SN$. Thus, by the obvious monotonicity of \gbars, $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$, as required for Condition~\ref{conds-defs}\ref{rpc}. } {\bf Proof of Theorem~\ref{JGL1} (JGL1)} Condition ({iv}) of Theorem~\ref{JGL1} is just condition \ref{ubg} of our Theorem~\ref{thm-allsn}, for if some $u \vtl s \not\in SN$, then trivially $s \in \gindy \vtl \SN$. Thus the requirement that ``{if every $u \vtl s$ is in SN}'' in (iv) of the statement of JGL1 is redundant, although its counterpart is needed in the statement of \cite[Theorem~2]{jgl}. As $\vtl$ is well-founded, for any object $v$ and set $S$ of objects, \mbox{$v \in \bars \vtl S$}, and so condition \ref{vbs} of our Theorem~\ref{thm-allsn} follows. Finally, Lemma~\ref{lemma-P1} shows that, as $\vtl$ is well-founded, Property~1 implies Condition~\ref{conds-defs}\ref{rpc}, whence Condition~\ref{conds-defs}\ref{rpc0} holds. Thus all the conditions of our Theorem~\ref{thm-allsn} hold, so $\rho$ is well-founded. \hfill$\Box$ We now explore the extent to which, conversely, JGL1 implies our Theorem~\ref{thm-allsn}. % We discuss in detail only whether our Conditions % \ref{conds-defs}\ref{rpc0} to \ref{rpc2} imply Property~1 of \cite{jgl}. % First we note a sort of converse to Lemma~\ref{lemma-P2}: % if $(t, s) \in \rho \Leftrightarrow t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$ % then, by the definition of \gbars, % \ref{P2a} or \ref{P2b} of Lemma~\ref{lemma-P2} hold, % even after deleting ``\emph{or} $u \in S$'' from \ref{P2b}. Suppose both $\vtl$ and $\ll$ are well-founded, and that Condition~\ref{conds-defs}\ref{rpca} holds: that is, with \mbox{$S = \{v\:|\ (v, s) \in (\vtl \circ\ \rho)\}$}, we have $(t, s) \in \rho \Rightarrow$ \mbox{$t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$}. Since \gbars\ is monotonic in its third argument and $S$ is monotonic in $\rho$, we can enlarge $\rho$ to get equivalence, so that $(t, s) \in \rho \iff $ \mbox{$t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$} ; then it can be seen that (i) and (ii) of Property~\ref{jgl-p1} hold. That is, JGL1 can be used to prove a weaker version of our Theorem~1 in which Condition~\ref{conds-defs}\ref{rpca}, rather than Condition~\ref{conds-defs}\ref{rpc0}, is assumed, and it is assumed that $\vtl$ and $\ll$ are well-founded. On the other hand, in Sections \ref{s-tc} and \ref{s-tc2}, the proofs of termination use our Theorem~\ref{thm-allsn}, and, in particular, use Condition~\ref{conds-defs}\ref{rpc}. The difference between Condition~\ref{conds-defs}\ref{rpc} and Condition~\ref{conds-defs}\ref{rpca} is crucial to these proofs, which suggests that JGL1 is a special case of our Theorem~\ref{thm-allsn}. \subsection{Application to the General Path Ordering} \label{s-gpo} The definition of the general path ordering of Dershowitz \& Hoot \cite{nat-term} presupposes terms in a first-order language, but the ordering is not necessarily monotonic. Therefore we deal with it in the context of an ARS. As noted by Goubault-Larrecq \cite{jgl}, JGL1 can be used to show that the general path ordering is well-founded. We now show how that ordering fits our Condition~\ref{conds-defs} for termination of an ARS presented earlier. The following treatment is similar to that of the recursive path orderings in our \cite[\S3.7]{dggt}, but that applied only to the cases where the derived ordering is monotonic (ie, closed under context). The general path ordering $<_{gpo}$ is defined as below where $s = f(s_1, \ldots, s_m)$ and $t = g(t_1, \ldots, t_n)$, and $\Lambda({<_{gpo}})$ (or $<_{\Lambda}$) is an ordering derived from $<_{gpo}$, where $\Lambda$ satisfies conditions given later. We omit defining $<_{gpo}$-equivalent terms. $$ \frac { s_i \geq_{gpo} t } { s >_{gpo} t } (G1) \qquad \frac { s >_\Lambda t \qquad \forall i \in \{1, \ldots, n\}.\ s >_{gpo} t_i } { s >_{gpo} t } (G2) $$ In practice, $<_{\Lambda}$, which is derived from $<_{gpo}$, depends on $<_{gpo}$ applied only to smaller terms, ie, determining whether $s >_\Lambda t$ depends on whether $s'>_{gpo} x$ only for proper subterms $s'$ of $s$ (and arbitrary terms $x$). Thus the above rules can be seen as mutually recursive definitions of $<_{gpo}$ and $<_{\Lambda}$. However in the formal Isabelle proof a different approach was taken to ensure a consistent definition: $<_{gpo}$ is an inductively defined set, which means that $s >_{gpo} t$ if and only if it can be shown so using the rules above. This approach requires that $<_{\Lambda}$ be a monotonic function of $<_{gpo}$. As in \cite{dggt}, we define an auxiliary function \fwf\ for ``from well-founded'' which maps a binary relation $\sigma$ to a binary relation $\fwf\ \sigma$ as below: \begin{definition} Given a relation $\sigma$, $(t, s) \in \fwf\ \sigma$ iff $(t, s) \in \sigma$ and $s \in \wfp\ \sigma$. \end{definition} Clearly $\fwf\ \rho$ is well-founded, regardless of whether $\rho$ is. We can let $\vtl$ be either the immediate subterm relation or the proper subterm relation --- in the latter case, the required condition~\ref{gpo-lam-psubt} below is weaker. We now list the conditions on $\Lambda$ required for the Isabelle proof: \begin{alphlist} \item \label{gpo-lam-mono} ${\Lambda}$ is a monotonic function \item \label{gpo-lam-wf} if $\sigma$ is well-founded then ${\Lambda (\sigma)}$ is well-founded \item \label{gpo-lam-psubt} if all $s' \vtl s$ are in $\wfp\ \sigma$ and if $(t, s) \in \Lambda (\sigma)$, then $(t, s) \in \Lambda (\fwf\ \sigma)$. \end{alphlist} In practice, condition \ref{gpo-lam-psubt} means that $\Lambda (\sigma)$ depends on $\sigma$ only as follows: whether $(t, s) \in \Lambda (\sigma)$ depends solely upon whether $(x, s') \in \sigma$ for $s' \vtl s$, and arbitrary $x$, although $\Lambda (\sigma)$ can also depend on, for example, a well-founded ordering on the function symbols $\{f, g, \ldots\}$. \begin{lemma} \label{lem-subt-gpo} If $s >_{gpo} t$ and $t'$ is a subterm of $t$ then $s >_{gpo} t'$. \end{lemma} {\bf Proof.} It is enough to show that if $s >_{gpo} t = g(t_1, \ldots, t_n)$ then $s >_{gpo} t_j$ for any $j \in \{1, \ldots, n\}$. We show it by induction on the size of $s$. \begin{itemlist} \item If $s >_{gpo} t$ via rule ($G2$), then it is immediate that $s >_{gpo} t_j$. \item If $s = f (s_1, \ldots, s_m) >_{gpo} t$ via rule ($G1$), then for some $s_i$, $s_i \geq_{gpo} t$. \begin{itemlist} \item If $s_i >_{gpo} t$ then $s_i >_{gpo} t_j$ by induction. \item % If $s_i = t$ then $s_i >_{gpo} t_j$ by rule ($G1$). If $s_i = t$ then, as rule ($G1$) gives $t >_{gpo} t_j$, so $s_i >_{gpo} t_j$. \end{itemlist} In either of these cases, $s >_{gpo} t_j$ by rule ($G1$). \hfill $\Box$ \end{itemlist} \begin{theorem} The general path ordering $<_{gpo}$ is well-founded. \end{theorem} \proof{ Define $\ll\ = \Lambda (\fwf\, (<_{gpo}))$. Then, as \fwf ($<_{gpo}$) is well-founded, $\ll$ is well-founded by condition \ref{gpo-lam-wf} above. As $\vtl$ is well-founded, conditions \ref{ubg} and \ref{vbs} of our Theorem~\ref{thm-allsn} are satisfied. Then, to show Condition~\ref{conds-defs}\ref{rpc1}, suppose for all $s' \vtl s$ that \mbox{$s' \in \SN = \wfp\, (<_{gpo})$}, $t <_{gpo} s$, and $t'$ is a subterm of $t$. Then Lemma~\ref{lem-subt-gpo} gives $t' <_{gpo} s$. If $t' <_{gpo} s$ by rule ($G1$), then $s_i \vtl s$ and $t' <_{gpo}^* s_i$, so $s_i$ and $t'$ are in \SN. If $t' <_{gpo} s$ by rule ($G2$), then $(t', s) \in \Lambda (<_{gpo})$. By condition \ref{gpo-lam-psubt}, $(t', s) \in \Lambda (\fwf\, (<_{gpo})) =\ \ll$. Thus Condition~\ref{conds-defs}\ref{rpc1} is satisfied, and so $<_{gpo}$ is well-founded. } An appropriate choice of $\Lambda$ can give us either the lexicographic or multiset path orderings for structured terms \cite[Defn~4.22, 4.24]{dersh-har}. To do so we let $f (s_1, \ldots, s_m) >_\Lambda g(t_1, \ldots, t_n)$ iff either $f > g$ (according to a given well-founded ordering on function symbols) or $(s_1, \ldots, s_m) > (t_1, \ldots, t_n)$ in the derived lexicographic or multiset ordering derived from $>_{gpo}$. Such a $\Lambda$ satisfies properties \ref{gpo-lam-mono} to \ref{gpo-lam-psubt} above. These examples of $\Lambda$ also have the property that: \begin{alphlist} \item[] if $(s'_i, s_i) \in \sigma$ then $(f (s_1, \ldots, s'_i, \ldots, s_n), f (s_1, \ldots, s_i, \ldots, s_n)) \in {\Lambda (\sigma)}$ \end{alphlist} which ensures that ${\Lambda (\sigma)}$ is closed under context, but is not needed for this more general treatment. \newpage \section{Application to Typed Combinators} \label{s-snst} % Proofs of the strong normalisation of $\beta$-reduction in typed % $\lambda$-calculi tend to be complex, relying on several inductions % as in \cite{gallier-oncr,david-nr}. % although there are also short but specialised proofs, as in \cite{david-nr}. In \cite{jgl} Goubault-Larrecq concludes that ``Theorem~1 seems to be insufficient to show that every simply-typed $\lambda$-term terminates''. He therefore takes notions like ``reducibility'' and ``the substitution of terms for variables'' from the classical strong normalisation proof of the simply-typed $\lambda$-calculus \cite{glt} and generalises them to obtain his Theorem~2 for termination of higher-order path orderings. % \comment{ % The extra complexity of Goubault-Larrecq's Theorem~2 \cite{jgl} % is for higher-order path orderings, % and, as he describes, uses notions like % ``reducibility'' and ``the substitution of terms for variables'' % taken from the classical strong normalisation proof % of the simply-typed $\lambda$-calculus \cite{glt}. % He also says ``Theorem~1 seems to be insufficient to show that every % simply-typed $\lambda$-term terminates''. % } As the $\lambda$-calculus can be imitated by using the combinators $S,K,I$ a related problem is to prove the strong normalisation for well-typed combinator terms. This result follows easily from the strong normalisation of $\beta$-reduction. But to prove the converse, that strong normalisation of $\beta$-reduction follows from that of well-typed combinator terms, is not so easy: one needs a translation from $\lambda$-terms to combinator terms that preserves reducibility, such as of Akama \cite{akama-trans}. We now describe two ways to use our Theorem~\ref{thm-allsn} to prove strong normalisation of well-typed combinator terms. These proofs resemble classic ``reducibility'' arguments, but do not handle substitution of terms for variables. By Akama \cite[Theorem~2.2]{akama-trans}, this is enough to show strong normalisation of $\beta$-reduction. Thus, the full power of the much more complex \cite[Theorem~2]{jgl} is not necessary for these tasks. However, we have been unable to prove termination of typed combinators using our \cite[Theorem~2]{dggt} as suggested by a referee. Also, although we could prove strong normalisation of the simply-typed $\lambda$-calculus by adapting the proof of our Theorem~\ref{thm-allsn}, we could not prove it as a corollary of our Theorem~\ref{thm-allsn}. In the examples of this section, we use some of the concepts and notation applicable to term rewriting systems (\S\ref{s-appl-rewr}). In particular, we define $\ctxt\ \sigma$ to be the ``closure under contexts'' of $\sigma$: that is, where $C[\_]$ is a context, and $(t, s) \in \sigma$, then $(C[t], C[s]) \in \ctxt\ \sigma$. Likewise we define \pctxt\ (``\emph{proper} context''): for $(t, s) \in \sigma$, if $t$ and $s$ are \emph{proper} subterms of $C[t]$ and $C[s]$, then $(C[t], C[s]) \in \pctxt\ \sigma$. \subsection{Reduction of Typed Combinator Expressions}\label{s-tc} Of the usual combinators, the problematic ones are \emph{S f g x = f x (g x)} and \emph{W f x = f x x}, since their right-hand-sides duplicate $x$. Thus, in the untyped setting, these do not satisfy strong normalisation: for example, $(S I I) (S I I) \longrightarrow^+ (S I I) (S I I)$, $(W I) (W I) \longrightarrow^+ (W I) (W I)$, and $W W W \longrightarrow W W W$. In the typed setting, we can use our Theorem~\ref{thm-allsn} to prove strong normalisation for combinators like $S, I,K,B,C,W$, but we must actually add extra rules to do so. Note that some rules are only applied to the whole term, whereas others can also be applied to any subterm. We use $\alpha, \beta, \gamma, \ldots$ for types, and the notation $<$ on types for the transitive relation given by: $\alpha < (\alpha \to \beta)$ and $\beta < (\alpha \to \beta)$. Let $\tyof\ t$ denote the type of $t$, and let $t <_{ty} s$ mean $\tyof\ t < \tyof\ s$. $\ $ We show in detail how to handle only the $S$ combinator, but many other combinators like $I,K,B,C,W$ can be dealt with similarly, and the proof holds for the single system containing all these combinators. We define the relations $\sigma$ and $\tau$ (as inductively defined sets) by rules, as shown below for the combinator $S$. Then let $\rho = \ctxt\ \sigma\ \cup\ \tau$. Note that the extra rules (\ref{Sfg}), (\ref{Sf}) and (\ref{S}) are added only because the proof uses them: for clearly, if $\rho \supseteq \rho'$, and $\rho$ terminates, then so does $\rho'$. These rules are motivated by the relation $\vtlo$ of \cite[\S 5]{jgl}: \begin{align} \label{Sfgx} S f g x & >_\sigma f x (g x) & \\[-0.5ex] \label{Sfg} S f g & >_\tau f x (g x) & & \mbox{if } x \in \SN \\[-0.5ex] \label{Sf} S f & >_\tau f x (g x) & & \mbox{if } g,x \in \SN \\[-0.5ex] \label{S} S & >_\tau f x (g x) & & \mbox{if } f,g,x \in \SN \end{align} with types $S : (\alpha \!\to\! \beta \!\to\! \gamma) \!\to\! (\alpha \!\to\! \beta) \!\to\! \alpha \!\to\! \gamma$, $f : \alpha \!\to\! \beta \!\to\! \gamma$, $g : \alpha \!\to\! \beta$, $x : \alpha$. Note that ``\SN'' means with respect to $\rho$: that is, $\SN = \wfp\ \rho$. Thus $\tau$ and $\rho$ (but \emph{not} $\sigma$) are being defined, indirectly, in terms of themselves. However the rule (\ref{Sfgx}) preserves the type of a term: so, when it is applied to a subterm, the whole term remains well-typed. The rules for $\tau$ change a well-typed term into a well-typed term of $<$-smaller type. Further, where a rule for reducing a term $s$ depends on another term $s'$ being in $SN$, then $s' <_{ty} s$. For example, in rule (\ref{Sf}), we have $S f : (\alpha \!\to\! \beta) \!\to\! \alpha \!\to\! \gamma$, where $g$ and $x$ have $<$-smaller types, $g : \alpha \!\to\! \beta$ and $x : \gamma$. That is, for $s : \alpha$, the set $\{t\:|\ (t, s) \in \rho\}$ depends on $\sigma$ and on $\{t\:|\ (t, s) \in \tau\}$, which depends on \mbox{$\{s' \in \SN \ |\ \tyof\ s' < \alpha\}$}. For given \mbox{$\beta < \alpha$}, the set $\{s' \in \SN \ |\ s' : \beta\}$ depends on \mbox{$\{(x, s'') \in \rho \ |\ \tyof\ s' \leq \beta\}$}. This ensures a consistent definition, as for $\vtlo$ in \cite{jgl}. In effect, whether \mbox{$(t, s) \in \rho$}, $(t, s) \in \tau$ and $u \in \SN$ are defined inductively on the types of $s$ and of $u$. We say $t <_{sn1} s$ if $(t, s) \in \ctxt\ \sigma$ via a reduction in an immediate subterm which is itself in $\wfp\, (\ctxt\ \sigma)$: that is, where $t$ and $s$ differ only in corresponding immediate subterms $t'$ and $s'$ with $(t', s') \in \ctxt\ \sigma$ and $s' \in \wfp\ (\ctxt\ \sigma)$. (Note that the immediate subterms of $f\ x\ y$ are $f\ x$ and $y$). \begin{lemma} \label{tc-c1} Let $\ll\ =\ <_{ty} \cup <_{sn1}$, and let $\vtl$ be the immediate subterm relation. Then Condition~\ref{conds-defs}\ref{rpc} holds. \end{lemma} \proof{ Let $(t, s) \in \rho$ and assume $\forall s' \vtl s.\ s' \in \SN$. If $(t, s) \in \rho$ via rule (\ref{Sfg}) (where $s = S f g$), we have $g \in \SN$, so $(t, S f) \in \rho$ by rule (\ref{Sf}). As $S f \vtl s$, we have $S f \in \SN$, so $t \in \SN \subseteq \gbars \vtl \{u\:|\ u \ll s\}\ \SN$. Similar arguments hold where $(t, s) \in \sigma \subseteq \rho$ by rule (\ref{Sfgx}), and where $(t, s) \in \tau \subseteq \rho$ via rule (\ref{Sf}). If $(t, s) \in \tau \subseteq \rho$ via rule (\ref{S}), then we see that the subterms $f,g$ and $x$ of $t$ are in \SN, while the subterms $f x : \beta \to \gamma$, $g x : \beta$ and $t = f x (g x) : \gamma$ are of $<$-smaller type than $S$. Thus any $\vtl$-descending chain from $t$ consists of terms in $\{u\:|\ u \ll s\}$ until reaching a term in \SN. That is, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$. Finally, in the case where $(t, s) \in \pctxt\ \sigma$, we have $t' \vtl t$ and $s' \vtl s$ such that \mbox{$(t', s') \in \ctxt\ \sigma$}. Since $s' \in \SN \subseteq \wfp\, (\ctxt\ \sigma)$, we have $t <_{sn1} s$ and $t \ll s$. Now consider any $t'' \vtl t$. Either $t'' = t'$ and $(t', s') \in \ctxt\ \sigma$ as just discussed, in which case $s' \in \SN$ and so $t' \in \SN$, or $t''$ is an immediate subterm of $s$ not affected by the reduction from $s$ to $t$, whence $t'' \in \SN$. Therefore $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$. } \begin{theorem} \label{tc-sn} Every term is strongly normalising. \end{theorem} \proof{ We use our Theorem~\ref{thm-allsn}, and Lemmas \ref{conds-lemma} and \ref{dth}. Apart from Lemma~\ref{tc-c1}, we need conditions \ref{ubg} and \ref{vbs} of our Theorem~\ref{thm-allsn}. Condition~\ref{vbs} holds as $\vtl$ is well-founded. Finally, to show condition~\ref{ubg}, we show that $\ll$ is well-founded. Clearly the ``smaller type'' relation $<$ is well-founded, and it is easy to show (analogously to Theorem~\ref{thm-sn12wf}) that $<_{sn1}$ is well-founded. Then, clearly, $<_{ty} \circ <_{sn1}\ \subseteq\ <_{ty}$, and so, by Lemma~\ref{wf-rs}\ref{tco}, $<_{ty} \cup <_{sn1}$ is well-founded. } Our rules (\ref{Sfg}), (\ref{Sf}) and (\ref{S}) were suggested by the definition of $\vtlo$ given just below Remark~13 in \cite{jgl} (where $\lambda x.\ M \vtro M [x := N]$ for $N$ strongly normalising). As in \cite{jgl}, therefore, there is a resemblance between our proof and the classic reducibility argument: for example, for $S\ f\ g$ to be in \SN, it is necessary that for all $x \in \SN$, $S\ f \ g\ x\in \SN$, which resembles the condition for reducibility in \cite[\S 6.1]{glt}. Likewise, reducibility and our \SN\ are both defined by induction on the type. \subsection{A Second Proof for Typed Combinator Expressions}\label{s-tc2} We now present another way of using our Theorem~\ref{thm-allsn} to prove the same result. This proof was suggested by a presentation of the classic reducibility argument given us by an unnamed referee. It is of independent interest since, unlike the proof in \S\ref{s-tc}, it uses a relation $\vtl$ which is distinct from the usual immediate subterm relation. We define $\vtl$ and the reduction relation $\rho$. Again, it is understood that terms are well-typed. Combinators other than $S$ could be included also. % \begin{gather} \label{onearg} N_i \vtl M N_1 \ldots N_i \ldots N_n \quad \mbox{ for } 1 \leq i \leq n \\ \label{aa} M >_\rho M N \quad\mbox{if $N \in \SN$} \\ \label{Sfgxy} S f g x y_1 \ldots y_n >_\sigma f x (g x) y_1 \ldots y_n \\ \sigma \subseteq \rho \\ \label{inarg} (x'_i, x_i) \in \ctxt\ \sigma \Rightarrow f x_1 \ldots x_i \ldots x_n >_\rho f x_1 \ldots x'_i \ldots x_n \end{gather} Note that rules (\ref{Sfgxy}) to (\ref{inarg}) together give \mbox{$\ctxt\ \sigma \subseteq \rho$}. These definitions are sound as before, since again, a reduction preserves type or gives a result of $<$-smaller type, and reduction from $s$ is defined involving \SN\ terms of $<$-smaller type. Note that, by rule (\ref{aa}), if $M,N \in SN$ then $M N \in \SN$. For this proof we define $f x_1 \ldots x_i \ldots x_n >_{sn1} f x_1 \ldots x'_i \ldots x_n$ where $(x'_i, x_i) \in \ctxt\ \sigma$ % (similar to rule (\ref{inarg})) and \mbox{$x_i \in \wfp\, (\ctxt\ \sigma)$}. That is, as before, $t <_{sn1} s$ if $(t, s) \in \ctxt\ \sigma$ by means of reduction in a ``$\vtl$-subterm'' which is itself in $\wfp\, (\ctxt\ \sigma)$. Also as before, let $\ll\ =\ <_{ty} \cup <_{sn1}$. \begin{theorem} \label{tc2-sn} Every term is strongly normalising. \end{theorem} \proof{ We first show that Condition~\ref{conds-defs}\ref{rpc} holds. Let $(t, s) \in \rho$ and assume that $\forall u \ll s$.\ $u \in \gindy \vtl \SN$, and $\forall v \vtl s$.\ $v \in \SN$. If $(t, s) \in \rho$ via rule (\ref{Sfgxy}), we have $f,g,x$ and each $y_i \in \SN$, so the combination $f x (g x) y_1 \ldots y_n \in \SN$. If $(t, s) = (M N, M) \in \rho$ via rule (\ref{aa}), then $t <_{ty} s$, so $t \ll s$, and, for $K \vtl M N$, either $K = N$ which is in \SN, or $K \vtl M$ and so $K \in \SN$. Finally, where $(t, s) \in \rho$ via rule (\ref{inarg}), the argument is similar to that before: $t <_{sn1} s$, and for $y \vtl t$, there is $x \vtl s$ such that $y \leq_\rho x$, so $y \in \SN$. That is, in each case, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$, so Condition~\ref{conds-defs}\ref{rpc} holds. From Condition~\ref{conds-defs}\ref{rpc}, we prove that every term is in \SN\ as in Theorem~\ref{tc-sn}. } \subsection{Strong Normalization for System $T$} \label{s-sysT} We can also develop the previous proofs to handle the strong normalization of System $T$, though in each case there is a complication. System $T$ \cite{altenkirch-Tait} consists of the system of typed combinators as above, with a distinguished type \nat, the usual two constructors for this type, $\Zero : \nat$ and $\Succ : \nat \to \nat$, and the general recursive function $R$ defined by $$R\ \Zero\ f\ z = z \qquad\qquad R\ (\Succ\ n)\ f\ z = f\ n\ (R\ n\ f\ z)$$ So to extend the first proof to this situation we add the rules \begin{align} \label{RZ} R\ \Zero\ f\ z & >_\sigma z \\[-0.5ex] \label{RSfz} R\ (\Succ\ n)\ f\ z & >_\sigma f\ n\ (R\ n\ f\ z) \\[-0.5ex] \label{RSf} R\ (\Succ\ n)\ f & >_\tau f\ n\ (R\ n\ f\ z) & & \mbox{if } z \in \SN \\[-0.5ex] \label{RS} R\ (\Succ\ n) & >_\tau f\ n\ (R\ n\ f\ z) & & \mbox{if } f, z \in \SN \\[-0.5ex] \label{Succ} \Succ\ n & >_\tau n \end{align} We now prove Lemma~\ref{tc-c1} for this extended system. % using the same $\vtl$ and $\ll$. \begin{lemma} \label{tc-c1T} Consider the system of \S\ref{s-tc}, extended by rules (\ref{RZ}) to (\ref{Succ}). Let $\ll$ be $<_{ty} \cup <_{sn1}$, and $\vtl$ the immediate subterm relation. Then Condition~\ref{conds-defs}\ref{rpc} holds. \end{lemma} \proof{ Let $(t, s) \in \rho$ and assume $\forall s' \vtl s.\ s' \in \SN$. If $(t, s) \in \rho$ via rule (\ref{RZ}) then $t = z \vtl s$, so $t \in \SN$. If $(t, s) \in \rho$ via rule (\ref{RSfz}) or rule (\ref{RSf}) the argument is as for rules (\ref{Sfgx}) to (\ref{Sf}). If $(t, s) \in \rho$ via rule (\ref{RS}) then first note that as $\Succ\ n \in \SN$, and $\Succ\ n >_\tau n$ by rule (\ref{Succ}), so $n \in \SN$. We now need to consider any $\vtl$-descending chain from $t = f\ n\ (R\ n\ f\ z)$, and consider the subterms $t'$ on such a chain. Since $s = R\ (\Succ\ n)$ is of type $(\nat \to \alpha \to \alpha) \to \alpha \to \alpha)$, we see that $t : \alpha$ and its subterms $f\ n : \alpha \to \alpha$, $R\ n\ f\ z : \alpha$ and $R\ n\ f : \alpha \to \alpha$ are of $<$-smaller type than $S$. Also $R\ n <_{sn1} R\ (\Succ\ n)$, since $R\ n$ is obtained by reducing the strongly normalizing subterm $(\Succ\ n)$. So for all these subterms $t'$, we have $t' \ll s$. Finally, we have that $f,z,n$ and $R$ are in \SN. Thus any $\vtl$-descending chain from $t$ consists of terms in $\{u\:|\ u \ll s\}$ until meeting a term in \SN; that is, $t \in \gbars \vtl \{u\:|\ u \ll s\}\ \SN$. } Finally, every term is strongly normalising, proved exactly as in Theorem~\ref{tc-sn}. \subsection{Adapting the second proof to System $T$} \label{s-sysT2} We now show how to adapt the proof of \S\ref{s-tc2} to System $T$. We add the following rules to those given earlier, ie, to rules (\ref{aa}) to (\ref{inarg}): \begin{align} \label{RZy} R\ \Zero\ f\ z\ y_1 \ldots y_k & >_\sigma z\ y_1 \ldots y_k \\[-0.5ex] \label{RSfzy} R\ (\Succ\ n)\ f\ z\ y_1 \ldots y_k & >_\sigma f\ n\ (R\ n\ f\ z)\ y_1 \ldots y_k \\[-0.5ex] \label{Succ2} \Succ\ n & >_\tau n \end{align} We define $\vtl$ as before, ie, by rule (\ref{onearg}), but we need a different definition of $\ll$, as follows where $<_{sn1}$ is defined as in \S\ref{s-tc2}, $f\ \overline{x'}$ means $f x_1 \ldots x'_i \ldots x_m$, $f\ \overline{x}$ means $f x_1 \ldots x_i \ldots x_m$, $f\ \overline{x}\ \overline{y}$ means $f\ \overline{x}\ y_1 \ldots y_k$, and applications are well-typed. \begin{align} \label{llarg} M N & \ll M \\ \label{sn1arg} f\ \overline{x'} & \ll f\ \overline{x}\ \overline{y} & \mbox{where } f\ \overline{x'} & <_{sn1} f\ \overline{x} \end{align} \begin{lemma} $\ll$ is well-founded. \end{lemma} \proof{ We use Lemma~\ref{wf-rs}\ref{dvk}, with $\phi$ and $\psi$ being the relations given by (\ref{llarg}) and (\ref{sn1arg}) respectively. Then we have the following cases for $u >_\phi v >_\psi w$: \begin{itemlist} \item $f\ \overline{x} >_\phi f\ \overline{x}\ y >_\psi f\ \overline{x}\ y'$, when $u >_\phi w$ \item $f\ \overline{x} >_\phi f\ \overline{x}\ y >_\psi f\ \overline{x'}\ y$, when $u >_\psi v' >_\phi w$ \item $f\ \overline{x}\ \overline{w} >_\phi f\ \overline{x}\ \overline{w}\ y >_\psi f\ \overline{x'}$ when $u >_\psi w$ \end{itemlist} so in each case $(w, u) \in (\psi \circ (\phi \cup \psi)^*) \cup \phi$. Since $<_{sn1}$ is well-founded it follows easily that $\psi$ is well-founded, and $\phi$ is well-founded since $M\ N <_{ty} M$. Thus $\phi \cup \psi =\ \ll$ is well-founded. } \begin{theorem} \label{tc2-snT} Every term is strongly normalising. \end{theorem} \proof{ In this case we cannot show that Condition~\ref{conds-defs}\ref{rpc} holds, but we can show that every term is in $\gindy \ll (\gindy \vtl \SN)$. Let $(t, s) \in \rho$ and assume that $\forall u \ll s$.\ $u \in \gindy \vtl \SN$, and $\forall v \vtl s$.\ $v \in \SN$. If $(t, s) \in \rho$ via rule (\ref{Sfgxy}), then, as in the proof of Theorem~\ref{tc2-sn} we have $f,g,x$ and each $y_i \in \SN$, so the combination $f x (g x) y_1 \ldots y_k \in \SN$. If $(t, s) = (M N, M) \in \rho$ via rule (\ref{aa}), then $t \ll s$, so $t \in \gindy \vtl \SN$. Then for $K \vtl M N$, either $K = N$ which is in \SN, or $K \vtl M$ and so $K \in \SN$. Thus $t \in \SN$. If $(t, s) \in \rho$ via rule (\ref{RZy}), then $z$ and each $y_i \in \SN$, so $t = z\ y_1 \ldots y_k \in \SN$. If $(t, s) \in \rho$ via rule (\ref{RSfzy}), then we have $f, z, \Succ\ n$ and each $y_i \in \SN$, and so by rule (\ref{Succ2}), $n \in \SN$. Thus, to get $t = f\ n\ (R\ n\ f\ z)\ y_1 \ldots y_k$, we need only show $R\ n\ f\ z \in \SN$. Now $R\ n\ f\ z \ll R\ (\Succ\ n)\ f\ z\ y_1 \ldots y_k = s$, so $R\ n\ f\ z \in \gindy \vtl \SN$. Now, for $t' \vtl R\ n\ f\ z$, $t' = n, f \mbox{ or } z$ and so $t' \in \SN$. Therefore $R\ n\ f\ z \in \SN$. If $(t, s) \in \rho$ via rule (\ref{Succ2}), then we have $t = n \in \SN$. Finally, where $(t, s) \in \rho$ via rule (\ref{inarg}), $t <_{sn1} s$, so $t \in \gindy \vtl \SN$. Then for $y \vtl t$, there is $x \vtl s$ such that $y \leq_\rho x$, so $y \in \SN$. Thus $t \in \SN$. That is, in each case, $t \in \SN$, and, discharging the assumptions as in the proof of Lemma~\ref{dth} we get $s \in \SN$ and $s \in \gindy \ll (\gindy \vtl \SN)$. Then we prove that every term is in \SN\ as in our Theorem~\ref{thm-allsn}, as both $\ll$ and $\vtl$ are well-founded. } \section{Application to Term Rewriting Systems} \label{s-appl-rewr} We now apply our Theorem~\ref{thm-allsn} to the special case of a TRS on terms of a first-order language $T (\Sigma, V)$ (see \cite[\S 3.1]{baader-nipkow}), thereby showing that our main result from \cite{dggt} is a special case of our Theorem~\ref{thm-allsn}. We consider a binary relation $\sigma$, which is the set of substitutional instances of a set of rewrite rules, and so is closed under substitutions. However $\sigma$ itself is typically not monotonic, ie, compatible with $\Sigma$-contexts (see \cite[Definition~3.1.9]{baader-nipkow}). % So we define $\ctxt\ \sigma$ and $\pctxt\ \sigma$ as in \S\ref{s-snst}. % \comment{ % To formalise ``closure under context'', % we must specify a language of terms. % This is a first-order language, with % a fixed set of function symbols, or % term constructors, of fixed or variable (finite) arity, % whose arguments and results are terms. % This language may or may not contain term variables. % The meta-language used to express rewrite rules and to % discuss rewrites \emph{does} contain term variables. % Given a term like $t = f(a,b,g(c,d))$, its \emph{immediate} subterms % are $a, b$ and $g(c,d)$, its \emph{proper} subterms are these and $c$ % and $d$, and its subterms are these and also $t$ itself. We write % $\overline{s}$ for a sequence of terms $s_1, \ldots, s_m$, % such that these % are the {immediate} subterms of $f(\overline{s})$. % We define the ``closure of $\rho$ under context'', $\ctxt\ \rho$: % for example, if $(c', c) \in \rho$, then $(f(a,g(c')), % f(a,g(c))) \in \ctxt\ \rho$. % } In \cite{dggt} we dealt with the termination of such rewrite relations. In discussing that work we will use ``$\sigma$'' for the relation there called ``$\rho$'', which is the set of substitutional instances of the rewrite rules. Then the rewrite relation is $\ctxt\ \sigma$, which here we will call $\rho$. So $\SN = \wfp\ \rho = \wfp\ (\ctxt\ \sigma)$. The relation $\vtl$ of the previous sections will now be interpreted as the immediate subterm relation. Recall that in \cite{dggt} we used a relation \mbox{$<_{dt}\ =\ <_{cut} \cup <_{sn1}$}, where $<_{cut}$ was chosen by the user, but $<_{sn1}$ was defined as below \cite[Definition 3]{dggt}. \begin{definition}[ $<_{sn1}$, $<_{sn2}$]\label{defn:porders} Given $\rho$ and $<_{cut}$ we define two further binary relations on terms, $<_{sn1}$ and $<_{sn2}$. \begin{itemlist} \item\label{defn:porders-sn1} ${t_1} <_{sn1} {t_0}$ if $t_0$ and $t_1$ are the same except that an immediate subterm $t'_0$ of $t_0$ is in \SN\ and reduces to the corresponding immediate subterm $t'_1$ of $t_1$. \item\label{defn:porders-sn2} ${t_1} <_{sn2} {t_0}$ if $t_0$ and $t_1$ are the same except that a proper subterm $t'_0$ of $t_0$ is in \SN\ and reduces to the corresponding proper subterm $t'_1$ of $t_1$. \end{itemlist} (that is, in both cases, $(t'_1, t'_0) \in \ctxt\ \sigma$). \end{definition} Note that ${t_1} <_{sn1} {t_0}$ implies ${t_1} <_{sn2} {t_0}$, and our main theorem uses only $<_{sn1}$. However $<_{sn2}$ is sometimes easier to work with because it is closed under context. \begin{theorem} \label{thm-sn12wf} The relations $<_{sn1}$ and $<_{sn2}$ are each well-founded \cite{dawson-gore-machine-checked-strong-normalisation}. \end{theorem} Then we apply our Theorem~\ref{thm-allsn} by letting $\ll$ be the relation $<_{dt}^+$, which is well-founded if and only if $<_{dt}$ is so. Also let $\ll'$ be $<_{cut}$, so \mbox{$\ll \ =\ \ll' \cup <_{sn1}$}. We now reproduce Theorem~2 of \cite{dggt} in our current notation, as Theorem~\ref{thm-csl} and Condition~\ref{rpc-csl}\ref{csl}. Condition~\ref{rpc-csl}\ref{csl'} implies Condition~\ref{rpc-csl}\ref{csl}, is more generally useful, and is used in \S\ref{s-inc}. \begin{condition}\label{rpc-csl} For all $(t, s) \in \sigma$, \begin{romanlist} \item \label{csl} If $\forall s' \vtl^+ s.\ s' \in \SN$ then, for all $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$. \item \label{csl'} For all $t' \vtl^* t$, either $(t', s) \in\ \vtl \circ\ (\rho\ \cup \vtl)^*$ or $t' \ll' s$. \end{romanlist} \end{condition} \begin{theorem} \label{thm-csl} If $\sigma$ satisfies Condition~\ref{rpc-csl}\ref{csl} or \ref{csl'}, $\ll$ contains $<_{sn1}$ and $\ll$ is well-founded, then every term is strongly normalising \cite{dggt}. \end{theorem} \proof{ We apply our Theorem~\ref{thm-allsn}. Since $\vtl$ is well-founded and we assume $\ll$ is well-founded, conditions \ref{ubg} and \ref{vbs} of our Theorem~\ref{thm-allsn} are satisfied. It remains only to check that Condition~\ref{conds-defs}\ref{rpc0} holds. In fact, the stronger Condition~\ref{conds-defs}\ref{rpc1} holds. Consider $(t, s) \in \rho$, and assume that $\forall s' \vtl s.$ \mbox{$s' \in \SN$}. As $\rho = \ctxt\ \sigma$ is closed under context, it follows that any subterm of a strongly normalising term is strongly normalising, so we can assume that $\forall s' \vtl^+ s.\ s' \in \SN$. For $(t, s) \in \rho$, there are two cases: $(t, s) \in \sigma$ or $(t, s) \in \rho \setminus \sigma$. For the case $(t, s) \in \sigma$, Condition~\ref{rpc-csl}\ref{csl} then implies that for $t' \vtl^* t$, either $t' \in \SN$ or $t' \ll s$, and so Condition~\ref{conds-defs}\ref{rpc1} holds in this case. We now consider the case $(t, s) \in \rho \setminus \sigma$: that is, where a proper subterm of $s$ is reduced, using $\sigma$, to the corresponding proper subterm of $t$. Consider any subterm $t'$ of $t$. We show that either $t' \in \SN$ or $t' <_{sn1} s$, whence $t' \ll s$. If $t' = t$, then $t' <_{sn1} s$ by definition of $<_{sn1}$. If $t'$ is a proper subterm of $t$, then if there is a corresponding subterm $s'$ of $s$ such that either $t' = s'$ or \mbox{$(t', s') \in \ctxt\ \sigma$}, then $s'$ and $t'$ are in \SN. Otherwise, there is a proper subterm $s'$ of $s$, where $s'$ is reduced to $t''$, so $(t'', s') \in \ctxt\ \sigma$, and $t'$ is a subterm of $t''$. Then $s'$, $t''$ and $t'$ are all in \SN. So Condition~\ref{conds-defs}\ref{rpc1} holds for this case also. } % \comment{ - from CSL'04 paper % \begin{condition}\label{csl04-rpc} % For all $(r, l) \in \rho$, % if all proper subterms of $l$ are in \SN\ then, % for all subterms $r'$ of $r$, either % \begin{enumerate} % \item \label{csl04-rpc-sn} $r' \in \SN$ or % \item \label{csl04-rpc-dt} $r' <_{dt}^+ l$. % \end{enumerate} % \end{condition} % In practice we use a simpler condition which implies % Condition~\ref{csl04-rpc}, such as % \begin{condition}\label{csl04-rpc1} % For all $(r, l) \in \rho$, % for all subterms $r'$ of $r$, either % \begin{enumerate} % \item \label{csl04-rpc-srp} $r'$ is a proper subterm of $l$ % or is a subterm of a reduction of a proper subterm of $l$ % \item \label{csl04-rpc-cut} $r' <_{cut} l$ % \item \label{csl04-rps} % $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm. % \end{enumerate} % \end{condition} % \begin{theorem} \label{thm:all-sn} % If $\rho$ satisfies Condition~\ref{csl04-rpc} and $<_{dt}$ is well-founded, % then every term is strongly normalising. % \end{theorem} % end comment } We next relate this theorem to known results on constricting derivations, and show how it implies known results relating to the the Knuth-Bendix Ordering, and to dependency pairs. Note that we have already discussed, in \S\ref{s-gpo}, how the termination of the recursive path orderings \cite[Defn~4.22, 4.24]{dersh-har} follows from our Theorem~\ref{thm-allsn}. We did in fact show, in \cite[\S 3.7]{dggt}, that this also follows from Theorem~\ref{thm-csl}. We then show how the theorem can be used in a number of specific examples. Further examples may be found in \cite{dggt}. In these examples, the crux is to find an appropriate definition of $\ll'$, for this determines $\ll$ as $\ll' \cup <_{sn1}$. Since we need to choose $\ll'$ so that $\ll$ is well-founded, we choose $\ll'$ well-founded, and such that $\ll'$ and $<_{sn1}$ satisfy one of the conditions of Lemma~\ref{wf-rs}. Since $<_{sn1}$ is necessarily well-founded, this ensures that $\ll$ is well-founded. In many examples of the use of Theorem~\ref{thm-csl}, the argument went as follows. We let $<_{sn2}$ be the set of those reductions where a strongly normalising \emph{proper} subterm is reduced, so $<_{sn1}\ \subseteq\ <_{sn2}$, and $<_{sn2}$ is also necessarily well-founded, by Theorem~\ref{thm-sn12wf}. Then, using $<_{sn2}$ in place of $<_{sn1}$, we prove that $\ll' \cup <_{sn2}$ is well-founded by proving that $\ll'$ is well-founded and then using Lemma~\ref{wf-rs} to prove that the union is well-founded, often by proving that $\ll' \circ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$. \subsection{Constricting Derivations} \label{s-cd} For a rewrite system on a first-order language (where the reduction relation is closed under context), a ``constricting derivation'' has been defined as an infinite reduction sequence where each reduction occurs at a subterm $t$ whose proper subterms are all strongly normalising \cite{dersh-td}. For a rewrite relation $\rho = \ctxt\ \sigma$, we define a \emph{constricting reduction} by: $(t, s) \in \constrict\ \sigma$ iff $(t, s) \in \sigma$ and the proper subterms of $s$ are in $\wfp\ \rho$. Here, $\vtl$ is the immediate subterm relation, and $<_{sn1}$ is defined as in \S\ref{s-appl-rewr}. The following results are easily proved by methods similar to those of \cite{dvk}. \begin{lemma} \label{util} For all binary relations $\sigma$ and $\tau$: \begin{romanlist} \item \label{o-rev} $\sigma \circ\ \tau$ is well-founded if and only if $\tau \circ \sigma$ is well-founded \item \label{o-u} if $\tau$ is well-founded then $\wfp\ (\tau^* \circ \sigma) = \wfp\ (\sigma \cup \tau)$ \item \label{wfp-otc} if $\tau$ is well-founded and $\tau \circ \sigma \subseteq \sigma \circ\ \tau^*$, then $\wfp\ (\sigma \cup \tau) = \wfp\ \sigma$. \end{romanlist} \end{lemma} The following theorem encapsulates mostly known results, for example Lemma~1 of %Hirokawa \& Middeldorp \cite{hm-dpr} resembles: ``if (\ref{snocos}) then (\ref{rhowf})'', % \comment{ % \footnote{\cite[Lemma~1]{hm-dpr} starts from a minimal non-terminating % term, refers to $<_\epsilon$ rather than $<_{sn1}$ and assumes a TRS, % with substitutable rewrite rules. The notation $<_\epsilon$ % refers to a rewrite of a proper subterm.} % } and Proposition~1 of %Borralleras, Ferreira \& Rubio \cite{bfr} is: ``if (\ref{rhowf}) then (\ref{rhous})''. \begin{theorem} \label{thm-ctalt} The following are equivalent, where $\rho = \ctxt\ \sigma$: \begin{eqnarray} \label{cosusn} (\constrict\ \sigma\ \circ \vtl^*)\ \cup <_{sn1} && \mbox{ is well-founded} \\[-0.5ex] \label{cososn} \constrict\ \sigma\ \circ \vtl^* \circ <_{sn1}^* && \mbox{ is well-founded} \\[-0.5ex] \label{sosnoc} \vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma && \mbox{ is well-founded} \\[-0.5ex] \label{snocos} <_{sn1}^* \circ\ \constrict\ \sigma\ \circ \vtl^* && \mbox{ is well-founded} \\[-0.5ex] \label{rhoos} \rho\ \circ \vtl^* && \mbox{ is well-founded} \\[-0.5ex] \label{rhous} \rho\ \cup \vtl && \mbox{ is well-founded} \\[-0.5ex] \label{rhowf} \rho && \mbox{ is well-founded} % \\[-0.5ex] % \label{rhotc} \rho^+ && \mbox{ is well-founded} \\[-0.5ex] % \label{rhotcs} \rho^+ \cup \vtl && \mbox{ is well-founded} \end{eqnarray} \end{theorem} \proof{ (\ref{sosnoc}) $\Rightarrow$ (\ref{rhowf}): If $t_0$ is not in $\SN = \wfp\ \rho$, then let $t_0'$ be a minimal subterm of $t_0$ which is not in \SN --- so the proper subterms of $t_0'$ are in \SN. Consider any infinite sequence of reductions from $t_0'$ --- these cannot all be reductions of proper subterms as the latter are in \SN, so find $t_0''$ and $t_1$ in this infinite sequence such that $(t_0'', t_0') \in (\ctxt\ \sigma \setminus \sigma)^*$ and $(t_1, t_0'') \in \sigma$. Now all proper subterms of $t_0'$, of $t_0''$ and of all terms between them in the reduction sequence are in \SN. So $(t_1, t_0) \in\ \vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma$, and as $t_1 \not\in \SN$, a ($\vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma$)-sequence can be continued. Similar proofs are at, eg, \cite[Theorem~6]{dps00}, \cite[Lemma~1]{hm-dpr}. (\ref{cososn}) $\Leftrightarrow$ (\ref{sosnoc}) $\Leftrightarrow$ (\ref{snocos}): these follow from Lemma~\ref{util}\ref{o-rev}. (\ref{cosusn}) $\Leftrightarrow$ (\ref{snocos}) and (\ref{rhoos}) $\Leftrightarrow$ (\ref{rhous}): use Lemma~\ref{util}\ref{o-u} since $<_{sn1}$ is well-founded. (\ref{rhowf}) $\Rightarrow$ (\ref{rhous}) : % (and (\ref{rhotc}) $\Rightarrow$ (\ref{rhotcs}) is similar) : follows from Lemma~\ref{util}\ref{wfp-otc}, as $\vtl \circ\ \rho \subseteq \rho\ \circ \vtl$, as $\rho$ is monotonic. % (\ref{rhous}) $\Rightarrow$ (\ref{rhowf}) : trivial, as % $\rho \subseteq \rho\ \cup \vtl$ % (\ref{rhotcs}) $\Rightarrow$ (\ref{snocos}) : similarly trivial, % as $<_{sn1}^* \circ\ \constrict\ \sigma \subseteq \rho^+$ % (\ref{rhotc}) $\Leftrightarrow$ (\ref{rhowf}) is a standard result (\ref{rhous}) $\Rightarrow$ all others : since every relation mentioned is contained in \mbox{$(\rho\ \cup \vtl)^+$}. } We now link Theorem~\ref{thm-ctalt} with Theorem~\ref{thm-csl}, by some simple proofs. Note that Condition~\ref{rpc-csl}\ref{csl} in \S \ref{s-appl-rewr} simply says: if $(t', s) \in \constrict\ \sigma\ \circ \vtl^*$ then $t' \in \SN$ or $t' \ll s$. Let $\tau = (\constrict\ \sigma\ \circ \vtl^*)\ \cup <_{sn1}$. We show $\SN = \wfp\ \rho \subseteq \wfp\ \tau$. Since $\tau \subseteq (\rho\ \cup \vtl)^+$, so $\wfp\ (\rho\ \cup \vtl) \subseteq \wfp\ \tau$. By Lemma~\ref{util}\ref{wfp-otc}, $\wfp\ \rho = \wfp\ (\rho\ \cup \vtl)$. Then, we can use Theorem~\ref{thm-csl} to prove (\ref{cosusn}) implies (\ref{rhowf}). Assume (\ref{cosusn}) of Theorem~\ref{thm-ctalt}, that is, $\tau$ is well-founded. Let $\ll\ = \tau$. Then Condition~\ref{rpc-csl}\ref{csl} holds trivially, $\ll\ \supseteq\ <_{sn1}$ and $\ll$ is well-founded. Hence, by Theorem~\ref{thm-csl}, $\rho$ is well-founded. The converse is also easy to prove, giving an alternative proof of Theorem~\ref{thm-csl}. Assume (\ref{cosusn}) $\Rightarrow$ (\ref{rhowf}); we will prove Theorem~\ref{thm-csl}. Suppose the assumptions of Theorem~\ref{thm-csl} hold, and we want to show its conclusion, (\ref{rhowf}). We show (\ref{cosusn}), ie, that $\tau$ is well-founded. Let $(t, s) \in \tau$. Then, if $(t, s) \in\ <_{sn1}$, then $t \ll s$. Otherwise, $(t, s) \in \constrict\ \sigma\ \circ \vtl^*$ and so $t \in \SN$ or $t \ll s$ by Condition~\ref{rpc-csl}\ref{csl}. % Now $\SN \subseteq \wfp\ \tau$, as shown above, so $(t, s) \in \tau$ implies $t \in \wfp\ \tau$ or $t \ll s$, where $\ll$ is well-founded. Thus any $\tau$-descending chain either terminates or hits a member of $\wfp\ \tau$: that is, every $s \in \bars\ \tau\ (\wfp\ \tau)$. So, by Lemma~\ref{l2}\ref{bars-wfp}, every $s \in \wfp\ \tau$, as required. \subsection{The Knuth-Bendix Ordering} \label{sec:knuth-bend-order} For a rewrite system (with rules containing variables), the Knuth-Bendix ordering $<_{kb}$ is based on a strict well-founded order $<$ on function symbols and, additionally, a weight function $w$ on function symbols and variables. Since our approach is based on a relation $\rho$ (which amounts to the rewrite rules after all possible substitutions for variables), we describe the Knuth-Bendix ordering in this context. Weights are natural numbers, and the weight of any constant or object language variable is positive: thus every subterm has positive weight. At most one unary function symbol (call it $k$) can have zero weight, and then $k > f$ for any other function symbol $f$. The weight of a term is the sum of the weights of the function symbols and variables in it. Then we have that $s >_{kb} t$ iff $w(s) \geq w(t)$ and one of \begin{eqnarray} && \label{kbo-h1} w(s) > w(t) \\[-0.5ex] \label{kbo-hn} && s = k^n(t) \mbox{ for some } n > 0 \\[-0.5ex] \label{kbo-fg} && s = f(\overline{s}) \mbox{ and } t = g(\overline{t}) \mbox{ where } f > g\\[-0.5ex] \label{kbo-lex} && s = f(\overline{s}), t = f(\overline{t}) \mbox{ and } (\overline{t}, \overline{s}) \in \lex\ (<_{kb}) \end{eqnarray} \begin{theorem} The Knuth-Bendix ordering is well-founded. \end{theorem} \textbf{Proof.} We define $s \gg' t$ iff $w(s) \geq w(t)$ and either one of the rules (\ref{kbo-h1}) or (\ref{kbo-fg}) holds, or $s >_{kw1} t$, where $<_{kw1}$ is defined by: \begin{eqnarray} \label{kbo-kw1} f(\overline{t}) <_{kw1} f(\overline{s}) & \mathrm{ iff } & (\overline{t}, \overline{s}) \in \lex\ (\fwf\ (<_{kb})) \end{eqnarray} To show $\ll'$ is well-founded, we have that each of rules (\ref{kbo-h1}), (\ref{kbo-fg}) and (\ref{kbo-kw1}) provides a well-founded relation and we can apply Lemma~\ref{wf-rs} repeatedly to show that their union is well-founded, noting that if $s >_{kw1} t$ then $w(s) \geq w(t)$. Further, $<_{sn1} \ \subseteq\ <_{kw1}$, so $\ll \ =\ \ll' \cup <_{sn1} \ =\ \ll'$ is well-founded. To show Condition~\ref{rpc-csl}\ref{csl'}, suppose that $l >_{kb} r$ and that $r'$ is a subterm of $r$. \begin{itemlist} \item First, let $r' = r$. Assume that all proper subterms of $l$ are in \SN, in which case, if $l >_{kb} r$ by rule \eqref{kbo-lex}, then $l >_{kw1} r$, so $l \gg' r$. If $l >_{kb} r$ by rules (\ref{kbo-h1}) or (\ref{kbo-fg}), then $l \gg' r$, and if $l >_{kb} r$ by rule (\ref{kbo-hn}) then $l \vtr^+ r$. \item Now suppose $r'$ is a proper subterm of $r$, so $w(r) \geq w(r')$. \begin{itemlist} \item If $w(r') < w(r)$ or $w(r) < w(l)$ then $w(l) > w(r')$, so $l \gg' r'$ by rule (\ref{kbo-h1}). % If $r' = r$ then $l >_{kb} r'$. \item If $w(l) = w(r) = w(r')$ then % and $r'$ is a proper subterm of $r$, then $r = k^n(r')$ for some $n > 0$, and so $l >_{kb} r$ by either (\ref{kbo-hn}) or (\ref{kbo-lex}) (as the $g$ of (\ref{kbo-fg}) cannot be $k$). \begin{itemlist} \item If $l >_{kb} r$ by (\ref{kbo-hn}) then $l \vtr^+ r'$. \item If $l >_{kb} r$ by (\ref{kbo-lex}), then, for some $l_1, r_1$, we must have $l = k(l_1)$, $r = k(r_1)$, $l_1 >_{kb} r_1$ and $r'$ is a subterm of $r_1$, so $(r', l) \in\ \vtl \circ <_{kb} \circ \vtl^*$, so satisfying Condition~\ref{rpc-csl}\ref{csl'}. \hfill $\Box$ \end{itemlist} \end{itemlist} \end{itemlist} \subsection{Dependency Pairs}\label{s-dps} Arts \& Giesl \cite{dps00} describe a method of establishing termination using ``dependency pairs''. They distinguish function symbols which appear at the head of the left-hand side of a rewrite rule (``defined symbols'') and those which do not (``constructor symbols''). They follow the convention that for a rule $l \to r$ of a rewrite system, $l$ is not a lone variable, and any variable in $r$ is also in $l$. For each defined symbol $d$ they introduce a new ``tuple symbol'' $d^\sharp$. From a term $t$ we obtain a term $t^\sharp$ by changing the head symbol of $t$ to the corresponding tuple symbol. Previously we have considered a ``rule'' $l \to r$ after substitution, and the variables in our analyses have been metavariables where, for example, we might have considered a rule $g(x) \to x$ with $l = g(x)$, $r = x$, and $r'$ a proper subterm of $x$. Here $l \to r$ will mean a rule before substitution, and we will use $\sigma$ for a substitution. For a rewrite rule $l \to r$, and subterm $r'$ of $r$, if the head of $r'$ is a defined symbol then $l^\sharp \to r'^\sharp$ is a \emph{dependency pair}. In \cite{dps00}, the relations $\precsim$ and $\prec$ below were a quasi-order and its strict part, but in subsequent papers \cite{giesl-mod-term}, \cite{hm-dpr} these relations needed only to be a \emph{reduction pair}, as defined next. \begin{definition} \label{def-red-pair} A \emph{reduction pair} $(\succsim,\succ)$ consists of a quasi-ordering (ie, a reflexive and transitive relation) $\succsim$, which is closed under contexts (monotonic), and a well-founded ordering $\succ$, where both are closed under substitutions and $\succ$ is \emph{compatible} with $\succsim$, ie either $\succsim \circ \succ \ \subseteq\ \succ$ or $\succ \circ \succsim \ \subseteq\ \succ$. \end{definition} (Some papers say $\succsim \circ \succ \ \subseteq\ \succ$ $\underline{and}$ $\succ \circ \succsim \ \subseteq\ \succ$ here, apparently because it makes some proofs simpler). We now state and prove the analogue, for reduction pairs, of the ``sufficiency'' part of \cite[Theorem~7]{dps00}. \begin{theorem} If there is a reduction pair $(\succsim,\succ)$ such that \begin{alphlist} \item \label{dpt-rule} $l \succsim r$ for all rules $l \to r$, and \item \label{dpt-dp} $s \succ t$ for all dependency pairs $s \to t$ \end{alphlist} then the rewrite system terminates. \end{theorem} {\bf Proof.} Assume that $\succsim$ and $\succ$ is minimal such that the conditions hold. Then there is no instance of $c(x) \succ d(y)$ or $c(x) \succsim d(y)$ where $c$ is a constructor symbol and $d$ is a defined symbol (either with or without $\sharp$), as neither \ref{dpt-rule} nor \ref{dpt-dp} nor the requirement that $\succsim$ be closed under context require it, whence the compatibility condition cannot require it. For a constructor symbol $c$ and defined symbol $d$, we define $\ll'$: \begin{eqnarray} \label{dp-sh} & s^\sharp \prec t^\sharp \Longrightarrow s \ll' t & \\ % s\sigma \ll' t\sigma & \\ \label{dp-cd} & c(x) \ll' d(y) & \end{eqnarray} Because $\prec$ is well-founded and, by the remark above, rule (\ref{dp-sh}) does not give any case of $ c(x) \gg' d(y)$, it follows that $\ll'$ is well-founded. To show that $\ll' \cup <_{sn1}$ is well-founded, in the case $\prec \circ \precsim \ \subseteq \ \prec$, we use Lemma~\ref{wf-rs}\ref{tco}, showing that $\ll' \circ <_{sn1} \ \subseteq\ \ll'$ ; in the case $\precsim \circ \prec \ \subseteq \ \prec$, we use Lemma~\ref{wf-rs}\ref{otc}, showing $<_{sn1} \circ \ll' \ \subseteq\ \ll'$. In the case that $\prec \circ \precsim \ \subseteq \ \prec$, suppose that $t \gg' u >_{sn1} v$. If $t \gg' u$ by rule (\ref{dp-cd}) then $t \gg' v$ by the same rule. If $t \gg' u$ by rule (\ref{dp-sh}) then $t^\sharp \succ u^\sharp$, and a proper subterm $u'$ of $u$ is rewritten to a corresponding subterm $v'$ of $v$. As $\precsim$ is closed under substitution, assumption \ref{dpt-rule} gives us that $u' \succsim v'$. Then, since $\succsim$ is closed under context, $u^\sharp \succsim v^\sharp$, and so $t^\sharp \succ v^\sharp$ and $t \gg' v$. In the case that $\precsim \circ \prec \ \subseteq \ \prec$, suppose that $t >_{sn1} u \gg' v$. If $u \gg' v$ by rule (\ref{dp-cd}) then $t \gg' v$ by the same rule. If $u \gg' v$ by rule (\ref{dp-sh}) then $u^\sharp \succ v^\sharp$, where a proper subterm $t'$ of $t$ is rewritten to a corresponding subterm $u'$ of $u$, and we have $t' \succsim u'$, $t^\sharp \succsim u^\sharp$, $t^\sharp \succ v^\sharp$ and $t \gg' v$. Finally, we show that Condition~\ref{rpc-csl}\ref{csl'} is satisfied. For a rule $l \to r$ and a substitution $\sigma$, so $(r \sigma, l \sigma) \in \rho$, and a subterm $r'$ of $r \sigma$, there are three cases: % for $r'$: \begin{itemlist} \item the head of $r'$ is a constructor symbol in $r$, in which case $l \sigma \gg' r'$ by (\ref{dp-cd}) \item the head of $r'$ is a defined symbol in $r$, in which case $r' = r_1 \sigma$ for some subterm $r_1$ of $r$, $l^\sharp \to r_1^\sharp$ is a dependency pair, and so $l^\sharp \succ r_1^\sharp$ ; then $l^\sharp\sigma \succ r_1^\sharp\sigma$ (since $\succ$ is closed under substitution), and $l \sigma \gg' r_1 \sigma = r'$ by (\ref{dp-sh}) \item $r'$ is a subterm of $x \sigma$ for some variable $x$ in $r$, in which case $r'$ is a proper subterm of $l \sigma$, since any variable in $r$ appears as a proper subterm of $l$. \hfill $\Box$ \end{itemlist} % \comment{ Multiset order % \subsection{Multiset order : PROPOSED TO BE OMITTED} % Given an irreflexive relation $\rho$ on a set $E$, we can define % the \emph{multiset order} derived from $\rho$ on multisets of elements of $E$. % We use $A, B$ and $C$ for finite multisets of elements of $E$, % by which we mean both that they contain only finitely many distinct elements % and that they contain only finitely many copies of each such element. % We use $A \sqcup B$ to stand for the multiset union. % We consider the irreflexive relation $<_{m1}$ % defined on finite multisets: % \begin{description} % \item[$<_{m1}$:] $\forall C, \forall b \in E$. % if, for all $c \in C$, $c <_\rho b$, % then $C \sqcup A <_{m1} \{b\} \sqcup A$. % % \item[$\leq_{m2}$:] $\forall C,B$ . % % if, for all $c \in C$, there exists $b \in B$ such that % % $c \leq_\rho b$, then $C \leq_{m2} B$. % \end{description} % If $\rho$ is a strict order (an irreflexive, transitive relation), % then $<_{m1}^+$ is equal to the multiset order derived from $\rho$. % % Clearly, $<_{m1}^+ = <_{m2}^+$ if $<_\rho^+$ is irreflexive, and % % $<_{m2}$ is transitive if $<_\rho$ is transitive. In the literature, % % we have seen the multiset ordering derived from $\rho$ defined as % % either $<_{m2}$, or as $<_{m1}^+$, which are equivalent when $<_\rho$ % % is transitive. Since we aim to prove that the multiset ordering for % % finite multisets is well-founded, or equivalently, that its transitive % % closure is well-founded, either definition will do. % We represent a multiset as a tree, with two sorts of node, ``inner'' % nodes ($I$) and ``leaf'' nodes ($L$). Viewing such a tree as a term, % the function symbols are $I$ and $L(e)$ for each $e \in E$, % where $I$ has arbitrary arity and each $L(e)$ is nullary. % % The arguments of the $I$ symbol are % % trees, and the argument of a leaf node is a member of the set $E$. % The ``leaf multiset'' % of a tree is the multiset of its leaf nodes, % but with each $L(e)$ changed to $e$. % Note that different trees can have the same leaf multiset. % We define a rewrite relation on such trees (terms) as follows. % For every (finite) multiset % $C = [c_1, c_2, \ldots, c_k]$ % and every element % $b \in E$ % satisfying % $\forall c_i \in C.\ c_i <_\rho b$ (as in the definition of $<_{m1}$) % we have a rule % $L(b) \longrightarrow I(L(c_1), L(c_2), \ldots, L(c_k)).$ % \begin{theorem} % Given a well-founded order $\rho$, the derived multiset order % (on finite multisets) is well-founded. % \end{theorem} % \proof{ % Clearly, whenever $A <_{m1} B$, any tree whose leaf multiset is $B$ % can be reduced to a tree whose leaf multiset is $A$ % using the rewrite relation defined above. % Since for any finite multiset $B$ there is a tree % whose leaf multiset is $B$, % when we show that rewriting terminates % we have shown that the multiset order is well-founded. % We prove that this rewrite system terminates. % We define $\ll'$ by the rules % $$ % L(x) \gg' I(y) % \qquad\qquad % L(x) \gg' L(y) \mbox{ iff } x >_\rho y % $$ % It is clear that $\ll'$ is well-founded when $\rho$ is. % To show that $\ll' \cup <_{sn1}$ is well-founded, we use % Lemma~\ref{wf-rs}, by showing that in fact % $<_{sn1} \circ \ll' = \emptyset$. % For suppose $t >_{sn1} u \gg' v$. % Then $u$ must be of the form $L(x)$, and a proper subterm of $t$ % must reduce to a proper subterm of $u$ -- but $u$ has no proper subterms % \footnote{$x$ is not a subterm of $L(x)$: recall that each $L(x)$ is % a nullary function symbol.}. % To show that Condition~\ref{rpc-csl}\ref{csl'} is satisfied, % when $L(b) \longrightarrow I(L(c_1), \ldots, L(c_k)) = r$, % we have $L(b) \gg' r$ % by the first rule for $\ll'$, and, % for every subterm $L(c_i)$ of $r$, % $L(b) \gg' L(c_i)$ by the second rule. % } % end of comment : Multiset order} \subsection{A non simplification ordering} Example 5 of \cite{33ex}, with the single rule $f(f(x)) \longrightarrow f(g(f(x)))$ is one for which a simplification ordering cannot be used, because a simplification ordering would take $g(f(x))$ to $f(x)$ and so $f(g(f(x)))$ to $f(f(x))$, giving a cycle. That is, as $f(f(x))$ is embedded in $f(g(f(x)))$, and the embedding is included in every simplification ordering, every simplification ordering orients that rule in the reverse direction. But Theorem~\ref{thm-csl} is not limited to simplification orderings. We define $\ll'$ according to the number of consecutive $f$ symbols starting from the head of a term. Alternatively, we could use the total number of pairs of adjacent $f$ symbols, as suggested in \cite{33ex}. Thus $f(f(x)) \gg' f(g(y))$, $f(f(x)) \gg' g(y)$, and $f(f(x)) \gg' f(x)$. Finally, any subterm of $x$ is a proper subterm of $f(f(x))$. Thus Condition~\ref{rpc-csl}\ref{csl'} is satisfied. Clearly also, rewriting a subterm cannot increase the number of consecutive $f$ symbols, so % $<_{sn1} \ \subseteq\ \leq_{cut}$, % following wrong - would need to consider a quasi-order % whence (as $\ll'$ is transitive), $<_{sn1} \circ \ll' \ \subseteq\ \ll'$ (and likewise $\ll' \circ <_{sn1} \ \subseteq\ \ll'$). Thus $\ll \;=\; \ll' \cup <_{sn1}$ is well-founded by Lemma~\ref{wf-rs}. Therefore the system terminates, by Theorem~\ref{thm-csl}. % \comment{ % \subsection{A recursive path ordering example} \label{s-diff} % We now consider a typical example whose termination is shown by the recursive % path ordering (see, for example, \cite{nat-term} or \cite{dersh-har}). % $$ % \begin{array}{rcl@{\qquad\qquad}rcl} % D(x + y) & \longrightarrow & Dx + Dy & % (x \times y) \times z & \longrightarrow & x \times (y \times z) \\ % D(x \times y) & \longrightarrow & x \times Dy + Dx \times y & % (x + y) + z & \longrightarrow & x + (y + z) \\ % x \times (y + z) & \longrightarrow & x \times y + x \times z & & & % \end{array} % $$ % The recursive path ordering is a simplification ordering. % To prove termination we must actually add % the following simplification rules as rewrite rules: % $$ % x + y \longrightarrow x \qquad % x + y \longrightarrow y \qquad % x \times y \longrightarrow x \qquad % x \times y \longrightarrow y % $$ % Clearly, if additional rules $R'$ are added to a rewrite system $R$, and the % resulting system $R \cup R'$ terminates, then the original system $R$ % terminates. % We define $\ll'$ as below by first defining % the relation $<_h$, which % depends on the head symbol, % and then defining the relations $<_\times$ and $<_+$ % which are for the rewrite rules capturing associativity: % \begin{itemize} % \item $D(x) >_h y \times z \qquad D(x) >_h y + z \qquad x \times y >_h z + w$ % \item if $x'$ is an immediate subterm of $x$, then % $x + y >_+ x' + z$ and % $x \times y >_\times x' \times z$ % \item $\ll' = (<_h \cup <_\times \cup <_+)$. % \end{itemize} % We now prove that this rewrite system terminates. % Clearly $\ll'$ is well-founded, since the immediate subterm relation is % well-founded. % To show that $\ll' \cup <_{sn1}$ is well-founded, % we in fact show that $\ll' \cup <_{sn2}$ is well-founded, % using Lemma~\ref{wf-rs}\ref{tco}. % First we show that $\ll' \circ <_{sn2} \ \subseteq\ % <_{sn2}^* \circ \ll'$. % For suppose $t \gg' u >_{sn2} v$. % If $t >_h u$ then clearly $t >_h v$. % Suppose $t >_\times u$, say $t = x \times y$, $u = x' \times z$ and % $x'$ is an immediate subterm of $x$. % There are two cases for $u >_{sn2} v$, % namely that a strongly normalising subterm of either $x'$ or $z$ % reduces to a corresponding subterm of $v$. % Firstly, if $z \longrightarrow w$, then we also have % $v = x' \times w$ and $t \gg' v$. % Secondly, if $x' \longrightarrow w'$, % then $v = w' \times z$. % As $x'$ is a subterm of $x$, let $w$ be the term obtained from $x$ by rewriting % its subterm $x'$ to $w'$. % Then $t = x \times y >_{sn2} w \times y$: but % note that this step of the argument would not hold for $>_{sn1}$. % Then $w'$ is an immediate subterm of $w$, so we have % $w \times y \gg' w' \times z = v$. % That is, $(v, t) \in\ <_{sn2} \circ \ll'$. % So, in each case, $(v, t) \in\ <_{sn2}^* \circ \ll'$, % and so $\ll' \cup <_{sn2}$ is well-founded, % by Lemma~\ref{wf-rs}\ref{tco}. % Finally, we need to consider all pairs $(r', l)$, % where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$. % In many cases $l >_h r'$: for example $D(x + y) >_h Dx + Dy$. % In other cases, $r'$ is a proper subterm of $l$: for example whenever % a (meta-)variable appears on the right-hand side of a rule, % and $r'$ is the term the variable stands for, or any subterm of it. % In the case of the associative rewrite rule % $l = (x \times y) \times z \longrightarrow r = x \times (y \times z) $, % we have that $l >_\times r$, by definition; % the rule for the associativity of $+$ is similar. % Finally, we have cases for $(r', l)$ such as % $(D(x), D(x + y))$ or $(y \times z, (x \times y) \times z)$. % Here, since a proper subterm $l'$ of $l$ is assumed to be strongly normalising, % and $x + y \longrightarrow x$ (likewise $x \times y \longrightarrow y$) % we have % $D(x + y) >_{sn1} D(x)$ and $(x \times y) \times z >_{sn1} y \times z$. % Thus in all cases either $r'$ is a proper subterm of $l$ or (assuming % proper subterms of $l$ are in \SN) $l >_{dt} % r'$, so the system terminates by Theorem~\ref{thm:all-sn}. % end of comment (D, +, * example) } % \comment{ % \subsection{Ackermann's function : PROPOSED TO BE OMITTED} % Ackermann's function on the natural numbers % can be defined by the following rewrite rules \cite[Example 29]{33ex} % \begin{eqnarray*} % A(0, y) & \longrightarrow & S(y) \\[-0.5ex] % A (S(x), 0) & \longrightarrow & A(x, S(0)) \\[-0.5ex] % A (S(x), S(y)) & \longrightarrow & A(x, A (S(x), y)) % \end{eqnarray*} % It can be shown to terminate using the lexicographic path ordering. % This is reflected in the relation $\gg'$ we use, % which is defined by the following cases: % % % \begin{eqnarray} % \label{Acut1} A(x, y) & \gg' & S(z) \\[-0.5ex] % \label{Acut2} A (S(x), y) & \gg' & A(x, z) \\[-0.5ex] % \label{Acut3} A (x, S(y)) & \gg' & A(x, y) % \end{eqnarray} % We now prove that this rewrite system terminates. % It is clear that $\gg'$ is well-founded using the % lexicographic ordering on arguments. % It is also clear that for each $(r', l)$, % where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$, % either $l \gg' r'$ or $r'$ is a proper subterm of $l$. % It remains to show that $\ll' \cup <_{sn1}$ is well-founded. % Again we show that $\ll' \cup <_{sn2}$ is well-founded, % using Lemma~\ref{wf-rs}\ref{tco}. % We show that $\ll' \circ <_{sn2} \ \subseteq\ % <_{sn2}^* \circ \ll'$. % For suppose $t \gg' u >_{sn2} v$. % \begin{itemlist} % \item % If $t \gg' u$ by rule (\ref{Acut1}), % ie $t = A(x, y)$ and $u = S(z)$, then $v = S(z')$ and so % $t \gg' v$. % \item % If $t \gg' u$ by rule (\ref{Acut2}), % then $t = A (S(x), y)$ and $u = A(x, z)$. % There are two cases for $u >_{sn2} v$: % \begin{itemlist} % \item % $v = A(x, z')$ where $z \longrightarrow z'$, in which case $t \gg' v$, or % \item % $v = A(x', y)$ where $x \longrightarrow x'$ % WRONG and $x \in \SN$, % by reducing a strongly normalising subterm of $x$, % in which case $t = A (S(x), y) >_{sn2} A (S(x'), y) \gg' A(x', z) = v$. % \end{itemlist} % \item % The case for rule (\ref{Acut3}) is similar. % \end{itemlist} % So in all cases % $(v, t) \in\ <_{sn2}^* \circ \ll'$, % and so $\ll' \cup <_{sn2}$ is well-founded, % by Lemma~\ref{wf-rs}\ref{tco}. % Therefore the system terminates by Theorem~\ref{thm-csl}. % end of comment : Ackermann's function} % \comment{ % \subsection{Insertion sort} % \newcommand{\sort}{\textit{sort}} % \newcommand{\ins}{\textit{insert}} % \newcommand{\choo}{\textit{choose}} % This example \cite[Example 32]{33ex} % is more difficult than the previous two, though the approach is similar. % The rules are % \begin{eqnarray*} % \sort(\nil) & \longrightarrow & \nil \\ % \sort(\cons (x, y)) & \longrightarrow & \ins (x, \sort (y)) \\ % \ins (x, \nil) & \longrightarrow & \cons (x, \nil) \\ % \ins (x, \cons (v, w)) & \longrightarrow & \choo (x, \cons (v, w), x, v) \\ % \choo (x, \cons (v, w), y, 0) & \longrightarrow & \cons (x, \cons (v, w)) \\ % \choo (x, \cons (v, w), 0, s(z)) & \longrightarrow & % \cons (v, \ins (x, w)) \\ % \choo (x, \cons (v, w), s(y), s(z)) & \longrightarrow & % \choo (x, \cons (v, w), y, z) % \end{eqnarray*} % To define $\gg'$, we start by defining an order $>_h$, % contained in $\gg'$, which depends on the head symbol, % using this (transitive) order on symbols: % $\sort > \{\ins, \choo\} > \cons$. % We notice that the rules (considered as definitions) % define \ins\ and \choo\ in terms of each other, % so we continue by defining % $$ % \begin{array}{c} % \ins (x, w) \gg' \choo (y, w, a, b) \gg' \ins (x, w') \\ % \choo (y, w, a, b) \gg' \choo (y', w, a', b') % \end{array} % $$ % where $\gg'$ is transitive and $w',a'$ are immediate subterms of $w,a$. % It is easy to see that $\gg'$ is well-founded. % As in \S\ref{s-diff}, we add a simplification rule % $$\cons (x, y) \longrightarrow y$$ % % where $l = \sort(\cons (x, y)) >_{sn1} \sort (y) = r'$. % Then, for every $(r', l)$ where $l \rightarrow r$ is a rewrite rule % and $r'$ is a subterm of $r$, % either $l \gg' r'$, $l >_{sn1} r'$ or $r'$ is a proper subterm of $l$. % Again we show that % $\ll' \circ <_{sn2} \ \subseteq\ <_{sn2}^* \circ \ll'$, % using the same technique as in the previous two examples. % Therefore the system terminates by Theorem~\ref{thm:all-sn}. % The ordering $\ll'$ is similar to that used in \cite[Example 32]{33ex}, % and \cite{nat-term}. % % and indeed our main theorem has apparent % % similarities to the recursive path orderings and the general path ordering of % % Dershowitz \cite{nat-term}. % % However, as we showed above, our theorem is not limited to simplification % % orderings, whereas the general path ordering and recursive path orderings % % are simplification orderings. % end of comment: Insertion sort} \subsection{The factorial example} \label{s-fact-ex} Example 21 of \cite{33ex} is almost the usual definition of the factorial function, but modified so that we can not use a simplification ordering. The rules are $$ \begin{array}{rcl@{\qquad\qquad}rcl} P(S(x)) & \longrightarrow & x & F(0) & \longrightarrow & 0 \\ F(S(x)) & \longrightarrow & S(x) \times F(P(S(x))) & 0 \times y & \longrightarrow & 0 \\ S(x) \times y & \longrightarrow & x \times y + y & x + 0 & \longrightarrow & x \\ x + S(y) & \longrightarrow & S(x + y) & & & \end{array} $$ As usual we define a (transitive) ordering $<_h$ where terms are compared by comparing their head symbols, using the following ordering: $ F > \times > + > S$, and also $F > P$. But we need to define $\ll'$ to be the union of $<_h$ and the following additional cases $$F(S(x)) \gg' F(P(S(x))) \qquad F(S(x)) \gg' F(P(x))$$ We can not use a simplification ordering because if we allowed $P(x) \longrightarrow x$ the system would not terminate, but would ``cycle'' between terms containing $F(S(x))$ and terms containing $F(P(S(x)))$. We do, however, need to add the rule $S(x) \longrightarrow x$. The proofs of termination given in \cite[Examples 21, 25]{33ex} are based on interpreting arguments to the function symbols as natural numbers. To verify Condition~\ref{rpc-csl}\ref{csl'}, it is reasonably easy to see that for each $(r', l)$ where $l \rightarrow r$ is a rewrite rule and $r'$ is a subterm of $r$, we have one of the following cases: \begin{itemlist} \item $r'$ is a proper subterm of $l$ \item $r' <_h l$ \item $r'$ is $l$, but with $S$ removed from a subterm (to give $r' <_{sn1} l$) \item $r'$ is $F(P(S(x)))$ and $l$ is $F(S(x))$ (so $r' \ll' l$). \end{itemlist} It is easy to see that $\ll'$ is well-founded. To show that $\ll' \cup <_{sn2}$ is well-founded we need to use a more general case of Lemma~\ref{wf-rs} than hitherto. In fact we show $\ll' \circ <_{sn2} \ \subseteq\ (<_{sn2}^* \circ \ll')\ \cup <_{sn2}^+$, which implies \ref{dvk} of Lemma~\ref{wf-rs}. Suppose $t \gg' u >_{sn2} v$. We consider the cases for $t \gg' u$. \begin{itemlist} \item If $t >_h u$ then clearly $t >_h v$, as $u$ and $v$ have the same head symbol. \item Suppose $t = F(S(x))$ and $u = F(P(S(x)))$ or $u = F(P(x))$. \begin{itemlist} \item If $u >_{sn2} v$ by way of reducing the $x$ in $u$ to $x'$ (reducing a strongly normalising subterm of $x$), then % we have $x \in \SN$ and so $t = F(S(x)) >_{sn2} F(S(x')) \gg' v$. \item Otherwise we need to consider specific cases: \begin{itemlist} \item[$u$] $ = F(P(S(x)))$, $S(x) \longrightarrow x$ where $S(x) \in \SN$, $v = F(P(x))$: \\ in this case, $t \gg' v$ \item[$u$] $ = F(P(S(x)))$, $P(S(x)) \longrightarrow x$ where $P(S(x)) \in \SN$, $v = F(x)$: \\ as $S(x) \longrightarrow x$ and $S(x) \in \SN$, we have $t >_{sn2} v$ \item[$u$] $ = F(P(x))$, where $x = S(y)$, $P(S(y)) \longrightarrow y$ and $P(S(y)) \in \SN$, $v = F(y)$: as $S(y) \longrightarrow y$ and $S(y) \in \SN$, \\ so $t = F(S(S(y)) >_{sn2} F(S(y)) >_{sn2} F(y) = v$. \end{itemlist} \end{itemlist} \end{itemlist} Thus $\ll' \cup <_{sn2}$ is well-founded and the system terminates by Theorem~\ref{thm-csl}. % \comment{ % \subsection{Semantic Path Ordering Example} % Example 31 of \cite{33ex} uses some rules from % \S\ref{s-diff}, but with an extra rule which prevents the recursive path % ordering from being used. % It can be shown to terminate using the ``semantic path ordering'' of % Kamin \& Levy \cite{kl,fz}. % The rules are % \begin{eqnarray*} % (x \times y) \times z & \longrightarrow & x \times (y \times z) \\ % (x + y) \times z & \longrightarrow & x \times z + y \times z \\ % z \times (x + f(y)) & \longrightarrow & g(z,y) \times (x + a) % \end{eqnarray*} % We add the same simplification rewrite rules as in \S\ref{s-diff}, % but we must also add the following rule to guarantee Condition~2(a): % $ f(y) \longrightarrow a $. % We then define $\ll'$ as the union of the orders $<_h$ (which % depends on the head symbol), and $<_\times$ and $<_g$. % The ordering of symbols for $<_h$ has $\times > \{+, g, a\}$ % For $<_\times$ and $<_g$, we have % \begin{eqnarray} % \label{31x} x \times u + y & >_\times & x \times z \\ % \label{31g1} z \times (x + f(y)) & >_{g} & g(z', y') \times (x + a) \\ % \label{31g2} z \times (x + f(y)) & >_{g} & g(z', y') \times x \\ % \label{31g3} z \times (x + f(y)) & >_{g} & g(z', y') \times a % \end{eqnarray} % We now prove that this rewrite system terminates. % To show that $\ll'$ is well-founded we note that % $<_\times$ is well-founded as the $x$ appearing in rule (\ref{31x}) % for $<_\times$is a proper subterm of $x \times u$, and % the proper subterm relation is % well-founded. % Clearly $<_g$ is well-founded, % and we notice that $<_g \circ <_\times = \emptyset$ since % $g(z', y')$ cannot match $x \times u$. % It follows easily that $\ll'$ is well-founded. % To show that $\ll' \cup <_{sn1}$ is well-founded, % we use Lemma~\ref{wf-rs}\ref{tco}, showing % that $\ll' \circ <_{sn2} \ \subseteq\ <_{sn2}^* \circ \ll'$, % as previously. % Supposing $t \gg' u >_{sn2} v$, % the only difficult case is where a proper subterm $u'$ of $u$ % is rewritten to get a corresponding subterm of $v$, % and $u'$ matches % a non-variable subterm of the right-hand side of a rule for $<_{g}$. % The only case where this happens is in rule (\ref{31g1}), where % $(x + a)$ can be rewritten to get $x$ or $a$. % In these cases, $t >_g v$ by rules (\ref{31g2}) or (\ref{31g3}): % these rules are included only for this reason. % It is easy to see that Condition~\ref{csl04-rpc1} is satisfied, and so % the rewrite system terminates by Theorem~\ref{thm:all-sn}. % } \newpage \section{Modular Proofs of Termination} \label{s-inc} A rewrite system can be defined by taking the union of two terminating systems. It is desirable to reduce a proof of termination of such a system into two smaller proofs of termination of smaller systems, which is possible under certain conditions (see, eg, \cite[\S 9.2]{baader-nipkow}, \cite{tkb-termination}, \cite{fgr-incremental}), but not in general. We show how to use Theorem~\ref{thm-csl} in certain cases to obtain modular proofs of termination. The assumptions required of the component systems appear where they first become relevant, and in Theorem~\ref{thm-incr-pf}. Let $\mathcal{R}_0$ be a set of rewrite rules, in a first-order language,\ where the function symbols appearing in the rules are from the set $\mathcal{F}_0$. Note, however, that the variables appearing in those rules may be replaced by any term (which may contain function symbols outside $\mathcal{F}_0$). The set of substitution instances of the rules in $\mathcal{R}_0$ is the relation $\sigma_0$, with corresponding rewrite relation $\rho_0 = \ctxt\ \sigma_0$. We consider the case where the rewrite relation $\rho_0$ has been proved terminating by any method, with only the extra condition that the rules of $\mathcal{R}_0$ be \emph{right-linear}: that is, no variable appears more than once on the right-hand side of a rule. This is a similar but stronger condition than the ``non-duplicating'' requirement of some modularity theorems (eg, \cite[Thm~9.2.4]{baader-nipkow}). Thus we define the \textit{$\mathcal{R}_0$-property}, (in which \ref{lhs-notvar} and \ref{rhs-nonew} are obviously necessary for any terminating system), and assume throughout that $\mathcal{R}_0$ satisfies it. The \emph{$\mathcal{R}_0$-property} is important for the next lemma. \begin{definition}[\textit{$\mathcal{R}_0$-property}] % in Isabelle, (i), (iii), (iv) are rule0_prop, (ii) is rule0_hd_S, % (i) to (iv) are rule0_proph A rule satisfies the $\mathcal{R}_0$-property if \begin{romanlist} \item its function symbols are in the set $\mathcal{F}_0$ \item \label{lhs-notvar} its left-hand side is not a variable \item \label{rhs-nodup} no variable appears more than once in the right-hand side \item \label{rhs-nonew} its right-hand side variables also appear on the left-hand side. \end{romanlist} \end{definition} \newcommand\ot{\overline t} \newcommand\os{\overline s} \begin{lemma} \label{lem-r0p} Let $\sigma$ be the set of substitution instances of a set of rules satisfying the $\mathcal{R}_0$-property. Then \begin{romanlist} \item \label{r0p-f1sub} For $f \not\in \mathcal{F}_0$ and $(t, s) \in \sigma$, if $t' = f (\ot) \vtl^* t$ then $t' \vtl^+ s$. \item \label{wfh-lem3b} Let $\tau$ be a relation such that for $(t, f (\ot)) \in \tau$, $f \not\in \mathcal{F}_0$. \\ Then $\sigma \circ \pctxt\ \tau \subseteq (\pctxt\ \tau)^* \circ \sigma$. \end{romanlist} \end{lemma} We then consider a second rewrite system $\rho_1 = \ctxt\ \sigma_1$ whose ``defined symbols'' are from a set of new symbols $\mathcal{F}_1$, where $\mathcal{F}_0 \cap \mathcal{F}_1 = \emptyset$. That is, for $(t, s) \in \sigma_1$, $s$ is of the form $f (\os)$, for some $f \in \mathcal{F}_1$ and some sequence $\os$ of terms. Note that, unlike in some modularity theorems (eg, \cite[Thm~9.2.4]{baader-nipkow}), rules used to define $\rho_1$ may contain symbols from $\mathcal{F}_0$. The system $\rho_1$ is assumed to have been proved terminating using Theorem~\ref{thm-csl} above: that is, by defining a relation $\ll_1'$ % (ie, the ``$<_{cut}$'' of \cite{dggt}), such that \mbox{$\ll_1 \ =\ \ll_1' \cup <_{sn1}$} is well-founded, where $<_{sn1}$ is defined in terms of $\rho_1$ only. Then let $\rho = \rho_0 \cup \rho_1$. Our proof involves ${<_{sn2}}$, as described after Theorem~\ref{thm-csl}. The key is to define a relation $\ll'$: we use \mbox{$\ll' \ =\ \ll_0' \cup \ll_1'$}, where $\ll_0'$ is a relation derived from $\mathcal{R}_0$. To help prove \mbox{$\ll' \circ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$} we assume $\ll_1'$ satisfies the \emph{$\ll_1'$-property}: \begin{definition}[\textit{$\ll_1'$-property}] \label{ll1-prop} A relation $\ll_1'$ satisfies the $\ll_1'$-property if, for \emph{any} relation $\sigma$, \mbox{$\ll_1' \circ\ \pctxt\ \sigma \subseteq\ (\pctxt\ \sigma)^*\ \circ \ll_1'$}. \end{definition} In fact, the $\ll_1'$-property could be weakened, to apply only to certain choices of $\sigma$, and to match (d) instead of (a) of Lemma~\ref{wf-rs}, and Theorem~\ref{thm-incr-pf} still holds. The example in \S\ref{s-fact-ex} satisfies only the weaker condition. To define $\ll_0'$ we first define $\vtl_0$ and $\ctxt_0$, and then a set of rules $\mathcal{R}_{\ll 0}$: \begin{definition}[$\vtl_0$] \label{def-vtl0} % subt_S in Isabelle $t \vtl_0 f(\ldots, t, \ldots)$ if $f \in \mathcal{F}_0$. \end{definition} \begin{definition}[$\ctxt_0$] \label{def-ctxt0} % ctxt_S in Isabelle For $(t, s) \in \sigma$, if the subterms of $C[x]$ which contain $x$ have head symbols in $\mathcal{F}_0$ then $(C[t], C[s]) \in \ctxt_0\ \sigma$. \end{definition} \begin{definition}[$\mathcal{R}_{\ll 0}$] % cut0 in Isabelle $(r_0', l_0) \in \mathcal{R}_{\ll 0}$ iff $r_0'$ is not a variable and there exists $r_0$ such that $r_0' \vtl^*_0 r_0$, $(r_0, l_0) \in \ctxt_0\ \mathcal{R}_0$ and $(r_0, l_0)$ satisfies the $\mathcal{R}_0$-property. \end{definition} Then let $\ll_0'$ be the set of substitution instances of the rules in $\mathcal{R}_{\ll 0}$. Clearly $\ll_0'\ \subseteq (\rho_0\ \cup \vtl)^+$ so $\ll_0'$ is well-founded. We now can define $\ll' \ =\ \ll_0' \cup \ll_1'$. If we assume that for $t \ll_1' f (\ot)$, $f \in \mathcal{F}_1$, and that $\ll_1'$ is well-founded, then $\ll'$ is well-founded as \mbox{$\ll_0' \circ \ll_1' \ =\ \emptyset$}. Then let $\ll \ =\ \ll' \cup <_{sn2}$. Since $<_{sn2}$ is well-founded (Theorem~\ref{thm-sn12wf}), to show that $\ll$ is well-founded it would suffice to show \mbox{$\ll' \circ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$}, but this does not actually hold. Instead, we can choose a suitable subset $<'_{sn2}$ of $<_{sn2}$ such that $\ll \ =\ \ll' \cup <'_{sn2}$ and prove that $\ll$ is well-founded in two steps. We define $\tau_1$: $(t, f (\ot)) \in \tau_1$ iff $f \not\in \mathcal{F}_0$. Recall that $SN$ means the set of strongly normalising terms, ie $SN = \wfp\ (\ctxt\ \rho)$, where $\rho = \rho_0 \cup \rho_1$. We define $\rho_{SN}$: $(t, s) \in \rho_{SN}$ iff $s \in SN$. Thus $<_{sn2} \ = \pctxt\ (\sigma \cap \rho_{SN})$. Then the required relation $<'_{sn2}$ is given in the following lemma, whose proof is detailed but tedious, and which has been proved in Isabelle (\cite{jdisa}, file {\tt hier.ML}), as have all these results. \begin{lemma} \label{lem-wfh-lem2,5'} Let % $<'_{sn2}$ is sn2_alt in Isabelle $<'_{sn2}\ = \ctxt\ (\tau_1 \ \cap\ \pctxt\ (\sigma_0 \cap \rho_{SN}))\ \cup\ \pctxt\ (\sigma_1 \cap \rho_{SN})$. Let $\mathcal{R}_0$ satisfy the \emph{$\mathcal{R}_0$-property}. Then $<'_{sn2} \ \subseteq\ <_{sn2} \ \subseteq\ \ll_0' \cup <'_{sn2}$. \end{lemma} \begin{lemma} \label{lem-llwf} Assume hypotheses \ref{r0p}, \ref{ll1p} and \ref{h1} of Theorem~\ref{thm-incr-pf} below. Then \begin{romanlist} % \item $\ll_1' \circ\ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll_1'$. \item \label{ll1-sn2-wf} $\ll_1' \cup <_{sn2}$ is well-founded; so $\ll_1' \cup <'_{sn2}$ is well-founded. \item \label{wfh-lem3} $\ll_0' \circ\ \tau_1 \ =\ \emptyset$ (so $\ll_0' \circ \ll_1' \ =\ \emptyset$) and $\ll_0' \circ <'_{sn2}\ \subseteq\ {<'_{sn2}}^*\ \circ \ll_0'$. \item \label{wfh-epr} $\ll_0' \cup\ (\ll'_1 \cup <'_{sn2})$, that is, $\ll$, is well-founded. \end{romanlist} \end{lemma} {\bf Proof.} \begin{romanlist} \item This follows from Lemma~\ref{wf-rs}\ref{tco} as $\ll_1'$ satisfies the $\ll_1'$-property. \item Recall that, for $f (\ot) \ll_0' s$, $f \in \mathcal{F}_0$, so $\ll_0' \circ\ \tau_1 \ =\ \emptyset$. Then we use the fact that $<'_{sn2}$ is of the form $(\tau_1 \cap X) \cup \pctxt\ Y \cup \pctxt\ Z$ and Lemma~\ref{lem-r0p}\ref{wfh-lem3b}. \item As $\ll_0'$ and, by \ref{ll1-sn2-wf}, $\ll'_1 \cup <'_{sn2}$ are well-founded, we can use \ref{wfh-lem3} and Lemma~\ref{wf-rs}\ref{tco} to get that $\ll_0' \cup\ (\ll'_1 \cup <'_{sn2})$ is well-founded. Then, by Lemma~\ref{lem-wfh-lem2,5'}, this is \mbox{$\ll_0' \cup\ (\ll'_1 \cup <_{sn2}) \ =\ \ll' \cup <_{sn2} \ = \ \ll$}. \hfill$\Box$ \end{romanlist} \begin{lemma} \label{rp-pc-cut0} If $\mathcal{R}_0$ satisfies the \emph{$\mathcal{R}_0$-property}, $\sigma_0$ and $\ll_0'$ satisfy Condition~\ref{rpc-csl}\ref{csl'}. \end{lemma} {\bf Proof.} Let $(t, s) \in \sigma_0$, an instance of the rule $(t_0, s_0) \in \mathcal{R}_0$, and let $t' \vtl^* t$. If $t' \vtl_0^* t$, then $(t', s) \in\ \ll_0'$. Otherwise, there must be $f \not \in \mathcal{F}_0$ and a sequence $\ot$ of terms with $t' \vtl^* f (\ot) \vtl^* t$, and so, by Lemma~\ref{lem-r0p}\ref{r0p-f1sub}, \mbox{$t' \vtl^* f (\ot) \vtl^+ s$}, as required.$\Box$ \begin{theorem} \label{thm-incr-pf} Assume that \begin{romanlist} \item \label{r0p} rules $\mathcal{R}_0$ satisfy the $\mathcal{R}_0$-property, and give a terminating rewrite system $\rho_0$, \item \label{ll1p} relation $\ll_1'$ is well-founded and satisfies the $\ll_1'$-property, \item \label{c2b} $\sigma_1$ and $\ll_1'$ satisfy Condition~\ref{rpc-csl}\ref{csl'}, \item \label{h1} for $(t, s) \in \sigma_1\ \cup \ll_1'$, $s$ is of the form $f (\os)$, with $f \not\in \mathcal{F}_0$. \end{romanlist} Then $\rho = \rho_0 \cup \rho_1$ is well-founded where $\rho_1 = \ctxt\ \sigma_1$. \end{theorem} \proof{ From assumption \ref{c2b} and Lemma~\ref{rp-pc-cut0}, we can see that {$\sigma_0 \cup \sigma_1$ and $\ll_0' \cup \ll_1'$} satisfy Condition~\ref{rpc-csl}\ref{csl'}. Then, since, by Lemma~\ref{lem-llwf}\ref{wfh-epr}, \mbox{$\ll \ =\ \ll_0' \cup \ll_1' \cup <_{sn2}$} is well-founded, and \mbox{$<_{sn1}\ \subseteq\ <_{sn2}$}, the result follows from Theorem~\ref{thm-csl}. } \section{An Incremental Path Ordering} \label{s-ipo} \newcommand{\ipo}{\textit{ipo}} We now use the previous results to describe a generalisation to an incrementally defined ordering of the general path ordering of Dershowitz \& Hoot \cite{nat-term}. The incremental path ordering $<_{ipo}$ or \ipo\ (``modular path ordering'' could be used but $mpo$ also stands for ``multiset path ordering'') is then defined as below, where $\overline s = s_1, \ldots, s_m$, $\overline t = t_1, \ldots, t_n$, $s = f(\overline s)$ and $t = g(\overline t)$. Let $\Lambda({\ipo})$ (or $<_{\Lambda}$) be an ordering on lists of terms, derived from $<_{ipo}$, satisfying conditions given later: the common examples for $\Lambda$ are the lexicographic or multiset extensions of $<_{ipo}$. As before, the rules $\mathcal{R}_0$ satisfy the $\mathcal{R}_0$-property. Again, let $\sigma_0$ be the set of substitution instances of the rules in $\mathcal{R}_0$, and let the corresponding rewrite relation $\rho_0 = \ctxt\ \sigma_0$ be well-founded. Let $<$ be a well-founded ordering on the function symbols. \begin{gather} \label{ipo-sub} \frac { f \not \in \mathcal{F}_0 \qquad s_i \geq_{ipo} t } { s >_{ipo} t } \\[1ex] \label{ipo-der} \frac { f = g \quad \overline s >_\Lambda \overline t \quad f \not \in \mathcal{F}_0 \quad \forall i \in \{1, \ldots, n\}.\ s >_{ipo} t_i } { s >_{ipo} t } \\[1ex] \label{ipo-symb} \frac { f > g \quad f \not \in \mathcal{F}_0 \quad \forall i \in \{1, \ldots, n\}.\ s >_{ipo} t_i } { s >_{ipo} t } \\[1ex] \label{ipo-0} \frac { (t, s) \in \sigma_0 } { s >_{ipo} t } \\[1ex] \label{ipo-pctxt} \frac { (t, s) \in \pctxt\ \ipo } { s >_{ipo} t } \end{gather} Rules (\ref{ipo-pctxt}) and (\ref{ipo-0}) imply $\rho_0 = \ctxt\ \sigma_0 \ \subseteq\ <_{ipo}$ and that $ipo$ is closed under contexts. In the Isabelle formulation $ipo$ is an inductively defined set, where $ipo$ is the set of all pairs whose inclusion in $ipo$ is established by the rules given. Note that if $\mathcal{F}_0$, and so $\mathcal{R}_0$ and $\sigma_0$ are empty, then this reduces to the recursive path ordering. In that case, if $\Lambda$ is the lexicographic or multiset ordering, then rule (\ref{ipo-der}) implies (\ref{ipo-pctxt}). Also, in that case, the rules themselves imply that the defined path ordering is transitive, and this fact is used in some proofs of well-foundedness (see, eg, \cite{nat-term}). But when $\mathcal{F}_0$, $\mathcal{R}_0$ and $\sigma_0$ are non-empty, it does not seem clear whether $<_{ipo}$ is transitive, and our proof of termination does not depend on it. As in \cite{dggt}, we define a function \fwf\ (``from well-founded'') which maps a binary relation $\sigma$ to a binary relation $\fwf\ \sigma$ thus: $(t, s) \in \fwf\ \sigma$ iff $(t, s) \in \sigma$ and $s \in \wfp\ \sigma$. Our proof needed the following conditions on $\Lambda$. Related conditions are discussed in \S\ref{s-gpo}. All are satisfied by the lexicographic and multiset extensions of an ordering. \begin{alphlist} \item \label{ipo-lam-mono} ${\Lambda}$ is a monotonic function \item \label{ipo-lam-wf} if $\sigma$ is well-founded then ${\Lambda (\sigma)}$ is well-founded \item \label{ipo-lam-psubt} if all $s_i$ are in $\wfp\ \tau$ and if $(t, s) \in \Lambda (\tau)$, then $(t, s) \in \Lambda (\fwf\ \tau)$ \item \label{ipo-lam-one} if $(s_i', s_i) \in \tau$ then $((s_1, \ldots, s_i', \ldots s_m),$ $ (s_1, \ldots, s_i, \ldots s_m)) \in \Lambda(\tau)$. \end{alphlist} The termination proof combines the proof of Theorem~\ref{thm-incr-pf} above with ideas from the termination proof of the recursive path ordering in \cite[\S 3.7]{dggt}. We omit details, but note that it has been checked using Isabelle, see \cite{jdisa}, in {\tt snabs/ipodef.\{thy,ML\}}. \begin{theorem} \label{thm-ipo} The relation $<_{ipo}$ is well-founded if: \begin{romanlist} \item \label{ipo-r0p} rules $\mathcal{R}_0$ satisfy the $\mathcal{R}_0$-property, and give a terminating rewrite system $\rho_0 = \ctxt\ \sigma_0$, \item \label{symo} the relation $<$ on the function symbols (see rule (\ref{ipo-symb})) is well-founded, and \item \label{lambda} the ordering extension function $\Lambda$ satisfies conditions (a)-(d) listed above. \end{romanlist} \end{theorem} \section{Observations and Conclusion} Our main Theorem~\ref{thm-allsn} about termination of reduction rules generalises two previous quite general theorems~in \cite{dggt} and the first theorem (JGL1) in \cite{jgl}. The following picture emerges. JGL1, i.e.\ Goubault-Larrecq's Theorem~1 \cite{jgl}, can handle ARSs but cannot handle reducibility arguments like those required for combinators or the simply-typed $\lambda$-calculus. Our Theorem~\ref{thm-csl}, i.e.\ \cite[Theorem~2]{dggt}, handles TRSs but also cannot handle such reducibility arguments. Our new Theorem~\ref{thm-allsn} handles both TRSs and some reducibility arguments such as those involved in the proofs of termination of the typed combinator systems. One of our proofs takes advantage of the abstract setting, using a relation $\vtl$ which is \emph{not} the usual immediate subterm relation. However our theorem had to be modified to reason indirectly about substitutions for the simply-typed $\lambda$-calculus. What is the exact relationship between \cite[Theorem~2]{jgl} and our Theorem~\ref{thm-allsn}~? Our Theorem~\ref{thm-allsn} can be used to prove termination of a rewrite system defined incrementally. We showed in \cite{dggt} that our Theorem~\ref{thm-allsn} strictly subsumes the termination of the recursive path ordering. Since \cite{fgr-incremental} contains a very general set of results which are nonetheless based on the recursive path ordering, neither \cite{fgr-incremental} nor the work in \S\ref{s-ipo} subsume each other. A goal is to unify the work in \S\ref{s-ipo} and \cite{fgr-incremental}. Our proofs were machine-checked in Isabelle/HOL. This was particularly valuable for \S\ref{s-inc}, where our initial paper proofs turned out to be wrong, as the correct choice of $\ll_2'$ was particularly difficult to find. Further, the possible instantiation of a variable by a term headed by a symbol in either $\mathcal{F}_0$ or $\mathcal{F}_1$ complicated matters as discussed following \cite[Proposition~1]{fgr-incremental}. Also, in \S\ref{s-tc} the Isabelle proof confirmed the validity of the rather tricky argument for the soundness of the mutually recursive definitions of $SN$, $\rho$ and $\tau$. \nonumsection{Acknowledgements} We thank Linda Postniece for researching the criteria for well-foundedness of a union of well-founded orderings, Jean Goubault-Larrecq and Hubert Comon for pointers to the literature, and Thorsten Altenkirch and J\"urgen Giesl for helpful discussions. Finally, we thank some anonymous referees for very helpful comments. \nonumsection{References} \bibliographystyle{plain} \begin{thebibliography}{99} \bibitem{akama-trans} Y~Akama. A $\lambda$-to-CL Translation for Strong Normalization. % Yohji Akama. A $\lambda$-to-CL Translation for Strong Normalization. In Proc.\ Typed Lambda Calculi and Applications (TLCA'97), LNCS 1210, 1--10, Springer, 1997. \bibitem{altenkirch-Tait} T~Altenkirch and J~Chapman. Tait in one big step. % Thorsten Altenkirch and James Chapman. Tait in one big step. % Mathematically Structured Functional Programming (MSFP 2006). In Proc.~MSFP 2006, Electronic Workshops in Computing, British Computer Society, 2006. \bibitem{dps00} T~Arts and J~Giesl. % Thomas Arts and J\"urgen Giesl. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236 (2000), 133--178, 2000. \bibitem{baader-nipkow} F~Baader and T~Nipkow. % Franz Baader and Tobias Nipkow. Term Rewriting and All That. CUP, 1998 \bibitem{bfr} C~Borralleras, M~Ferreira and A~Rubio. Complete Monotonic Semantic Path Orderings. In Proc.\ CADE-17, LNCS 1831, 346--364, Springer, 2000. \bibitem{buchholz-pta} W~Buchholz. % Wilfried Buchholz. Proof-theoretic analysis of termination proofs. Annals of Pure and Applied Logic 75 (1995), 57--65. \bibitem{dawson-gore-machine-checked-strong-normalisation} J~E~Dawson and R~Gor{\'e}. % Jeremy~E.~Dawson and Rajeev Gor{\'e}. A New Machine-checked Proof of Strong Normalisation for Display Logic. In Computing: The Australasian Theory Symposium, 2003, Electronic Notes in Theoretical Computer Science 78, 16--35, Elsevier. \bibitem{dggt} J~E~Dawson and R~Gor{\'e}. % Jeremy~E~Dawson and Rajeev Gor{\'e}. A General Theorem on Termination of Rewriting. \newblock In Proc.\ Computer Science Logic (CSL 2004), LNCS 3210, 100--114, 2004. \bibitem{jdisa} J~E~Dawson. Isabelle code, \newblock \url{http://web.rsise.anu.edu.au/~jeremy/isabelle} \bibitem{33ex} N~Dershowitz. 33 Examples of Termination. % Nachum Dershowitz. 33 Examples of Termination. In Proc. French Spring School of Theoretical Computer Science (1993), LNCS 909, 16--25, Springer 1995. \bibitem{dersh-har} N~Dershowitz \& D~A~Plaisted. % Nachum Dershowitz \& David A~Plaisted. Rewriting. In Alan Robinson \& Andrei Voronkov, eds, Handbook of Automated Reasoning, 535--610, Elsevier, 2001. \bibitem{dersh-td} N~Dershowitz. Termination Dependencies (Extended Abstract). In Proc.\ Sixth Int'l Workshop on Termination (WST '03), A~ Rubio, ed., Valencia, Spain, pp. 27--30. \bibitem{nat-term} N~Dershowitz \& C~Hoot. Natural Termination. TCS 142 (1995), 179--207. \bibitem{dvk} H~Doornbos \& B~Von Karger. % Henk Doornbos \& Burghard Von Karger. On the Union of Well-Founded Relations. L. J. of the IGPL 6 (1998), 195--201. \bibitem{dummett} M~A~E~Dummett. Elements of intuitionism. Clarendon Press, 1977. \bibitem{fgr-incremental} M-L~Fern\'andez, G~Godoy, A~Rubio. % Mirtha-Lina Fern\'andez, Guillem Godoy, Albert Rubio. Recursive Path Orderings Can Also Be Incremental. In Proc.\ LPAR2005, LNCS 3835, 230--245, Springer, 2005. \bibitem{fissore-gnaedig-kirchner-termination} {O~Fissore, I~Gnaedig and H~Kirchner}. Termination of Rewriting with Local Strategies. Electronic Notes in Theoretical Computer Science 58, 2001. \bibitem{giesl-mod-term} J~Giesl, T~Arts, and E~Ohlebusch. Modular Termination Proofs for Rewriting Using Dependency Pairs. Journal of Symbolic Computation 34(1):21--58, 2002. \bibitem{glt} J-Y~Girard, Y~Lafont and P~Taylor. % Jean-Yves Girard, Yves Lafont and Paul Taylor. Proofs and Types. CUP, 1990. \bibitem{gnaedig-kirchner-properties} {I~Gnaedig and H~Kirchner}. % {Isabelle Gnaedig and H{\'e}l{\`e}ne Kirchner}. {Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations}, %In {Rewriting, Computation and Proof}. LNCS 4600, 44--67, Springer, 2007. \bibitem{jgl} J~Goubault-Larrecq. Well-founded recursive relations. In Proc.\ CSL'2001, LNCS 2142, 484--497, Springer, 2001. \bibitem{hm-dpr} N~Hirokawa and A~Middeldorp. % Nao Hirokawa and Aart Middeldorp. Dependency Pairs Revisited. In Proc.\ Rewriting Techniques and Applications (RTA-04), LNCS 3091, 249--268, Springer, 2004. \bibitem{kv} S~C~Kleene and R~E~Vesley. The foundations of intuitionistic mathematics: especially in relation to recursive functions. North-Holland, 1965. \bibitem{tkb-termination} {Y~Toyama and J~W~Klop and H~P~Barendregt}. {Termination for direct sums of left-linear complete term rewriting systems}. J of the ACM 42(6):1275--1304, 1995. \end{thebibliography} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: