doc-src/TutorialI/Advanced/document/WFrec.tex
author paulson
Fri Jan 05 18:32:57 2001 +0100 (2001-01-05)
changeset 10795 9e888d60d3e5
parent 10654 458068404143
child 10842 4649e5e3905d
permissions -rw-r--r--
minor edits to Chapters 1-3
     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 \rmindex{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 definition above:
    80 \indexbold{*recdef_wf}%
    81 \end{isamarkuptext}%
    82 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%
    83 %%% Local Variables:
    84 %%% mode: latex
    85 %%% TeX-master: "root"
    86 %%% End: