10654
|
1 |
(*<*)theory Partial = While_Combinator:(*>*)
|
|
2 |
|
|
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
|
11196
|
9 |
exists, but we do not know what it is. When defining functions that are
|
10654
|
10 |
normally considered partial, underdefinedness turns out to be a very
|
|
11 |
reasonable alternative.
|
|
12 |
|
|
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 |
*}
|
|
17 |
|
|
18 |
consts hd :: "'a list \<Rightarrow> 'a"
|
|
19 |
primrec "hd (x#xs) = x"
|
|
20 |
|
|
21 |
text{*\noindent
|
|
22 |
although it generates a warning.
|
|
23 |
Even ordinary definitions allow underdefinedness, this time by means of
|
|
24 |
preconditions:
|
|
25 |
*}
|
|
26 |
|
|
27 |
constdefs minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
|
|
28 |
"n \<le> m \<Longrightarrow> minus m n \<equiv> m - n"
|
|
29 |
|
|
30 |
text{*
|
|
31 |
The rest of this section is devoted to the question of how to define
|
|
32 |
partial recursive functions by other means that non-exhaustive pattern
|
|
33 |
matching.
|
|
34 |
*}
|
|
35 |
|
10885
|
36 |
subsubsection{*Guarded Recursion*}
|
10654
|
37 |
|
|
38 |
text{* Neither \isacommand{primrec} nor \isacommand{recdef} allow to
|
|
39 |
prefix an equation with a condition in the way ordinary definitions do
|
|
40 |
(see @{term minus} above). Instead we have to move the condition over
|
|
41 |
to the right-hand side of the equation. Given a partial function $f$
|
|
42 |
that should satisfy the recursion equation $f(x) = t$ over its domain
|
|
43 |
$dom(f)$, we turn this into the \isacommand{recdef}
|
|
44 |
@{prop[display]"f(x) = (if x \<in> dom(f) then t else arbitrary)"}
|
|
45 |
where @{term arbitrary} is a predeclared constant of type @{typ 'a}
|
|
46 |
which has no definition. Thus we know nothing about its value,
|
|
47 |
which is ideal for specifying underdefined functions on top of it.
|
|
48 |
|
|
49 |
As a simple example we define division on @{typ nat}:
|
|
50 |
*}
|
|
51 |
|
|
52 |
consts divi :: "nat \<times> nat \<Rightarrow> nat"
|
|
53 |
recdef divi "measure(\<lambda>(m,n). m)"
|
|
54 |
"divi(m,n) = (if n = 0 then arbitrary else
|
|
55 |
if m < n then 0 else divi(m-n,n)+1)"
|
|
56 |
|
|
57 |
text{*\noindent Of course we could also have defined
|
|
58 |
@{term"divi(m,0)"} to be some specific number, for example 0. The
|
|
59 |
latter option is chosen for the predefined @{text div} function, which
|
10885
|
60 |
simplifies proofs at the expense of deviating from the
|
|
61 |
standard mathematical division function.
|
10654
|
62 |
|
|
63 |
As a more substantial example we consider the problem of searching a graph.
|
|
64 |
For simplicity our graph is given by a function (@{term f}) of
|
|
65 |
type @{typ"'a \<Rightarrow> 'a"} which
|
11196
|
66 |
maps each node to its successor, i.e.\ the graph is really a tree.
|
|
67 |
The task is to find the end of a chain, modelled by a node pointing to
|
|
68 |
itself. Here is a first attempt:
|
10654
|
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.
|
11149
|
72 |
The snag is that it may not terminate if @{term f} has non-trivial cycles.
|
10654
|
73 |
Phrased differently, the relation
|
|
74 |
*}
|
|
75 |
|
|
76 |
constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set"
|
|
77 |
"step1 f \<equiv> {(y,x). y = f x \<and> y \<noteq> x}"
|
|
78 |
|
|
79 |
text{*\noindent
|
|
80 |
must be well-founded. Thus we make the following definition:
|
|
81 |
*}
|
|
82 |
|
|
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)
|
|
89 |
|
|
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.
|
|
93 |
|
11196
|
94 |
What complicates the termination proof is that the argument of @{term find}
|
|
95 |
is a pair. To express the required well-founded relation we employ the
|
|
96 |
predefined combinator @{term same_fst} of type
|
10654
|
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]}
|
11196
|
100 |
This combinator is designed for
|
|
101 |
recursive functions on pairs where the first component of the argument is
|
|
102 |
passed unchanged to all recursive calls. Given a constraint on the first
|
|
103 |
component and a relation on the second component, @{term same_fst} builds the
|
|
104 |
required relation on pairs. The theorem
|
|
105 |
@{thm[display]wf_same_fst[no_vars]}
|
|
106 |
is known to the well-foundedness prover of \isacommand{recdef}. Thus
|
|
107 |
well-foundedness of the relation given to \isacommand{recdef} is immediate.
|
|
108 |
Furthermore, each recursive call descends along that relation: the first
|
|
109 |
argument stays unchanged and the second one descends along @{term"step1
|
|
110 |
f"}. The proof merely requires unfolding of some definitions, as specified in
|
|
111 |
the \isacommand{hints} above.
|
10654
|
112 |
|
|
113 |
Normally you will then derive the following conditional variant of and from
|
|
114 |
the recursion equation
|
|
115 |
*}
|
|
116 |
|
|
117 |
lemma [simp]:
|
|
118 |
"wf(step1 f) \<Longrightarrow> find(f,x) = (if f x = x then x else find(f, f x))"
|
|
119 |
by simp
|
|
120 |
|
|
121 |
text{*\noindent and then disable the original recursion equation:*}
|
|
122 |
|
|
123 |
declare find.simps[simp del]
|
|
124 |
|
|
125 |
text{*
|
|
126 |
We can reason about such underdefined functions just like about any other
|
|
127 |
recursive function. Here is a simple example of recursion induction:
|
|
128 |
*}
|
|
129 |
|
|
130 |
lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
|
|
131 |
apply(induct_tac f x rule:find.induct);
|
|
132 |
apply simp
|
|
133 |
done
|
|
134 |
|
10885
|
135 |
subsubsection{*The {\tt\slshape while} Combinator*}
|
10654
|
136 |
|
|
137 |
text{*If the recursive function happens to be tail recursive, its
|
|
138 |
definition becomes a triviality if based on the predefined \isaindexbold{while}
|
10885
|
139 |
combinator. The latter lives in the Library theory
|
10654
|
140 |
\isa{While_Combinator}, which is not part of @{text Main} but needs to
|
|
141 |
be included explicitly among the ancestor theories.
|
|
142 |
|
|
143 |
Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
|
|
144 |
and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}
|
|
145 |
That is, @{term"while b c s"} is equivalent to the imperative program
|
|
146 |
\begin{verbatim}
|
|
147 |
x := s; while b(x) do x := c(x); return x
|
|
148 |
\end{verbatim}
|
|
149 |
In general, @{term s} will be a tuple (better still: a record). As an example
|
11157
|
150 |
consider the following definition of function @{term find} above:
|
10654
|
151 |
*}
|
|
152 |
|
|
153 |
constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
154 |
"find2 f x \<equiv>
|
|
155 |
fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"
|
|
156 |
|
|
157 |
text{*\noindent
|
|
158 |
The loop operates on two ``local variables'' @{term x} and @{term x'}
|
|
159 |
containing the ``current'' and the ``next'' value of function @{term f}.
|
|
160 |
They are initalized with the global @{term x} and @{term"f x"}. At the
|
|
161 |
end @{term fst} selects the local @{term x}.
|
|
162 |
|
11158
|
163 |
Although the definition of tail recursive functions via @{term while} avoids
|
|
164 |
termination proofs, there is no free lunch. When proving properties of
|
|
165 |
functions defined by @{term while}, termination rears its ugly head
|
|
166 |
again. Here is @{thm[source]while_rule}, the well known proof rule for total
|
10654
|
167 |
correctness of loops expressed with @{term while}:
|
11158
|
168 |
@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be true of
|
|
169 |
the initial state @{term s} and invariant under @{term c} (premises 1
|
|
170 |
and~2). The post-condition @{term Q} must become true when leaving the loop
|
|
171 |
(premise~3). And each loop iteration must descend along a well-founded
|
|
172 |
relation @{term r} (premises 4 and~5).
|
10654
|
173 |
|
|
174 |
Let us now prove that @{term find2} does indeed find a fixed point. Instead
|
|
175 |
of induction we apply the above while rule, suitably instantiated.
|
|
176 |
Only the final premise of @{thm[source]while_rule} is left unproved
|
|
177 |
by @{text auto} but falls to @{text simp}:
|
|
178 |
*}
|
|
179 |
|
10885
|
180 |
lemma lem: "\<lbrakk> wf(step1 f); x' = f x \<rbrakk> \<Longrightarrow>
|
|
181 |
\<exists>y. while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,x') = (y,y) \<and>
|
|
182 |
f y = y"
|
10654
|
183 |
apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
|
|
184 |
r = "inv_image (step1 f) fst" in while_rule);
|
|
185 |
apply auto
|
|
186 |
apply(simp add:inv_image_def step1_def)
|
|
187 |
done
|
|
188 |
|
|
189 |
text{*
|
|
190 |
The theorem itself is a simple consequence of this lemma:
|
|
191 |
*}
|
|
192 |
|
|
193 |
theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"
|
|
194 |
apply(drule_tac x = x in lem)
|
|
195 |
apply(auto simp add:find2_def)
|
|
196 |
done
|
|
197 |
|
|
198 |
text{* Let us conclude this section on partial functions by a
|
|
199 |
discussion of the merits of the @{term while} combinator. We have
|
|
200 |
already seen that the advantage (if it is one) of not having to
|
|
201 |
provide a termintion argument when defining a function via @{term
|
|
202 |
while} merely puts off the evil hour. On top of that, tail recursive
|
|
203 |
functions tend to be more complicated to reason about. So why use
|
|
204 |
@{term while} at all? The only reason is executability: the recursion
|
|
205 |
equation for @{term while} is a directly executable functional
|
|
206 |
program. This is in stark contrast to guarded recursion as introduced
|
|
207 |
above which requires an explicit test @{prop"x \<in> dom f"} in the
|
|
208 |
function body. Unless @{term dom} is trivial, this leads to a
|
11196
|
209 |
definition that is impossible to execute or prohibitively slow.
|
10885
|
210 |
Thus, if you are aiming for an efficiently executable definition
|
10654
|
211 |
of a partial function, you are likely to need @{term while}.
|
|
212 |
*}
|
|
213 |
|
|
214 |
(*<*)end(*>*)
|