Homework 7: State

• Due: 04/12 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. Call-by-reference

In class, we defined the following transformation from Scheme-style mutation to ML-style:

``````     T⟦x⟧ = !x
T⟦λx. t⟧ = λx. let x = ref x in T⟦t⟧
T⟦t1 t2⟧ = T⟦t1⟧ T⟦t2⟧
T⟦x := t⟧ = x := T⟦t⟧``````

Some languages allow call-by-reference: in C++, this is indicated by putting `&` in front of the name of the formal parameter. In the lambda calculus, we could introduce new syntax

``````t ::= ...
&x. t
t @ x``````

where `&` is like `λ` but uses call-by-reference, and `t @ x` applies a call-by-reference function to `x`, so that

``````let inc = &x. x:=succ x in
let x = 0 in
inc @ x;
x
⟶* succ 0``````

How would you extend the above transformation to handle this?

`````` T⟦&x. t⟧ =
T⟦t @ x⟧ = ``````

The right-hand sides should use only simply-typed or untyped (your choice) λ-calculus with references.

Hint: The answer is not very complicated, so don’t worry if it looks too simple.

2. Mutable lists

Assume simply-typed λNB with NatList (`cons`, `car`, `cdr`) recursive types (`μ`) and references (`ref`, `!`, and `:=`).

In Scheme, `set!` corresponds roughly to `:=`. It also has `set-car!` and `set-cdr!`, which can be used to modify lists:

``````> (define l (list 1 2 3))
> (set-car! l 4)
> l
(4 2 3)
> (set-cdr! l (list 5 6))
> l
(4 5 6)``````
1. Define a type `MutableNatList` and associated functions:

``````  nil' : MutableNatList
cons' : Nat → MutableNatList → MutableNatList
car' : MutableNatList → Nat
cdr' : MutableNatList → MutableNatList
setcar : MutableNatList → Nat → Unit
setcdr : MutableNatList → MutableNatList → Unit``````

They should satisfy the following equations:

``````car' nil'        = 0
car' (cons' x y) = x
cdr' nil'        = nil'
cdr' (cons' x y) = y
(let l = cons' x y in setcar l x'; car' l) = x'
(let l = cons' x y in setcar l x'; cdr' l) = y
(let l = cons' x y in setcdr l y'; car' l) = x
(let l = cons' x y in setcdr l y'; cdr' l) = y'``````
2. Show how to build a circular list of zeros such that the following equations are true:

``````car' zeros = 0
cdr' zeros = zeros``````

3. Recursion via references

Assume simply-typed λNB with multiplication (`times`) and references (`ref`, `!`, and `:=`).

1. Define a factorial function `fac : Nat→Nat`. Hint: A function that calls itself is not so different from a list that contains itself as a tail (1c 2b).

2. Define `fix : ((Nat→Nat) → Nat→Nat) → Nat→Nat`. It should be possible to use `fix` to define a factorial function in the usual way:

``fac ≡ fix (λf: Nat→Nat. λn:Nat. if iszero n then succ 0 else times n (f (pred n)))``