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