doc-src/TutorialI/Inductive/inductive.tex
 changeset 10242 028f54cd2cc9 parent 10225 b9fd52525b69 child 10327 19214ac381cf
equal inserted replaced
10241:e0428c2778f1 10242:028f54cd2cc9
     1 \chapter{Inductively Defined Sets}
     1 \chapter{Inductively Defined Sets}

     2 \index{inductive definition|(}

     3 \index{*inductive|(}

     4

     5 This chapter is dedicated to the most important definition principle after

     6 recursive functions and datatypes: inductively defined sets.

     7

     8 We start with a simple example \ldots . A slightly more complicated example, the

     9 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,

    10 some standard induction heuristics are discussed. To demonstrate the

    11 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 of advanced forms of inductive definitions.
     2
    14
     3 \input{Inductive/document/Star}
    15 \input{Inductive/document/Star}
     4 \input{Inductive/document/AB}
    16 \input{Inductive/document/AB}

    17

    18 \index{inductive definition|)}

    19 \index{*inductive|)}

    20

    21 \section{Advanced inductive definitions}