1.1 --- a/doc-src/TutorialI/fp.tex Fri May 18 16:45:55 2001 +0200
1.2 +++ b/doc-src/TutorialI/fp.tex Fri May 18 17:18:43 2001 +0200
1.3 @@ -1,54 +1,4 @@
1.4 -\chapter{Functional Programming in HOL}
1.5 -
1.6 -Although on the surface this chapter is mainly concerned with how to write
1.7 -functional programs in HOL and how to verify them, most of the constructs and
1.8 -proof procedures introduced are general purpose and recur in any specification
1.9 -or verification task. In fact, we really should speak of functional
1.10 -\emph{modelling} rather than \emph{programming}: our primary aim is not
1.11 -to write programs but to design abstract models of systems. HOL is
1.12 -a specification language that goes well beyond what can be expressed as a
1.13 -program. However, for the time being we concentrate on the computable.
1.14 -
1.15 -The dedicated functional programmer should be warned: HOL offers only
1.16 -\emph{total functional programming} --- all functions in HOL must be total,
1.17 -i.e.\ they must terminate for all inputs; lazy data structures are not
1.18 -directly available.
1.19 -
1.20 -\section{An Introductory Theory}
1.21 -\label{sec:intro-theory}
1.22 -
1.23 -Functional programming needs datatypes and functions. Both of them can be
1.24 -defined in a theory with a syntax reminiscent of languages like ML or
1.25 -Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
1.26 -We will now examine it line by line.
1.27 -
1.28 -\begin{figure}[htbp]
1.29 -\begin{ttbox}\makeatother
1.30 -\input{ToyList2/ToyList1}\end{ttbox}
1.31 -\caption{A theory of lists}
1.32 -\label{fig:ToyList}
1.33 -\end{figure}
1.34 -
1.35 -{\makeatother\input{ToyList/document/ToyList.tex}}
1.36 -
1.37 -The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
1.38 -concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
1.39 -constitutes the complete theory \texttt{ToyList} and should reside in file
1.40 -\texttt{ToyList.thy}. It is good practice to present all declarations and
1.41 -definitions at the beginning of a theory to facilitate browsing.
1.42 -
1.43 -\begin{figure}[htbp]
1.44 -\begin{ttbox}\makeatother
1.45 -\input{ToyList2/ToyList2}\end{ttbox}
1.46 -\caption{Proofs about lists}
1.47 -\label{fig:ToyList-proofs}
1.48 -\end{figure}
1.49 -
1.50 -\subsubsection*{Review}
1.51 -
1.52 -This is the end of our toy proof. It should have familiarized you with
1.53 -\begin{itemize}
1.54 -\item the standard theorem proving procedure:
1.55 +\chapter{Functional Programming in HOL}
1.56
1.57 Although on the surface this chapter is mainly concerned with how to write
1.58 functional programs in HOL and how to verify them, most of the constructs and
1.59 proof procedures introduced are general purpose and recur in any specification
1.60 or verification task. In fact, we really should speak of functional
1.61 \emph{modelling} rather than \emph{programming}: our primary aim is not
1.62 to write programs but to design abstract models of systems. HOL is
1.63 a specification language that goes well beyond what can be expressed as a
1.64 program. However, for the time being we concentrate on the computable.
1.65
1.66 The dedicated functional programmer should be warned: HOL offers only
1.67 \emph{total functional programming} --- all functions in HOL must be total,
1.68 i.e.\ they must terminate for all inputs; lazy data structures are not
1.69 directly available.
1.70
1.71 \section{An Introductory Theory}
1.72 \label{sec:intro-theory}
1.73
1.74 Functional programming needs datatypes and functions. Both of them can be
1.75 defined in a theory with a syntax reminiscent of languages like ML or
1.76 Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
1.77 We will now examine it line by line.
1.78
1.79 \begin{figure}[htbp]
1.80 \begin{ttbox}\makeatother
1.81 \input{ToyList2/ToyList1}\end{ttbox}
1.82 \caption{A theory of lists}
1.83 \label{fig:ToyList}
1.84 \end{figure}
1.85
1.86 {\makeatother\input{ToyList/document/ToyList.tex}}
1.87
1.88 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
1.89 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
1.90 constitutes the complete theory \texttt{ToyList} and should reside in file
1.91 \texttt{ToyList.thy}. It is good practice to present all declarations and
1.92 definitions at the beginning of a theory to facilitate browsing.
1.93
1.94 \begin{figure}[htbp]
1.95 \begin{ttbox}\makeatother
1.96 \input{ToyList2/ToyList2}\end{ttbox}
1.97 \caption{Proofs about lists}
1.98 \label{fig:ToyList-proofs}
1.99 \end{figure}
1.100
1.101 \subsubsection*{Review}
1.102
1.103 This is the end of our toy proof. It should have familiarized you with
1.104 \begin{itemize}
1.105 \item the standard theorem proving procedure:
1.106 state a goal (lemma or theorem); proceed with proof until a separate lemma is
1.107 required; prove that lemma; come back to the original goal.
1.108 \item a specific procedure that works well for functional programs:
1.109 @@ -374,58 +324,7 @@
1.110 {\makeatother\input{Datatype/document/Nested.tex}}
1.111
1.112
1.113 -\subsection{The Limits of Nested Recursion}
1.114 -
1.115 -How far can we push nested recursion? By the unfolding argument above, we can
1.116 -reduce nested to mutual recursion provided the nested recursion only involves
1.117 -previously defined datatypes. This does not include functions:
1.118 -\begin{isabelle}
1.119 -\isacommand{datatype} t = C "t \isasymRightarrow\ bool"
1.120 -\end{isabelle}
1.121 -This declaration is a real can of worms.
1.122 -In HOL it must be ruled out because it requires a type
1.123 -\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
1.124 -same cardinality --- an impossibility. For the same reason it is not possible
1.125 -to allow recursion involving the type \isa{set}, which is isomorphic to
1.126 -\isa{t \isasymFun\ bool}.
1.127 -
1.128 -Fortunately, a limited form of recursion
1.129 -involving function spaces is permitted: the recursive type may occur on the
1.130 -right of a function arrow, but never on the left. Hence the above can of worms
1.131 -is ruled out but the following example of a potentially infinitely branching tree is
1.132 -accepted:
1.133 -\smallskip
1.134 -
1.135 -\input{Datatype/document/Fundata.tex}
1.136 -\bigskip
1.137 -
1.138 -If you need nested recursion on the left of a function arrow, there are
1.139 -alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
1.140 -\begin{isabelle}
1.141 -\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
1.142 -\end{isabelle}
1.143 -do indeed make sense. Note the different arrow,
1.144 -\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
1.145 -expressing the type of \emph{continuous} functions.
1.146 -There is even a version of LCF on top of HOL,
1.147 -called HOLCF~\cite{MuellerNvOS99}.
1.148 -
1.149 -\index{*primrec|)}
1.150 -\index{*datatype|)}
1.151 -
1.152 -\subsection{Case Study: Tries}
1.153 -\label{sec:Trie}
1.154 -
1.155 -Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
1.156 -indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
1.157 -trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
1.158 -``cat''. When searching a string in a trie, the letters of the string are
1.159 -examined sequentially. Each letter determines which subtrie to search next.
1.160 -In this case study we model tries as a datatype, define a lookup and an
1.161 -update function, and prove that they behave as expected.
1.162 -
1.163 -\begin{figure}[htbp]
1.164 -\begin{center}
1.165 +\subsection{The Limits of Nested Recursion}
1.166
1.167 How far can we push nested recursion? By the unfolding argument above, we can
1.168 reduce nested to mutual recursion provided the nested recursion only involves
1.169 previously defined datatypes. This does not include functions:
1.170 \begin{isabelle}
1.171 \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
1.172 \end{isabelle}
1.173 This declaration is a real can of worms.
1.174 In HOL it must be ruled out because it requires a type
1.175 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
1.176 same cardinality --- an impossibility. For the same reason it is not possible
1.177 to allow recursion involving the type \isa{set}, which is isomorphic to
1.178 \isa{t \isasymFun\ bool}.
1.179
1.180 Fortunately, a limited form of recursion
1.181 involving function spaces is permitted: the recursive type may occur on the
1.182 right of a function arrow, but never on the left. Hence the above can of worms
1.183 is ruled out but the following example of a potentially infinitely branching tree is
1.184 accepted:
1.185 \smallskip
1.186
1.187 \input{Datatype/document/Fundata.tex}
1.188 \bigskip
1.189
1.190 If you need nested recursion on the left of a function arrow, there are
1.191 alternatives to pure HOL\@. In the Logic for Computable Functions
1.192 (LCF), types like
1.193 \begin{isabelle}
1.194 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
1.195 \end{isabelle}
1.196 do indeed make sense~\cite{paulson87}. Note the different arrow,
1.197 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
1.198 expressing the type of \emph{continuous} functions.
1.199 There is even a version of LCF on top of HOL,
1.200 called HOLCF~\cite{MuellerNvOS99}.
1.201
1.202 \index{*primrec|)}
1.203 \index{*datatype|)}
1.204
1.205 \subsection{Case Study: Tries}
1.206 \label{sec:Trie}
1.207
1.208 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
1.209 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
1.210 trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
1.211 ``cat''. When searching a string in a trie, the letters of the string are
1.212 examined sequentially. Each letter determines which subtrie to search next.
1.213 In this case study we model tries as a datatype, define a lookup and an
1.214 update function, and prove that they behave as expected.
1.215
1.216 \begin{figure}[htbp]
1.217 \begin{center}
1.218 \unitlength1mm
1.219 \begin{picture}(60,30)
1.220 \put( 5, 0){\makebox(0,0)[b]{l}}
1.221 @@ -442,58 +341,7 @@
1.222 %
1.223 \put( 5,10){\makebox(0,0)[b]{l}}
1.224 \put(15,10){\makebox(0,0)[b]{n}}
1.225 -\put(25,10){\makebox(0,0)[b]{p}}
1.226 -\put(45,10){\makebox(0,0)[b]{a}}
1.227 -%
1.228 -\put(14,19){\line(-3,-2){9}}
1.229 -\put(15,19){\line(0,-1){5}}
1.230 -\put(16,19){\line(3,-2){9}}
1.231 -\put(45,19){\line(0,-1){5}}
1.232 -%
1.233 -\put(15,20){\makebox(0,0)[b]{a}}
1.234 -\put(45,20){\makebox(0,0)[b]{c}}
1.235 -%
1.236 -\put(30,30){\line(-3,-2){13}}
1.237 -\put(30,30){\line(3,-2){13}}
1.238 -\end{picture}
1.239 -\end{center}
1.240 -\caption{A sample trie}
1.241 -\label{fig:trie}
1.242 -\end{figure}
1.243 -
1.244 -Proper tries associate some value with each string. Since the
1.245 -information is stored only in the final node associated with the string, many
1.246 -nodes do not carry any value. This distinction is modeled with the help
1.247 -of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
1.248 -\input{Trie/document/Trie.tex}
1.249 -
1.250 -\section{Total Recursive Functions}
1.251 -\label{sec:recdef}
1.252 -\index{*recdef|(}
1.253 -
1.254 -Although many total functions have a natural primitive recursive definition,
1.255 -this is not always the case. Arbitrary total recursive functions can be
1.256 -defined by means of \isacommand{recdef}: you can use full pattern-matching,
1.257 -recursion need not involve datatypes, and termination is proved by showing
1.258 -that the arguments of all recursive calls are smaller in a suitable (user
1.259 -supplied) sense. In this section we restrict ourselves to measure functions;
1.260 -more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
1.261 -
1.262 -\subsection{Defining Recursive Functions}
1.263 -\label{sec:recdef-examples}
1.264 -\input{Recdef/document/examples.tex}
1.265 -
1.266 -\subsection{Proving Termination}
1.267 -
1.268 -\input{Recdef/document/termination.tex}
1.269 -
1.270 -\subsection{Simplification with Recdef}
1.271 -\label{sec:recdef-simplification}
1.272 -
1.273 -\input{Recdef/document/simplification.tex}
1.274 -
1.275 -\subsection{Induction}
1.276 -\index{induction!recursion|(}
1.277 +\put(25,10){\makebox(0,0)[b]{p}}
1.278 \put(45,10){\makebox(0,0)[b]{a}}
1.279 %
1.280 \put(14,19){\line(-3,-2){9}}
1.281 \put(15,19){\line(0,-1){5}}
1.282 \put(16,19){\line(3,-2){9}}
1.283 \put(45,19){\line(0,-1){5}}
1.284 %
1.285 \put(15,20){\makebox(0,0)[b]{a}}
1.286 \put(45,20){\makebox(0,0)[b]{c}}
1.287 %
1.288 \put(30,30){\line(-3,-2){13}}
1.289 \put(30,30){\line(3,-2){13}}
1.290 \end{picture}
1.291 \end{center}
1.292 \caption{A sample trie}
1.293 \label{fig:trie}
1.294 \end{figure}
1.295
1.296 Proper tries associate some value with each string. Since the
1.297 information is stored only in the final node associated with the string, many
1.298 nodes do not carry any value. This distinction is modeled with the help
1.299 of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
1.300 \input{Trie/document/Trie.tex}
1.301
1.302 \section{Total Recursive Functions}
1.303 \label{sec:recdef}
1.304 \index{*recdef|(}
1.305
1.306 Although many total functions have a natural primitive recursive definition,
1.307 this is not always the case. Arbitrary total recursive functions can be
1.308 defined by means of \isacommand{recdef}: you can use full pattern-matching,
1.309 recursion need not involve datatypes, and termination is proved by showing
1.310 that the arguments of all recursive calls are smaller in a suitable (user
1.311 supplied) sense. In this section we restrict ourselves to measure functions;
1.312 more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
1.313
1.314 \subsection{Defining Recursive Functions}
1.315 \label{sec:recdef-examples}
1.316 \input{Recdef/document/examples.tex}
1.317
1.318 \subsection{Proving Termination}
1.319
1.320 \input{Recdef/document/termination.tex}
1.321
1.322 \subsection{Simplification with Recdef}
1.323 \label{sec:recdef-simplification}
1.324
1.325 \input{Recdef/document/simplification.tex}
1.326
1.327 \subsection{Induction}
1.328 \index{induction!recursion|(}
1.329 \index{recursion induction|(}
1.330
1.331 \input{Recdef/document/Induction.tex}