Inductive definitions are an indispensable tool in the study of programming languages. This chapter develops the basic framework of inductive definitions and gives some examples of their use. An inductive definition consists of a set of rules for deriving judgments, or assertions, of a variety of forms. Judgments are statements about one or more syntactic objects of a specified sort. The rules specify necessary and sufficient conditions for the validity of a judgment and hence fully determine its meaning.
We start with the notion of a judgment, or assertion, about a syntactic object. We make use of many forms of judgment, including examples such as these:
|n nat||n is a natural number|
|n = ...|