6 Formalism🔗

We have reached a point now where we have quite a complicated little garden of languages, each with their own syntax and semantics. It is time to bring order to this situation by introducing a concise and powerful system of notation for describing program’s behavior. This new notation will empower us to quickly and precisely write down how a description of a program’s semantics. As we move through the course, you will see more of this notation as we use it to describe type systems and other facets of how programs operate.

This lecture is heavily based on Chapter 3 of  (Pierce 2002).

6.1 Inference Rules and Derivation Trees🔗

Let’s go back to our CalcLang example we’ve been studying since the first lecture:

> (define-type CalcLang     (numE [value : Number])     (addE [left : CalcLang] [right : CalcLang]))

We’ve seen two examples of how to give semantics to CalcLang: big-step and small-step. Let’s start with the small-step semantics. Recall the surface syntax for our calculator language:

	‹expr›	::=	( + ‹expr› ‹expr› )
		|	‹n›

Figure 4: Surface syntax for CalcLang.

This is quite a mouthful, and it is a bit awkward to describe these rules in English. So, we will introduce the following notation to summarize these rules:

\dfrac{~}{\texttt{n} \rightarrow \texttt{n}}~\text{(E-Num)}\dfrac{~}{\texttt{(+ n1 n2)} \rightarrow \texttt{n1 + n2}}~\text{(E-Add1)}\dfrac{\texttt{e1} \rightarrow \texttt{e1{}’} }{\texttt{(+ e1 e2)} \rightarrow \texttt{(+ e1{}’ e2)}}~\text{(E-Add2)}\dfrac{\texttt{e2} \rightarrow \texttt{e2{}’} }{\texttt{(+ n e2)} \rightarrow \texttt{(+ n e2{}’)}}~\text{(E-Add3)}

Figure 5: Small-step semantics for CalcLang.

Obviously this notation is unfamiliar, so we need to define what it means. An inference rule is a collection of premises followed by a conclusion and separated by a horizontal line. For example, the following is a simple inference rule that says that if it is raining and you have no umbrella, then you are wet:

\dfrac{\text{It is raining.} \quad \text{You have no umbrella.}}{\text{You are wet.}}

If an inference rule has no premises, then it is called an axiom. Axioms are always true. The following is an example of an axiom:

\dfrac{~}{\text{The sun is hot.}}

A question you may ask is: what is the meta-language for interpreting the symbols in these inference rules? This is a very good question! In general, we will assume that Plait is still how we interpret data manipulation (so, addition, branching, etc. are all Plait).

The figure above uses inference rules to describe a relation between abstract syntax of CalcLang: a syntactic term e1 is related to a syntactic term e2 if e1 steps to e2. The (E-Num) rule is an axiom: it says that numbers n step to themselves.

Next, the (E-Add) perform case analysis to describe how the term \texttt{(+ e1 e2)} steps. (E-Add1) handles the case when both arguments are numbers, (E-Add2) handles the case when e1 is not a number, and (E-Add3) handles the case when e1 is a number and e2 isn’t.

The above inference rules contain meta-variables in them like n and e1; these are symbols that can be replaced when an inference rule is applied. For instance, we can use the inference rule (E-Add1) to establish that the following step is valid, meaning it is permitted by our inference rules:

\dfrac{~}{\texttt{(+ 1 2)} \rightarrow \texttt{3}}~\text{(E-Add1)}

It is typical to write the name of the applied inference rule whenever it is used, but it may sometimes be elided for brevity, especially in the case of axioms.

6.1.1 Derivation Trees🔗

One of the key properties of inference rules is that they can be chained together, conclusions of one rule feeding into premises of the next rule. For instance, we can chain together the (E-Add1) and (E-Add2) rule to establish a more complicated fact:

\dfrac{\dfrac{~}{\texttt{(+ 1 2)} \rightarrow \texttt{3}}~\text{E-Add1}} {\texttt{(+ (+ 1 2) 2)} \rightarrow \texttt{(+ 3 3)}}~\text{(E-Add2)}

This structure is called a derivation tree. At the bottom of the tree is the final conclusion. A derivation tree is called a valid derivation tree if each the leaves of the tree are all axioms, i.e. statements that hold without premises.

6.1.2 Big-Step Semantics🔗

Recall our definitional interpreter for CalcLang:

> (interp : (CalcLang -> Number))

> (define (interp e)     (type-case CalcLang e                [(numE n) n]                [(addE e1 e2)                 (+ (interp e1) (interp e2))]))

A big-step semantics relates terms to the values that they run to. We can use our inference rule notation to describe this relation in a manner similar to the small-step semantics. We will use denote a program e running to value v as e \Downarrow v.

\dfrac{~}{\texttt{n} \Downarrow \texttt{n}}~\text{(B-Num)}\dfrac{\texttt{e1} \Downarrow v_1 \quad \texttt{e2} \Downarrow v_2 }{\texttt{(+ e1 e1)} \Downarrow v_1 + v_2}~\text{(B-Add)}

Figure 6: Big-step semantics for CalcLang.

Now we can use these inference rules to draw derivation trees that describe running CalcLang programs to values:

\dfrac{\dfrac{~}{1 \Downarrow 1}~\text{(B-Num)} \qquad \dfrac{~}{2 \Downarrow 2}~\text{(B-Num)}}{\texttt{(+ 1 2)} \Downarrow 3}~\text{(B-Add)}

Another example:

\dfrac{ \dfrac{ \dfrac{~}{1 \Downarrow 1} \quad \dfrac{~}{2 \Downarrow 2} } {\texttt{(+ 1 2)} \Downarrow 3}~\text{(B-Add)} \quad \dfrac{~}{3 \Downarrow 3}~\text{(B-Num)}} {\texttt{(+ (+ 1 2) 3)} \Downarrow 6}~\text{(B-Add)}

Observe: this derivation tree looks exactly like a trace of running your definition interpreter program interp. In this way, one can think of the big-step semantics as a concise shorthand for describing how definitional interpreters behave.

6.2 Structural Induction🔗

Inference rules give us the scaffolding to argue carefully about what programs do. Suppose I want to establish the following seeming obvious fact: all CalcLang programs terminate. This seems quite obviously true (as long as the abstract stynax trees of programs we consider are finite in size, which is an assumption we always make). How might we go about proving such a thing is true?

Let’s translate this statement into something about derivation trees. The depth of a derivation tree is length of the longest chain of inference rules in the tree. Concretely, an axiom has depth 0, and each time an inference rule is used it increases the depth by 1. We will argue that all CalcLang programs terminate by showing that all derivation trees have finite depth.

Theorem: All CalcLang programs e have finite-depth big-step derivation trees.

The base cases in CalcLang are the numbers. Our theorem clearly holds for these numbers, since they are axioms and by definition their derivation trees have depth 0 which is finite.

6.3 Small-step Semantics for the Lambda Calculus🔗

Now we can see the small-step semantics for the lambda calculus. For this, we need just a bit more notation. If e_1 is a lambda calculus program, then we denote substituting x for e_2 in e_1 as e_1[x \mapsto e_2]. We will use v as a shorthand for value; in the case of the lambda calculus, all values are lambda abstractions. Then, we can write the small-step semantics for the call-by-value lambda calculus:

\dfrac{e_1 \rightarrow e_1{}’}{(e_1 ~ e_2) \rightarrow (e_1{}’~e_2)}~\text{(E-App1)}\dfrac{e_2 \rightarrow e_2{}’}{(v_1 ~ e_2) \rightarrow (v_1~e_2{}’)}~\text{(E-App2)}\dfrac{~}{((\lambda x . e) ~ v_2) \rightarrow e[x \mapsto v_2]}~\text{(E-Beta)}

Figure 7: Small-step semantics for the call-by-value lambda calculus.

We can see some examples of stepping specific lambda terms:

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

Another one:

\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-App1)}

Another one:

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

6.4 Relating the Big and Small-Step Semantics🔗

So far, we’ve seen the big-step and the small-step semantics as two separate means of defining semantics for programs. But, intuitively, these two semantics ought to agree. The formal relationship we want is that if one repeatedly performs small steps until a term is fully-simplified, then this fully-simplified value is equal to value given by the big-step semantics.

Let’s make this relationship precise by defining an additional relation \rightarrow^* (called the transitive closure of the step relation, sometimes also called "star step" or "multi-step".) that repeatedly performs small steps. We can define this using the small-step semantics as:

\dfrac{e \rightarrow e{}’ \quad e{}’ \rightarrow^* e{}’{}’}{e \rightarrow^* e{}’{}’}~\text{(E-Trans)} \qquad \dfrac{e \rightarrow e}{e \rightarrow^* e}~\text{(E-Refl)}

The (E-Trans) rule, short for transitivity, says e multi-steps to e{}’{}’ if there is some intermediate e{}’ that e steps to that multi-steps to e{}’{}’. The (E-Refl) rule, short for reflexivity, says if a term steps to itself then it multisteps to itself. We implemented this relation in the step-interp function in a previous lecture: The Stepper: Simplifying Calculator Programs.

Let’s see an example:

\dfrac{ \dfrac{\dfrac{~}{\texttt{(+ 1 2)} \rightarrow 3}~\text{(E-Add1)}} {\texttt{(+ (+ 1 2) 3)} \rightarrow \texttt{(+ 3 3)}}~\text{(E-Add2)} \quad \dfrac{ \dfrac{~}{\texttt{(+ 3 3)} \rightarrow 6}~\text{(E-Add1)} \quad \dfrac{\dfrac{~}{6 \rightarrow 6}~\text{(E-Num)}}{6 \rightarrow^* 6}~\text{(E-Refl)} } {\texttt{(+ 3 3)} \rightarrow^* 6}~\text{(E-Trans)} } {\texttt{(+ (+ 1 2) 3)} \rightarrow^* 6}~\text{(E-Trans)}

Theorem: For any calculator program e, e \rightarrow^* n if and only if e \Downarrow n.

We won’t prove this theorem right now, but the proof is a structural inductive argument not unlike the one we did for showing that all CalcLang programs terminate. It’s not too difficult, but it is quite tedious, since it requires handling many cases.

6.5 Errors and Being Stuck🔗

Finally we will conclude this discussion by adding Booleans to our calculator language and see how these are handled:

	‹expr›	::=	( + ‹expr› ‹expr› )
		|	‹true›
		|	‹false›
		|	( if ‹expr› ‹expr› ‹expr› )
		|	‹n›

Figure 8: Surface syntax for IteLang.

Let’s define our semantics so that we have the usual IteLang semantics where the guards of if-expressions are expected to be Booleans. Here is what the rules look like for this:

\dfrac{e_1 \rightarrow e_1{}’}{(e_1 ~ e_2) \rightarrow (e_1{}’~e_2)}~\text{(E-App1)}\dfrac{~}{\texttt{n} \rightarrow \texttt{n}}~\text{(E-Num)}\dfrac{~}{\texttt{(+ n1 n2)} \rightarrow \texttt{(+ n1 n2)}}~\text{(E-Add1)}\dfrac{\texttt{e1} \rightarrow \texttt{e1{}’} }{\texttt{(+ e1 e2)} \rightarrow \texttt{(+ e1{}’ e2)}}~\text{(E-Add2)}\dfrac{\texttt{e2} \rightarrow \texttt{e2{}’} }{\texttt{(+ n e2)} \rightarrow \texttt{(+ n e2{}’)}}~\text{(E-Add3)}\dfrac{~}{\texttt{(if true e1 e2)} \rightarrow \texttt{e1}}~\text{(E-IteT)}\dfrac{~}{\texttt{(if false e1 e2)} \rightarrow \texttt{e2}}~\text{(E-IteF)}\dfrac{\texttt{e1} \rightarrow \texttt{e1{}’}} {\texttt{(if e1 e2 e3)} \rightarrow \texttt{(if e1{}’ e2 e3)}}~\text{(E-IteStep)}

Figure 9: Small-step semantics for IteLang.

Note what happens if we try to step the program (if 10 true false): there is no rule that applies to this program! So, we say this program is stuck. When giving semantics using small-step relations, if a term is stuck it is considered to not be a valid term. In our previous interpreters, we raised a runtime error when this happened.

Bibliography🔗