# 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⟦t
```_{1} t_{2}⟧ = T⟦t_{1}⟧ T⟦t_{2}⟧
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 (~~ recursive types (`cons`

, `car`

, `cdr`

)`μ`

) 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)
```

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'`

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 `:=`

).

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).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)))`