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.
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
& 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 (
μ) and references (
set! corresponds roughly to
:=. It also has
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
MutableNatListand 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 (
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 (
fix : ((Nat→Nat) → Nat→Nat) → Nat→Nat. It should be possible to use
fixto 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)))