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 \ldots . A slightly more complicated example, the |
8 We start with a simple example: the set of even numbers. |
|
9 A slightly more complicated example, the |
9 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, |
10 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, |
10 some standard induction heuristics are discussed. To demonstrate the |
11 some standard induction heuristics are discussed. To demonstrate the |
11 versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study |
12 versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study |
12 from the realm of context-free grammars. The chapter closes with a discussion |
13 from the realm of context-free grammars. The chapter closes with a discussion |
13 of advanced forms of inductive definitions. |
14 of advanced forms of inductive definitions. |
14 |
15 |
|
16 \input{Inductive/Even} |
15 \input{Inductive/document/Star} |
17 \input{Inductive/document/Star} |
16 \input{Inductive/document/AB} |
18 \input{Inductive/document/AB} |
17 |
19 |
18 \index{inductive definition|)} |
20 \index{inductive definition|)} |
19 \index{*inductive|)} |
21 \index{*inductive|)} |