doc-src/TutorialI/Recdef/document/examples.tex
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10362 c6b197ccf1f1
child 11160 e0ab13bec5c8
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{examples}%
     4 %
     5 \begin{isamarkuptext}%
     6 Here is a simple example, the Fibonacci function:%
     7 \end{isamarkuptext}%
     8 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
     9 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
    10 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
    11 \ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
    12 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
    13 \begin{isamarkuptext}%
    14 \noindent
    15 The definition of \isa{fib} is accompanied by a \bfindex{measure function}
    16 \isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a
    17 natural number. The requirement is that in each equation the measure of the
    18 argument on the left-hand side is strictly greater than the measure of the
    19 argument of each recursive call. In the case of \isa{fib} this is
    20 obviously true because the measure function is the identity and
    21 \isa{Suc\ {\isacharparenleft}Suc\ x{\isacharparenright}} is strictly greater than both \isa{x} and
    22 \isa{Suc\ x}.
    23 
    24 Slightly more interesting is the insertion of a fixed element
    25 between any two elements of a list:%
    26 \end{isamarkuptext}%
    27 \isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    28 \isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    29 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    30 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
    31 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
    32 \begin{isamarkuptext}%
    33 \noindent
    34 This time the measure is the length of the list, which decreases with the
    35 recursive call; the first component of the argument tuple is irrelevant.
    36 The details of tupled $\lambda$-abstractions \isa{{\isasymlambda}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlsub n{\isacharparenright}} are
    37 explained in \S\ref{sec:products}, but for now your intuition is all you need.
    38 
    39 Pattern matching need not be exhaustive:%
    40 \end{isamarkuptext}%
    41 \isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
    42 \isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    43 \ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline
    44 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
    45 \begin{isamarkuptext}%
    46 Overlapping patterns are disambiguated by taking the order of equations into
    47 account, just as in functional programming:%
    48 \end{isamarkuptext}%
    49 \isacommand{consts}\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    50 \isacommand{recdef}\ sep{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    51 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
    52 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
    53 \begin{isamarkuptext}%
    54 \noindent
    55 This defines exactly the same function as \isa{sep} above, i.e.\
    56 \isa{sep{\isadigit{1}}\ {\isacharequal}\ sep}.
    57 
    58 \begin{warn}
    59   \isacommand{recdef} only takes the first argument of a (curried)
    60   recursive function into account. This means both the termination measure
    61   and pattern matching can only use that first argument. In general, you will
    62   therefore have to combine several arguments into a tuple. In case only one
    63   argument is relevant for termination, you can also rearrange the order of
    64   arguments as in the following definition:
    65 \end{warn}%
    66 \end{isamarkuptext}%
    67 \isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    68 \isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
    69 \ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline
    70 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
    71 \begin{isamarkuptext}%
    72 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
    73 for the definition of non-recursive functions:%
    74 \end{isamarkuptext}%
    75 \isacommand{consts}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    76 \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
    77 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
    78 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
    79 \begin{isamarkuptext}%
    80 \noindent
    81 For non-recursive functions the termination measure degenerates to the empty
    82 set \isa{{\isacharbraceleft}{\isacharbraceright}}.%
    83 \end{isamarkuptext}%
    84 \end{isabellebody}%
    85 %%% Local Variables:
    86 %%% mode: latex
    87 %%% TeX-master: "root"
    88 %%% End: