3 \def\isabellecontext{Partial}%
6 \noindent Throughout the tutorial we have emphasized the fact
7 that all functions in HOL are total. Hence we cannot hope to define
8 truly partial functions but must totalize them. A straightforward
9 totalization is to lift the result type of the function from $\tau$ to
10 $\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
11 returned if the function is applied to an argument not in its
12 domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example.
13 We do not pursue this schema further because it should be clear
14 how it works. Its main drawback is that the result of such a lifted
15 function has to be unpacked first before it can be processed
16 further. Its main advantage is that you can distinguish if the
17 function was applied to an argument in its domain or not. If you do
18 not need to make this distinction, for example because the function is
19 never used outside its domain, it is easier to work with
20 \emph{underdefined}\index{underdefined function} functions: for
21 certain arguments we only know that a result exists, but we do not
22 know what it is. When defining functions that are normally considered
23 partial, underdefinedness turns out to be a very reasonable
26 We have already seen an instance of underdefinedness by means of
27 non-exhaustive pattern matching: the definition of \isa{last} in
28 \S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%
30 \isacommand{consts}\ hd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
31 \isacommand{primrec}\ {\isachardoublequote}hd\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}%
32 \begin{isamarkuptext}%
34 although it generates a warning.
35 Even ordinary definitions allow underdefinedness, this time by means of
38 \isacommand{constdefs}\ minus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
39 {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}%
40 \begin{isamarkuptext}%
41 The rest of this section is devoted to the question of how to define
42 partial recursive functions by other means than non-exhaustive pattern
46 \isamarkupsubsubsection{Guarded Recursion%
49 \begin{isamarkuptext}%
50 Neither \isacommand{primrec} nor \isacommand{recdef} allow to
51 prefix an equation with a condition in the way ordinary definitions do
52 (see \isa{minus} above). Instead we have to move the condition over
53 to the right-hand side of the equation. Given a partial function $f$
54 that should satisfy the recursion equation $f(x) = t$ over its domain
55 $dom(f)$, we turn this into the \isacommand{recdef}
57 \ \ \ \ \ f\ x\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymin}\ dom\ f\ then\ t\ else\ arbitrary{\isacharparenright}%
59 where \isa{arbitrary} is a predeclared constant of type \isa{{\isacharprime}a}
60 which has no definition. Thus we know nothing about its value,
61 which is ideal for specifying underdefined functions on top of it.
63 As a simple example we define division on \isa{nat}:%
65 \isacommand{consts}\ divi\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
66 \isacommand{recdef}\ divi\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}\ m{\isacharparenright}{\isachardoublequote}\isanewline
67 \ \ {\isachardoublequote}divi{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ arbitrary\ else\isanewline
68 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ m\ {\isacharless}\ n\ then\ {\isadigit{0}}\ else\ divi{\isacharparenleft}m{\isacharminus}n{\isacharcomma}n{\isacharparenright}{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}%
69 \begin{isamarkuptext}%
70 \noindent Of course we could also have defined
71 \isa{divi\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}} to be some specific number, for example 0. The
72 latter option is chosen for the predefined \isa{div} function, which
73 simplifies proofs at the expense of deviating from the
74 standard mathematical division function.
76 As a more substantial example we consider the problem of searching a graph.
77 For simplicity our graph is given by a function \isa{f} of
78 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
79 maps each node to its successor, i.e.\ the graph is really a tree.
80 The task is to find the end of a chain, modelled by a node pointing to
81 itself. Here is a first attempt:
83 \ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
85 This may be viewed as a fixed point finder or as one half of the well known
86 \emph{Union-Find} algorithm.
87 The snag is that it may not terminate if \isa{f} has non-trivial cycles.
88 Phrased differently, the relation%
90 \isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
91 \ \ {\isachardoublequote}step{\isadigit{1}}\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharequal}\ f\ x\ {\isasymand}\ y\ {\isasymnoteq}\ x{\isacharbraceright}{\isachardoublequote}%
92 \begin{isamarkuptext}%
94 must be well-founded. Thus we make the following definition:%
96 \isacommand{consts}\ find\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
97 \isacommand{recdef}\ find\ {\isachardoublequote}same{\isacharunderscore}fst\ {\isacharparenleft}{\isasymlambda}f{\isachardot}\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}{\isacharparenright}\ step{\isadigit{1}}{\isachardoublequote}\isanewline
98 \ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline
99 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline
100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline
101 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
102 \begin{isamarkuptext}%
104 The recursion equation itself should be clear enough: it is our aborted
105 first attempt augmented with a check that there are no non-trivial loops.
106 To express the required well-founded relation we employ the
107 predefined combinator \isa{same{\isacharunderscore}fst} of type
109 \ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%
113 \ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%
115 This combinator is designed for
116 recursive functions on pairs where the first component of the argument is
117 passed unchanged to all recursive calls. Given a constraint on the first
118 component and a relation on the second component, \isa{same{\isacharunderscore}fst} builds the
119 required relation on pairs. The theorem
121 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%
123 is known to the well-foundedness prover of \isacommand{recdef}. Thus
124 well-foundedness of the relation given to \isacommand{recdef} is immediate.
125 Furthermore, each recursive call descends along that relation: the first
126 argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions, as specified in
127 the \isacommand{hints} above.
129 Normally you will then derive the following conditional variant of and from
130 the recursion equation%
132 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
133 \ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
134 \isacommand{by}\ simp%
135 \begin{isamarkuptext}%
136 \noindent and then disable the original recursion equation:%
138 \isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
139 \begin{isamarkuptext}%
140 We can reason about such underdefined functions just like about any other
141 recursive function. Here is a simple example of recursion induction:%
143 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
144 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
145 \isacommand{apply}\ simp\isanewline
147 \isamarkupsubsubsection{The {\tt\slshape while} Combinator%
150 \begin{isamarkuptext}%
151 If the recursive function happens to be tail recursive, its
152 definition becomes a triviality if based on the predefined \isaindexbold{while}
153 combinator. The latter lives in the Library theory
154 \isa{While_Combinator}, which is not part of \isa{Main} but needs to
155 be included explicitly among the ancestor theories.
157 Constant \isa{while} is of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a}
158 and satisfies the recursion equation \begin{isabelle}%
159 \ \ \ \ \ while\ b\ c\ s\ {\isacharequal}\ {\isacharparenleft}if\ b\ s\ then\ while\ b\ c\ {\isacharparenleft}c\ s{\isacharparenright}\ else\ s{\isacharparenright}%
161 That is, \isa{while\ b\ c\ s} is equivalent to the imperative program
163 x := s; while b(x) do x := c(x); return x
165 In general, \isa{s} will be a tuple (better still: a record). As an example
166 consider the following definition of function \isa{find} above:%
168 \isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
169 \ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
170 \ \ \ fst{\isacharparenleft}while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
171 \begin{isamarkuptext}%
173 The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}
174 containing the ``current'' and the ``next'' value of function \isa{f}.
175 They are initalized with the global \isa{x} and \isa{f\ x}. At the
176 end \isa{fst} selects the local \isa{x}.
178 Although the definition of tail recursive functions via \isa{while} avoids
179 termination proofs, there is no free lunch. When proving properties of
180 functions defined by \isa{while}, termination rears its ugly head
181 again. Here is \isa{while{\isacharunderscore}rule}, the well known proof rule for total
182 correctness of loops expressed with \isa{while}:
184 \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
185 \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline
186 \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline
187 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}%
188 \end{isabelle} \isa{P} needs to be true of
189 the initial state \isa{s} and invariant under \isa{c} (premises 1
190 and~2). The post-condition \isa{Q} must become true when leaving the loop
191 (premise~3). And each loop iteration must descend along a well-founded
192 relation \isa{r} (premises 4 and~5).
194 Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead
195 of induction we apply the above while rule, suitably instantiated.
196 Only the final premise of \isa{while{\isacharunderscore}rule} is left unproved
197 by \isa{auto} but falls to \isa{simp}:%
199 \isacommand{lemma}\ lem{\isacharcolon}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
200 \ \ {\isasymexists}y{\isachardot}\ while\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}f\ x{\isacharprime}{\isacharparenright}{\isacharparenright}\ {\isacharparenleft}x{\isacharcomma}f\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}y{\isacharparenright}\ {\isasymand}\isanewline
201 \ \ \ \ \ \ \ f\ y\ {\isacharequal}\ y{\isachardoublequote}\isanewline
202 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ P\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}x{\isacharprime}{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ f\ x{\isachardoublequote}\ \isakeyword{and}\isanewline
203 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ r\ {\isacharequal}\ {\isachardoublequote}inv{\isacharunderscore}image\ {\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ fst{\isachardoublequote}\ \isakeyword{in}\ while{\isacharunderscore}rule{\isacharparenright}\isanewline
204 \isacommand{apply}\ auto\isanewline
205 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
207 \begin{isamarkuptext}%
208 The theorem itself is a simple consequence of this lemma:%
210 \isacommand{theorem}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ f{\isacharparenleft}find{\isadigit{2}}\ f\ x{\isacharparenright}\ {\isacharequal}\ find{\isadigit{2}}\ f\ x{\isachardoublequote}\isanewline
211 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline
212 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
214 \begin{isamarkuptext}%
215 Let us conclude this section on partial functions by a
216 discussion of the merits of the \isa{while} combinator. We have
217 already seen that the advantage (if it is one) of not having to
218 provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
219 functions tend to be more complicated to reason about. So why use
220 \isa{while} at all? The only reason is executability: the recursion
221 equation for \isa{while} is a directly executable functional
222 program. This is in stark contrast to guarded recursion as introduced
223 above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the
224 function body. Unless \isa{dom} is trivial, this leads to a
225 definition that is impossible to execute or prohibitively slow.
226 Thus, if you are aiming for an efficiently executable definition
227 of a partial function, you are likely to need \isa{while}.%
232 %%% TeX-master: "root"