How does one deduce small step operational semantics?

Question

This question arises from my reading of "Types and Programming Languages" (WoldCat) by Benjamin C. Pierce.

For the small step operational semantic evaluation rules for the arithmetic expressions (NB) in Figure 3-2 on page 41, there is the rule

$pred\;(succ\;nv_1)\rightarrow\;nv_1$

My understanding is that it is to keep out invalid input like

$pred\;(false)$

but how did he come to that exact syntax for the rule? Is there some algorithm that is used to massage the rules into the necessary form? Is there some book or paper that explains how to formulate rules for small step operational semantics?

Note: I am aware that there is a forum dedicated to questions for the book here.

Answer 1

Devising an operational semantics of a programming language requires ingenuity, just like engineering a new car does. Nevertheless, there are some principle and correctness criteria by which we can judge whether a given semantics is "good".

For example, a good operational semantics should make sure that "valid programs do not do bad things". In practice this translates to "if a program succesfully compiled it is not going to dump core when we run it". Some languages are unsafe in this respect (C/C++), some are designed with safety in mind (Java, Python), and some are proved to be safe (Standard ML).

One way of translating "valid programs do not do bad things" is to interpret "valid program" as "well typed program" and "bad thing" as "getting stuck during evalution, even though we have not reached a final value". For this to make sense you have to define what "well typed" and "value" means. The central theorem then is

Safety: If a program $p$ has type $\tau$ then its evaluation diverges or terminates in a value of type $\tau$.

The theorem is typically proved by combining two lemmas:

Type preservation: If $p$ has type $\tau$ and $p \mapsto p'$ then $p'$ has type $\tau$. Remember this as "types do not change during evaluation".

Progress: If $p$ has type $\tau$ then it is either a value or there is a program $p'$ such that $p \mapsto p'$.

On the other hand, it does not matter what the operational semantics does with senseless programs, such as $\mathtt{pred}(\mathtt{false})$ because those do not have a type. It is the combination of typing and operational semantics that ensures safety. You cannot ensure safety just with the operational semantics, unless you are willing to make bizarre evaluation rules that will make your language awfully hard to debug.

Answer 2

The operational semantics is determined by what the language designer wants programs to do. If you define $\mathrm{pred}$ by $\mathrm{pred} \: \mathrm{false} \to \mathrm{true}$ and $\mathrm{pred}$ by $\mathrm{pred} \: \mathrm{true} \to \mathrm{false}$, that's perfectly fine mathematically speaking. On the other hand, humans are likely to puzzle as to why you called that operator $\mathrm{pred}$ instead of $\mathrm{not}$.

Informally, the predecessor of an integer $n$ is the integer $m$ such that $n$ is the successor of $m$: $\mathrm{pred}(m) = n$ when $n = \mathrm{succ}(n)$. The purpose of an operational semantics is generally to simplify expressions. Simplifying $\mathrm{pred} \: (\mathrm{succ} \: m)$ to $m$ is obvious.

You might wonder why not simplify $\mathrm{succ} \: (\mathrm{pred} \: n)$ to $n$. It's possible to prove that (for a reasonable calculus) this is unnecessary: with only the first rule, all normal forms contain only $\mathrm{succ}$ and no $\mathrm{pred}$ except inside functions that couldn't be evaluated for lack of an argument (this is covered a bit later in the book).

The asymmetry between $\mathrm{succ}$ and $\mathrm{pred}$ comes from $\mathrm{succ}$ being a constructor, and $\mathrm{pred}$ being the corresponding destructor. $\mathrm{succ}$ is a constructor because unary integers are defined as being either $0$ or $\mathrm{succ}(n)$ where $n$ is a unary integer. $\mathrm{succ}$ is a way to build an integer from something more primitive (a smaller integer). $\mathrm{pred}$ is a destructor: from what you feed it, it returns a more primitive integer. Rules of the form destructor(constructor(thing)) → thing are common.