3.2 Syntax
 Types and Programming Languages Authors: Pierce B.C. Published year: 2002 Pages: 26/262
 < Free Open Study >

## 3.2 Syntax

There are several equivalent ways of defining the syntax of our language. We have already seen one in the grammar on page 24. This grammar is actually just a compact notation for the following inductive definition:

### 3.2.1 Definition [Terms, Inductively]

The set of terms is the smallest set T such that

1. { true, false, 0 } T ;

2. if t 1 T , then { succ t 1 , pred t 1 , iszero t 1 } T ;

3. if t 1 T , t 2 T , and t 3 T , then if t 1 then t 2 else t 3 T .

Since inductive definitions are ubiquitous in the study of programming languages, it is worth pausing for a moment to examine this one in detail. The first clause tells us three simple expressions that are in T . The second and third clauses give us rules by which we can judge that certain compound expressions are in T . Finally, the word "smallest" tells us that T has no elements besides the ones required by these three clauses.

Like the grammar on page 24, this definition says nothing about the use of parentheses to mark compound subterms. Formally, what's really going on is that we are defining T as a set of trees , not as a set of strings. The use of parentheses in examples is just a way of clarifying the relation between the linearized form of terms that we write on the page and the real underlying tree form.

A different shorthand for the same inductive definition of terms employs the two-dimensional inference rule format commonly used in "natural deduction style" presentations of logical systems:

### 3.2.2 Definition [Terms, by Inference Rules]

The set of terms is defined by the following rules:

The first three rules here restate the first clause of Definition 3.2.1; the next four capture clauses (2) and (3). Each rule is read, "If we have established the statements in the premise (s) listed above the line, then we may derive the conclusion below the line." The fact that T is the smallest set satisfying these rules is often (as here) not stated explicitly.

Two points of terminology deserve mention. First, rules with no premises (like the first three above) are often called axioms . In this book, the term inference rule is used generically to include both axioms and "proper rules" with one or more premises. Axioms are usually written with no bar, since there is nothing to go above it. Second, to be completely pedantic, what we are calling "inference rules" are actually rule schemas , since their premises and conclusions may include metavariables. Formally, each schema represents the infinite set of concete rules that can be obtained by replacing each metavariable consistently by all phrases from the appropriate syntactic category i.e., in the rules above, replacing each t by every possible term.

Finally, here is yet another definition of the same set of terms in a slightly different, more "concrete" style that gives an explicit procedure for generating the elements of T .

### 3.2.3 Definition [Terms, Concretely]

For each natural number i , define a set S i as follows :

 S = S i +1 = { true, false, 0 } { succ t 1 , pred t 1 , iszero t 1 t 1 S i } { if t 1 then t 2 else t 3 t 1 , t 2 , t 3 S i }.

Finally, let

S is empty; S 1 contains just the constants; S 2 contains the constants plus the phrases that can be built with constants and just one succ, pred, iszero , or if ; S 3 contains these and all phrases that can be built using succ, pred, iszero , and if on phrases in S 2 ; and so on. S collects together all the phrases that can be built in this way i.e., all phrases built by some finite number of arithmetic and conditional operators, beginning with just constants.

### 3.2.4 Exercise [ ⋆⋆ ]

How many elements does S 3 have?

### 3.2.5 Exercise [ ⋆⋆ ]

Show that the sets S i are cumulative that is, that for each i we have S i S i +1 .

The definitions we have seen characterize the same set of terms from different directions: Definitions 3.2.1 and 3.2.2 simply characterize the set as the smallest set satisfying certain "closure properties"; Definition 3.2.3 shows how to actually construct the set as the limit of a sequence.

To finish off the discussion, let us verify that these two views actually define the same set. We'll do the proof in quite a bit of detail, to show how all the pieces fit together.

### 3.2.6 Proposition

T = S .

Proof: T was defined as the smallest set satisfying certain conditions. So it suffices to show (a) that S satisfies these conditions, and (b) that any set satisfying the conditions has S as a subset (i.e., that S is the smallest set satisfying the conditions).

For part (a), we must check that each of the three conditions in Definition 3.2.1 holds of S . First, since S 1 = { true, false, 0 }, it is clear that the constants are in S . Second, if t 1 S , then (since S = i S i ) there must be some i such that t 1 S i . But then, by the definition of S i +1 , we must have succ t 1 S i +1 , hence succ t 1 S ; similarly, we see that pred t 1 S and iszero t 1 S . Third, if t 1 S , t 2 S , and t 3 S , then if t 1 then t 2 else t 3 S , by a similar argument.

For part (b), suppose that some set S satisfies the three conditions in Definition 3.2.1. We will argue, by complete induction on i , that every S i S , from which it clearly follows that S S .

Suppose that S j S for all j < i ; we must show that S i S . Since the definition of S i has two clauses (for i = 0 and i > 0), there are two cases to consider. If i = 0, then S i = ; but S trivially. Otherwise, i = j + 1 for some j . Let t be some element of S j +1 . Since S j +1 is defined as the union of three smaller sets, t must come from one of these sets; there are three possibilities to consider. (1) If t is a constant, then t S by condition 1. (2) If t has the form succ t 1 , pred t 1 , or iszero t 1 , for some t 1 S j then, by the induction hypothesis, t 1 S , and so, by condition (2), t S . (3) If t has the form if t 1 then t 2 , else t 3 , for some t 1 , t 2 , t 3 S , then again, by the induction hypothesis, t 1 , t 2 , and t 3 are all in S , and, by condition 3, so is t .

Thus, we have shown that each S i S . By the definition of S as the union of all the S i , this gives S S , completing the argument.

It is worth noting that this proof goes by complete induction on the natural numbers , not the more familiar "base case / induction case" form. For each i , we suppose that the desired predicate holds for all numbers strictly less than i and prove that it then holds for i as well. In essence, every step here is an induction step; the only thing that is special about the case where i = 0 is that the set of smaller values of i , for which we can invoke the induction hypothesis, happens to be empty. The same remark will apply to most induction proofs we will see throughout the book particularly proofs by "structural induction."

 < Free Open Study >
 Types and Programming Languages Authors: Pierce B.C. Published year: 2002 Pages: 26/262