3 \index{*inductive|(} |
3 \index{*inductive|(} |
4 |
4 |
5 This chapter is dedicated to the most important definition principle after |
5 This chapter is dedicated to the most important definition principle after |
6 recursive functions and datatypes: inductively defined sets. |
6 recursive functions and datatypes: inductively defined sets. |
7 |
7 |
8 We start with a simple example: the set of even numbers. |
8 We start with a simple example: the set of even numbers. A slightly more |
9 A slightly more complicated example, the |
9 complicated example, the reflexive transitive closure, is the subject of |
10 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, |
10 {\S}\ref{sec:rtc}. In particular, some standard induction heuristics are |
11 some standard induction heuristics are discussed. To demonstrate the |
11 discussed. Advanced forms of inductive definitions are discussed in |
12 versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study |
12 {\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive |
13 from the realm of context-free grammars. The chapter closes with a discussion |
13 definitions, the chapter closes with a case study from the realm of |
14 of advanced forms of inductive definitions. |
14 context-free grammars. The first two sections are required reading for anybody |
|
15 interested in mathematical modelling. |
15 |
16 |
16 \input{Inductive/even-example} |
17 \input{Inductive/even-example} |
17 \input{Inductive/document/Mutual} |
18 \input{Inductive/document/Mutual} |
18 \input{Inductive/document/Star} |
19 \input{Inductive/document/Star} |
19 |
20 |
20 \section{Advanced inductive definitions} |
21 \section{Advanced inductive definitions} |
|
22 \label{sec:adv-ind-def} |
21 \input{Inductive/advanced-examples} |
23 \input{Inductive/advanced-examples} |
22 |
24 |
23 \input{Inductive/document/AB} |
25 \input{Inductive/document/AB} |
24 |
26 |
25 \index{inductive definition|)} |
27 \index{inductive definition|)} |