%% %% \documentclass{CRPITStyle} % \documentclass{llncs} %\documentclass[a4paper,11pt,twocolumn]{article} %\usepackage{makeidx} %\usepackage{acmnew-xref} % \usepackage[scrtime]{prelim2e} \usepackage{latexsym} \usepackage{amssymb} \usepackage{amsmath} % \usepackage{exptrees} \usepackage{url} %\RequirePackage{mathptm} %\RequirePackage{times} %\RequirePackage{palatino} \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}{\texttt{gindy}} \newcommand{\indy}{\texttt{indy}} \newcommand{\gbars}{\texttt{gbars}} \newcommand{\bars}{\texttt{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\cfile{} \newcommand\comment[1]{} \newcommand\isabelle[1]{} % \newcommand\cc[1]{} % for label names \newcommand\cc[1]{#1} % for label names % \renewcommand\footnote[1]{} % for footnotes % \pagestyle{myheadings} % \newcommand{\mystrut}[1]{ % \bpf \A ; "$\vphantom{X}$" \U ['] ; "$\vphantom{X}$" "#1" \epf \ % % } \newcommand{\idrule}[2]{ \mbox{#1 \ $\mbox{#2}$}} \newcommand{\ds}{\displaystyle\strut} \newcommand{\urule}[3]{ \mbox{#1 \ $\frac{\ds \mbox{#2}}{\ds \mbox{#3}}$}} \newcommand{\brule}[4]{ \mbox{#1 \ $\frac{\ds \mbox{#2}\ \ \ \ \mbox{#3}} {\ds \mbox{#4}}$}} \newcommand\invrule[2]{ % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline \hline $ #2 $ \end{tabular}} \newcommand\slrule[2]{ % similar to \frac, except % for use in non-math mode, args interpreted in math mode \begin{tabular}{@{}c@{}} $ #1 $ \\ \hline $ #2 $ \end{tabular}} \renewcommand\theenumi{(\alph{enumi})} \renewcommand\labelenumi{\theenumi} \renewcommand\theenumii{(\roman{enumii})} \renewcommand\labelenumii{\theenumii} %\newcommand\proof{\noindent\textbf{Proof.}} \newcommand\src[1]{source file \texttt{#1}} \newcommand\apsrc[1]{Appendix \ref{app:code}} %\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})} \newcommand\seesrc[1]{(see source file \texttt{#1})} %\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})} \newcommand\insrc[1]{in source file \texttt{#1}} \newcommand\page[1]{page~\pageref{#1}} \newcommand\fig[1]{Fig.~\ref{fig:#1}} \newcommand\ch[1]{Chapter~\ref{ch:#1}} \newcommand\tbl[1]{Table~\ref{tbl:#1}} \newcommand\thrm[1]{Theorem~\ref{thrm:#1}} \newcommand\lem[1]{Lemma~\ref{lem:#1}} \newcommand\ttl[1]{\tti{#1}\label{#1}} \newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}} \newcommand\ttdef[1]{\texttt{#1}\tti{#1}} \newcommand\tti[1]{\index{#1@\texttt{#1}}} \newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}} \newcommand\up[1]{\vspace{-#1ex}} \newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree \newcommand\cut{(\emph{cut})} \newcommand\dt{\texttt{dt}} \newcommand\dtn{\texttt{dtn}} \newcommand{\pordered}[3]{#1 <_{{#2}} #3} \newcommand{\Revpordered}[3]{#1 >_{{#2}} #3} \newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}} \newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}} \newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}} \newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}} \newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 \newtheorem{condition}{Condition} % automatically defined in LLNCS style %\newtheorem{thm}{Theorem}%[chapter] %\newtheorem{lemma}[thm]{Lemma} \newtheorem{theorem}{Theorem} \newtheorem{definition}{Definition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \newenvironment{proof}{{\it Proof.}}{} \newcommand\qed{\hfill$\Box$} %\renewcommand\thecor{\thethm(\arabic{cor})} \pagestyle{plain} \begin{document} %% Here begins the main text \title{Termination of Abstract Reduction Systems} \author{ Jeremy E.\ Dawson \ \ and \ \ Rajeev Gor\'e } \affiliation{ Logic and Computation Program, NICTA\thanks{National ICT Australia is funded by the Australian Government's Dept of Communications, Information Technology and the Arts and the Australian Research Council through \textit{Backing Australia's Ability} and the ICT Research Centre of Excellence programs.} and \\ Automated Reasoning Group \\ Australian National University, Canberra, ACT 0200, Australia \\ \texttt{Jeremy.Dawson@nicta.com.au} \ \ \texttt{Rajeev.Gore@anu.edu.au} } \date{\today} %% Title \maketitle \toappear{Copyright copyright 2007, Australian Computer Society, Inc. This paper appeared at Computing: The Australasian Theory Symposium (CATS2007), Ballarat, Australia. Conferences in Research and Practice in Information Technology (CRPIT), Vol. 65. Joachim Gudmundsson and Barry Jay, Eds. Reproduction for academic, not-for profit purposes permitted provided this text is included.} \begin{abstract} \comment{ old abstract We take our previous theorem showing the well-foundedness (termination) of certain rewrite orderings, and generalise this to abstract reduction relations. We show how this implies a very general theorem of Goubault-Larrecq. We consider constricting derivations, which provide an alternative proof of our theorem for monotonic orderings, and we show how our theorem covers the general path ordering of Dershowitz \& Hoot. Next, we show how to adapt our proof to prove Goubault-Larrecq's second general theorem for higher-order path orderings. Finally, we discuss how our theorem applies to the termination of reduction of well-typed combinator expressions, and how it can be adapted to show the strong normalisation of the simply-typed $\lambda$-calculus. } 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. % and the simply-typed lambda calculus. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. % and can be modified to handle the simply-typed $\lambda$-calculus. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. % general theorem due to Jean Goubault-Larrecq. All proofs have been formally machine-checked in % the theorem prover Isabelle/HOL. \\ {\bf Keywords}: rewriting, termination, well-founded ordering, strong normalisation % $\beta$-reduction, simply-typed $\lambda$-calculus \end{abstract} \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 according to some formal syntax. 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]$. There are several general methods capturing termination of such term rewriting systems % in this common 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 \cite{dps00,nat-term,dggt}. Recently, Jean Goubault-Larrecq \cite{jgl} has proved termination results for the more general setting of an abstract reduction system (ARS) where objects need not have a term structure and so there is no monotonicity assumption or subterm relation. Where proofs for TRSs involve the subterm relation, he uses an arbitrary well-founded relation $\vtl$ in a similar way. 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}. While the theorems from \cite{dggt} and \cite{jgl} use remarkably similar ideas, it was frustrating to see that none actually subsumed the other, even though \cite{dggt} applies to TRSs and \cite{jgl} applies to ARSs. Indeed, there is something in common between the two results: a more general theorem that subsumes both. We first present this more general theorem and its proof in \S\ref{s-tt}. Then, in \S\ref{s-opr}, we show that it generalises \cite[Theorem~1]{jgl} and \cite[Theorem~2]{dggt}, and we discuss its application to constricting derivations. 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 \cite[Theorem~1]{jgl}. 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. In the longer paper \cite{dgtars} we apply our theorem to % constricting derivations and the general path ordering of Dershowitz \& Hoot \cite{nat-term}, 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. % 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. Commonly, a rewrite system can be defined by taking a base system, known to be terminating, and adding new function symbols and rules to it. 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}. Our proofs were formalised and machine-checked in the theorem prover Isabelle/HOL: see \cite{jdisa}, directories {\tt snabs,snlc}. % \url{http://web.rsise.anu.edu.au/~jeremy/isabelle/{snabs,snlc}}. This was particularly valuable for \S\ref{s-inc}, where our initial paper proofs turned out to be wrong, as the choice of $\ll_2'$ was particularly difficult to get right. 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: see the discussion 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$. % Also in \S\ref{s-tc}, the argument for the % soundness of the mutually recursive definitions % of $SN$, $\rho$ and $\tau$ is rather tricky. \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. % When a relation is defined by a set of rewrite rules, 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. % abstract reduction relation. 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{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, % abstract reduction relation, 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. } \subsection{Notation, Terminology, Definitions and Basic Lemmas} \label{s-ntd} \comment{ moved earlier Assume that we have a fixed set of ``objects''. 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$. end of comment moved earlier } We assume 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 will 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$ or $\ll$ we will write $(r, t) \in\ \vtl$, $(t, r) \in\ \vtr$, $r \vtl t$ or $t \vtr r$ interchangeably. % Relations are assumed irreflexive unless the contrary is stated, but % are not assumed transitive even when written using $<_\rho$. 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 the relational composition of relations $\sigma$ and $\rho$: % in the sense that $(r, s) \in \sigma \circ \rho$ that is, $(r, s) \in \sigma \circ \rho$ if there exists $t$ such that $(r, t) \in \rho$ and $(t, s) \in \sigma$. \comment{ moved earlier 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. % When a relation is defined by a set of rewrite rules, It is also usually taken that it is \emph{monotonic}, or \emph{closed under context}, in that where $C[\_]$ is a context (a term with a ``hole''), and $l$ rewrites to $r$, then $C[l]$ rewrites to $C[r]$. % Such a relation is commonly called a \emph{reduction}, such as % the ``$\beta$-reduction'' of the lambda calculus. end of comment moved earlier } In our formal treatment in Isabelle/HOL we used the following inductive definition 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 % (ie, $(t, s) \in \rho$, ie $t >_\rho s$) is in \SN\ then $s \in \SN$. % % That is: for all $s$, % if $\forall t.\,(t, s) \in \rho \Rightarrow t \in \SN$, % then $s \in \SN$. % % It follows that if $s$ cannot be reduced then $s \in \SN$. % \end{definition} Our previous work \cite{dggt}, on term rewriting systems, dealt with the well-founded-ness of the closure under context of a relation called $\rho$. In contrast, we are dealing here with an abstract reduction system, usually calling the reduction relation $\rho$. So %it is to be understood that concepts such as ``strongly normalising'', ``reduction'', etc, relate to $\rho$, and not, even when discussing structured terms, to the closure of $\rho$ under context. Furthermore, in the ARS setting, we use an arbitrary relation where we used the immediate subterm relation in the TRS setting. % as in \cite{jgl}, we call this arbitrary relation $\vtl$. % Therefore if $t \in \SN$ it does not follow that % subterms of $t$ are in \SN. In \cite{dggt} %the term rewriting setting, 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\ \cite[\S 2.2]{dggt}. Clearly, $\SN \subseteq \ISN$. % We now generalise this definition to apply to the arbitrary relation $\vtl$ % in place of the immediate subterm relation \isubt. We now define \gindy\ as a generalised notion of ``inductively'' for an arbitrary relation $\sigma$ in place of the immediate subterm relation \isubt. Use of \gindy\ enables us to express the principle of well-founded induction succinctly: it says that 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 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 more 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 $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{enumerate} \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{enumerate} \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}. % \mbox{} % SPACE HERE \begin{definition}[\wfp, \bars] \label{def-wfp,bars} % Let $\mathcal{U}$ be the universal set of objects. Then \begin{enumerate} \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$ ''). %or $s$ is in the \emph{well-founded part} of $\sigma$ \end{enumerate} \end{definition} Thus $\SN = \wfp\ \rho$ and $\ISN = \gindy\ \isubt\ \SN$. Now from Lemma~\ref{def-gbars} we get the following characterisation of \bars, which was given as a definition 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$. Our Lemma~\ref{gindy-gbars} below generalises \cite[Lemma~2]{dggt}. It relies on the \gbars-induction principle, which is analogous to the principles of well-founded induction, and of \bars-induction (see \cite[Proposition~1]{jgl}). It is generated automatically by the Isabelle theorem prover from the inductive definition of \gbars\ above. We write $\mathcal P\ s$ to mean that object $s$ satisfies property $\mathcal P$. \begin{proposition}[\gbars-induction]\label{gbars-ind} For sets $Q$ and $S$, and any property $\mathcal P$, if % Let $Q$ and $S$ be sets of objects. % Then, for every property $\mathcal P$, if \begin{enumerate} \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{enumerate} then every $s \in \gbars\ \sigma\ Q\ S$ satisfies $\mathcal P$. \end{proposition} \begin{lemma}\label{gindy-gbars} ~ % to align parts \begin{enumerate} \item \label{2a}$S = \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S $ \item \label{2b}$Q \subseteq \gindy\ \sigma\ (\gbars\ \sigma\ Q\ S) $ \end{enumerate} \end{lemma} \begin{proof} \begin{enumerate} \item $\subseteq$: this is trivial, from Definition~\ref{def-gbars-isa}\ref{gbars-inI}, by letting $Q$ be $\gindy\ \sigma\ S$. % -- if $t \in S$, this is the case $n = 0$ in Definition~\ref{def-gbars}. $\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}. % So Proposition~\ref{gbars-ind} gives the result. \item Follows directly from Definitions \ref{def-gindy} and \ref{def-gbars-isa}\ref{gbars-gbarsI}. \qed \end{enumerate} \end{proof} \comment{ old proof, not valid Assume that $t \in \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S$. Consider, simultaneously, every downward $\sigma$-chain (starting from $t$) $t = t_0 >_\sigma t_1 >_\sigma t_2 >_\sigma \ldots$, but disregard objects in such a chain beyond the first member of $S$. Thus we are considering finite chains, like $t_0 >_\sigma t_1 >_\sigma \ldots >_\sigma t_{n-1}$ or $t_0 >_\sigma t_1 >_\sigma \ldots >_\sigma t_{n-1} >_\sigma t_{n}$ where $\{t_0, t_1, t_2, \ldots, t_{n-1}\} \subseteq Q$ and $t_n \in S$. We prove by reverse induction on the index $i$ of a member $t_i$, that $t_i \in S$, noting that the necessary hypothesis $t_i \in \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S$ holds. So assume that for $j > i$, $t_j \in S$. Since $t_i \in \gindy\ \sigma\ S$ and, by induction, every possible choice of $t_{i+1}$ is in $S$, that is, for every $t_{i+1}$ such that $t_i >_\sigma t_{i+1}$, $t_{i+1} \in S$. Therefore $t_i \in S$, as required. } \begin{lemma}\label{l2} ~ % to align parts \begin{enumerate} \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{enumerate} \end{lemma} \begin{proof} \begin{enumerate} \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 follows as every object is in $\gindy\ \sigma\ (\wfp\ \sigma)$, which follows from Lemma~\ref{gindy-gbars}\ref{2b}. \end{enumerate} \end{proof} \section{The Termination Theorem} \label{s-tt} % We now have enough terminology to prove termination, % but we require some further properties of $\rho$. % % \subsection{Properties we require of $\rho$} \label{s-rho-props} Given a reduction relation $\rho$, our general termination result requires relations $\vtl$ and $\ll$ which satisfy certain properties. 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 of Lemma~\ref{dth} below). \begin{condition}\label{conds-defs} ~ % to align parts \begin{enumerate} \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 \\ for all $t' \vtl^* t$, either $(t', s) \in (\vtl \circ\ \rho^*)$ or $t' \ll s$. \end{enumerate} \end{condition} % \mbox{} % SPACE HERE \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} \begin{proof} It is easy to see that Condition~\ref{conds-defs}\ref{rpc} implies Condition~\ref{conds-defs}\ref{rpc0} 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)$. \qed \end{proof} % \subsection{The Proof of Termination} Our key lemma, Lemma~\ref{dth} below, corresponds to \cite[Lemma~3]{dggt}, but is considerably simpler. We thank an unnamed referee for pointing out that our proof and that of \cite[Lemma~3]{dggt} % bears considerable resemblance to the proof by resembles the proof by Buchholz \cite{buchholz-pta} of the well-foundedness of the lexicographic path ordering, although it was obtained independently. \comment{ \begin{lemma} \label{dth} For any object $s$, if $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, then $s \in \gindy \ll (\gindy \vtl \SN)$. % If all objects ${t' \ll s}$ are in $\gindy \vtl \SN$, % then $s \in \gindy \vtl \SN$. \end{lemma} } \begin{lemma} \label{dth} If object $s$ satisfies Condition~\ref{conds-defs}\ref{rpc0}, then \mbox{$s \in \gindy \ll (\gindy \vtl \SN)$}. % If all objects ${t' \ll s}$ are in $\gindy \vtl \SN$, % then $s \in \gindy \vtl \SN$. \end{lemma} \begin{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$. % To show that $s \in \SN$, it is enough to show % $s \in \bars\ \rho\ \SN$ by Lemma~\ref{l2}\ref{bars-wfp}. % By Condition~\ref{conds-defs}\ref{rpc0} % (whose antecedent condition holds by assumption (b)) The antecedent of Condition~\ref{conds-defs}\ref{rpc0} holds by assumption (b), and so \mbox{$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, we have $\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq$ \mbox{$\gbars \vtl (\gindy \vtl \SN)\ \SN = \SN$}, by Lemma~\ref{gindy-gbars}\ref{2a}. 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)$. \qed \end{proof} 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} Relation $\rho$ is well-founded if % Suppose that $\rho$, $\vtl$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0} holds for all $s$ and \begin{enumerate} \item \label{ubg} every object is in $\bars \ll (\gindy \vtl \SN)$, and \item \label{vbs} every object is in $\bars \vtl \SN$. \end{enumerate} % Then $\rho$ is well-founded. \end{theorem} \begin{proof} If $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, then 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. \qed \end{proof} %% \begin{theorem} \label{thm-allsn} %% Relation $\rho$ is well-founded if %% % Suppose that $\rho$, $\vtl$ and $\ll$ satisfy %% Condition~\ref{conds-defs}\ref{rpc0} holds and %% \begin{enumerate} %% \item \label{ubg} every object $u$ is in $\bars \ll (\gindy \vtl \SN)$, and %% \item \label{vbs} every object $v$ is in $\bars \vtl \SN$. %% \end{enumerate} %% % Then $\rho$ is well-founded. %% \end{theorem} %% \begin{proof} %% If $\rho$ and $\ll$ satisfy Condition~\ref{conds-defs}\ref{rpc0}, %% then every $s \in \gindy \ll (\gindy \vtl \SN)$ by Lemma~\ref{dth}. %% As $u \in \bars \ll (\gindy \vtl \SN)$ then, %% by Lemma~\ref{l2}\ref{gindy-bars}, $u \in \gindy \vtl \SN$. %% As this holds for every $u$, and %% $v \in \bars \vtl \SN$, then, %% again by Lemma~\ref{l2}\ref{gindy-bars}, $v \in \SN$. %% As this holds for every $v$, we have that $\rho$ is well-founded. %% \qed \end{proof} 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 % there are well-founded relations $\rho$ % where $\rho\ \cup \vtl$ is not well-founded. 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). \section{Generalising Previous Results} \label{s-opr} %% We now obtain both \cite[Theorem~1]{jgl} and %% \cite[Theorem~2]{dggt} from our Theorem~1. \subsection{Generalising Goubault-Larrecq's General Theorem for ARSs} We show that Theorem~1 of Goubault-Larrecq \cite{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$. We first require two lemmas. \begin{lemma} \label{lemma-P2} Given set $S$ and object $s$, suppose for all $t$ that, if $(t, s) \in \rho$, then \begin{enumerate} \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{enumerate} Assume $\vtl$ is well-founded. Then $(t, s) \in \rho$ implies $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. \end{lemma} \begin{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. Firstly, if $t \in S$, then $t \in \gbars \vtl \{x\:|\ x \ll s\}\ S$ by Definition~\ref{def-gbars-isa}\ref{gbars-inI}. Secondly, 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 again two cases. In the first case, $(u, s) \in \rho$ % $u <_\rho s$ (from \ref{P2b} above), and so, by the inductive hypothesis, $u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$. In the second case, $u \in S$ and so \mbox{$u \in \gbars \vtl \{x\:|\ x \ll s\}\ S$} by Definition~\ref{def-gbars-isa}\ref{gbars-inI}. \qed \end{proof} \begin{lemma} \label{lemma-P1} Suppose that, whenever $(t, s) \in \rho$, either \begin{enumerate} \item \label{P1a} for some object $u$, $s \vtr u$ and $u \geq_\rho t$, or \item \label{P1b} $s \gg t$ and, for every $u \vtl t$, $s >_\rho u$. \end{enumerate} Suppose also that $\vtl$ is well-founded. Then Condition~\ref{conds-defs}\ref{rpc} holds. \end{lemma} \begin{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 $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}. \comment{ Let $(t, s) \in \rho$ and assume that for all $s' \vtl s$, $s' \in \SN$. We prove the result by well-founded induction on $\vtl$, so assume that for all $v \vtl t$ such that $v <_\rho s$, $v \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$. We consider the two cases \ref{P1a} and \ref{P1b}. Firstly, suppose that $s \vtr u$ and $u \geq_\rho t$. Then $u \in \SN$, so $t \in \SN$, so $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$ by clause \ref{gbars-inI} of Definition~\ref{def-gbars-isa}. Secondly, if \ref{P1b} holds, we show that $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$ using clause \ref{gbars-gbarsI} of Definition~\ref{def-gbars-isa}. We have $t \ll s$, and for any $u \vtl t$, $u <_\rho s$ (from \ref{P1b} above), and so, by the inductive hypothesis, $u \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$. Therefore $t \in \gbars \vtl \{x\:|\ x \ll s\}\ \SN$. } \qed \end{proof} \begin{corollary} Theorem~1 of \cite{jgl} holds. % if the conditions of Lemma~\ref{lemma-P1} hold, % condition~\ref{ubg} of Theorem~\ref{thm-allsn} holds, % and $\vtl$ is well-founded, then $\rho$ is well-founded. \end{corollary} \begin{proof} Theorem~1 of \cite{jgl} says: if Property~1 and conditions (\emph{iii}) and (\emph{iv}) (as given in \cite{jgl}) hold, then $\rho$ is well-founded. % Condition (\emph{iii}) of \cite{jgl} says that $\vtl$ is well-founded. Condition (\emph{iv}) of \cite{jgl} is just condition \ref{ubg} of our Theorem~\ref{thm-allsn} because $\underline{SN}$ of \cite{jgl} is $\gindy \vtl \SN$, and if some $u \vtl s \not\in SN$, then $s \in \underline{SN}$. Thus the requirement that ``{if every $u \vtl s$ is in SN}'' in the statement of Theorem~1 of \cite{jgl} is redundant, although its counterpart is needed in the statement of Theorem~2 of \cite{jgl}. % (since if $u \vtl s \not\in SN$, then $s \in \underline{SN}$). % is that every object $u$ is in $\bars \ll (\gindy \vtl \SN)$, % because $\underline{SN}$ of \cite{jgl} is $\gindy \vtl \SN$. % % Thus, by condition (\emph{iv}) of \cite{jgl} % condition \ref{ubg} of Theorem~\ref{thm-allsn} holds. Condition (\emph{iii}) of \cite{jgl} says that $\vtl$ is well-founded. Then, for any object $v$ and set $S$ of objects, \mbox{$v \in \bars \vtl S$}, and so condition \ref{vbs} of Theorem~\ref{thm-allsn} follows. Property~1 of \cite{jgl} says that for $(t, s) \in \rho$, either \ref{P1a} or \ref{P1b} of Lemma~\ref{lemma-P1} holds. % Finally we show that, in the presence of condition (iii) of \cite{jgl} % (ie, that $\vtl$ is well-founded), Finally, Lemma~\ref{lemma-P1} shows that if $\vtl$ is well-founded, as ensured by condition (\emph{iii}) of \cite{jgl}, then Property~1 % which is \ref{P1a} and \ref{P1b} of Lemma~\ref{lemma-P1}, implies Condition~\ref{conds-defs}\ref{rpc}, whence Condition~\ref{conds-defs}\ref{rpc0} holds. Thus all the conditions of Theorem~\ref{thm-allsn} hold, so $\rho$ is well-founded. \qed \end{proof} We explore the extent to which, conversely, Theorem~1 of Goubault-Larrecq \cite{jgl} 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 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$ so that Condition~\ref{conds-defs}\ref{rpca} holds as an equivalence, giving \ref{P1a} and \ref{P1b} of Lemma~\ref{lemma-P1} (\textit{i.e.} Property~1 of \cite{jgl}). That is, \cite[Theorem~1]{jgl} 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$ is well-founded. On the other hand, in Sections \ref{s-tc} and \ref{s-tc2}, the proofs of termination use 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 shows that \cite[Theorem~1]{jgl} is a special case of our Theorem~\ref{thm-allsn}. \subsection{Generalising our Previous Theorem for TRSs} \label{s-appl-rewr} We now apply 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 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$ to be the ``closure under contexts'' of $\sigma$: that is, where $C[\_]$ is a context, % (a term with a ``hole''), and $(r, l) \in \sigma$, then $(C[r], C[l]) \in \ctxt\ \sigma$. Likewise we define \pctxt\ (``\emph{proper} context''): for $(r, l) \in \sigma$, if $r$ and $l$ are \emph{proper} subterms of $C[r]$ and $C[l]$, then $(C[r], C[l]) \in \pctxt\ \sigma$. \comment{ \begin{definition}[{closure under contexts}] \footnote{could delete this} Given a relation $\sigma$ and terms $s$ and $t$, the pair $(t, s) \in \ctxt\ \sigma$ (pronounced ``$s$ reduces to $t$'') if either \emph{(a)} $(t, s) \in \sigma$, or \emph{(b)} $s$ and $t$ are identical except that exactly one immediate subterm of $s$ reduces to the corresponding immediate subterm of $t$. \end{definition} } \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 % $s_1,\ldots, s_m$ 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. % We now show that the main theorem there follows from Theorem~\ref{thm-allsn}. 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 to be the set of those reductions where a strongly normalising immediate subterm is reduced \cite[Definition 3]{dggt}. Then we apply 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 Condition~\ref{rpc-csl}\ref{csl}. Condition~\ref{rpc-csl}\ref{csl'} implies Condition~\ref{rpc-csl}\ref{csl}, is more generally useful, and will be used in \S\ref{s-inc}. \begin{condition}\label{rpc-csl} ~ % to align parts \begin{enumerate} \item \label{csl} For all $(t, s) \in \sigma$, 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, s) \in \sigma$, and $t' \vtl^* t$, \\ either $(t', s) \in\ \vtl \circ\ (\rho\ \cup \vtl)^*$ or $t' \ll' s$. \end{enumerate} \end{condition} \begin{theorem} \label{thm-csl} If $\sigma$ satisfies Condition~\ref{rpc-csl}\ref{csl}, $\ll$ contains $<_{sn1}$ and $\ll$ is well-founded, then every term is strongly normalising \cite{dggt}. \end{theorem} \begin{proof} We apply Theorem~\ref{thm-allsn} to this situation. Since $\vtl$ is well-founded and we assume $\ll$ is well-founded, conditions \ref{ubg} and \ref{vbs} of Theorem~\ref{thm-allsn} are satisfied. It remains only to check that Condition~\ref{conds-defs}\ref{rpc0} holds. In fact we can show that 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 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 also need to 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. \qed \end{proof} \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$. As before, $\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{enumerate} \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{enumerate} \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} \\ \label{cososn} \constrict\ \sigma\ \circ \vtl^* \circ <_{sn1}^* && \mbox{ is well-founded} \\ \label{sosnoc} \vtl^* \circ <_{sn1}^* \circ\ \constrict\ \sigma && \mbox{ is well-founded} \\ \label{snocos} <_{sn1}^* \circ\ \constrict\ \sigma\ \circ \vtl^* && \mbox{ is well-founded} \\ \label{rhoos} \rho\ \circ \vtl^* && \mbox{ is well-founded} \\ \label{rhous} \rho\ \cup \vtl && \mbox{ is well-founded} \\ \label{rhowf} \rho && \mbox{ is well-founded} \\ \label{rhotc} \rho^+ && \mbox{ is well-founded} \\ \label{rhotcs} \rho^+ \cup \vtl && \mbox{ is well-founded} \end{eqnarray} \end{theorem} \begin{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 in the literature, % 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}) : follows from 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 other relation mentioned is contained in \mbox{$(\rho\ \cup \vtl)^+$}. \qed \end{proof} 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}). Let $\ll\ = \tau$. Then Condition~\ref{rpc-csl} holds trivially, $\ll\ \supseteq\ <_{sn1}$ and $\ll$ is well-founded, which is just (\ref{cosusn}) of Theorem~\ref{thm-ctalt}. 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. \comment{ Suppose that the assumptions of Theorem~\ref{thm-csl} hold, and assume that (\ref{cosusn}) implies (\ref{rhowf}). Then we need to show 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}. 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. \section{Application to Typed Combinators} % and the $\lambda$-calculus \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 Theorem~2.2 of Akama \cite{akama-trans}, this is enough to show strong normalisation of $\beta$-reduction. % We also show how to adapt Theorem~\ref{thm-allsn} % to prove strong normalisation of the simply-typed $\lambda$-calculus directly. Thus, the full power of the much more complex Theorem~2 of \cite{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 an anonymous referee. % Also, although we have been able to prove strong normalisation Also, although we could prove strong normalisation of the simply-typed $\lambda$-calculus by adapting the proof of Theorem~\ref{thm-allsn}, we could not prove it as a corollary of Theorem~\ref{thm-allsn}. % We also show how to adapt Theorem~\ref{thm-allsn} \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 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. % as indicated by rule (\ref{tc-others}). 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}: % % It is easy to extend the proof to the case where there are % several of these combinators. \comment{ (we show types where there is space). \begin{eqnarray} \label{Sfgx} S f g x : \gamma >_\sigma f x (g x) : \gamma & & \\ % \label{csr} \ctxt\ \sigma \subseteq \rho & & \\ \label{Sfg} S f g : \alpha \to \gamma >_\rho f x (g x) : \gamma & & \quad\mbox{if $x \in \SN$} \\ \label{Sf} S f : (\alpha \to \beta) \to \alpha \to \gamma >_\rho f x (g x) : \gamma & & \quad\mbox{if $g,x \in \SN$} \\ \label{S} S >_\rho f x (g x) : \gamma & & \quad\mbox{if $f,g,x \in \SN$} \end{eqnarray} } % \begin{eqnarray} \label{Sfgx} S f g x >_\sigma f x (g x) & & \\ % \label{csr} \ctxt\ \sigma \cup \tau \subseteq \rho & & \\ \label{Sfg} S f g >_\tau f x (g x) & & \quad\mbox{if $x \in \SN$} \\ \label{Sf} S f >_\tau f x (g x) & & \quad\mbox{if $g,x \in \SN$} \\ \label{S} S >_\tau f x (g x) & & \quad\mbox{if $f,g,x \in \SN$} % \\ % \label{tc-others} % I x >_\sigma x, \quad & K x y >_\sigma x, & \mbox{ etc.} \end{eqnarray} % where $S,f,g,x$ have types 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, $\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$. % Further, the rules for reducing a term $s$ depend on % other terms $s'$, where $s' <_{ty} s$, being in $SN$, 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\}$}. % Thus we consider $(t, s) \in \rho$ as being defined in terms of % whether $s' \in \SN$, which depends on whether $(x, s'') \in \rho$, % for terms $s'$ and $s''$ where $\tyof\ s'' \leq \tyof\ s' < \tyof\ s$ % (ie $s'' \leq_{ty} s' <_{ty} s$). 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} \begin{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$ by rule (\ref{Sfgx}), % Here, there are corresponding terms $t' \vtl t$ and $s' \vtl s$ 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$. \qed \end{proof} \begin{theorem} \label{tc-sn} Every term is strongly normalising. \end{theorem} \begin{proof} We use Theorem~\ref{thm-allsn}. Apart from Lemma~\ref{tc-c1}, we need conditions \ref{ubg} and \ref{vbs} of 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 that $<_{sn1}$ is well-founded. Then, clearly, $<_{ty} \circ <_{sn1}\ \subseteq\ <_{ty}$, and so, by \cite[Lemma~1]{dggt}, $<_{ty} \cup <_{sn1}$ is well-founded. \qed \end{proof} Our rules (\ref{Sfg}), (\ref{Sf}) and (\ref{S}) were suggested by the definition of $\vtlo$ given just below Remark~13 in \cite{jgl}. As in \cite{jgl}, therefore, there is a resemblance between our proof and the classic reducibility argument: we have, for example, that 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. % \mbox{} % SPACE HERE \subsection{A Second Proof for Typed Combinator Expressions} \label{s-tc2} We now present another way of using 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 \\ % N \vtl M & \Rightarrow & N A \vtl M A \\ \label{aa} M >_\rho M N \quad\mbox{if $N \in \SN$} \\ % \label{Sfgx} S f g x >_\sigma f x (g x) & & \\ % \label{csr} \ctxt\ \sigma \subseteq \rho & & \\ \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} \begin{split} (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{split} \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} \begin{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}. \qed \end{proof} % \subsection{Strong Normalisation of the Simply-typed $\lambda$-calculus} % \label{s-lc} OMITTED - see the CSL'05 submission \section{Incremental Proofs of Termination} \label{s-inc} A rewrite system can be defined by taking the union of two terminating systems. Obviously, it would be desirable to be able to reduce a proof of termination of such a system into two smaller proofs of termination of smaller systems. This is possible under certain conditions (see, eg, \cite{fgr-incremental}), but not in general. We show how Theorem~2 of \cite{dggt}, as described in \S\ref{s-appl-rewr}, can be used to prove termination incrementally in certain cases. The assumptions we require of the component systems are mentioned where they first become relevant, and all appear 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$. \comment{ this para now not really significant This is the first point in this paper where we consider a rewrite relation necessarily arising by instantiating a set of rules. Proofs in this context are complicated by the fact that a variable may be replaced by a term whose head may either be in $\mathcal{F}_0$ or not, as illustrated in \cite{fgr-incremental}, after Proposition~1. % Thus the fact that the results of this section (as of the whole paper) have been proved in Isabelle is of particular value. } We consider a rewrite system $\rho_0$ which has been proved terminating by any method, with only the extra condition that the rules $\mathcal{R}_0$ be \emph{right-linear}: that is, no variable appears more than once on the right-hand side of a rule. 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 lemma which follows. \begin{definition}[\textit{$\mathcal{R}_0$-property}] A rule satisfies the $\mathcal{R}_0$-property if \begin{enumerate} \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} its right-hand side variables are not duplicated \item \label{rhs-nonew} its right-hand side variables also appear on the left-hand side \end{enumerate} \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{enumerate} \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{lem-subs0-nured} % so called in Isabelle code 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{enumerate} \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. The system $\rho_1$ is assumed to have been proved terminating using Theorem~\ref{thm-csl} above (ie, using Theorem~2 of \cite{dggt}): 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. In many examples of the use of Theorem~\ref{thm-csl}, the argument went as follows. Firstly, 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. Secondly, 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 \cite{dvk} to prove that the union is well-founded, often by proving that $\ll' \circ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$ (see Theorem~1 and Lemma~1 of \cite{dggt}). % To achieve this even just for $\ll_1'$, % for a somewhat arbitrary $<_{sn2}$, which depends also on $\rho_0$, % we will require a stronger condition on $\ll_1'$: We will use this proof method. The key point is to define a suitable relation $\ll'$: we will use \mbox{$\ll' \ =\ \ll_0' \cup \ll_1'$}, where $\ll_0'$ is a suitable relation which we derive from $\mathcal{R}_0$. To help prove \mbox{$\ll' \circ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$} we will 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 \cite[Lemma~1]{dggt}, and Theorem~\ref{thm-incr-pf} still holds. Details will be in \cite{dgtars}. % See \cite{dgtars} for details. The example in \cite[\S 3.6]{dggt} 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}$: % \mbox{} % SPACE HERE \begin{definition}[$\vtl_0$] \label{def-vtl0} $t \vtl_0 f(\ldots, t, \ldots)$ if $f \in \mathcal{F}_0$. \end{definition} \begin{definition}[$\ctxt_0$] \label{def-ctxt0} For $(t, s) \in \sigma$, if the subterms of $C[x]$ which are super-terms of $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}$] $(r_0', l_0) \in \mathcal{R}_{\ll 0}$ iff it satisfies the $\mathcal{R}_0$-property and there exists $r_0$ such that $r_0' \vtl^*_0 r_0$ and $r_0'$ is not a variable, and $(r_0, l_0) \in \ctxt_0\ \mathcal{R}_0$. \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 define $\ll \ =\ \ll' \cup <_{sn2}$. Since $<_{sn2}$ is well-founded (\cite[Theorem~1]{dggt}), to show that $\ll$ is well-founded it would be enough to show \mbox{$\ll' \circ\ <_{sn2}\ \subseteq\ {<_{sn2}}^*\ \circ \ll'$}. We cannot do this, but we can choose a suitable subset $<'_{sn2}$ of $<_{sn2}$ such that $\ll \ =\ \ll' \cup <'_{sn2}$ and we prove that $\ll$ is well-founded in two steps. % and $\ll' \circ\ <'_{sn2}\ \subseteq\ {<'_{sn2}}^*\ \circ \ll'$. 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)$. 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}\ = \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}$. % \textup{; so} % $\ll' \cup <'_{sn2} \ =\ \ll' \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{enumerate} % \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 \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{enumerate} \end{lemma} \begin{proof} \begin{enumerate} \item This follows from \cite[Lemma~1]{dggt} as $\ll_1'$ satisfies the $\ll_1'$-property. \item Recall that, for $f (\ot) \ll_0' s$, $f \in \mathcal{F}_0$. % Then the result for $<'_{sn2}$ can be proved using Then use Lemma~\ref{lem-r0p}\ref{lem-subs0-nured}. \item As $\ll_0'$ and, by \ref{ll1-sn2-wf}, $\ll'_1 \cup <'_{sn2}$ are well-founded, we can use \ref{wfh-lem3} and \cite[Lemma~1(a)]{dggt} 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$}. \qed \end{enumerate} \end{proof} \comment{ \begin{lemma} \label{lem-wfh46} Assume \ref{r0p}, \ref{ll1p} and \ref{h1} of Theorem~\ref{thm-incr-pf}. Then \begin{enumerate} \item \label{wfh-lem4} $\ll' \circ\ <'_{sn2}\ \subseteq\ {<'_{sn2}}^*\ \circ \ll'$. \item \label{wfh-lem6} $\ll$ is well-founded. \end{enumerate} \end{lemma} \begin{proof} \begin{enumerate} \item Since both $\ll'$ and $<'_{sn2}$ are unions, this splits into a number of cases. For $\ll_0'$ this follows from Lemma~\ref{lem-r0p}\ref{lem-subs0-nured} (recalling that, for $f (\ot) \ll_0' s$, $f \in \mathcal{F}_0$). For $\ll_1'$ this follows from the {$\ll_1'$-property} assumed. \item By Lemma~\ref{lem-wfh-lem2,5'}, $<'_{sn2}$ is well-founded, so by \ref{wfh-lem4} and \cite[Lemma~1(a)]{dggt}, $\ll' \cup <'_{sn2}$ is well-founded. By Lemma~\ref{lem-wfh-lem2,5'}, this is equal to $\ll' \cup <_{sn2} \ =\ \ll$. \qed \end{enumerate} \end{proof} } \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} \begin{proof} Let $(t, s) \in \sigma_0$, got by substituting 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 then, by Lemma~\ref{lem-r0p}\ref{r0p-f1sub}, \mbox{$t' \vtl^* f (\ot) \vtl^+ s$}, as required. \qed \end{proof} \begin{theorem} \label{thm-incr-pf} Assume that \begin{enumerate} \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{enumerate} Then $\rho_0 \cup \rho_1$ is well-founded. \end{theorem} \begin{proof} % We use Theorem~\ref{thm-csl}. From assumption \ref{c2b} and Lemma~\ref{rp-pc-cut0}, it can be seen that \mbox{$\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}. \qed \end{proof} \section{An Incremental Path Ordering} \label{s-ipo} \newcommand{\ipo}{\textit{ipo}} We now use the previous results to describe an incremental generalisation of the general path ordering of Dershowitz \& Hoot \cite{nat-term}. The incremental path ordering $<_{ipo}$ (or \ipo) is then defined as below, where $\overline s = s_1, \ldots, s_m$, $\overline t = t_1, \ldots, t_n$, and $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 certain conditions given later: the common examples for $\Lambda$ are the lexicographic or multiset extensions of $<_{ipo}$. As before we have a set of rules $\mathcal{R}_0$ satisfying the 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. % outside $\mathcal{F}_0$. \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: % \begin{definition} % Given a relation $\sigma$, $(t, s) \in \fwf\ \sigma$ iff % if and only if $(t, s) \in \sigma$ and $s \in \wfp\ \sigma$. % is strongly normalising (for $\sigma$). % \end{definition} We now list the conditions on $\Lambda$ required at some point in the proof: \begin{enumerate} \item \label{lam-mono} ${\Lambda}$ is a monotonic function \item \label{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)$ \item \label{lam-wf} if $\sigma$ is well-founded then ${\Lambda (\sigma)}$ is well-founded \item \label{lam-psubt} if all $s_i$ are in $\wfp\ \tau$ % strongly normalising (for $\tau$), and if $(t, s) \in \Lambda (\tau)$, then $(t, s) \in \Lambda (\fwf\ \tau)$ \end{enumerate} In practice, condition \ref{lam-psubt} means that the dependence of $\Lambda (\sigma)$ upon $\sigma$ is only as follows: whether $(\overline t, \overline s) \in \Lambda (\sigma)$ depends solely upon $\sigma$-comparisons between the $s_i$ and the $t_j$. The lexicographic and multiset extensions of an ordering satisfy these conditions. The proof of termination consists mostly of combining the proof of Theorem~\ref{thm-incr-pf} above with ideas from the proof of the termination of the recursive path ordering in \cite[\S 3.7]{dggt}. We omit the details, but note that it has been proved using the Isabelle theorem prover, see \cite{jdisa}, in {\tt snabs/hpodef.\{thy,ML\}}. \begin{theorem} \label{thm-ipo} Assume that \begin{enumerate} \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 the conditions listed above \end{enumerate} Then $<_{ipo}$ is well-founded. \end{theorem} \section{Observations and Conclusion} % NOTE - the two paragraphs that were here are now following Theorem1, % since this enables it to fit in 15 pages \comment{ In \S\ref{s-tc}, as in \cite[\S3.3]{dggt}, we had the somewhat paradoxical situation that it was necessary to add additional rules to enlarge the relation $\rho$ to prove termination. We would like to extend Theorem~\ref{thm-allsn} to avoid this need since, the larger $\rho$ is, the more difficult it should be to prove termination. } \comment{ following moved after Theorem 1, saves much space 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 there are well-founded relations $\rho$ where $\rho\ \cup \vtl$ is not well-founded. 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 method of proving termination (as are several other orderings in the literature). } %% 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\ = \rho^+$, which is well-founded. %% Then even Condition~\ref{conds-defs}\ref{rpc2} applies, for %% $\vtl\ \subseteq \rho$ is well-founded and, %% if $(t, s) \in \rho$ and $t' \vtl^* t$, %% then $(t', s) \in \rho^+ =\ \ll$. %% 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 method of proving %% termination (as are several other orderings in the literature). We have proved a theorem about termination of reduction rules which generalises the previous quite general theorems, in \cite{dggt} and the first theorem in \cite{jgl}. \comment{ % and the general path ordering \cite{nat-term}. % \footnote{ may omit the general path ordering} % We have shown how to adapt the framework of our proof to give % a proof of the complex second theorem in \cite{jgl} for % higher-order path orderings. % \footnote{ may omit the second theorem in \cite{jgl}} } % Finally % motivated by the complexity of proofs of the termination of % $\beta$-reduction in a typed setting, We use our main theorem to prove the termination of the reduction of well-typed combinator expressions. One of our proofs takes advantage of the abstract setting, using a relation $\vtl$ which is \emph{not} the usual immediate subterm relation. \comment{ and to adapt its proof to prove the strong normalisation of the simply-typed $\lambda$-calculus. Our proofs for the simply-typed $\lambda$-calculus %have some resemblances to the differ from classic reducibility proofs by circumventing the usual step that $M [\overline x := \overline A] \in \SN$ for $A \subseteq \SN$. An open question is whether our indirect method for handling substitutions can be adapted to prove termination for the higher-order recursive path ordering of Jouannaud \& Rubio \cite{jr-horpo}. } The picture that emerges is the following. 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 \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, but had to be be modified to reason indirectly about substitutions for the simply-typed $\lambda$-calculus. An important goal is to find the exact relationship between \cite[Theorem~2]{jgl} and our Theorem~\ref{thm-allsn}. Finally, we show how our main theorem can be used to prove termination of a rewrite system defined incrementally. We showed in \cite{dggt} that our main theorem 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 it nor the work in \S\ref{s-inc} subsume each other. A goal of further work is to explore the relationship between their results and the work in \S\ref{s-ipo}. \paragraph{Acknowledgements} Finally, we thank some anonymous referees for very helpful comments. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Here begins the end matter % \bibliography{/home/users/rpg/bib/ce,/home/users/rpg/bib/fm,/home/users/rpg/bib/modal,/home/users/rpg/bib/mtl,/home/users/rpg/bib/logic,/home/users/rpg/bib/tl,/home/users/rpg/bib/paracon,/home/users/rpg/bib/linear,/home/users/rpg/bib/algebra,/home/users/rpg/bib/relevant,/home/users/rpg/bib/dl,/home/users/rpg/bib/atp,/home/users/rpg/bib/tphols} %\vspace*{-1em} \bibliographystyle{plain} \begin{thebibliography}{1} \bibitem{akama-trans} 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{dps00} Thomas Arts and J\"urgen Giesl. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236 (2000), 133-178, 2000. \bibitem{baader-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} Wilfried Buchholz. Proof-theoretic analysis of termination proofs. Annals of Pure and Applied Logic 75 (1995), 57--65. % \bibitem{david-nr} % R~David. % Normalization without Reducibility. % APAL 107:121--130, 2001 Elsevier. \bibitem{dggt} 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{dgtars} J~E~Dawson and R~Gor{\'e}. Machine-checked Termination Proofs for Abstract Reduction Systems. % \newblock \url{http://web.rsise.anu.edu.au/~jeremy/pubs/rewr_term/mcars/} In preparation. \bibitem{jdisa} J~E~Dawson. Isabelle/HOL code, \newblock \url{http://web.rsise.anu.edu.au/~jeremy/isabelle} \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} Henk Doornbos \& Burghard Von Karger. On the Union of Well-Founded Relations. L. J. of the IGPL 6 (1998), 195-201. \bibitem{fgr-incremental} Mirtha-Lina Fern\'andez, Guillem Godoy, Albert Rubio. Recursive Path Orderings Can Also Be Incremental. Proc.\ LPAR2005, LNCS 3835, 230--245, Springer, 2005. \comment{ \bibitem{fz} M~C~F~Ferreira and H~Zantema. Well-foundedness of Term Orderings. In Proc.\ Conditional Term Rewriting Systems (CTRS-94), LNCS 968, 106--123, 1995. } % \bibitem{gallier-oncr} % Jean Gallier. On Girard's "Candidats de Reductibilite". % Logic and Computer Science, P.Odifreddi (ed), Academic Press, 1989, 123-203. \bibitem{glt} Jean-Yves Girard, Yves Lafont and Paul Taylor. Proofs and Types. CUP, 1990. \bibitem{jgl} J~Goubault-Larrecq. Well-founded recursive relations. In Proc.\ CSL'2001, LNCS 2142, 484--497, Springer, 2001. \bibitem{hm-dpr} Nao Hirokawa and Aart Middeldorp. Dependency Pairs Revisited. In Proc.\ Rewriting Techniques and Applications (RTA-04), LNCS 3091, 249--268, Springer, 2004. % \bibitem{jr-horpo} % J-P~Jouannaud and A~Rubio. % The Higher-order Recursive Path Ordering. % In Proc. 14th Logic in Computer Science (LICS'99), 402--411, 1999. \end{thebibliography} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: