9.1.1 The design recipe always applies🔗

Our work follows the recipe introduced in How to Design Programs and adapted to language implementation in the previous lecture.

1. From Problem Analysis to Data Definitions

2. Signature, Purpose Statement, Header

3. Functional Examples

4. Function Template

5. Function Definition

6. Testing

9.1.2 Trace a program🔗

Skill F3. "I can trace a short Plait program that uses function application, local bindings, conditionals, and datatype case analysis."

9.2.1 Building on our small-step interpreter🔗

Our Lam language from last class includes numeric literals:

e ::= n\mid x\mid\lambda x.e\mid(e\;e) \quad\quad v ::= n\mid\lambda x.e.

> (define-type Lam     (num [n : Number])     (var [name : Symbol])     (lam [arg : Symbol] [body : Lam])     (app [fn : Lam] [arg : Lam]))

We followed the call-by-value semantics for λ, which uses three rules:

1. [cbv1] Once the function and argument are values, apply the function.

2. [cbv2] If the function is a value but the argument is not, then evaluate it.

3. [cbv3] If the function is not a value, evaluate it until it is.

and our interpreter was as follows:

> (subst : (Symbol Lam Lam -> Lam))

> (define (subst id assignment body)     (type-case Lam body       [(num x) (num x)]       [(var x)        (if (equal? id x)         assignment         (var x))]       [(app e1 e2)        (app (subst id assignment e1)              (subst id assignment e2))]       [(lam x body)        (if (equal? x id)            (lam x body)            (lam x (subst id assignment body)))]))

> (value? : (Lam -> Boolean))

> (define (value? e)     (type-case Lam e       [(num n) #t]       [(var x) #f]       [(lam x body) #t]       [(app fn arg) #f]))

> (step : (Lam -> Lam))

> (define (step e)       (type-case Lam e         [(num n) e]         [(var x) (error 'runtime "unbound variable")]         [(lam x body) e]         [(app fn arg)          (type-case Lam fn            [(lam x body)             (if (value? arg)                 (subst x arg body)                 (app fn (step arg)))]            [(app f a) (app (step fn) arg)]            [else (error 'runtime "application on non-function")])]))

We could have also written these as a derivation tree:

\frac{}{((\lambda x.b)\;v)\longrightarrow b[x\mapsto v]} \quad[\mathrm{cbv1}]

\frac{a\text{ not a value}\quad a\longrightarrow a{}’} {((\lambda x.b)\;a)\longrightarrow((\lambda x.b)\;a{}’)} \quad[\mathrm{cbv2}] \quad \frac{f\text{ not a value}\quad f\longrightarrow f{}’} {(f\;a)\longrightarrow(f{}’\;a)} \quad[\mathrm{cbv3}].

We also allow values to step to themselves for our interpreter: \frac{}{v\longrightarrow v}\quad[\mathrm{val}].

Technically, in our small-step semantics, once you reach a value you are at a successful stopping point (otherwise our semantics would loop, infinitely). We add this rule in order to perform multi-stepping, which we will talk about next.

The subst helper respects shadowing and considers only substitutions with variables that do not have free variables ("closed expressions"). Substitutions with open expressions will need to be alpha-renamed (also discussed in a minute).

> (define eid (lam 'x (var 'x)))

> (test (step (app eid (num 7))) (num 7))

- Void good (step (app eid (num 7))) at line 10   expected: (num 7)   given: (num 7)

> (test (step (app eid (app eid (num 7)))) (app eid (num 7)))

- Void good (step (app eid (app eid (num 7)))) at line 11   expected: (app (lam 'x (var 'x)) (num 7))   given: (app (lam 'x (var 'x)) (num 7))

> (test (step (app (app (lam 'x (lam 'y (var 'x))) (num 7)) (num 9)))         (app (lam 'y (num 7)) (num 9)))

- Void good (step (app (app (lam (quote x) (lam (quote y) (var (quote x)))) (num 7)) (num 9))) at line 12   expected: (app (lam 'y (num 7)) (num 9))   given: (app (lam 'y (num 7)) (num 9))

> (test/exn (step (app (num 1) eid)) "application on non-function")

- Void good (step (app (num 1) eid)) at line 13   expected: "application on non-function"   given: "runtime: application on non-function"

Each time we step we are finding the next reducible expression and performing a whole-program transition, hence transitions using –>.

9.2.2 Shadowing in Lam and Let🔗

Skill R2. [intuition] Understand variable shadowing and how to perform substitution

Let’s look at: \lambda x.\lambda x.x \quad\text{and}\quad \lambda x.\lambda y.x.

The final variable x belongs to the inner binder in the first term and to the outer binder in the second. So if we perform substituton then:

(\lambda x.x)[x\mapsto7]=\lambda x.x \quad\text{but}\quad (\lambda y.x)[x\mapsto7]=\lambda y.7.

What is happening here is variable shadowing. This is exactly the situation that we wanted avoid with substitution!

Variable shadowing is closely related to alpha-renaming and alpha-equivalence. For instance, back in the lecture of System-F, we had a similar question (but at the type level):

Is \lambda x.\lambda y.x \quad\text{equal to}\quad \lambda y.\lambda x.y.

The answer here is a definitive "yes." For instance, let’s perform alpha-renaming on the outer-variables from before, mapping the outer x to z: \lambda z.\lambda x.x \quad\text{and}\quad \lambda z.\lambda y.z.

Now it is quite clear that these two programs are not the same.

This is the same as what happens when we look at LetLang. Recall LetLang:

How do we fill the ? in the first pseudo-syntax? We perform function application!

Of course (λ x . (λ x . x)) 7 performs a reduction and arrives at (λ x . x)

The inner initializer’s x refers to the outer binding. The final x refers to the inner binding. Renaming the inner binder must not rename its initializer.

Question! What happens if we performed a function application like the following:

(\lambda x . (\lambda y.x)) (\lambda z.y)

Naive substitution actually produces \lambda y.\lambda z.y which accidentally captures the free variable y. To correct this, we want to perform an alpha-renaming first:

Choose fresh variables so there are no new name conflicts.

9.2.3 Multi-stepping Lam🔗

As pointed out before, if we keep this "value" rule in our small-step semantics, our interpreters will actually loop infinitely. However to give our operational semantics computational meaning, we don’t necessarily know if our expression is guaranteed to terminate, so we need to perform generative recursion.

Whereas before we wrote e1 –> e2, Now we will write e1 –>* e2 for zero or more transitions. Under these new rules, the resulting e2 may actually be another intermediate reducible expression and is not necessarily going to be a value.

Formally, we can state the rules for this "step-star" as the following:

\frac{}{e\longrightarrow^{*}e}\quad[\mathrm{ms-refl}] \quad \frac{e\longrightarrow e_1\quad e_1\longrightarrow^{*}e_2} {e\longrightarrow^{*}e_2}\quad[\mathrm{ms-step}].

With the rule "ms-refl" encompassing stepping to yourself, and the rule "ms-step" making a single step (or more).

> (define ex0     (app (lam 'x               (app (lam 'x (var 'x))                    (app (lam 'y (var 'y)) (var 'x))))          (num 7)))

However, to be very precise, the rules of our multi-stepper would convert this into the following derivation tree:

Here we are using –> from our small-step interpreter. We can now implement this

Notice how this is different than big-step semantics! Big step semantics very much feels like multi-stepping, however the rules for big-step semantics are much simpler. When we write a big-step semantics, we usually want some more interesting rules than what is provided by the lambda calculus. For instance, CBV would amount to the single rule:

While big step is a little simpler, it is not able to express many computations (like nondeterminism and concurrency).

9.2.4 Skill assessment🔗