0
$\begingroup$

Pierce's Types and Programming Languages has the following definition of terms:

$$S_0=\emptyset$$ $$S_{i+1} = \{true,false,0\} \cup \{succ(t), pred(t),iszero(t)|t \in S_i\} \cup\{if(t_1)then (t_2)else(t_3) |t_1,t_2,t_3\in S_i\}$$

So then that means this language has terms like $succ(false)$ and $if(succ(0))then(true)else(false)$, am I interpreting that correctly?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
2
$\begingroup$

You're interpreting this correctly. $S_1$ contains the constants, $S_2$ contains the terms you can build using one application of if/else, the successor function, the predecessor function and the zero predicate with these constants. The language is the limit $S = \bigcup_i S_i$ which can be interpreted as allowing any number of applications of these constructions.

If you're confused about using $\mathtt{succ}\;0$ as the condition in an if-statement then notice that it is still a term in the language but one that is 'meaningless'. See section 3.5 Evaluation for more on this and see 3.5.15 specifically for more on these terms.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ As we don't have the specifications of $\text{succ}$, it could turn out that this function returns a boolean value, rescuing us. Likewise, $\text{if}$ could return one ot $t_2$ or $t_3$. $\endgroup$
    – user16034
    Commented Jan 12, 2023 at 10:33
  • $\begingroup$ @YvesDaoust Yes, many programming languages would do that, but I was wondering if Pierce was trying to make the point that defining terms is a purely syntactic affair. We can define a grammar for terms that have no inherent meaning. For example, if the identity matrices are added as constants, then there is no clear meaning to assign to the successor of the 2x2 identity matrix, $succ(I_2)$. Nevertheless, $succ(I_2)$ could be a term in this language even though it is meaningless. In other words, we haven't finished our language design yet. Is that correct? $\endgroup$
    – Hank Igoe
    Commented Jan 12, 2023 at 10:52
  • $\begingroup$ "was trying to make the point...": I don't see that. $\endgroup$
    – user16034
    Commented Jan 12, 2023 at 11:05
1
$\begingroup$

By applying the definition,

$$S_0=\emptyset\\ S_1=\{\text{true},\text{false},0\}\\ S_2=\{\text{true},\text{false},0,\\ \text{succ}(\text{true}) , \text{pred}(\text{true}) , \text{iszero}(\text{true}) ,\\ \text{succ}(\text{false}) , \text{pred}(\text{false}) , \text{iszero}(\text{false}) ,\\ \text{succ}(0) , \text{pred}(0) , \text{iszero}(0) ,\\ \text{if }(\text{true})\text{ then }(\text{true})\text{ else }(\text{true}) ,\\ \text{if }(\text{true})\text{ then }(\text{true})\text{ else }(\text{false}) ,\\ \text{if }(\text{true})\text{ then }(\text{true})\text{ else }(0) ,\\ \text{if }(\text{true})\text{ then }(\text{false})\text{ else }(\text{true}) ,\\ \text{if }(\text{true})\text{ then }(\text{false})\text{ else }(\text{false}) ,\\ \text{if }(\text{true})\text{ then }(\text{false})\text{ else }(0) ,\\ \text{if }(\text{true})\text{ then }(0)\text{ else }(\text{true}) ,\\ \text{if }(\text{true})\text{ then }(0)\text{ else }(\text{false}) ,\\ \text{if }(\text{true})\text{ then }(0)\text{ else }(0) ,\\ \text{if }(\text{false})\text{ then }(\text{true})\text{ else }(\text{true}) ,\\ \text{if }(\text{false})\text{ then }(\text{true})\text{ else }(\text{false}) ,\\ \text{if }(\text{false})\text{ then }(\text{true})\text{ else }(0) ,\\ \text{if }(\text{false})\text{ then }(\text{false})\text{ else }(\text{true}) ,\\ \text{if }(\text{false})\text{ then }(\text{false})\text{ else }(\text{false}) ,\\ \text{if }(\text{false})\text{ then }(\text{false})\text{ else }(0) ,\\ \text{if }(\text{false})\text{ then }(0)\text{ else }(\text{true}) ,\\ \text{if }(\text{false})\text{ then }(0)\text{ else }(\text{false}) ,\\ \text{if }(\text{false})\text{ then }(0)\text{ else }(0) ,\\ \text{if }(0)\text{ then }(\text{true})\text{ else }(\text{true}) ,\\ \text{if }(0)\text{ then }(\text{true})\text{ else }(\text{false}) ,\\ \text{if }(0)\text{ then }(\text{true})\text{ else }(0) ,\\ \text{if }(0)\text{ then }(\text{false})\text{ else }(\text{true}) ,\\ \text{if }(0)\text{ then }(\text{false})\text{ else }(\text{false}) ,\\ \text{if }(0)\text{ then }(\text{false})\text{ else }(0) ,\\ \text{if }(0)\text{ then }(0)\text{ else }(\text{true}) ,\\ \text{if }(0)\text{ then }(0)\text{ else }(\text{false}) ,\\ \text{if }(0)\text{ then }(0)\text{ else }(0)\} $$

The expansion of $S_3$ is huge ($59475$ terms). That of $S_4$ astronomical ($210379467994775$ terms).

Improve this answer
$\endgroup$
2
  • $\begingroup$ How did you get 59475 as the value for $S_3$? $\endgroup$
    – Hank Igoe
    Commented Jan 12, 2023 at 10:38
  • $\begingroup$ @HankIgoe: $39+3\cdot39+39^3$. $\endgroup$
    – user16034
    Commented Jan 12, 2023 at 10:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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