Semantics of NB

Reading: TAPL 3.4-5

TAPL describes three main approaches to semantics: operational, denotational, and axiomatic. We won’t talk about axiomatic semantics at all, but I’ll say a few words about denotational semantics.

Denotational semantics

Denotational semantics assigns to every expression in the language a meaning. For NB, that would look like this:

〚true〛                  = true
〚false〛                 = false
〚if t1 then t2 else t3〛 = 〚t2〛if 〚t1〛is true, 〚t3〛if 〚t1〛is false
〚0〛                     = 0
〚succ t〛                = 〚t〛 + 1
〚pred t〛                = max {0, 〚t〛 - 1}
〚iszero t〛              = true if 〚t〛 = 0, false if 〚t〛 ≠ 0

The double brackets 〚·〛 are read “denotation of”; everything inside the double brackets is a piece of syntax and everything outside them is a mathematical object. So true inside double brackets is a symbol, but true outside double brackets is The Platonic Ideal of Truth.

Denotational semantics, especially denotational semantics of the λ-calculus, is a very interesting subject, but unfortunately we don’t see much of it in this class. However, we do frequently make use of the above style of definition when translating a larger language to a smaller language. Then expressions inside double brackets are expressions of the source language, and expressions outside double brackets are expressions of the target language.

Operational semantics

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 the semantics of NB (called 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, 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