5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 Here is a simple example, the Fibonacci function:% |
6 Here is a simple example, the Fibonacci function:% |
7 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
8 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
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 |
9 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
10 \ \ {\isachardoublequote}fib\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline |
10 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
11 \ \ {\isachardoublequote}fib\ \isadigit{1}\ {\isacharequal}\ \isadigit{1}{\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}% |
12 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}% |
13 \begin{isamarkuptext}% |
13 \begin{isamarkuptext}% |
14 \noindent |
14 \noindent |
15 The definition of \isa{fib} is accompanied by a \bfindex{measure function} |
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 |
16 \isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a |
42 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}% |
42 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}% |
43 \begin{isamarkuptext}% |
43 \begin{isamarkuptext}% |
44 Overlapping patterns are disambiguated by taking the order of equations into |
44 Overlapping patterns are disambiguated by taking the order of equations into |
45 account, just as in functional programming:% |
45 account, just as in functional programming:% |
46 \end{isamarkuptext}% |
46 \end{isamarkuptext}% |
47 \isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
47 \isacommand{consts}\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\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 |
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 |
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}% |
50 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}% |
51 \begin{isamarkuptext}% |
51 \begin{isamarkuptext}% |
52 \noindent |
52 \noindent |
53 This defines exactly the same function as \isa{sep} above, i.e.\ |
53 This defines exactly the same function as \isa{sep} above, i.e.\ |
54 \isa{sep\isadigit{1}\ {\isacharequal}\ sep}. |
54 \isa{sep{\isadigit{1}}\ {\isacharequal}\ sep}. |
55 |
55 |
56 \begin{warn} |
56 \begin{warn} |
57 \isacommand{recdef} only takes the first argument of a (curried) |
57 \isacommand{recdef} only takes the first argument of a (curried) |
58 recursive function into account. This means both the termination measure |
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 |
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 |
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 |
61 argument is relevant for termination, you can also rearrange the order of |
62 arguments as in the following definition: |
62 arguments as in the following definition: |
63 \end{warn}% |
63 \end{warn}% |
64 \end{isamarkuptext}% |
64 \end{isamarkuptext}% |
65 \isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
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 |
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 |
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}% |
68 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}% |
69 \begin{isamarkuptext}% |
69 \begin{isamarkuptext}% |
70 Because of its pattern-matching syntax, \isacommand{recdef} is also useful |
70 Because of its pattern-matching syntax, \isacommand{recdef} is also useful |
71 for the definition of non-recursive functions:% |
71 for the definition of non-recursive functions:% |
72 \end{isamarkuptext}% |
72 \end{isamarkuptext}% |
73 \isacommand{consts}\ swap\isadigit{1}\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
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 |
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 |
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}% |
76 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}% |
77 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
78 \noindent |
78 \noindent |
79 For non-recursive functions the termination measure degenerates to the empty |
79 For non-recursive functions the termination measure degenerates to the empty |
80 set \isa{{\isacharbraceleft}{\isacharbraceright}}.% |
80 set \isa{{\isacharbraceleft}{\isacharbraceright}}.% |
81 \end{isamarkuptext}% |
81 \end{isamarkuptext}% |