1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{WFrec}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \noindent |
|
20 So far, all recursive definitions were shown to terminate via measure |
|
21 functions. Sometimes this can be inconvenient or |
|
22 impossible. Fortunately, \isacommand{recdef} supports much more |
|
23 general definitions. For example, termination of Ackermann's function |
|
24 can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
|
25 \end{isamarkuptext}% |
|
26 \isamarkuptrue% |
|
27 \isacommand{consts}\isamarkupfalse% |
|
28 \ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
|
29 \isacommand{recdef}\isamarkupfalse% |
|
30 \ ack\ {\isachardoublequoteopen}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
31 \ \ {\isachardoublequoteopen}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\isanewline |
|
32 \ \ {\isachardoublequoteopen}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
33 \ \ {\isachardoublequoteopen}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
|
34 \begin{isamarkuptext}% |
|
35 \noindent |
|
36 The lexicographic product decreases if either its first component |
|
37 decreases (as in the second equation and in the outer call in the |
|
38 third equation) or its first component stays the same and the second |
|
39 component decreases (as in the inner call in the third equation). |
|
40 |
|
41 In general, \isacommand{recdef} supports termination proofs based on |
|
42 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}. |
|
43 This is called \textbf{well-founded |
|
44 recursion}\indexbold{recursion!well-founded}. A function definition |
|
45 is total if and only if the set of |
|
46 all pairs $(r,l)$, where $l$ is the argument on the |
|
47 left-hand side of an equation and $r$ the argument of some recursive call on |
|
48 the corresponding right-hand side, induces a well-founded relation. For a |
|
49 systematic account of termination proofs via well-founded relations see, for |
|
50 example, Baader and Nipkow~\cite{Baader-Nipkow}. |
|
51 |
|
52 Each \isacommand{recdef} definition should be accompanied (after the function's |
|
53 name) by a well-founded relation on the function's argument type. |
|
54 Isabelle/HOL formalizes some of the most important |
|
55 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For |
|
56 example, \isa{measure\ f} is always well-founded. The lexicographic |
|
57 product of two well-founded relations is again well-founded, which we relied |
|
58 on when defining Ackermann's function above. |
|
59 Of course the lexicographic product can also be iterated:% |
|
60 \end{isamarkuptext}% |
|
61 \isamarkuptrue% |
|
62 \isacommand{consts}\isamarkupfalse% |
|
63 \ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
|
64 \isacommand{recdef}\isamarkupfalse% |
|
65 \ contrived\isanewline |
|
66 \ \ {\isachardoublequoteopen}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
67 {\isachardoublequoteopen}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
68 {\isachardoublequoteopen}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
69 {\isachardoublequoteopen}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
70 {\isachardoublequoteopen}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}% |
|
71 \begin{isamarkuptext}% |
|
72 Lexicographic products of measure functions already go a long |
|
73 way. Furthermore, you may embed a type in an |
|
74 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you |
|
75 will never have to prove well-foundedness of any relation composed |
|
76 solely of these building blocks. But of course the proof of |
|
77 termination of your function definition --- that the arguments |
|
78 decrease with every recursive call --- may still require you to provide |
|
79 additional lemmas. |
|
80 |
|
81 It is also possible to use your own well-founded relations with |
|
82 \isacommand{recdef}. For example, the greater-than relation can be made |
|
83 well-founded by cutting it off at a certain point. Here is an example |
|
84 of a recursive function that calls itself with increasing values up to ten:% |
|
85 \end{isamarkuptext}% |
|
86 \isamarkuptrue% |
|
87 \isacommand{consts}\isamarkupfalse% |
|
88 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
|
89 \isacommand{recdef}\isamarkupfalse% |
|
90 \ f\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
|
91 {\isachardoublequoteopen}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
|
92 \begin{isamarkuptext}% |
|
93 \noindent |
|
94 Since \isacommand{recdef} is not prepared for the relation supplied above, |
|
95 Isabelle rejects the definition. We should first have proved that |
|
96 our relation was well-founded:% |
|
97 \end{isamarkuptext}% |
|
98 \isamarkuptrue% |
|
99 \isacommand{lemma}\isamarkupfalse% |
|
100 \ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequoteopen}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}% |
|
101 \isadelimproof |
|
102 % |
|
103 \endisadelimproof |
|
104 % |
|
105 \isatagproof |
|
106 % |
|
107 \begin{isamarkuptxt}% |
|
108 \noindent |
|
109 The proof is by showing that our relation is a subset of another well-founded |
|
110 relation: one given by a measure function.\index{*wf_subset (theorem)}% |
|
111 \end{isamarkuptxt}% |
|
112 \isamarkuptrue% |
|
113 \isacommand{apply}\isamarkupfalse% |
|
114 \ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}% |
|
115 \begin{isamarkuptxt}% |
|
116 \begin{isabelle}% |
|
117 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
|
118 \end{isabelle} |
|
119 |
|
120 \noindent |
|
121 The inclusion remains to be proved. After unfolding some definitions, |
|
122 we are left with simple arithmetic that is dispatched automatically.% |
|
123 \end{isamarkuptxt}% |
|
124 \isamarkuptrue% |
|
125 \isacommand{by}\isamarkupfalse% |
|
126 \ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
|
127 \endisatagproof |
|
128 {\isafoldproof}% |
|
129 % |
|
130 \isadelimproof |
|
131 % |
|
132 \endisadelimproof |
|
133 % |
|
134 \begin{isamarkuptext}% |
|
135 \noindent |
|
136 |
|
137 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
|
138 crucial hint\cmmdx{hints} to our definition:% |
|
139 \end{isamarkuptext}% |
|
140 \isamarkuptrue% |
|
141 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
|
142 \begin{isamarkuptext}% |
|
143 \noindent |
|
144 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
|
145 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
|
146 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
|
147 termination proof, where we have less control. A tailor-made termination |
|
148 relation makes even more sense when it can be used in several function |
|
149 declarations.% |
|
150 \end{isamarkuptext}% |
|
151 \isamarkuptrue% |
|
152 % |
|
153 \isadelimtheory |
|
154 % |
|
155 \endisadelimtheory |
|
156 % |
|
157 \isatagtheory |
|
158 % |
|
159 \endisatagtheory |
|
160 {\isafoldtheory}% |
|
161 % |
|
162 \isadelimtheory |
|
163 % |
|
164 \endisadelimtheory |
|
165 \end{isabellebody}% |
|
166 %%% Local Variables: |
|
167 %%% mode: latex |
|
168 %%% TeX-master: "root" |
|
169 %%% End: |
|