|
1 \contentsline {section}{\numberline {1}Introduction}{1} |
|
2 \contentsline {section}{\numberline {2}Fixedpoint operators}{2} |
|
3 \contentsline {section}{\numberline {3}Elements of an inductive or co-inductive definition}{2} |
|
4 \contentsline {subsection}{\numberline {3.1}The form of the introduction rules}{2} |
|
5 \contentsline {subsection}{\numberline {3.2}The fixedpoint definitions}{3} |
|
6 \contentsline {subsection}{\numberline {3.3}Mutual recursion}{4} |
|
7 \contentsline {subsection}{\numberline {3.4}Proving the introduction rules}{4} |
|
8 \contentsline {subsection}{\numberline {3.5}The elimination rule}{4} |
|
9 \contentsline {section}{\numberline {4}Induction and co-induction rules}{5} |
|
10 \contentsline {subsection}{\numberline {4.1}The basic induction rule}{5} |
|
11 \contentsline {subsection}{\numberline {4.2}Mutual induction}{5} |
|
12 \contentsline {subsection}{\numberline {4.3}Co-induction}{6} |
|
13 \contentsline {section}{\numberline {5}Examples of inductive and co-inductive definitions}{6} |
|
14 \contentsline {subsection}{\numberline {5.1}The finite set operator}{7} |
|
15 \contentsline {subsection}{\numberline {5.2}Lists of $n$ elements}{7} |
|
16 \contentsline {subsection}{\numberline {5.3}A demonstration of {\ptt mk\unhbox \voidb@x \kern .06em \vbox {\hrule width.3em}cases}}{9} |
|
17 \contentsline {subsection}{\numberline {5.4}A co-inductive definition: bisimulations on lazy lists}{9} |
|
18 \contentsline {subsection}{\numberline {5.5}The accessible part of a relation}{10} |
|
19 \contentsline {subsection}{\numberline {5.6}The primitive recursive functions}{11} |
|
20 \contentsline {section}{\numberline {6}Datatypes and co-datatypes}{13} |
|
21 \contentsline {subsection}{\numberline {6.1}Constructors and their domain}{13} |
|
22 \contentsline {subsection}{\numberline {6.2}The case analysis operator}{14} |
|
23 \contentsline {subsection}{\numberline {6.3}Example: lists and lazy lists}{15} |
|
24 \contentsline {subsection}{\numberline {6.4}Example: mutual recursion}{16} |
|
25 \contentsline {subsection}{\numberline {6.5}A four-constructor datatype}{18} |
|
26 \contentsline {subsection}{\numberline {6.6}Proving freeness theorems}{19} |
|
27 \contentsline {section}{\numberline {7}Conclusions and future work}{20} |
|
28 \contentsline {section}{\numberline {A}Inductive and co-inductive definitions: users guide}{22} |
|
29 \contentsline {subsection}{\numberline {A.1}The result structure}{22} |
|
30 \contentsline {subsection}{\numberline {A.2}The argument structure}{23} |
|
31 \contentsline {section}{\numberline {B}Datatype and co-datatype definitions: users guide}{24} |
|
32 \contentsline {subsection}{\numberline {B.1}The result structure}{24} |
|
33 \contentsline {subsection}{\numberline {B.2}The argument structure}{24} |