4.1.1 Observational Equivalence🔗

What does it mean for two lambda programs to be semantically equivalent? An intuitive notion of equivalence is that two lambda calculus programs should be equivalent if there is no way to tell them apart by calling them.

So, what should be our notion of observable behavior for comparing equivalence of lambda calculus programs? Well, our lambda calculus can do very few things, so we don’t have many choices about what we can or cannot observe. Let’s take a leap of faith: let’s decide that we can observe whether or not a lambda calculus program terminates.

4.1.2 Establishing Inequivalence🔗

How do we know if this is a decent notion of observation? Well, we can use it to check whether or not programs we want to be equivalent or inequivalent are consistent with this choice. Let’s start by looking at two programs we assume should not be semantically equivalent: Ltrue and Lfalse. How can we tell if these two programs are equivalent or not by calling them? We need to find a particular way to call them that exhibits different termination behavior.

To do this, let’s define a function called poison-pill that loops forever when it is called, i.e., it simply calls \Omega:

\Omega = (\lambda x . x ~ x) ~ (\lambda x . x ~ x)

\texttt{poison-pill} = \lambda z . \Omega = \lambda z . ((\lambda x . x ~ x) ~ (\lambda x . x ~ x))

How can we use this function to distinguish Ltrue from Lfalse?

Observe, the following two programs have different terminating behavior (where we’ve shorted \lambda x . x to \texttt{id}):

(\texttt{Ltrue} ~ \texttt{poison-pill} ~ \texttt{id}) ~ \texttt{id} (\texttt{Lfalse} ~ \texttt{poison-pill} ~ \texttt{id}) ~ \texttt{id}

The first one runs forever, and the second one doesn’t. Carefully think about why. So, this establishes that these two programs are observationally inequivalent.

4.3.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]))

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

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.

Recall we had the following English description of small-step semantics:

• 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.

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.

4.3.2 Derivation Trees and Running Programs by Hand🔗

Back to small-step semantics. 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)

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.

4.3.3 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)}

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.

4.3.4 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.