TaPL Summary Part 2: Adding Operations on Natural Numbers
This is part 2 of a series summarizing Types and Programming Languages (TaPL). In the previous post we looked at a simple language which described basic boolean operations. We will now examine what happens to the language when we add natural numbers into our language.
Review of the Expanded Syntax
Let us recall our limited boolean arithmetic's syntax:
t ::= true false if t then t else t
The expanded syntax now looks like this:
t ::= true false if t then t else t 0 succ t pred t iszero t
Expanding the Semantics
Shown below is a continuation of the semantics table from Part 1. The parts mentioned in the previous table have been omitted for conciseness, and an ellipsis has been included where omissions have taken place to indicate that the new definitions are continuations of the previous tabe.
Of particular note is the addition of a new set, , which describes values that are numbers.
Since there is no rule to transition from
0, as well as
succ 0, we can use these to construct any arbitrary natural number.
Another thing to note is that in , we use instead of . This means that, for example, cannot transition
pred (succ (pred 0)) to
pred 0, we first need to convert
pred 0 to
0 using and then apply to
0, which then applies to
succ 0 to get
pred (succ 0) which can finally be evaluated as
0 using . This explanation can be quite lengthly and difficult to follow, so we introduce a new notation using a derivation tree to show how terms are evaluated:
You proceed along the left side of the tree, reducing each term until it can be evaluated to a value, which then gets passed along back down the tree where the reduced term is shown on the right hand side. The transition rule which was applied to perform the reduction is shown next to the line above the particular state change.
Now there is a problem in this language that we haven't seen before. For example, terms such as
if 0 then true else false or
iszero true are syntactically valid statements to make, but there is no transition function to evaluate the terms to a value. These "dead end" states in our semantics are called deadlock states. These are analogous to runtime errors like segmentation faults, illegal operations, or exceptions in real world programming languages.
Being unable to express and reason about these states is troublesome if we want to form a solid foundation for a theoretical understanding of programming languages. Therefore, we will expand our existing language for untyped arithmetic.
We can see that both
wrong. Thus, any
wrongs in the evaluation will propagate to the final result, indicating that there was some invalid term. This is similar to how exceptions bubble upwards in most programming languages. Thus, we are now able to evaluate all clauses to a value once again. Although this is not the most elegant way of dealing with error cases as the errors will still be detected at runtime, we have at least subverted the problem of being unable to express there being cases where we have irreducible terms.
To be continued...
I assume that the rest of TaPL will work towards introducing various type systems to detect these
wrongs at compile time, instead of bubbling them up as exceptions at run time. I will hopefully be able to continue with this series given I have enough time..