We introduce inductive types, which allow for a natural description of most of the data structures used in both computer science and logic, such as inductive sets à la ML (e.g. trees, lists, natural numbers). Besides the syntactic aspect of inductive definitions, is the computation part, recursion, and the logical part, induction. The expressivity of the different recursion and induction principles will be discussed. Definitions by induction are also convenient to define logical properties as least predicates satisfying some closure properties.
This document was translated from LATEX by HEVEA.