3.2 Syntax

< Free Open Study >

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

{true, false, 0} ⊆ T;
if t₁ Î T, then {succ t₁, pred t₁, iszero t₁} ⊆ T;
if t₁ Î T, t₂ Î T, and t₃ Î T, then if t₁ then t₂ else t₃ Î 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₁, pred t₁, iszero t₁ \| t₁ Î S_i}
		È	{if t₁ then t₂ else t₃ \| t₁, t₂, t₃ Î S_i}.

Finally, let

S₀ is empty; S₁ contains just the constants; S₂ contains the constants plus the phrases that can be built with constants and just one succ, pred, iszero, or if; S₃ contains these and all phrases that can be built using succ, pred, iszero, and if on phrases in S₂; 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₃ 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₁ = {true, false, 0}, it is clear that the constants are in S. Second, if t₁ Î S, then (since S = È_i S_i) there must be some i such that t₁ Î S_i. But then, by the definition of S_i+1, we must have succ t₁ Î S_i+1, hence succ t₁ Î S; similarly, we see that pred t₁ Î S and iszero t₁ Î S. Third, if t₁ Î S, t₂ Î S, and t₃ Î S, then if t₁ then t₂ else t₃ Î 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₁, pred t₁, or iszero t₁, for some t₁ Î S_j then, by the induction hypothesis, t₁ Î S′, and so, by condition (2), t Î S′. (3) If t has the form if t₁ then t₂, else t₃, for some t₁, t₂, t₃ Î S′, then again, by the induction hypothesis, t₁, t₂, and t₃ 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 >