15 Control Formalism🔗

Once again we encounter formalism: translating intuitive ideas, or programs, into a precise mathematical description that is easier to parse, read, and extend. This time we will see it for control. First we will revisit our compiler from last lecture and give a formal description as inference rules. Then, we will describe how to give a small-step reduction semantics to programs with control-flow operators using evaluation contexts.

15.1 Evaluation Contexts🔗

So far in class we’ve studied language features by a progression: (1) we’ve introduced the feature in English, (2) designed definitional interpreters for it, and (3) then given a formal semantics for the feature that crisply captures what the feature is supposed to do. We’ve done steps 1 and 2; now, let’s do step 3 and study how to design a formal operational semantics for languages with control-flow constructs like return and exceptions.

Recall CalcRet, the simple calculator language with return:

> (define-type CalcRet     (numR [n : Number])     (addR [e1 : CalcRet] [e2 : CalcRet])     (returnR [n : Number]))

Here is a surface syntax grammar for CalcRet that we will use for our semantics:

	‹e›	::=	( + ‹e› ‹e› )
		|	‹num›
		|	( return ‹num› )

Figure 17: Surface syntax for CalcRet.

As we’ve seen in our definitional interpreter for CalcRet, in order to implement non-local control-flow like returnR, it’s very useful to have an explicit representation of the call-stack (i.e., a continuation). So, in order to write down a small-step style reduction semantics for languages with these features, it is useful to have this notion be explicit as well. This will be captured by an evaluation context E. We will see that the evaluation context will play the role of the continuation in our semantics.

	‹E›	::=	[.]
		|	( + ‹num› ‹E› )
		|	( + ‹E› ‹e› )

Figure 18: Evaluation context grammar for CalcRet.

The form [.] (sometimes also written [\cdot]) is called the hole. Note that there can only ever be at most a single hole in any context E due to the way we’ve set up the grammar: for instance, there is no valid parse tree for the surface syntax (+ [.] [.]).

We write E[e] to denote replacing the hole in E[\cdot] with the expression e. Here are some examples:

• If we let E1 = (+ 1 [.]), then E1[(+ 2 3)] is (+ 1 (+ 2 3))

• If we let E2 = (+ (+ 1 [.]) (+ 2 3)), then E2[3] is (+ (+ 1 3) (+ 2 3))

Now we can use these evaluation contexts to give a small-step style reduction semantics for CalcRet programs:

As usual, these rules contain a surprising amount of information, so we need to see some examples of applying them before they really make sense.

First, let’s evaluate the program (+ 2 3). This is an immediate application of the (E-Add) rule, as usual:

\dfrac{~} {\texttt{(+ 2 3)} \rightarrow 5}~\text{(E-Add)}

\dfrac{\dfrac{~}{\texttt{(+ 1 2)} \rightarrow 3}~\text{(E-Add)}} {\texttt{(+ [.] 3)[(+ 1 2)]} \rightarrow \texttt{(+ 3 3)}}~\text{(E-Ctx)}

As shorthand, we sometimes write the above derivation instead in this way, which clearly shows where the evaluation context is: \dfrac{\dfrac{~}{\texttt{(+ 1 2)} \rightarrow 3}~\text{(E-Add)}} {\texttt{(+ [(+ 1 2)] 3)} \rightarrow \texttt{(+ 3 3)}}~\text{(E-Ctx)}

Notice what happened here: we are evaluating the subexpression (+ 1 2) in the context of (+ [.] 3). For this reason, this style of semantics is sometimes referred to as evaluation in context.

Let’s see what happens in an even more interesting case: (+ (+ 1 2) (+ 3 4)). We apply the (E-Ctx) rule as follows: \dfrac{\dfrac{~}{\texttt{(+ 1 2)} \rightarrow 3}~\text{(E-Add)}} {\texttt{(+ [(+ 1 2)] (+ 2 3))} \rightarrow \texttt{(+ 3 (+ 2 3))}}~\text{(E-Ctx)}

Notice that, when parsing an expression (+ e1 e2) the grammar of ‹E› only permits us to place an evaluation context in place of e1. So, we are forced to find a reducible expression in e1, and must parse e2 as using the ‹e› production.

Now for the big payoff for all this work. Let’s see how to evaluate a statement with a return construct in it, like (+ 1 (return 1)):

\dfrac{~}{\texttt{(+ 1 [(return 1)])} \rightarrow 1}~\text{(E-Ret)}

\dfrac{~}{\texttt{(+ [(return 1)] (return 2))} \rightarrow 1}~\text{(E-Ret)}

15.2 Evaluation Contexts for the Lambda Calculus🔗

Let’s start by writing down a semantics for the call-by-value lambda calculus in this new style. Recall the grammar for untyped lambda calculus programs, where this time we’ve added a syntactic category for values v:

e ::= \lambda x . e \mid e~e \mid x

v ::= \lambda x . e

The evaluation context E is a syntactic form that can be thought of as "an expression with a hole in it". Here is its definition as a BNF grammar:

E ::= [\cdot] \mid E~e \mid v~E

Here are some examples of working with evaluation contexts for the lambda calculus:

• If we let E_1 = (\lambda x . x)~[\cdot], then E_1[\lambda y . y] is (\lambda x . x)~(\lambda y . y).

• If we let E_2 = [\cdot]~(\lambda y .y), then E_2[\lambda y . y] is (\lambda x . x)~(\lambda y . y).

Now, similar to what we did for CalcRet, we can give a small step evaluation semantics using evaluation contexts, now for the lambda calculus:

\dfrac{e \rightarrow e{}’}{E[e] \rightarrow E[e{}’]}~\text{(E-Ctx)}\dfrac{~}{(\lambda x . e)~v \rightarrow e[x \mapsto v]}~\text{(E-Beta)}

Figure 20: Call-by-value semantics for the untyped lambda calculus using evaluation contexts.

Let’s see some examples:

\dfrac{} {(\lambda x . x)~(\lambda y . y) \rightarrow \lambda y . y}~\text{(E-Beta)}

Here is another example:

\dfrac{\dfrac{~}{((\lambda x . x) ~ (\lambda y . y)) \rightarrow (\lambda y . y)}~\text{(E-Beta)}} {[((\lambda x . x) ~ (\lambda y . y))]~(\lambda z . z) \rightarrow (\lambda y . y)~(\lambda z . z)}~\text{(E-Ctx)}

Bibliography🔗