summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/fp.tex

author | nipkow |

Wed, 30 Jul 2008 16:07:00 +0200 | |

changeset 27712 | 007a339b9e7d |

parent 27015 | f8537d69f514 |

child 44048 | 64f574163ca2 |

permissions | -rw-r--r-- |

added hint about writing "x : set xs".

\chapter{Functional Programming in HOL} This chapter describes how to write functional programs in HOL and how to verify them. However, most of the constructs and proof procedures introduced are general and recur in any specification or verification task. We really should speak of functional \emph{modelling} rather than functional \emph{programming}: our primary aim is not to write programs but to design abstract models of systems. HOL is a specification language that goes well beyond what can be expressed as a program. However, for the time being we concentrate on the computable. If you are a purist functional programmer, please note that all functions in HOL must be total: they must terminate for all inputs. Lazy data structures are not directly available. \section{An Introductory Theory} \label{sec:intro-theory} Functional programming needs datatypes and functions. Both of them can be defined in a theory with a syntax reminiscent of languages like ML or Haskell. As an example consider the theory in figure~\ref{fig:ToyList}. We will now examine it line by line. \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList1}\end{ttbox} \caption{A Theory of Lists} \label{fig:ToyList} \end{figure} \index{*ToyList example|(} {\makeatother\medskip\input{ToyList/document/ToyList.tex}} The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} constitutes the complete theory \texttt{ToyList} and should reside in file \texttt{ToyList.thy}. % It is good practice to present all declarations and %definitions at the beginning of a theory to facilitate browsing.% \index{*ToyList example|)} \begin{figure}[htbp] \begin{ttbox}\makeatother \input{ToyList2/ToyList2}\end{ttbox} \caption{Proofs about Lists} \label{fig:ToyList-proofs} \end{figure} \subsubsection*{Review} This is the end of our toy proof. It should have familiarized you with \begin{itemize} \item the standard theorem proving procedure: state a goal (lemma or theorem); proceed with proof until a separate lemma is required; prove that lemma; come back to the original goal. \item a specific procedure that works well for functional programs: induction followed by all-out simplification via \isa{auto}. \item a basic repertoire of proof commands. \end{itemize} \begin{warn} It is tempting to think that all lemmas should have the \isa{simp} attribute just because this was the case in the example above. However, in that example all lemmas were equations, and the right-hand side was simpler than the left-hand side --- an ideal situation for simplification purposes. Unless this is clearly the case, novices should refrain from awarding a lemma the \isa{simp} attribute, which has a global effect. Instead, lemmas can be applied locally where they are needed, which is discussed in the following chapter. \end{warn} \section{Some Helpful Commands} \label{sec:commands-and-hints} This section discusses a few basic commands for manipulating the proof state and can be skipped by casual readers. There are two kinds of commands used during a proof: the actual proof commands and auxiliary commands for examining the proof state and controlling the display. Simple proof commands are of the form \commdx{apply}(\textit{method}), where \textit{method} is typically \isa{induct_tac} or \isa{auto}. All such theorem proving operations are referred to as \bfindex{methods}, and further ones are introduced throughout the tutorial. Unless stated otherwise, you may assume that a method attacks merely the first subgoal. An exception is \isa{auto}, which tries to solve all subgoals. The most useful auxiliary commands are as follows: \begin{description} \item[Modifying the order of subgoals:] \commdx{defer} moves the first subgoal to the end and \commdx{prefer}~$n$ moves subgoal $n$ to the front. \item[Printing theorems:] \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$ prints the named theorems. \item[Reading terms and types:] \commdx{term} \textit{string} reads, type-checks and prints the given string as a term in the current context; the inferred type is output as well. \commdx{typ} \textit{string} reads and prints the given string as a type in the current context. \end{description} Further commands are found in the Isabelle/Isar Reference Manual~\cite{isabelle-isar-ref}. \begin{pgnote} Clicking on the \pgmenu{State} button redisplays the current proof state. This is helpful in case commands like \isacommand{thm} have overwritten it. \end{pgnote} We now examine Isabelle's functional programming constructs systematically, starting with inductive datatypes. \section{Datatypes} \label{sec:datatype} \index{datatypes|(}% Inductive datatypes are part of almost every non-trivial application of HOL. First we take another look at an important example, the datatype of lists, before we turn to datatypes in general. The section closes with a case study. \subsection{Lists} \index{*list (type)}% Lists are one of the essential datatypes in computing. We expect that you are already familiar with their basic operations. Theory \isa{ToyList} is only a small fragment of HOL's predefined theory \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. The latter contains many further operations. For example, the functions \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first element and the remainder of a list. (However, pattern matching is usually preferable to \isa{hd} and \isa{tl}.) Also available are higher-order functions like \isa{map} and \isa{filter}. Theory \isa{List} also contains more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we always use HOL's predefined lists by building on theory \isa{Main}. \begin{warn} Looking ahead to sets and quanifiers in Part II: The best way to express that some element \isa{x} is in a list \isa{xs} is \isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the set of its elements. By the same device you can also write bounded quantifiers like \isa{$\forall$x $\in$ set xs} or embed lists in other set expressions. \end{warn} \subsection{The General Format} \label{sec:general-datatype} The general HOL \isacommand{datatype} definition is of the form \[ \isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~ C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~ C@m~\tau@{m1}~\dots~\tau@{mk@m} \] where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct constructor names and $\tau@{ij}$ are types; it is customary to capitalize the first letter in constructor names. There are a number of restrictions (such as that the type should not be empty) detailed elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them. Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically during proofs by simplification. The same is true for the equations in primitive recursive function definitions. Every\footnote{Except for advanced datatypes where the recursion involves ``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$ comes equipped with a \isa{size} function from $t$ into the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}. In general, \cdx{size} returns \begin{itemize} \item zero for all constructors that do not have an argument of type $t$, \item one plus the sum of the sizes of all arguments of type~$t$, for all other constructors. \end{itemize} Note that because \isa{size} is defined on every datatype, it is overloaded; on lists \isa{size} is also called \sdx{length}, which is not overloaded. Isabelle will always show \isa{size} on lists as \isa{length}. \subsection{Primitive Recursion} \index{recursion!primitive}% Functions on datatypes are usually defined by recursion. In fact, most of the time they are defined by what is called \textbf{primitive recursion} over some datatype $t$. This means that the recursion equations must be of the form \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \] such that $C$ is a constructor of $t$ and all recursive calls of $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus Isabelle immediately sees that $f$ terminates because one (fixed!) argument becomes smaller with every recursive call. There must be at most one equation for each constructor. Their order is immaterial. A more general method for defining total recursive functions is introduced in {\S}\ref{sec:fun}. \begin{exercise}\label{ex:Tree} \input{Misc/document/Tree.tex}% \end{exercise} \input{Misc/document/case_exprs.tex} \input{Ifexpr/document/Ifexpr.tex} \index{datatypes|)} \section{Some Basic Types} This section introduces the types of natural numbers and ordered pairs. Also described is type \isa{option}, which is useful for modelling exceptional cases. \subsection{Natural Numbers} \label{sec:nat}\index{natural numbers}% \index{linear arithmetic|(} \input{Misc/document/fakenat.tex}\medskip \input{Misc/document/natsum.tex} \index{linear arithmetic|)} \subsection{Pairs} \input{Misc/document/pairs.tex} \subsection{Datatype {\tt\slshape option}} \label{sec:option} \input{Misc/document/Option2.tex} \section{Definitions} \label{sec:Definitions} A definition is simply an abbreviation, i.e.\ a new name for an existing construction. In particular, definitions cannot be recursive. Isabelle offers definitions on the level of types and terms. Those on the type level are called \textbf{type synonyms}; those on the term level are simply called definitions. \subsection{Type Synonyms} \index{type synonyms}% Type synonyms are similar to those found in ML\@. They are created by a \commdx{types} command: \medskip \input{Misc/document/types.tex} \input{Misc/document/prime_def.tex} \section{The Definitional Approach} \label{sec:definitional} \index{Definitional Approach}% As we pointed out at the beginning of the chapter, asserting arbitrary axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order to avoid this danger, we advocate the definitional rather than the axiomatic approach: introduce new concepts by definitions. However, Isabelle/HOL seems to support many richer definitional constructs, such as \isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each \isacommand{primrec} function definition is turned into a proper (nonrecursive!) definition from which the user-supplied recursion equations are automatically proved. This process is hidden from the user, who does not have to understand the details. Other commands described later, like \isacommand{fun} and \isacommand{inductive}, work similarly. This strict adherence to the definitional approach reduces the risk of soundness errors. \chapter{More Functional Programming} The purpose of this chapter is to deepen your understanding of the concepts encountered so far and to introduce advanced forms of datatypes and recursive functions. The first two sections give a structured presentation of theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). You can skip them if you are not planning to perform proofs yourself. We then present a case study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced datatypes, including those involving function spaces, are covered in {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search trees (``tries''). Finally we introduce \isacommand{fun}, a general form of recursive function definition that goes well beyond \isacommand{primrec} ({\S}\ref{sec:fun}). \section{Simplification} \label{sec:Simplification} \index{simplification|(} So far we have proved our theorems by \isa{auto}, which simplifies all subgoals. In fact, \isa{auto} can do much more than that. To go beyond toy examples, you need to understand the ingredients of \isa{auto}. This section covers the method that \isa{auto} always applies first, simplification. Simplification is one of the central theorem proving tools in Isabelle and many other systems. The tool itself is called the \textbf{simplifier}. This section introduces the many features of the simplifier and is required reading if you intend to perform proofs. Later on, {\S}\ref{sec:simplification-II} explains some more advanced features and a little bit of how the simplifier works. The serious student should read that section as well, in particular to understand why the simplifier did something unexpected. \subsection{What is Simplification?} In its most basic form, simplification means repeated application of equations from left to right. For example, taking the rules for \isa{\at} and applying them to the term \isa{[0,1] \at\ []} results in a sequence of simplification steps: \begin{ttbox}\makeatother (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[] \end{ttbox} This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the equations are referred to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification'' because the terms do not necessarily become simpler in the process. The simplifier proves arithmetic goals as described in {\S}\ref{sec:nat} above. Arithmetic expressions are simplified using built-in procedures that go beyond mere rewrite rules. New simplification procedures can be coded and installed, but they are definitely not a matter for this tutorial. \input{Misc/document/simp.tex} \index{simplification|)} \input{Misc/document/Itrev.tex} \begin{exercise} \input{Misc/document/Plus.tex}% \end{exercise} \begin{exercise} \input{Misc/document/Tree2.tex}% \end{exercise} \input{CodeGen/document/CodeGen.tex} \section{Advanced Datatypes} \label{sec:advanced-datatypes} \index{datatype@\isacommand {datatype} (command)|(} \index{primrec@\isacommand {primrec} (command)|(} %|) This section presents advanced forms of datatypes: mutual and nested recursion. A series of examples will culminate in a treatment of the trie data structure. \subsection{Mutual Recursion} \label{sec:datatype-mut-rec} \input{Datatype/document/ABexpr.tex} \subsection{Nested Recursion} \label{sec:nested-datatype} {\makeatother\input{Datatype/document/Nested.tex}} \subsection{The Limits of Nested Recursion} \label{sec:nested-fun-datatype} How far can we push nested recursion? By the unfolding argument above, we can reduce nested to mutual recursion provided the nested recursion only involves previously defined datatypes. This does not include functions: \begin{isabelle} \isacommand{datatype} t = C "t \isasymRightarrow\ bool" \end{isabelle} This declaration is a real can of worms. In HOL it must be ruled out because it requires a type \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the same cardinality --- an impossibility. For the same reason it is not possible to allow recursion involving the type \isa{t set}, which is isomorphic to \isa{t \isasymFun\ bool}. Fortunately, a limited form of recursion involving function spaces is permitted: the recursive type may occur on the right of a function arrow, but never on the left. Hence the above can of worms is ruled out but the following example of a potentially \index{infinitely branching trees}% infinitely branching tree is accepted: \smallskip \input{Datatype/document/Fundata.tex} If you need nested recursion on the left of a function arrow, there are alternatives to pure HOL\@. In the Logic for Computable Functions (\rmindex{LCF}), types like \begin{isabelle} \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" \end{isabelle} do indeed make sense~\cite{paulson87}. Note the different arrow, \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, expressing the type of \emph{continuous} functions. There is even a version of LCF on top of HOL, called \rmindex{HOLCF}~\cite{MuellerNvOS99}. \index{datatype@\isacommand {datatype} (command)|)} \index{primrec@\isacommand {primrec} (command)|)} \subsection{Case Study: Tries} \label{sec:Trie} \index{tries|(}% Tries are a classic search tree data structure~\cite{Knuth3-75} for fast indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and ``cat''. When searching a string in a trie, the letters of the string are examined sequentially. Each letter determines which subtrie to search next. In this case study we model tries as a datatype, define a lookup and an update function, and prove that they behave as expected. \begin{figure}[htbp] \begin{center} \unitlength1mm \begin{picture}(60,30) \put( 5, 0){\makebox(0,0)[b]{l}} \put(25, 0){\makebox(0,0)[b]{e}} \put(35, 0){\makebox(0,0)[b]{n}} \put(45, 0){\makebox(0,0)[b]{r}} \put(55, 0){\makebox(0,0)[b]{t}} % \put( 5, 9){\line(0,-1){5}} \put(25, 9){\line(0,-1){5}} \put(44, 9){\line(-3,-2){9}} \put(45, 9){\line(0,-1){5}} \put(46, 9){\line(3,-2){9}} % \put( 5,10){\makebox(0,0)[b]{l}} \put(15,10){\makebox(0,0)[b]{n}} \put(25,10){\makebox(0,0)[b]{p}} \put(45,10){\makebox(0,0)[b]{a}} % \put(14,19){\line(-3,-2){9}} \put(15,19){\line(0,-1){5}} \put(16,19){\line(3,-2){9}} \put(45,19){\line(0,-1){5}} % \put(15,20){\makebox(0,0)[b]{a}} \put(45,20){\makebox(0,0)[b]{c}} % \put(30,30){\line(-3,-2){13}} \put(30,30){\line(3,-2){13}} \end{picture} \end{center} \caption{A Sample Trie} \label{fig:trie} \end{figure} Proper tries associate some value with each string. Since the information is stored only in the final node associated with the string, many nodes do not carry any value. This distinction is modeled with the help of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). \input{Trie/document/Trie.tex} \index{tries|)} \section{Total Recursive Functions: \isacommand{fun}} \label{sec:fun} \index{fun@\isacommand {fun} (command)|(}\index{functions!total|(} Although many total functions have a natural primitive recursive definition, this is not always the case. Arbitrary total recursive functions can be defined by means of \isacommand{fun}: you can use full pattern matching, recursion need not involve datatypes, and termination is proved by showing that the arguments of all recursive calls are smaller in a suitable sense. In this section we restrict ourselves to functions where Isabelle can prove termination automatically. More advanced function definitions, including user supplied termination proofs, nested recursion and partiality, are discussed in a separate tutorial~\cite{isabelle-function}. \input{Fun/document/fun0.tex} \index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}