Arithmetic expressions: terms, derivations and a first interpreter

This is the first exercise sheet of Foundations of Programming Languages, written by Prof. Vasco T. Vasconcelos, on the arithmetic expressions of chapter 3 of Benjamin C. Pierce’s Types and Programming Languages (TAPL). These are my answers, including the places where my first attempt got something wrong, because that’s usually where the learning is.

The notation (grammars, metavariables, inference rules, axioms, derivations, evaluation) is explained in part 1 of this series. This post puts it to work.

The language#

The language has booleans, natural numbers built from zero and successor, a test for zero, and a conditional.

$t$::=terms|$\mathsf{true}$constant true|$\mathsf{false}$constant false|$\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t$conditional|$0$constant zero|$\mathsf{succ}\ t$successor|$\mathsf{pred}\ t$predecessor|$\mathsf{iszero}\ t$zero test

As part 1 explains, the grammar is shorthand for the smallest set of terms $\T$ closed under these inference rules (TAPL, Definition 3.2.2). T-True, T-False and T-Zero are the axioms.

(T-True)

axiom, by T-True:$\ttrue \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-Zero)

axiom, by T-Zero:$0 \in \T$

$t_1 \in \T$

(T-Succ)

therefore, by T-Succ:$\tsucc\ t_1 \in \T$

$t_1 \in \T$

(T-Pred)

therefore, by T-Pred:$\tpred\ t_1 \in \T$

$t_1 \in \T$

(T-IsZero)

therefore, by T-IsZero:$\tiszero\ t_1 \in \T$

$t_1 \in \T$

$t_2 \in \T$

$t_3 \in \T$

(T-If)

therefore, by T-If:$\ite{t_1}{t_2}{t_3} \in \T$

The same set, built in layers (TAPL, Definition 3.2.3), which exercise 3 will use:

$$\begin{aligned} S_0 &= \emptyset \\ S_{i+1} &= \{\ttrue, \tfalse, 0\} \\ &\quad \cup \{\tsucc\ t_1,\ \tpred\ t_1,\ \tiszero\ t_1 \mid t_1 \in S_i\} \\ &\quad \cup \{\ite{t_1}{t_2}{t_3} \mid t_1, t_2, t_3 \in S_i\} \\ S &= \textstyle\bigcup_i S_i \qquad \text{and } \T = S \text{ (Proposition 3.2.6)} \end{aligned}$$

Exercise 1: writing terms#

Natural numbers. There are no digits beyond $0$, so numbers are built by applying $\tsucc$:

$$1 = \tsucc\ 0 \qquad 2 = \tsucc\ (\tsucc\ 0) \qquad 3 = \tsucc\ (\tsucc\ (\tsucc\ 0))$$

Two or more conditionals, nested in the branches or in the condition:

$$\ite{\ttrue}{(\ite{\ttrue}{\ttrue}{\tfalse})}{\tfalse}$$ $$\ite{(\ite{\ttrue}{\ttrue}{\tfalse})}{\ttrue}{\tfalse}$$

Arithmetic mixed with booleans:

$$\ite{(\tiszero\ 0)}{(\tsucc\ 0)}{(\tsucc\ (\tsucc\ 0))} \qquad \tiszero\ (\tsucc\ 0)$$

not, or, and, isone, gz#

My first answer treated these as new syntax: add $\kw{not}\ t$ to the grammar, then a rule so that $\kw{not}\ t_1 \in \T$ whenever $t_1 \in \T$, and the same for the others.

$t_1 \in \T$

(T-Not)

therefore, by T-Not:$\kw{not}\ t_1 \in \T$

$t_1 \in \T$

$t_2 \in \T$

(T-Or)

therefore, by T-Or:$t_1\ \kw{or}\ t_2 \in \T$

$t_1 \in \T$

$t_2 \in \T$

(T-And)

therefore, by T-And:$t_1\ \kw{and}\ t_2 \in \T$

$t_1 \in \T$

(T-IsOne)

therefore, by T-IsOne:$\kw{isone}\ t_1 \in \T$

$t_1 \in \T$

(T-Gz)

therefore, by T-Gz:$\kw{gz}\ t_1 \in \T$

Those rules are correct, but they answer a different question. The exercise asks for these operators to be encoded in the existing language, without touching the grammar. Extending the language means a bigger set $\T$, and every later proof and every evaluation rule has to cover the new cases. An encoding is a derived form: a shorthand that stands for a term we already have, so nothing else changes.

Each one falls out of $\kw{if}$:

So my examples become terms of the original language. $\kw{not}\ (\tiszero\ (\tsucc\ 0))$, for instance, is

$$\ite{(\tiszero\ (\tsucc\ 0))}{\tfalse}{\ttrue}$$

Exercise 2: proving a term is a term#

Show that $\ite{(\tiszero\ (\tsucc\ 0))}{\tfalse}{(\tsucc\ \tfalse)} \in \T$.

Membership is proved with a derivation tree: stack the rules until every branch ends in an axiom.

(T-Zero)

axiom, by T-Zero:$0 \in \T$

(T-Succ)

therefore, by T-Succ:$\tsucc\ 0 \in \T$

(T-IsZero)

therefore, by T-IsZero:$\tiszero\ (\tsucc\ 0) \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-Succ)

therefore, by T-Succ:$\tsucc\ \tfalse \in \T$

(T-If)

therefore, by T-If:$\ite{(\tiszero\ (\tsucc\ 0))}{\tfalse}{(\tsucc\ \tfalse)} \in \T$

Notice what the tree does not care about: $\tsucc\ \tfalse$ is a perfectly good term even though it means nothing. Being a term is about shape, not sense. Sense comes later, with evaluation, and much later with types.

Exercise 3: proving a term is not a term#

Show that $\tsucc\ (\ite{(\tiszero\ \tsucc)}{\tfalse}{(\tiszero\ \tfalse)}) \notin \T$.

A tree can’t prove non-membership, because a derivation only ever builds terms up. But it’s the best way to see why no derivation exists: try to build one, bottom up, and watch where it breaks. That’s what my notes drew.

$\tsucc \in \T\ \ \text{✗ no rule applies}$

(T-IsZero)

therefore, by T-IsZero:$\tiszero\ \tsucc \in \T\ \ ?$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-False)

axiom, by T-False:$\tfalse \in \T$

(T-IsZero)

therefore, by T-IsZero:$\tiszero\ \tfalse \in \T$

(T-If)

therefore, by T-If:$\ite{(\tiszero\ \tsucc)}{\tfalse}{(\tiszero\ \tfalse)} \in \T\ \ ?$

(T-Succ)

therefore, by T-Succ:$\tsucc\ (\ite{(\tiszero\ \tsucc)}{\tfalse}{(\tiszero\ \tfalse)}) \in \T\ \ ?$

Each step up is forced: a term of the form $\tsucc\ t_1$ can only be concluded by T-Succ, an $\kw{if}$ only by T-If, an $\tiszero$ only by T-IsZero. So there’s no other tree to try. The two right branches close fine, ending in the axiom T-False. The left branch reaches the bare keyword $\tsucc$, which is not an axiom’s conclusion ($\ttrue$, $\tfalse$ or $0$) and has no argument to match T-Succ. That leaf can never be closed, so no derivation of the whole term exists.

The same argument, written as a proof:

The concrete definition gives the same result from a different angle, with no contradiction needed. Look at how stages are built: every element of every $S_{i+1}$ is a constant, or a keyword applied to terms from $S_i$. The bare keyword $\tsucc$ is neither, so it’s in no $S_i$, and so not in $S = \T$. Then $\tiszero\ \tsucc$ is in no stage either, because it would need $\tsucc$ in the stage before; the same goes for the conditional around it, and for the $\tsucc$ around that.

Exercise 4: terms that evaluate, and terms that don’t#

Evaluation is another set of rules, this time for a relation $t \eval t'$: ”$t$ takes one step to $t'$”. For booleans (TAPL, Figure 3-1):

(E-IfTrue)

axiom, by E-IfTrue:$\ite{\ttrue}{t_2}{t_3} \eval t_2$

(E-IfFalse)

axiom, by E-IfFalse:$\ite{\tfalse}{t_2}{t_3} \eval t_3$

$t_1 \eval t_1'$

(E-If)

therefore, by E-If:$\ite{t_1}{t_2}{t_3} \eval \ite{t_1'}{t_2}{t_3}$

A term that evaluates takes a step. $\ite{(\ite{\ttrue}{\tfalse}{\ttrue})}{\ttrue}{\tfalse}$ does, with this derivation:

(E-IfTrue)

axiom, by E-IfTrue:$\ite{\ttrue}{\tfalse}{\ttrue} \eval \tfalse$

(E-If)

therefore, by E-If:$\ite{(\ite{\ttrue}{\tfalse}{\ttrue})}{\ttrue}{\tfalse} \eval \ite{\tfalse}{\ttrue}{\tfalse}$

and one more step, by E-IfFalse, gives $\tfalse$.

A term that doesn’t evaluate is one no rule matches, a normal form. There are two very different kinds:

• Values are finished: $\ttrue$ and $\tfalse$. For numbers (TAPL, Figure 3-2) the values are $0$ and $\tsucc$ applied to a value, so $\tsucc\ 0$ is not “stuck”, it is the number one. My notes wrote $\tsucc\ 0 \eval$ void; the better way to say it is that it’s already a value.
• Stuck terms are normal forms that aren’t values: $\ite{0}{\ttrue}{\tfalse}$, $\tsucc\ \tfalse$, $\tiszero\ \ttrue$. They’re the runtime errors of this tiny language, and ruling them out before running anything is what the type systems later in the course are for.

With the numeric rules added, arithmetic and conditions combine. E-IsZeroZero says $\tiszero\ 0 \eval \ttrue$, so:

(E-IsZeroZero)

axiom, by E-IsZeroZero:$\tiszero\ 0 \eval \ttrue$

(E-If)

therefore, by E-If:$\ite{(\tiszero\ 0)}{\ttrue}{\tfalse} \eval \ite{\ttrue}{\ttrue}{\tfalse}$

Exercise 5: the width of a term#

The width of a term is 1 for each constant, the width of $t_1$ for $\tsucc\ t_1$, $\tpred\ t_1$ and $\tiszero\ t_1$, and the sum of the three for a conditional. Written as an inductive definition in the style of TAPL’s $\mathit{Consts}$ and $\mathit{size}$:

$$\begin{aligned} \mathit{width}(\ttrue) &= 1 \\ \mathit{width}(\tfalse) &= 1 \\ \mathit{width}(0) &= 1 \\ \mathit{width}(\tsucc\ t_1) &= \mathit{width}(t_1) \\ \mathit{width}(\tpred\ t_1) &= \mathit{width}(t_1) \\ \mathit{width}(\tiszero\ t_1) &= \mathit{width}(t_1) \\ \mathit{width}(\ite{t_1}{t_2}{t_3}) &= \mathit{width}(t_1) + \mathit{width}(t_2) + \mathit{width}(t_3) \end{aligned}$$

In tree terms, the width is the number of leaves of the term’s syntax tree, where $\mathit{size}$ counts every node and $\mathit{depth}$ the longest path. For the term from exercise 2:

Width counts occurrences and $\mathit{Consts}$ counts distinct constants, so $\mathit{width}(t) \geq |\mathit{Consts}(t)|$ always: here $3 \geq 2$, because $\tfalse$ appears twice.

Exercises 6 to 10: the same, in Haskell#

The syntax becomes a data type, one constructor per production. My version also carries the extension from exercise 1, which is why it has Not, And and friends.

data Term
  = TTrue
  | FFalse
  | If Term Term Term
  | TZero
  | Succ Term
  | Pred Term
  | IsZero Term
  | IsOne Term
  | Not Term
  | GZ Term
  | And Term Term
  | Or Term Term
  deriving (Show, Eq, Ord)

-- exercise 6: the terms from exercise 1
num3 = Succ (Succ (Succ TZero))
mixed = If (IsZero TZero) (Succ TZero) (Pred TZero)
notEx = Not (IsZero (Succ TZero))

Every inductive definition turns into a recursive function with one equation per rule, so size, depth and width read almost exactly like the maths:

size :: Term -> Int                                   -- exercise 8
size TTrue         = 1
size FFalse        = 1
size TZero         = 1
size (Succ t1)     = size t1 + 1
size (Pred t1)     = size t1 + 1
size (IsZero t1)   = size t1 + 1
size (If t1 t2 t3) = size t1 + size t2 + size t3 + 1

depth :: Term -> Int                                  -- exercise 9
depth TTrue         = 1
depth FFalse        = 1
depth TZero         = 1
depth (Succ t1)     = depth t1 + 1
depth (Pred t1)     = depth t1 + 1
depth (IsZero t1)   = depth t1 + 1
depth (If t1 t2 t3) = maximum [depth t1, depth t2, depth t3] + 1

width :: Term -> Int                                  -- exercise 10
width TTrue         = 1
width FFalse        = 1
width TZero         = 1
width (Succ t1)     = width t1
width (Pred t1)     = width t1
width (IsZero t1)   = width t1
width (If t1 t2 t3) = width t1 + width t2 + width t3

(My file also has an equation for each extension constructor, following the same pattern: one argument like Succ, two like a smaller If.)

Exercise 7: what happens when there’s no rule#

My first step covered only a few rules:

step :: Term -> Term
step (If TTrue t2 _)     = t2
step (If FFalse _ t3)    = t3
step (If t1 t2 t3)       = If (step t1) t2 t3
step (IsZero TZero)      = TTrue
step (IsZero (Succ t1))  = FFalse

Calling it on a term with no matching equation, like step (Succ TZero), crashes:

*** Exception: Arithmetic.hs: Non-exhaustive patterns in function step

That is the answer to exercise 7, and it’s a good one to sit with. A term with no applicable rule is a normal form, and the Haskell function has nothing to return. Note that Succ TZero isn’t even stuck, it’s a value; the function just has no way to say “done”.

I also left myself a note next to this code: these steps still confuse me, it feels like there are so many possibilities. What helped was noticing that the rules come in only two kinds:

• Computation rules do the actual work, on a term whose parts are already values: E-IfTrue, E-IfFalse, E-IsZeroZero, E-IsZeroSucc, E-PredZero, E-PredSucc.
• Congruence rules say where to work next, by stepping inside a subterm: E-If, E-Succ, E-Pred, E-IsZero.

So step only ever asks: can I compute here? If not, which subterm must go first? And there’s never more than one answer. TAPL proves that evaluation is deterministic (Theorem 3.5.4, extended to numbers in exercise 3.5.14), so there are fewer possibilities than it feels like.

Two fixes turn the sketch into a real interpreter. Maybe makes “no rule applies” an ordinary result instead of a crash, and the numeric rules only fire on numeric values, which my version missed: it would happily evaluate IsZero (Succ FFalse) to FFalse, when that term should be stuck.

isNumericVal :: Term -> Bool
isNumericVal TZero    = True
isNumericVal (Succ t) = isNumericVal t
isNumericVal _        = False

step :: Term -> Maybe Term
step (If TTrue t2 _)   = Just t2                                  -- E-IfTrue
step (If FFalse _ t3)  = Just t3                                  -- E-IfFalse
step (If t1 t2 t3)     = (\t1' -> If t1' t2 t3) <$> step t1       -- E-If
step (Succ t1)         = Succ <$> step t1                         -- E-Succ
step (Pred TZero)      = Just TZero                               -- E-PredZero
step (Pred (Succ nv))
  | isNumericVal nv    = Just nv                                  -- E-PredSucc
step (Pred t1)         = Pred <$> step t1                         -- E-Pred
step (IsZero TZero)    = Just TTrue                               -- E-IsZeroZero
step (IsZero (Succ nv))
  | isNumericVal nv    = Just FFalse                              -- E-IsZeroSucc
step (IsZero t1)       = IsZero <$> step t1                       -- E-IsZero
step _                 = Nothing                                  -- a normal form

-- evaluate until no rule applies
eval :: Term -> Term
eval t = maybe t eval (step t)

Each equation is one rule, labelled with its name. When a guard fails, Haskell moves on to the next equation, which is exactly how the congruence rule takes over when a computation rule doesn’t apply. The extension constructors (Not, And…) fall through to Nothing: they’d need evaluation rules of their own, which is one more argument for encoding them as derived forms instead.

What I’m taking from this#

• A language is a set, and “smallest” matters. It’s what lets us prove a term isn’t in it.
• Extending a language and encoding in it are different moves. Extensions grow every definition and proof; derived forms are free.
• Normal forms split into values and stuck terms. Types, coming up in this series, exist largely to rule out the second kind.
• Rules are either computation or congruence. Seeing that made evaluation feel much less like a maze.