1
$\begingroup$

In Pierce's book, on page 26-27 it is given a definition of terms for a simple language using inference rules.

In the picture below it is marked by red highlighting the problematic part.

What is Pierce referring to exactly by the red-highlighted word term in this context?

Is he referring to the terms given by the grammar on page 24 ?

In that case I see no point in defining the terms using the inference rules given in the Definition 3.2.2 because he is using the definition of terms already defined by the grammar on page 24, so there is no point in defining it again.

How should one really understand what the red-highlighted word term refers to on page 27, so that the definition 3.2.2 makes sense ?

The only way the last sentence would make sense to me if it would be changed to something like this: ... replacing each t by every possible term that has been generated inductively so far., meaning that the highlighted word term does not refer to the terms defined on page 24 but to the terms which already have been generated inductively by the inference rules given in Def 3.2.2.

What do you think ?

The grammar from page 24:

t ::=                                   terms:
      true                       constant true
      false                     constant false
      if t then t else t           conditional
      0                          constant zero
      succ t                         successor
      pred t                       predecessor
      iszero t                       zero test

From page 26:

3.2.2. DEFINITION [TERMS, BY INFERENCE RULES]: The set of terms is defined by the following rules

$$\begin{gather} \texttt{true}\in\mathcal{T} \qquad\qquad \texttt{false}\in\mathcal{T} \qquad\qquad 0\in\mathcal{T}\\\\ \frac{\texttt{t}_1\in\mathcal{T}}{\texttt{succ t}_1\in\mathcal{T}} \qquad \frac{\texttt{t}_1\in\mathcal{T}}{\texttt{pred t}_1\in\mathcal{T}} \qquad \frac{\texttt{t}_1\in\mathcal{T}}{\texttt{iszero t}_1\in\mathcal{T}}\\\\ \frac{\texttt{t}_1\in\mathcal{T} \qquad \texttt{t}_2\in\mathcal{T} \qquad \texttt{t}_3\in\mathcal{T}}{\texttt{if t}_1\texttt{ then t}_2\texttt{ else t}_3\in\mathcal{T}} \end{gather}$$

From page 27:

enter image description here

$\endgroup$
4
$\begingroup$

Part of your intuition is correct: "terms" really means "the collection of terms generated thus far". I think you will also find in Pierce a definition that makes this explicit on the next page (Definition 3.2.3).

What Pierce is actually doing is giving three equivalent and common ways of presenting syntax. In fact, the first one (page 24) is what you often see in papers and programming language specifications. Definition 3.2.2 is a way of understanding this as an inductive set of rules. And Definition 3.2.3 is a way of understanding the inductive set of rules by explicitly building larger terms from smaller terms.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.