9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{examples}%
|
8749
|
4 |
%
|
|
5 |
\begin{isamarkuptext}%
|
|
6 |
Here is a simple example, the Fibonacci function:%
|
|
7 |
\end{isamarkuptext}%
|
9674
|
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}%
|
8749
|
13 |
\begin{isamarkuptext}%
|
|
14 |
\noindent
|
|
15 |
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
|
9792
|
16 |
\isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a
|
8749
|
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
|
9792
|
21 |
\isa{Suc\ {\isacharparenleft}Suc\ x{\isacharparenright}} is strictly greater than both \isa{x} and
|
|
22 |
\isa{Suc\ x}.
|
8749
|
23 |
|
|
24 |
Slightly more interesting is the insertion of a fixed element
|
|
25 |
between any two elements of a list:%
|
|
26 |
\end{isamarkuptext}%
|
9674
|
27 |
\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\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}%
|
8749
|
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 |
|
|
37 |
Pattern matching need not be exhaustive:%
|
|
38 |
\end{isamarkuptext}%
|
9674
|
39 |
\isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
|
|
40 |
\isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
|
|
41 |
\ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline
|
|
42 |
\ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
|
8749
|
43 |
\begin{isamarkuptext}%
|
|
44 |
Overlapping patterns are disambiguated by taking the order of equations into
|
|
45 |
account, just as in functional programming:%
|
|
46 |
\end{isamarkuptext}%
|
9674
|
47 |
\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
|
|
48 |
\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
|
|
49 |
\ \ {\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
|
|
50 |
\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
|
8749
|
51 |
\begin{isamarkuptext}%
|
|
52 |
\noindent
|
|
53 |
This defines exactly the same function as \isa{sep} above, i.e.\
|
9792
|
54 |
\isa{sep\isadigit{1}\ {\isacharequal}\ sep}.
|
8749
|
55 |
|
|
56 |
\begin{warn}
|
|
57 |
\isacommand{recdef} only takes the first argument of a (curried)
|
|
58 |
recursive function into account. This means both the termination measure
|
|
59 |
and pattern matching can only use that first argument. In general, you will
|
|
60 |
therefore have to combine several arguments into a tuple. In case only one
|
|
61 |
argument is relevant for termination, you can also rearrange the order of
|
|
62 |
arguments as in the following definition:
|
|
63 |
\end{warn}%
|
|
64 |
\end{isamarkuptext}%
|
9674
|
65 |
\isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
|
|
66 |
\isacommand{recdef}\ sep\isadigit{2}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
|
|
67 |
\ \ {\isachardoublequote}sep\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{2}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
|
|
68 |
\ \ {\isachardoublequote}sep\isadigit{2}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
|
8749
|
69 |
\begin{isamarkuptext}%
|
|
70 |
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
|
|
71 |
for the definition of non-recursive functions:%
|
|
72 |
\end{isamarkuptext}%
|
9674
|
73 |
\isacommand{consts}\ swap\isadigit{1}\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
|
|
74 |
\isacommand{recdef}\ swap\isadigit{1}\isadigit{2}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
|
|
75 |
\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
|
|
76 |
\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
|
8749
|
77 |
\begin{isamarkuptext}%
|
|
78 |
\noindent
|
8771
|
79 |
For non-recursive functions the termination measure degenerates to the empty
|
9792
|
80 |
set \isa{{\isacharbraceleft}{\isacharbraceright}}.%
|
8749
|
81 |
\end{isamarkuptext}%
|
9722
|
82 |
\end{isabellebody}%
|
9145
|
83 |
%%% Local Variables:
|
|
84 |
%%% mode: latex
|
|
85 |
%%% TeX-master: "root"
|
|
86 |
%%% End:
|