O'Reilly logo

Practical Foundations for Programming Languages by Robert Harper

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

2 Inductive Definitions

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.

2.1 Judgments

   

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 natn is a natural number
n = ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required