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