\documentclass[pdf]{prosper}
\usepackage{alltt}
%\usepackage{proof}
\usepackage{amssymb}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{fancyvrb}

\newrgbcolor{nictablue}{0.0 0.310 0.490}

\newrgbcolor{purple}{0.63 0.13 0.94}
\newrgbcolor{redbrown}{0.698 0.133 0.133}
\newrgbcolor{brown}{0.647 0.165 0.165}
\newrgbcolor{darkviolet}{0.4 0.2 0.6}
\newrgbcolor{lightazure}{0.2 0.6 1.0}
\newrgbcolor{darkazure}{0.0 0.4 0.8}
\newrgbcolor{dkdullazure}{0.2 0.4 0.6}
\newrgbcolor{obsdullazure}{0.0 0.2 0.4}
\newrgbcolor{dkazureblue}{0.0 0.2 0.6}
\newrgbcolor{dkazurecyan}{0.0 0.4 0.6}
\newrgbcolor{dkblueazure}{0.0 0.2 0.8}
\newrgbcolor{obsdullcyan}{0.0 0.4 0.4}

\newrgbcolor{varcolor}{0.2 0.4 0.0}
\newrgbcolor{tycolor}{0.6 0.2 0.2}

\newcommand{\constcolor}{\nictablue}  % have used nictablue, darkviolet

\newcommand{\mytt}{\usefont{OT1}{ppl}{m}{n}}

\newcommand{\fld}[1]{{\nictablue\textsf{#1}}}
\newcommand{\var}[1]{{\varcolor\ensuremath{\mathit{#1}}}}
\newcommand{\tyname}[1]{\textrm{\usefont{OT1}{put}{m}{it}\tycolor #1}}
\newcommand{\constname}[1]{\textrm{\constcolor\mytt #1}}

\newcommand{\ints}{\ensuremath{\mathbb{Z}}}
\newcommand{\nats}{\ensuremath{\mathbb{N}}}
\newcommand{\reals}{\ensuremath{\mathbb{R}}}
\newcommand{\rats}{\ensuremath{\mathbb{Q}}}
\newcommand{\bools}{\ensuremath{\mathbb{B}}}



\title{Termination of rewriting
}
\author{Jeremy Dawson
}
\email{Jeremy.Dawson@nicta.com.au
}
\institution{{\includegraphics{nicta-colour-on-pale.eps}}
}
\date{26th February 2004
}
\slideCaption{Termination of rewriting
}
% \Logo(-1,-1.3){\includegraphics[width=1.7cm]{nicta-colour-on-pale.eps}}
\Logo(-1,-1.3){\includegraphics[width=1.7cm]{nicta-colour-on-pale.eps}
\raisebox{2.5mm}{\scriptsize Propositional
\hspace{3mm} Modal\hspace{3mm} {\red First-Order}\hspace{3mm} Higher-Order}}

\begin{document}

\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{Rewriting}

  \begin{itemize}
  \item Using rewrite rule $(x + 0) \ \ \longrightarrow\ \  x$
  \begin{itemize}
  \item $(a + 0) \times b \ \ \longrightarrow\ \  a \times b$
  \item $((a + 0) + 0) \times (b + 0) \ \ \longrightarrow\ \ 
    a \times b$ (3 steps)
  \end{itemize}
  \item Does this procedure always finish ?
    \begin{itemize}
    \item In this case, yes --- terms get smaller each time
    \end{itemize}
  \item Add the rule
    $(x + y) \times z \ \ \longrightarrow\ \  (x \times z) + (y \times z)$
  \begin{itemize}
  \item $(a + b + c) \times d \times e \ \ \longrightarrow\ \  
  a \times d \times e + b \times d \times e + c \times d \times e$
  \end{itemize}
     % (4 steps)
  \item Can we prove that this terminates?
  \end{itemize}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 1a
\begin{slide}{A tricky one}

  \begin{itemize}
  \item Single rule (integer values, \emph{not} expressions)
  \begin{itemize}
  \item if $n$ odd, $n \geq 2$, $n \ \ \longrightarrow\ \  3n+1$
  \item if $n$ even, $n \geq 2$, $n \ \ \longrightarrow\ \  n/2$
  \end{itemize}
  \item Can express this using term rewrite rules
  \item Not known whether this rewriting always terminates
  \item Example: starting at $27$, get the sequence \\
\scriptsize
$27$ $82$ $41$ $124$ $62$ $31$ $94$ $47$ $142$ $71$ $214$ $107$ $322$
$161$ $484$ $242$ $121$ $364$ $182$ $91$ $274$ $137$ $412$ $206$ $103$
$310$ $155$ $466$ $233$ $700$ $350$ $175$ $526$ $263$ $790$ $395$ $1186$
$593$ $1780$ $890$ $445$ $1336$ $668$ $334$ $167$ $502$ $251$ $754$ $377$
$1132$ $566$ $283$ $850$ $425$ $1276$ $638$ $319$ $958$ $479$ $1438$ $719$
$2158$ $1079$ $3238$ $1619$ $4858$ $2429$ $7288$ $3644$ $1822$ $911$ 
$2734$ $1367$ $4102$ $2051$ $6154$ $3077$ $9232$ $4616$ $2308$ $1154$ $577$
$1732$ $866$ $433$ $1300$ $650$ $325$ $976$ $488$ $244$ $122$ $61$ $184$
$92$ $46$ $23$ $70$ $35$ $106$ $53$ $160$ $80$ $40$ $20$ $10$ $5$ $16$
$8$ $4$ $2$ $1$
  \end{itemize}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{Why does this matter?}

  \begin{itemize}
  \item Assume the rules are true as equalities
  \item Then we can \emph{prove} $(a + 0) \times b = a \times b$
    by \emph{rewriting} $(a + 0) \times b$ to $a \times b$
  \item We can also add logical rules, 
    eg add the rule $x = x \ \ \longrightarrow\ \  True$
  \item Anything that can be rewritten to $True$ is thereby proved
    \begin{itemize}
    \item eg, $(a + 0) \times b = a \times b \ \ \longrightarrow\ \ 
    a \times b = a \times b \ \ \longrightarrow\ \  True$
    \end{itemize}
  \item Rewriting much used in automated theorem proving
  \item For automation, must know that it will terminate
  \end{itemize}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{Cut-elimination a special case}

  \begin{itemize}
  \item Logical system (set of rules) $S$ 
    \begin{itemize}
    \item Additional rule, $ Cut$
    \item Automated proof much easier using $S$ than $S \cup \{Cut\}$ 
    \end{itemize}
  \item Want to show that anything which can be proved using $S \cup \{Cut\}$
    can also be proved using $S$
    \begin{itemize}
    \item Method is to take an arbitrary
    proof using $S \cup \{Cut\}$, and transform
      (\emph{rewrite}) it to a proof using $S$
    \item This transformation is done in several steps,
      called \emph{cut-reduction} steps
    \item Need to show 
    \begin{itemize}
      \item So long as proof still uses $Cut$
	there is still a rewrite step available
      \item the rewriting terminates
    \end{itemize}
    \end{itemize}
    \end{itemize}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Slide 4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}{My work}

\begin{itemize}
  \item There is a published proof of strong normalisation (ie, that \emph{any}
  sequence of \emph{cut-reduction} steps terminates)
  \item Tried to implement this in the Isabelle theorem prover
  \begin{itemize}
  \item discovered a ``bug'' in the proof
  \item one case not dealt with
  \end{itemize}
  \item Devised a new proof, implemented in Isabelle, now published
  \item Realized that this new proof could be expressed as a proof 
  of rewriting termination generally 
  \begin{itemize}
  \item Of course it depends on assumptions about
  the system of rewrite rules
  \end{itemize}
  \item Am now working on using my proof to show termination of various examples
  of rewrite systems, in Isabelle

\end{itemize}

\end{slide}


\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
