|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{WFrec}% |
|
4 % |
|
5 \begin{isamarkuptext}% |
|
6 \noindent |
|
7 So far, all recursive definitions where shown to terminate via measure |
|
8 functions. Sometimes this can be quite inconvenient or even |
|
9 impossible. Fortunately, \isacommand{recdef} supports much more |
|
10 general definitions. For example, termination of Ackermann's function |
|
11 can be shown by means of the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:% |
|
12 \end{isamarkuptext}% |
|
13 \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
|
14 \isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
|
15 \ \ {\isachardoublequote}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline |
|
16 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
|
17 \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
|
18 \begin{isamarkuptext}% |
|
19 \noindent |
|
20 The lexicographic product decreases if either its first component |
|
21 decreases (as in the second equation and in the outer call in the |
|
22 third equation) or its first component stays the same and the second |
|
23 component decreases (as in the inner call in the third equation). |
|
24 |
|
25 In general, \isacommand{recdef} supports termination proofs based on |
|
26 arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded |
|
27 recursion}\indexbold{recursion!wellfounded}\index{wellfounded |
|
28 recursion|see{recursion, wellfounded}}. A relation $<$ is |
|
29 \bfindex{wellfounded} if it has no infinite descending chain $\cdots < |
|
30 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set |
|
31 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation |
|
32 and $r$ the argument of some recursive call on the corresponding |
|
33 right-hand side, induces a wellfounded relation. For a systematic |
|
34 account of termination proofs via wellfounded relations see, for |
|
35 example, \cite{Baader-Nipkow}. |
|
36 |
|
37 Each \isacommand{recdef} definition should be accompanied (after the |
|
38 name of the function) by a wellfounded relation on the argument type |
|
39 of the function. For example, \isa{measure} is defined by |
|
40 \begin{isabelle}% |
|
41 \ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}% |
|
42 \end{isabelle} |
|
43 and it has been proved that \isa{measure\ f} is always wellfounded. |
|
44 |
|
45 In addition to \isa{measure}, the library provides |
|
46 a number of further constructions for obtaining wellfounded relations. |
|
47 |
|
48 wf proof auto if stndard constructions.% |
|
49 \end{isamarkuptext}% |
|
50 \end{isabellebody}% |
|
51 %%% Local Variables: |
|
52 %%% mode: latex |
|
53 %%% TeX-master: "root" |
|
54 %%% End: |