# Homework 3: Semantics of λ

- Due: 02/15 at 11:55pm
- Points: 15 (each question 5 points)

Please prepare your solutions as a PDF file (scanned handwriting is okay, but no .doc or .docx, please). Submit your PDF file in Sakai.

## 1. Normal-order and call-by-name evaluation

Evaluate the term

`(λx. λy. x x) ((λx. λy. y y) (λx. λy. y y))`

using (i) normal-order and (ii) call-by-name evaluation, underlining the redex at each step.

(cf. Exercise 5.3.6, but please do it yourself before peeking at the answer.)

*Using evaluation contexts*, modify the semantics of the call-by-value λ-calculus to use call-by-name evaluation instead.

## 2. Big-step operational semantics

At the top of page 71, the definition of substitution is missing a case, for `[x↦s](λy. t`

where _{1})`y ≠ x`

and `y ∈ FV(s)`

. But if the initial term is closed (has no free variables), then we’ll never need this missing case. In this problem, we’ll prove this for the big-step operational semantics of λ. (Something similar can be shown for the small-step semantics as well.)

Prove that

`FV([x↦s]t) ⊆ FV(t) \ {x} ∪ FV(s)`

.Prove that if

`t ⇓ v`

, then`FV(v) ⊆ FV(t)`

and in every substitution`[x↦s]`

in the derivation of`t ⇓ v`

,`FV(s) ⊆ FV(t)`

.

In particular, if `t`

is closed, then in every substitution `[x↦s]`

in the derivation of `t ⇓ v`

, we know that `s`

is closed, so the missing case is never needed.

## 3. Pythonic scope

Python introduced nested functions in version 2.0. Initially, its scoping rules worked like this. Consider the following code:

```
x = 1
def f(x):
return lambda y: x
def g(x):
return f(2)(0)
print(g(3))
```

In modern Python, which has lexical scope, this prints `2`

, because the `x`

inside the `lambda`

is bound by the nearest enclosing binder of `x`

, which is `def f(x):`

, so it has the value `2`

. But in Python 2.0, it printed `1`

. This is because all variables are either bound by the smallest enclosing function, or else they are global. So the `x`

inside the `lambda`

is global and has the value `1`

. (If Python had dynamic scoping, it would print `3`

.) This oddity was corrected quickly; lexical scoping was added in 2.1 as an option, and in 2.2 by default.

In this exercise, we’ll ~~break~~ modify the λ-calculus to be like Python 2.0.

Our definition of the λ-calculus doesn’t really have any concept of global variables, so let’s add the following syntax (with

`g`

as the new start symbol):`g ::= let x = t ;; g t t ::= ...`

This is basically the same as Scheme’s

`let`

except restricted to be global; the term`let x = t`

should behave just like_{1};; g_{2}`(λx. g`

. For example: the term_{2}) t_{1}`let a = 0;; let b = true;; let a = succ a;; λf. f a b`

should evaluate to

`λf. f (succ 0) true`

.Extend the operational semantics of λNB (page 63) to handle this new construction. Don’t forget to extend the definition of substitution.

Modify the operational semantics so that, as in Python 2.0, no local variables bound outside an abstraction

`λx. t`

are visible inside it (as in Python 2.0). For example, we should have`(λx. λy. y) true false ⟶* false (λx. λx. x) true false ⟶* false (λx. λy. x) true false gets stuck`

But global variables should be visible everywhere:

`let x = 0 ;; (λx. λy. y) true false ⟶* false let x = 0 ;; (λx. λx. x) true false ⟶* false let x = 0 ;; (λx. λy. x) true false ⟶* 0`

Hint: The only changes you need to make have to do with substitution. You’ll probably need to create a new definition of substitution alongside the old one; use square brackets vs. curly braces to distinguish them.

Why do you think it’s important to base this modification on λNB instead of pure λ with Church numerals/booleans?