summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Advanced/Partial.thy

author | nipkow |

Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) | |

changeset 10654 | 458068404143 |

child 10885 | 90695f46440b |

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

*** empty log message ***

1 (*<*)theory Partial = While_Combinator:(*>*)

3 text{*\noindent

4 Throughout the tutorial we have emphasized the fact that all functions

5 in HOL are total. Hence we cannot hope to define truly partial

6 functions. The best we can do are functions that are

7 \emph{underdefined}\index{underdefined function}:

8 for certain arguments we only know that a result

9 exists, but we don't know what it is. When defining functions that are

10 normally considered partial, underdefinedness turns out to be a very

11 reasonable alternative.

13 We have already seen an instance of underdefinedness by means of

14 non-exhaustive pattern matching: the definition of @{term last} in

15 \S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}

16 *}

18 consts hd :: "'a list \<Rightarrow> 'a"

19 primrec "hd (x#xs) = x"

21 text{*\noindent

22 although it generates a warning.

24 Even ordinary definitions allow underdefinedness, this time by means of

25 preconditions:

26 *}

28 constdefs minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"

29 "n \<le> m \<Longrightarrow> minus m n \<equiv> m - n"

31 text{*

32 The rest of this section is devoted to the question of how to define

33 partial recursive functions by other means that non-exhaustive pattern

34 matching.

35 *}

37 subsubsection{*Guarded recursion*}

39 text{* Neither \isacommand{primrec} nor \isacommand{recdef} allow to

40 prefix an equation with a condition in the way ordinary definitions do

41 (see @{term minus} above). Instead we have to move the condition over

42 to the right-hand side of the equation. Given a partial function $f$

43 that should satisfy the recursion equation $f(x) = t$ over its domain

44 $dom(f)$, we turn this into the \isacommand{recdef}

45 @{prop[display]"f(x) = (if x \<in> dom(f) then t else arbitrary)"}

46 where @{term arbitrary} is a predeclared constant of type @{typ 'a}

47 which has no definition. Thus we know nothing about its value,

48 which is ideal for specifying underdefined functions on top of it.

50 As a simple example we define division on @{typ nat}:

51 *}

53 consts divi :: "nat \<times> nat \<Rightarrow> nat"

54 recdef divi "measure(\<lambda>(m,n). m)"

55 "divi(m,n) = (if n = 0 then arbitrary else

56 if m < n then 0 else divi(m-n,n)+1)"

58 text{*\noindent Of course we could also have defined

59 @{term"divi(m,0)"} to be some specific number, for example 0. The

60 latter option is chosen for the predefined @{text div} function, which

61 simplifies proofs at the expense of moving further away from the

62 standard mathematical divison function.

64 As a more substantial example we consider the problem of searching a graph.

65 For simplicity our graph is given by a function (@{term f}) of

66 type @{typ"'a \<Rightarrow> 'a"} which

67 maps each node to its successor, and the task is to find the end of a chain,

68 i.e.\ a node pointing to itself. Here is a first attempt:

69 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}

70 This may be viewed as a fixed point finder or as one half of the well known

71 \emph{Union-Find} algorithm.

72 The snag is that it may not terminate if @{term f} has nontrivial cycles.

73 Phrased differently, the relation

74 *}

76 constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set"

77 "step1 f \<equiv> {(y,x). y = f x \<and> y \<noteq> x}"

79 text{*\noindent

80 must be well-founded. Thus we make the following definition:

81 *}

83 consts find :: "('a \<Rightarrow> 'a) \<times> 'a \<Rightarrow> 'a"

84 recdef find "same_fst (\<lambda>f. wf(step1 f)) step1"

85 "find(f,x) = (if wf(step1 f)

86 then if f x = x then x else find(f, f x)

87 else arbitrary)"

88 (hints recdef_simp:same_fst_def step1_def)

90 text{*\noindent

91 The recursion equation itself should be clear enough: it is our aborted

92 first attempt augmented with a check that there are no non-trivial loops.

94 What complicates the termination proof is that the argument of

95 @{term find} is a pair. To express the required well-founded relation

96 we employ the predefined combinator @{term same_fst} of type

97 @{text[display]"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b\<times>'b)set) \<Rightarrow> (('a\<times>'b) \<times> ('a\<times>'b))set"}

98 defined as

99 @{thm[display]same_fst_def[no_vars]}

100 This combinator is designed for recursive functions on pairs where the first

101 component of the argument is passed unchanged to all recursive

102 calls. Given a constraint on the first component and a relation on the second

103 component, @{term same_fst} builds the required relation on pairs.

104 The theorem @{thm[display]wf_same_fst[no_vars]}

105 is known to the well-foundedness prover of \isacommand{recdef}.

106 Thus well-foundedness of the given relation is immediate.

107 Furthermore, each recursive call descends along the given relation:

108 the first argument stays unchanged and the second one descends along

109 @{term"step1 f"}. The proof merely requires unfolding of some definitions.

111 Normally you will then derive the following conditional variant of and from

112 the recursion equation

113 *}

115 lemma [simp]:

116 "wf(step1 f) \<Longrightarrow> find(f,x) = (if f x = x then x else find(f, f x))"

117 by simp

119 text{*\noindent and then disable the original recursion equation:*}

121 declare find.simps[simp del]

123 text{*

124 We can reason about such underdefined functions just like about any other

125 recursive function. Here is a simple example of recursion induction:

126 *}

128 lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"

129 apply(induct_tac f x rule:find.induct);

130 apply simp

131 done

133 subsubsection{*The {\tt\slshape while} combinator*}

135 text{*If the recursive function happens to be tail recursive, its

136 definition becomes a triviality if based on the predefined \isaindexbold{while}

137 combinator. The latter lives in the library theory

138 \isa{While_Combinator}, which is not part of @{text Main} but needs to

139 be included explicitly among the ancestor theories.

141 Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}

142 and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}

143 That is, @{term"while b c s"} is equivalent to the imperative program

144 \begin{verbatim}

145 x := s; while b(x) do x := c(x); return x

146 \end{verbatim}

147 In general, @{term s} will be a tuple (better still: a record). As an example

148 consider the tail recursive variant of function @{term find} above:

149 *}

151 constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"

152 "find2 f x \<equiv>

153 fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"

155 text{*\noindent

156 The loop operates on two ``local variables'' @{term x} and @{term x'}

157 containing the ``current'' and the ``next'' value of function @{term f}.

158 They are initalized with the global @{term x} and @{term"f x"}. At the

159 end @{term fst} selects the local @{term x}.

161 This looks like we can define at least tail recursive functions

162 without bothering about termination after all. But there is no free

163 lunch: when proving properties of functions defined by @{term while},

164 termination rears its ugly head again. Here is

165 @{thm[source]while_rule}, the well known proof rule for total

166 correctness of loops expressed with @{term while}:

167 @{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be

168 true of the initial state @{term s} and invariant under @{term c}

169 (premises 1 and 2).The post-condition @{term Q} must become true when

170 leaving the loop (premise 3). And each loop iteration must descend

171 along a well-founded relation @{term r} (premises 4 and 5).

173 Let us now prove that @{term find2} does indeed find a fixed point. Instead

174 of induction we apply the above while rule, suitably instantiated.

175 Only the final premise of @{thm[source]while_rule} is left unproved

176 by @{text auto} but falls to @{text simp}:

177 *}

179 lemma lem: "\<lbrakk> wf(step1 f); x' = f x \<rbrakk> \<Longrightarrow> \<exists>y y'.

180 while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,x') = (y,y') \<and>

181 y' = y \<and> f y = y"

182 apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and

183 r = "inv_image (step1 f) fst" in while_rule);

184 apply auto

185 apply(simp add:inv_image_def step1_def)

186 done

188 text{*

189 The theorem itself is a simple consequence of this lemma:

190 *}

192 theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"

193 apply(drule_tac x = x in lem)

194 apply(auto simp add:find2_def)

195 done

197 text{* Let us conclude this section on partial functions by a

198 discussion of the merits of the @{term while} combinator. We have

199 already seen that the advantage (if it is one) of not having to

200 provide a termintion argument when defining a function via @{term

201 while} merely puts off the evil hour. On top of that, tail recursive

202 functions tend to be more complicated to reason about. So why use

203 @{term while} at all? The only reason is executability: the recursion

204 equation for @{term while} is a directly executable functional

205 program. This is in stark contrast to guarded recursion as introduced

206 above which requires an explicit test @{prop"x \<in> dom f"} in the

207 function body. Unless @{term dom} is trivial, this leads to a

208 definition which is either not at all executable or prohibitively

209 expensive. Thus, if you are aiming for an efficiently executable definition

210 of a partial function, you are likely to need @{term while}.

211 *}

213 (*<*)end(*>*)