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