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 a program’s behavior. This new notation will empower us to quickly and precisely write down 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›
Numbers are values and step to themselves.
To step (addE e1 e2), if e1 and e2 are both numbers then step to (numE (+ e1 e2)); if e1 is a number then step e2; if e1 isn’t a number then step e1.
Inference rules can be tricky the first time you see them! It’s good to get some practice using them.
\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)}
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 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. The meta-variable n stands for a number, and the meta-variables like e1 stand for expressions.
Going through each of these rules one at a time:
(E-Add1) handles the case when both arguments are numbers. It is an axiom: it says that if both arguments to addE are numbers, then (addE n1 n2) steps to (numE (+ n1 n2)), where the + is the meta-language addition.
(E-Add2) handles says that if e1 can take a step to some other expression e1’, then (+ e1 e2) steps to (+ e1’ e2).
(E-Add3) says that if e2 can take a step to e2’ then (+ n e2) steps to (+ n e2’). Note that the metavariable n is used as the first argument to +: this indicates that the first argument must be a number in order for this step to apply.
Note that these inference rules are deterministic: this means that at most 1 inference rule can apply to any given syntactic term.
6.2 Derivation Trees and Running Programs by Hand
The process of applying an inference rule typically involves substituting metavariables for bound variables: this process is called unification. For example, suppose we want to determine what the following CalcLang program steps to:
(+ 10 20)
The (E-Add1) rule does apply because the syntax (+ 10 20) matches the expression on the left-hand side of the \rightarrow symbol. Concretely, the syntax 10 unifies with metavariable n1 and the syntax 20 unifies with metavariable n2.
So, we can draw the following derivation that shows how to apply the (E-Add1) rule to take a step for the above term:
\dfrac{~}{\texttt{(+ 10 20)} \rightarrow \texttt{30}}~\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.
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 2)}}~\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. Notice how in the above derivation tree, the metavariable e1 for the (E-Add2) rule unifies with the syntax (+ 1 2), and the metavariable e2 unifies with the syntax 2.
6.3 From Inference Rules to Implementation
Inference rules are a specification language: they are an improvement over English for describing the semantics of programs. So, it is important to know how to translate inference rules into implementations.
The inference rules defining the small-step semantics for CalcLang specify a function from expressions to expressions. This exactly defines an interpreter as follows:
(step : (CalcLang -> CalcLang)) (define (step e) (type-case CalcLang e [(addE e1 e2) (cond [(and (numE? e1) (numE? e2)) ;------------------------- ; (+ n1 n2) -> n1 + n2 (numE (+ (numE-value e1) (numE-value e2)))] [(numE? e1) ; e2 -> e2' ; ----------------------- ; (+ n e2) -> (+ n e2') (addE e1 (step e2))] [else ; e1 -> e1' ; ------------------------ ; (+ e1' e2) (addE (step e1) e2)]) ]))
Notice how each arm of the type-case corresponds to a particular application of an inference rule.
6.4 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 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 e2)} \Downarrow v_1 + v_2}~\text{(B-Add)}
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.5 Structural Induction
Inference rules give us the scaffolding to argue carefully about what programs do. Suppose I want to establish the following seemingly 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.
A base case, which establishes the theorem holds for syntactic terms without sub-terms.
An inductive case, which proves that the theorem holds for syntactic terms with sub-terms, but can inductively assume that the theorem holds for those sub-terms.
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.
You may notice here a subtle difference between this notion of induction and the one you may have seen in your math class. In math class, you typically make inductive arguments using the natural numbers, like "first, show the theorem holds for objects of size 1. Then, assuming the theorem holds for objects of size n, show that the theorem holds for objects of size n+1. Then, we can conclude that the theorem holds for all objects of size greater than 1." Here, we are not inducting on the naturals; we instead inducting on our abstract syntax tree. This changes the shape of our inductive hypothesis.
6.6 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.7 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{~}{v \rightarrow^* v}~\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 value 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{~}{6 \rightarrow^* 6}~\text{(E-Refl)} } {\texttt{(+ 3 3)} \rightarrow^* 6}~\text{(E-Trans)} } {\texttt{(+ (+ 1 2) 3)} \rightarrow^* 6}~\text{(E-Trans)}
This theorem justifies our providing only small-step semantics for the lambda calculus above: we can define the big-step semantics using \rightarrow^*.
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.8 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›
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{~}{\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)}
Note what happens if we try to step the program (if 10 true false): there is no rule that applies to this program! Formally, a term is stuck if (1) there is no small-step semantics rule that can apply to it, and (2) it is not a value. Stuck terms cause runtime errors in interpreters when they are evaluated. In our previous interpreters, we raised a runtime error when this happened.