\documentclass{lecture}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{proof}
\usepackage{exptrees}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{condition}{Condition}

\newcommand\proof{\noindent\textit{Proof.}}

\newcommand{\pordered}[3]{#1 <_{\scriptsize #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{\SN}{\textit{SN}}
% \newcommand{\ISN}{\textit{ISN}}
\newcommand{\SN}{\ensuremath{S\!N}}
\newcommand{\ISN}{\ensuremath{I\!S\!N}}
\newcommand{\lpo}{\textit{lpo}}
\newcommand{\lex}{\textit{lex}}
\newcommand{\fwf}{\textit{fwf}}

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

%\input{/home/discus/disk1/rpg/papers/relalg/csl96/defs}

\newcommand{\comment}[1]{}
\newcommand{\mytilde}{\scriptstyle\sim}

\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

\newcommand{\SNo}{{SN}^\circ} % needs math mode 
\newcommand{\SNSig}{\textit{SN}^\Sigma}
\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{\tyof}{\textit{tyof}}
\newcommand{\ctxt}{\textit{ctxt}}
\newcommand{\pctxt}{\textit{pctxt}}
\newcommand{\ictxt}{\textit{ictxt}}
\newcommand{\constrict}{\textit{constrict}}

%%%%% Rule Forming Commands

\newcommand{\idrule}[2]{
 \mbox{#1 \ $\mbox{#2}$}}

\newcommand{\ds}{\displaystyle\strut}


\newcommand{\Drel}{\mbox{\bf DRA }}
\newcommand{\Lg}[1]{\mbox{$\bf #1$}}

\newcommand{\Fml}{\mbox{$\mathbf{Fml}$}}
\newcommand{\LAlg}{\mbox{$\mathfrak{Fml}/\!\!\equiv$}}

\newcommand{\stc}{\bullet}

\newcommand{\blob}{\bullet}

\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}

\newcommand{\mcal}[1]{\mbox{$\cal #1$}}

\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}

\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }

\newcommand{\Dl}[1]{\mbox{$\bf \mathbf{\delta}#1$}}
\newcommand{\eqded}{\dashv \vdash}


\newcommand{\id}{
\idrule{(id)}{$p \vdash p$}
}

\definecolor{altmagenta}{rgb}{1,0,1}
\definecolor{altyellow}{rgb}{1,1,0}
\definecolor{altcyan}{rgb}{0,1,1}
\definecolor{darkmagenta}{rgb}{0.5,0,0.5}
\definecolor{darkyellow}{rgb}{0.5,0.5,0}
\definecolor{darkcyan}{rgb}{0,0.5,0.5}
\definecolor{darkgreen}{rgb}{0,0.5,0}
\definecolor{darkblue}{rgb}{0,0,0.5}
\definecolor{darkred}{rgb}{0.5,0,0}

\begin{document}


\title{ }
\begin{slide}
  \begin{Heading}
{Termination of Abstract Reduction Systems}
  \end{Heading}

\begin{center}
\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
\multicolumn{2}{c}{Jeremy E.\ Dawson and Rajeev Gor\'{e}}
\\ \\
Logic \& Computation Programme      & Automated Reasoning Group 	\\
National ICT Australia 	&  Computer Sciences Laboratory   \\
& Res.\ Sch.\ of Inf.\ Sci.\ and Eng.\  \\
& {Australian National University}                    \\
\texttt{http://rsise.anu.edu.au/{\small$\mytilde$}jeremy} &
		      \texttt{http://rsise.anu.edu.au/{\small$\mytilde$}rpg} \\
\end{tabular*}
\end{center}
~
\footnote{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.}

\end{slide}

\comment{
\begin{slide}
  \begin{Heading}
    {Colours}
  \end{Heading}
 
 \color{yellow} yellow
 \color{cyan} cyan
 \color{magenta} magenta
 \color{altyellow} altyellow
 \color{altcyan} altcyan
 \color{altmagenta} altmagenta
 \color{darkyellow} darkyellow
 \color{darkcyan} darkcyan
 \color{darkmagenta} darkmagenta
 \color{green} green
 \color{blue} blue
 \color{red} red
 \color{darkgreen} darkgreen
 \color{darkblue} darkblue
 \color{darkred} darkred

\end{slide}
}

\begin{slide}
  \begin{Heading}
    {Overview and Motivation}
  \end{Heading}

  \begin{description}
  \item[Term Rewriting:] 
    Structured first-order terms ---
    rewrite may be at any subterm

  \item[Termination Proof:] Earlier paper (CSL'04) gave conditions
  and termination proof (based on our result on termination of a
  cut-elimination procedure)

  \item[Abstract reduction systems:] 
   Goubault-Larrecq's (first) termination theorem resembles ours,
   but in a more general setting (but doesn't subsume ours)

  \item[We generalised our result to abstract reduction systems:] ~ \\
   We found that this also generalised Goubault-Larrecq's result.

  \item[An example using the generality:] 
   Our new result (following Goubault-Larrecq) uses a relation $\vtl$
   in place of subterm relation. \\
   We prove termination of typed combinators, using
   a \emph{different} relation as $\vtl$

\comment{
  \item[Termination of reduction in $\lambda$-calculus:] 
    Completed a proof of this along the same lines, but not a
    direct application of our theorem, and not a particularly elegant proof

  \item[Goubault-Larrecq's Theorem 2:] also proved this, not a direct
  application of our theorem, but using similar ideas
  }
  \end{description}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Term Rewriting}
  \end{Heading}

 Have a language for defining first-order ``terms'', such as
   $f (a, g (b, c))$ 

 Have a collection of rewrite rules:
  $\{ l_1 \rightarrow r_1, \cdots , l_n \rightarrow r_n\}$
  in which can substitute for variables.
  NB: as pairs, $(r_1 , l_1)$, etc

  We consider the rewrite relation \emph{after} substitution -- 
  call it $\rho$

  \emph{closure} under \emph{contexts}
  of relation $\rho$ \quad(eg, if $l \stackrel\rho\longrightarrow r$ then 
  $C[l] \longrightarrow C[r]$) 

 Question: Does this rewriting process terminate for all terms?

 An ordering $<_{cut}$ must be defined, depending on the problem. \\
Typically, it looks at or near the head of the term (root of the tree).

 \comment{
 Example: Ackermann's function: 

 \begin{eqnarray*}
 A(0, y) & \longrightarrow & S(y) \\
 A (S(x), 0) & \longrightarrow & A(x, S(0)) \\
 A (S(x), S(y)) & \longrightarrow & A(x, A (S(x), y)) 
 \end{eqnarray*}
 }
 
\end{slide}

\begin{slide}
  \begin{heading}
    {Defining Reductions}
    {and Strongly Normalising Terms}
  \end{heading}

  \begin{definition}
    Assuming a relation $\rho$,
    term $t_0$ \emph{reduces} to term
    $t_1$ if either
  % \begin{itemize}
  % \item[(a)] 
  
 (a)  $(t_1, t_0) \in \rho$, or
  % \item[(b)]
  
  (b) $t_0$ and $t_1$ are identical except that exactly one
       proper subterm of $t_0$ reduces to the
       corresponding proper subterm of $t_1$.
  % \end{itemize}
  \end{definition}

 % We shall later define $\rho$ as a system of rewriting rules 
 % $\{(r_1, l_1), (r_2 , l_2), \cdots \}$

    {(this is the closure of $\rho$ under context)}
\comment{
 Intuition: a reduction is due to a rewrite $l \rightarrow r$ at the
 top level or happens at some deeper level.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Defining Strongly Normalising Terms}
  \end{Heading}
  }
  
  \begin{definition}
    The set \emph{$\SN$} is the {smallest} set of terms
    such that:
  % \begin{itemize}
  % \item[(a)] 

  (a) if $t_0$ cannot be reduced then $t_0 \in \SN$ 
  % \item[(b)] 
  
  (b) if every term $t_1$ to which $t_0$ reduces is in $\SN$ then $t_0 \in \SN$
  % \end{itemize}
  
  A term is \emph{strongly normalising} iff it is a member of $\SN$.
  \end{definition}

  Usual definition is: a term $t$ is in $\SN$ iff there is no infinite
  sequence of reductions starting with $t$.  
  These two definitions are equal in classical logic.
\end{slide}

\begin{slide}
  \begin{heading}
    {Various Binary Orderings -- $\snoneord{}{}$, etc}
  \end{heading}

\begin{enumerate}

\item\label{defn:porders-sn1} $\snoneord{t_1}{t_0}$ 
  if $t_0$ and $t_1$ are the same except that one of the \emph{immediate} 
  subterms of  $t_0$ is strongly normalising and reduces to the 
  corresponding \emph{immediate} subterm of $t_1$.
  
\item\label{defn:porders-sn2} ${t_1} <_{sn2} {t_0}$ -- as above,
  except put \emph{proper} for \emph{immediate}

\item\label{defn:porders-dt} 
  $\dtord{t_1}{t_0}$\quad iff 
   \quad$\cutord{t_1}{t_0}$\quad or \quad$\snoneord{t_1}{t_0}$.

\end{enumerate}

  Despite notation, these relations need \textit{not} be transitive.  
  
  Intuitively, $t_1 <_{dt} t_0$ means that
  $t_1$ is closer to a normal form (being cut-free)
  (in some sense) than is $t_0$.

Necessarily, $<_{sn1} \subseteq <_{sn2}$, both are well-founded.

We need to be able to prove that 
  $\dtord{}{}\ =\ \cutord{}{} \cup \snoneord{}{}$
is well-founded.

Use lemma on the union of well-founded orderings.

\end{slide}

\begin{slide}
\begin{Heading}
{Union of Well-Founded Relations}
\end{Heading}
\begin{lemma} \label{wf-rs}
Let $\tau$ and $\sigma$ be well-founded relations.
Then each of the following implies that 
$\tau \cup \sigma$ is well-founded:
\begin{enumerate}
\item \label{tco} $\tau \circ \sigma \ \subseteq\ \sigma^* \circ \tau$,
\item \label{otc} $\tau \circ \sigma \ \subseteq\ \sigma \circ \tau^*$,
\item \label{runs} $\tau \circ \sigma \ \subseteq\ \tau \cup \sigma$,
\item \label{dvk} $\tau \circ \sigma \ \subseteq\ (\sigma 
  \circ (\tau \cup \sigma)^*) \cup \tau$.
\end{enumerate}
\end{lemma}

{(d)} is from Doornbos \& von Karger; other conditions imply {(d)}
\end{slide}

\begin{slide}
  \begin{Heading}
    {Conditions on the rewrite relation $\rho$}
  \end{Heading}
  
\begin{condition}\label{st-rpc}
For all $(r, l) \in \rho$,
if all proper subterms of $l$ are in \SN\ then, \\
for all subterms $r'$ of $r$, either 
\comment{
  $$ (a) \quad r' \in \SN 
    \qquad \qquad \mbox{or} \qquad \qquad
  (b) \quad r' <_{dt}^+ l$$
  }

  (a)$ \quad r' \in \SN $
  \qquad \mbox{or} \qquad 
  (b)$ \quad r' <_{dt}^+ l$
\end{condition}

Condition~\ref{st-rpc1} is simpler and implies Condition~\ref{st-rpc}
\begin{condition}\label{st-rpc1}
For all $(r, l) \in \rho$,
for all subterms $r'$ of $r$, either 

  (a)\quad  $r'$ is a proper subterm of $l$ 
  % (or is a subterm of a reduction of a proper subterm of $l$)
  (or is a reduction of a proper subterm of $l$)

  (b)\quad  $r' <_{cut} l$

  (c)\quad  $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm.

\comment{
\begin{enumerate}
  \item \label{rpc-srp} $r'$ is a proper subterm of $l$ \\
  % (or is a subterm of a reduction of a proper subterm of $l$)
  \item \label{rpc-cut} $r' <_{cut} l$
  \item \label{rps} 
  $r'$ is obtained from $l$ by reduction of $l$ at a proper subterm.
\end{enumerate}
}
\end{condition}

For assuming that all proper subterms of $l$ are in \SN\,
then Condition~\ref{st-rpc1}(a) implies that $r' \in \SN$, and
\ref{st-rpc1}(c) implies that $r' <_{sn1} l$, so
$r' <_{dt}^+ l$.

Note that sometimes
% , as in Example~\ref{s-diff}, 
we \emph{enlarge} the relation $\rho$ to satisfy 
Conditions 1 and 2.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Inductive Strong Normalisation}
  \end{Heading}

Recall $t \in \SN$ iff $t$ is strongly normalising. 

We define \ISN:\\
$t \in \ISN$ 
if $t$ is in \SN\ provided that its immediate subterms are.

\begin{definition}
  $t \in \ISN$ iff: if all the immediate subterms
  of $t$ are strongly normalising then $t$ is strongly
  normalising.
\end{definition}


\begin{lemma}\label{hereds-sn}
  A term $t$ is in \SN\ iff every subterm of $t$ is in \ISN.
\end{lemma}

Proof: The immediate subterm relation is well-founded. \\
The result is proved using well-founded induction.
\end{slide}

\begin{slide}
  \begin{Heading}
    {Strong-Normalisation Proof -- outline}
  \end{Heading}
  
  \begin{lemma}\label{dtho}
  Assume that the rewrite relation satisfies Condition 1 or 2.
    For a given term $t_0$, if all terms
    ${t'} <_{dt}^+ {t_0}$ are in \ISN, then so is $t_0$.
  \end{lemma}

Proof: 
Given $t_0$, assume that $\rho$ satisfies Condition~\ref{st-rpc} and that

(a): all terms ${t'} <_{dt}^+ {t_0}$ are in \ISN.

\noindent We need to show $t_0 \in \ISN$, so we assume that 

(b): all immediate subterms of $t_0$ are in \SN,

\noindent and we show that $t_0 \in \SN$.
To show this, let $t_0$ reduce to $t_1$, show $t_1 \in \SN$. \ldots

\begin{theorem} \label{thm:all-sno}
    If $\rho$ satisfies Condition~\ref{st-rpc}
    and $\dtord{}{} \ = \ \cutord{}{} \cup \snoneord{}{}$
    is well-founded, then 
    every term is strongly normalising.
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dtho} that
every term is in \ISN; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}

\comment{
\begin{slide}
  \begin{Heading}
    {Strong-Normalisation Proof}
  \end{Heading}
  
  \begin{lemma}\label{dth}
  Assume that the rewrite relation satisfies Condition 1 or 2.
    For a given term $t_0$, if all terms
    $\dtord{t'}{t_0}$ are in \ISN, then so is $t_0$.
  \end{lemma}

Proof: 
Given $t_0$, assume that $\rho$ satisfies Condition~\ref{st-rpc} and that

(a): all terms ${t'} <_{dt}^+ {t_0}$ are in \ISN.

\noindent We need to show $t_0 \in \ISN$, so we assume that 

(b): all immediate subterms of $t_0$ are in \SN,

\noindent and we show that $t_0 \in \SN$.
To show this, let $t_0$ reduce to $t_1$, show $t_1 \in \SN$.

Two cases:
reduction occurs in a proper subterm of $t_0$, 
or of $t_0$ as a whole.

Reduction in a proper subterm of $t_0$ (which is in \SN, by (b)): 

So $\snoneord{t_1}{t_0}$ and $\dtord{t_1}{t_0}$.
Therefore $t_1 \in \ISN$ by assumption (a). %~\ref{ass1}. 

\end{slide}

\begin{slide}
  \begin{heading}
    {Strong-Normalisation Proof (ctd)}
  \end{heading}
Now each immediate subterm of $t_1$ is equal to, or is a reduction of,
an immediate subterm of $t_0$,
which itself is in \SN\ by assumption (b). %~\ref{ass2}.

All immediate subterms of $t_1$ are therefore in \SN. \\
Then, as $t_1 \in \ISN$, we have $t_1 \in \SN$.

$({t_1}, {t_0}) \in \rho$:
By Condition~\ref{st-rpc},
subterms of $t_1$ are either in \SN\ \\
or are $<_{dt}^+$-smaller than $t_0$ (and so in \ISN, by (a)).

That is, every subterm $t_1^s$ of $t_1$ (including
$t_1$ itself) is in \ISN, \\
so $t_1 \in \SN$ by Lemma~\ref{hereds-sn}.

\begin{theorem} \label{thm:all-sn}
    If $\rho$ satisfies Condition~\ref{st-rpc}
    and $\dtord{}{} \ = \ \cutord{}{} \cup \snoneord{}{}$
    is well-founded, then 
    every term is strongly normalising.
\end{theorem}

Proof: By well-founded induction, it follows from Lemma~\ref{dth} that
every term is in \ISN; the result follows
from Lemma~\ref{hereds-sn}. 

\end{slide}
}

\begin{slide}
  \begin{Heading}
    {Generalisation to Abstract Terms}
  \end{Heading}
  \begin{heading}
    {The Termination Conditions}
  \end{heading}

\begin{condition}\label{conds-defs}
\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} \ldots
% 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} \ldots
% $\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}
Think of $s' \vtl s$ as like $s'$ is an immediate subterm of $s$.

Note: Each of \ref{rpc} to \ref{rpc2} implies \ref{rpc0}
\end{slide}

\begin{slide}
  \begin{heading}
    {Definitions: \gbars}
  \end{heading}
\begin{definition}[\gbars] \label{def-gbars-isa} 
(Generalises \bars) 
For sets $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}

\begin{lemma}[\gbars -alternative] \label{def-gbars} 
$t \in \gbars\ \sigma\ Q\ S$ iff: \\
for every downward $\sigma$-chain 
$t = t_0 >_\sigma t_1 >_\sigma t_2 >_\sigma \ldots$,
either
\begin{itemize}
\item the chain is finite and all $t_i \in Q$, or 
\item 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{itemize}
\end{lemma}
\end{slide}

\begin{slide}
  \begin{heading}
    {Definitions: \bars, \wfp, \gindy}
  \end{heading}
\begin{definition}[\wfp, \bars] \label{def-wfp,bars} 
Let $\mathcal{U}$ be the universal set of objects.  Then
\begin{enumerate}
\item $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$ is \emph{accessible} in $\sigma$ '').
  %or $s$ is in the \emph{well-founded part} of $\sigma$
\end{enumerate}
\end{definition}

\begin{definition}[\gindy] \label{def-gindy} 
(Generalises \ISN) 
For a relation $\sigma$ and set $S$, an object $t \in \gindy\ \sigma\ S$ iff: 
\quad if $\forall u.\ (u, t) \in \sigma \Rightarrow u \in S$, then $t \in S$.
\end{definition}

\begin{lemma}\label{gindy-gbars}
  $S = \gbars\ \sigma\ (\gindy\ \sigma\ S)\ S $
\end{lemma}

\begin{lemma}\label{l2}
\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}

\end{slide}

\begin{slide}
  \begin{heading}
    {The Termination Theorem} 
  \end{heading}
\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}


\textit{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 that 

(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}.

\end{slide}

\begin{slide}
  \begin{heading}
    {The Termination Theorem --- proof (ctd)} 
  \end{heading}
% 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 $s \in \bars\ \rho\ (\gbars \vtl \{u\:|\ u \ll s\}\ \SN)$.

As \bars\ is monotonic in its second argument, 
to show $s \in \bars\ \rho\ \SN$, \\ 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, by Lemma~\ref{gindy-gbars},
$$\gbars \vtl \{u\:|\ u \ll s\}\ \SN \subseteq
\gbars \vtl (\gindy \vtl \SN)\ \SN = \SN$$

So we have $s \in \SN$.
Thus, discharging assumptions (b) and then (a),
we have $s \in \gindy \vtl \SN$,
and then $s \in \gindy \ll (\gindy \vtl \SN)$. 

\end{slide}

\begin{slide}
  \begin{heading}
    {The Termination Theorem --- 
    wrapping up the proof}
  \end{heading}
\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}

Note: enough that $\vtl$ and $\ll$ are well-founded.

\textit{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.  
\end{slide}

\begin{slide}
  \begin{heading}
    {Goubault-Larrecq's Theorem 1}
  \end{heading}
Suppose that, whenever $s >_\rho t$, either  
\begin{enumerate}
\item[(i)] \label{P1a} for some object $u$, $s \vtr u$ and $u \geq_\rho t$, or
\item[(ii)] \label{P1b} $s \gg t$ and, for every $u \vtl t$, $s >_\rho u$.
\end{enumerate}
Assume also that
\begin{enumerate}
\item[(iii)] $\vtl$ is well-founded
  \quad (whence \ref{vbs} of Theorem~\ref{thm-allsn})
\item[(iv)] every object is in $\bars \ll (\gindy \vtl \SN)$
  \quad (ie, \ref{ubg} of Theorem~\ref{thm-allsn})
\end{enumerate}
Then $\rho$ is well-founded.

Proved that this follows from Theorem~\ref{thm-allsn}: key step is to \\
use (i) and (ii), and well-founded induction on $\vtl$
(by (iii)), to get Condition~\ref{conds-defs}\ref{rpc}.
\end{slide}

\begin{slide}
  \begin{heading}
    {Typed Combinators}
  \end{heading}
${S f g x = f x (g x)} \qquad {W f x = f x x}$

Untyped, these do not terminate: 

$(S I I) (S I I) \longrightarrow^+ (S I I) (S I I)$

$(W I) (W I) \longrightarrow^+ (W I) (W I)$

$W W W \longrightarrow W W W$

\end{slide}

\begin{slide}
  \begin{heading}
    {Typed Combinators --- first proof}
  \end{heading}
Define reduction relations $\sigma, \tau$, and
let $\rho = \ctxt\ \sigma \cup \tau$.
Note that ``\SN'' is wrt $\rho$.
\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
where
$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$. 

Now $\tau$ and $\rho$ (but \emph{not} $\sigma$)
are defined, indirectly, in terms of themselves.
%
But recursive definitions are in terms of ``smaller'' types
(checked in Isabelle!)
% (a bit tricky --- definitions in Isabelle correspondingly so,
% but Isabelle definitions ensure well-definedness)

$t <_{sn1} s$ if $(t, s) \in \ctxt\ \sigma$ by reducing
an immediate subterm in $\wfp\, (\ctxt\ \sigma)$
\\
$t <_{ty} s$ if $t$ has smaller type than $s$.

\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}

Finally show $\vtl$ and $\ll$ well-founded to complete the proof.
\end{slide}


\begin{slide}
  \begin{heading}
    {Typed Combinators --- second proof}
  \end{heading}
  Uses a \emph{different} relation as $\vtl$ 
  (not the immediate subterm relation!)
\begin{eqnarray}
\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
  \qquad \mbox{and } \sigma \subseteq \rho \\
\label{inarg} (x'_i, x_i) \in \ctxt\ \sigma & \Rightarrow &
  f x_1 \ldots x_i \ldots x_n >_\rho f x_1 \ldots x'_i \ldots x_n
\end{eqnarray}
%
From (\ref{Sfgxy}) and (\ref{inarg}),
$\ctxt\ \sigma \subseteq \rho$.

Again, definitions sound, 
as a reduction preserves or reduces 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 $x_i \in \wfp\, (\ctxt\ \sigma)$. \\[1ex]

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)$.

\end{slide}

\begin{slide}
  \begin{heading}
    {Typed Combinators --- second proof, ctd}
  \end{heading}
  Let $\ll\ =\ <_{ty} \cup <_{sn1}$.
We show Condition~\ref{conds-defs}\ref{rpc} holds.

Rule (\ref{aa}), $M >_\rho M N$ if $N \in \SN$:
$M >_{ty} M N$.
For $K \vtl M N$, $K = N \in \SN$, or $K \vtl M$ and so $K \in \SN$.

Rule (\ref{Sfgxy}):
as we can assume $f,g,x,y_i \in \SN$, so $f x (g x) y_1 \ldots y_n \in \SN$

Rule (\ref{inarg}): $lhs >_{sn1} rhs$, and each $\vtl$-subterm of $rhs$
is a $\vtl$-subterm of $lhs$, \\
or a reduction thereof, and so is in \SN.

So Condition~\ref{conds-defs}\ref{rpc} holds, 
and $vtl$ and $\ll$ are well-founded, \\
so $\rho$ is well-founded, by Theorem~\ref{thm-allsn}.
\end{slide}

\begin{slide}
  \begin{heading}
    {Incremental Proofs of Termination}
  \end{heading}
Terminating system of rewrite rules $\mathcal R_0$,
head symbols in $\mathcal F_0$.

Additional rules, head symbols in $\mathcal F_1$.

If additional rules satisfy conditions similar to main theorem, \\
then whole system is terminating: subject to some restrictions.

Most significant restriction is that rules $\mathcal R_0$
be right linear.

  \begin{heading}
    {Incremental Path Ordering}
  \end{heading}
Like recursive path ordering, but built on top of 
rewrite system based on $\mathcal R_0$. 

Same restriction on $\mathcal R_0$.

Proofs in Isabelle only!
\end{slide}

\end{document}