2
$\begingroup$

I'm autodidacting Pierce's Types and Programming Languages. On page 27 he states a definition for "terms, concretely" in constructing a language of terms, thus:

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

\begin{align} S_0 & = \emptyset \\ S_{i+1} & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \{succ \: t_1, pred \: t_1, iszero \: t_1\ |\: t_1 \in S_i\} \\ & \;\;\;\cup \; \{if\: t_1 \:then \: t_2 \:else \: t_3\: |\; t_1, t_2, t_3 \in S_i\} \\ \end{align}

where $succ\: t$ is the successor of $t$, $pred \:t$ is the predecessor of $t$ and $iszero \:t$ tests if $t = 0$. Finally, let

$$S = \bigcup_i{S_i}$$

where $S_0$ is empty; $S_1$ contains just the constants (I assume $true, false, 0$ is meant); $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$ in $S_2$; and so on. $S$ collects together all the phrases that can be built in this way, i.e., all the phrases built by some finite number of arithmetic and conditional operators, beginning with just constants.

Then as an exercise: How many elements does $S_3$ have? And the answer is (from back of book): $|S_{i+1}| = {|S_i|}^3 + |S_i| \,\times\,3+3$, and $|S_0| = 0$. So $|S_3| = 59439.$

I really get lost when he says what $S_1$ and $S_2$ are. Anyone who could get me started on what is going on here, or could point me to another treatment of these ideas would be appreciated.

$\endgroup$
1
  • $\begingroup$ The way to understand here is to try to understand as little as needed (which might be very difficult sometimes). $\endgroup$
    – John L.
    Jan 19 '19 at 4:00
4
$\begingroup$

$S_0$ is the empty set.

Let $i=0$. $$\begin{align} S_1= S_{0+1} & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \{succ \: t_1, pred \: t_1, iszero \: t_1\ |\: t_1 \in S_0\} \\ & \;\;\;\cup \; \{if\: t_1 \:then \: t_2 \:else \: t_3\: |\; t_1, t_2, t_3 \in S_0\} \\ & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \emptyset \\ & \;\;\;\cup \; \emptyset \\ & = \;\;\;\{true, false, 0\} \\ \end{align}$$

So $S_1$ contains 3 elements.

Let $i=1$. $$\begin{align} S_2= S_{1+1} & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \{succ \: t_1, pred \: t_1, iszero \: t_1\ |\: t_1 \in S_1\} \\ & \;\;\;\cup \; \{if\: t_1 \:then \: t_2 \:else \: t_3\: |\; t_1, t_2, t_3 \in S_1\} \\ & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \{succ \: true, pred \: true, iszero \: true, \\ &\quad\quad\;\;succ \: false, pred \: false, iszero \: false, \\ &\quad\quad\;\;succ \: 0, pred \: 0, iszero \: 0\} \\ & \;\;\;\cup \; \{if\: true \:then \: true \:else \: true,\\ &\quad\quad\;\;if\: true \:then \: true \:else \: false,\\ &\quad\quad\;\;if\: true \:then \: true \:else \: 0,\\ &\quad\quad\;\;if\: true \:then \: false \:else \: true,\\ &\quad\quad\;\;if\: true \:then \: false \:else \: false,\\ &\quad\quad\;\;if\: true \:then \: false \:else \: 0,\\ &\quad\quad\;\;if\: true \:then \: 0 \:else \: true,\\ &\quad\quad\;\;if\: true \:then \: 0 \:else \: false,\\ &\quad\quad\;\;if\: true \:then \: 0 \:else \: 0,\\ &\quad\quad\;\;if\: false \:then \: true \:else \: true,\\ &\quad\quad\;\;if\: false \:then \: true \:else \: false,\\ &\quad\quad\;\;if\: false \:then \: true \:else \: 0,\\ &\quad\quad\;\;if\: false \:then \: false \:else \: true,\\ &\quad\quad\;\;if\: false \:then \: false \:else \: false,\\ &\quad\quad\;\;if\: false \:then \: false \:else \: 0,\\ &\quad\quad\;\;if\: false \:then \: 0 \:else \: true,\\ &\quad\quad\;\;if\: false \:then \: 0 \:else \: false,\\ &\quad\quad\;\;if\: false \:then \: 0 \:else \: 0,\\ &\quad\quad\;\;if\: 0 \:then \: true \:else \: true,\\ &\quad\quad\;\;if\: 0 \:then \: true \:else \: false,\\ &\quad\quad\;\;if\: 0 \:then \: true \:else \: 0,\\ &\quad\quad\;\;if\: 0 \:then \: false \:else \: true,\\ &\quad\quad\;\;if\: 0 \:then \: false \:else \: false,\\ &\quad\quad\;\;if\: 0 \:then \: false \:else \: 0,\\ &\quad\quad\;\;if\: 0 \:then \: 0 \:else \: true,\\ &\quad\quad\;\;if\: 0 \:then \: 0 \:else \: false,\\ &\quad\quad\;\;if\: 0 \:then \: 0 \:else \: 0\} \end{align}$$

So $S_2$ contains 3+9+27= 39 elements.

Let $i= 2$, we will get $S_3=S_{2+1}=\cdots$, which contains 3+39*3+39^3=59439 elements.


You are supposed to get lost in case you want to find the meaning or the semantics of the elements in $S_1$ and $S_2$, because there is no meaning attached to those elements yet at this stage of the book. In other words, although you, I suspect, have understood all that are supposed to be understood, you do not feel or know that you have. Be relaxed, this introductory book is not supposed to be difficult here.

At this stage of the book, $S_0, S_1, S_2, \cdots$ are just sets of words over the alphabet $\Sigma=\{ true, false, 0, succ, pred, iszero, if, then, else \}$. In fact, 3.2.1 Definition [Terms, inductively] defines the language $\mathcal T$ by the following context-free grammar.

$S\to true \mid false \mid 0$
$S\to succ\ S \mid pred\ S \mid iszero\ S$
$S\to if\ S\ then\ S\ else\ S $

Once again, let me emphasize that there is no meaning to each symbol in the alphabet $\Sigma$. For example, $true$ is just one symbol, which happens to look like "true". It should have worked equally well had we used $asdf$ or $easypeasy$ or $humptydumpty$ instead. It is expected that we will assign meaning or semantics to all symbols in $\Sigma$ and many words in $\mathcal T$; however, that has not been done yet at this stage of the book.


To compute $|S_3|$, we need to prove the formula, $|S_{i+1}| = {|S_i|}^3 + |S_i| \times3+3$, which comes from the following equality, where $\sqcup$ means disjoint union.

\begin{align} S_{i+1} & = \;\;\;\{true,\, false,\, 0\} \\ & \;\;\; \sqcup \, \{succ \: t_1\mid t_1 \in S_i\} \,\sqcup\, \{pred \: t_1\mid t_1 \in S_i\} \; \sqcup \; \{iszero \: t_1\mid t_1 \in S_i\} \\ & \;\;\;\sqcup \, \{if\: t_1 \:then \: t_2 \:else \: t_3\: |\; t_1, t_2, t_3 \in S_i\} \\ \end{align}

Note that it might not be trivial to show the cardinality of the last set $\{if\: t_1 \:then \: t_2 \:else \: t_3\: |\; t_1, t_2, t_3 \in S_i\}$ is $|S_i|^3$ for $i\ge2$ in general since we need to show more or less that the grammar above is deterministic. However, the cases of $i=0,1,2$ that are needed for the moment can be easily enumerated.

$\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.