Question

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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top