Untyped arithmetic expressions

The book uses a very simple programming language, NB, to introduce some key concepts we will use again and again.

This language just has natural numbers and Booleans and doesn’t let you do all that much with them. One thing that may be unfamiliar in this language is the way it represents natural numbers: zero is 0, one is succ 0, two is succ (succ 0), and so on.

Syntax

Reading: TAPL 3.1-3

The language used in TAPL, and in many programming language research papers, is (I believe) based on ISWIM, an imaginary programming language presented in a classic paper called “The Next 700 Programming Languages.”

TAPL’s notation for context-free grammars is a little different from what you may be used to.

If the syntax of NB were written in typical CFG notation, it would look like this:

Term → true
      | false
      | if Term then Term else Term
      | 0
      | succ Term
      | pred Term
      | iszero Term

TAPL writes it like this:

t ::= true
      false
      if t then t else t
      0
      succ t
      pred t
      iszero t

The use of ::= instead of → is standard. Some authors use | but TAPL omits it to reduce clutter.

Although some authors do, TAPL doesn’t typographically distinguish nonterminals (metavariables) from terminals; generally, single letters are nonterminal symbols and everything else is a terminal symbol.

In a syntax rule, like if t then t else t, there’s no need to distinguish between the three terms t. But these are, in general, three different terms, so pretty much everywhere outside of syntax rules, we distinguish them by writing t1, t2, t', etc.

We distinguish between concrete syntax (which defines the strings that you actually type into your editor) and abstract syntax (which defines the trees on which, in turn, are defined the semantics). In this course, we’re only concerned with abstract syntax; nevertheless, because we have to write down terms somehow (and it would be too cumbersome to draw trees), we do make use of concrete syntax constantly. So, you do need to know:

• succ, pred, and iszero have higher precedence and are right-associative
• if...then...else has lower precedence

But we make no attempt to formalize these conventions.

Semantics

Reading: TAPL 3.4-5

TAPL describes three main approaches to semantics: operational, denotational, and axiomatic.

The book focuses almost exclusively on operational semantics and so do we. One possible point of confusion is that operational semantics is said to define the meanings of programs in terms of the moves of of an abstract machine. Finite automata, pushdown automata, and Turing machines are examples of abstract machines that you encountered in Theory of Computing, and more specialized machines like the SECD machine exist for defining programming languages. But the “machines” we use in this class don’t have stacks or tapes; they just operate directly on programs, rewriting them until they become answers.

Evaluation contexts

In small-step operational semantics, there are two kinds of inference rules: congruence rules and computation rules. The congruence rules find the place in the program where a reduction happens, and the computation rules do the reduction itself.

Another way to write small-step operational semantics that is much more compact is to use evaluation contexts [1], which are terms with a single “hole” [·] that indicates where a reduction can happen. For NB, evaluation contexts are defined using BNF, as follows:

E ::= [⋅]
      succ E
      pred E
      if E then t else t
      iszero E

The first production generates the hole [·], and the remaining productions each correspond to one of the congruence rules. Intuitively, this means that you can reduce inside a succ, pred, or iszero, but inside a conditional, you can only reduce inside the condition.

If E is an evaluation context, then E[t] is the term that results from substituting t for the hole [⋅]. Then the congruence rules (E-Succ, E-Pred, E-IsZero) can all be replaced by a single congruence rule,

   t ⟶ t'
――――――――――――――  (E-Context)
E[t] ⟶ E[t']

For example, the term

if iszero 0 then false else true

is equal to E[t] where

E = if [⋅] then false else true
t = iszero 0

So there’s only one way to reduce this term, which is

                        iszero 0 ⟶ true
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
if iszero 0 then false else true ⟶ if true then false else true

Although TAPL doesn’t use evaluation contexts, they are convenient and very commonly used in research papers, so it’s good to be familiar with this notation. Evaluation contexts will become especially useful in the last unit of the course, when we study effects.

Big-step semantics

You might feel that congruence rules and/or evaluation contexts are more complex than necessary. At every single step, we have to find the place to perform a reduction, which involves a lot of repeated work. If you were to implement an interpreter for NB, you could write it this way, but there’s a simpler way, based on big-step operational semantics, introduced in Exercise 3.5.17. Whereas small-step operation semantics defines ⟶ for a single step of evaluation, big-step operational semantics defines a relation ⇓ that evaluates a term all the way to its final value.

          —————              (B-Value)
          v ⇓ v

    t1 ⇓ true   t2 ⇓ v2
——————————————————————————   (B-IfTrue)
if t1 then t2 else t3 ⇓ v2

   t1 ⇓ false   t3 ⇓ v3
——————————————————————————   (B-IfFalse)
if t1 then t2 else t3 ⇓ v3

          t ⇓ nv
     ————————————————        (B-Succ)
     succ t ⇓ succ nv

          t ⇓ 0
       ——————————            (B-PredZero)
       pred t ⇓ 0

       t ⇓ succ nv
       ———————————           (B-PredSucc)
       pred t ⇓ nv

          t ⇓ 0
     ———————————————         (B-IsZeroZero)
     iszero t ⇓ true

        t ⇓ succ nv
     ————————————————        (B-IsZeroSucc)
     iszero t ⇓ false

Exercise. Do the “only if” direction of Exercise 3.5.17: show that if t ⟶* v and v is a value, then t ⇓ v.

Big-step semantics translates into a simpler interpreter than small-step semantics does. The interpreter is a recursive function of one argument t. If t ⇓ v, it returns v; otherwise it raises an error. The function has one case for each evaluation rule, which makes one recursive call to evaluate for each premise. For example, the case for B-IfTrue is:

function evaluate(t)
    ⋮
    if t is of the form (if t1 then t2 else t3)
        if evaluate(t1) = true
            return evaluate(t2)
    ⋮

References