author paulson Mon Dec 04 17:29:48 2000 +0100 (2000-12-04) changeset 10577 b9c290f0343d parent 10522 ed3964d1f1a4 child 10654 458068404143 permissions -rw-r--r--
auto update
     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 well-founded relations as introduced in \S\ref{sec:Well-founded}.

    27 This is called \textbf{well-founded

    28 recursion}\indexbold{recursion!well-founded}. Clearly, a function definition

    29 is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the

    30 left-hand side of an equation and $r$ the argument of some recursive call on

    31 the corresponding right-hand side, induces a well-founded relation.  For a

    32 systematic account of termination proofs via well-founded relations see, for

    33 example, \cite{Baader-Nipkow}.

    34

    35 Each \isacommand{recdef} definition should be accompanied (after the name of

    36 the function) by a well-founded relation on the argument type of the

    37 function.  The HOL library formalizes some of the most important

    38 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For

    39 example, \isa{measure\ f} is always well-founded, and the lexicographic

    40 product of two well-founded relations is again well-founded, which we relied

    41 on when defining Ackermann's function above.

    42 Of course the lexicographic product can also be interated:%

    43 \end{isamarkuptext}%

    44 \isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline

    45 \isacommand{recdef}\ contrived\isanewline

    46 \ \ {\isachardoublequote}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}{\isachardoublequote}\isanewline

    47 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline

    48 {\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline

    49 {\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline

    50 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}%

    51 \begin{isamarkuptext}%

    52 Lexicographic products of measure functions already go a long

    53 way. Furthermore you may embed some type in an

    54 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you

    55 will never have to prove well-foundedness of any relation composed

    56 solely of these building blocks. But of course the proof of

    57 termination of your function definition, i.e.\ that the arguments

    58 decrease with every recursive call, may still require you to provide

    59 additional lemmas.

    60

    61 It is also possible to use your own well-founded relations with \isacommand{recdef}.

    62 Here is a simplistic example:%

    63 \end{isamarkuptext}%

    64 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline

    65 \isacommand{recdef}\ f\ {\isachardoublequote}id{\isacharparenleft}less{\isacharunderscore}than{\isacharparenright}{\isachardoublequote}\isanewline

    66 {\isachardoublequote}f\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline

    67 {\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}%

    68 \begin{isamarkuptext}%

    69 \noindent

    70 Since \isacommand{recdef} is not prepared for \isa{id}, the identity

    71 function, this leads to the complaint that it could not prove

    72 \isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}.

    73 We should first have proved that \isa{id} preserves well-foundedness%

    74 \end{isamarkuptext}%

    75 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline

    76 \isacommand{by}\ simp%

    77 \begin{isamarkuptext}%

    78 \noindent

    79 and should have appended the following hint to our above definition:%

    80 \end{isamarkuptext}%

    81 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf\ add{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%

    82 %%% Local Variables:

    83 %%% mode: latex

    84 %%% TeX-master: "root"

    85 %%% End: