Pierce's Types and Programming Languages : circular definition of terms?
-
01-11-2019 - |
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:
No correct solution