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 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₁ ;; g₂ should behave just like (λx. g₂) t₁. For example: the term
```
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?