COS 441 Take-home Midterm Fall 2007
This Midterm should be the individual work of each student in the class. Please to not talk to anyone other than myself (David Walker) or TA (Kenny Zhu) about the questions on this midterm. If neither I nor Kenny are available while you are taking the exam and you have a question, make a reasonable assumption, write down that assumption clearly and continue working. Talking to anyone else about this exam while you are taking it constitutes a violation of Princeton's code of academic integrity.
You may consult your lecture notes, or any of the textbooks listed as required or recommended on the course Web pages, but do not search for the answers on the general Web.
Details:
- You must complete the exam in a 5-hour period of time. Write down the time you download the exam and the time you hand it at the top of the exam itself.
- You will work on the exam during a single, continuous 5-hour period occurring between the 19th and 26th of Oct, 2006.
- At the top of the exam you turn in, sign your name and write: “This exam represents my own work in accordance with University regulations.”
- Hand in exams by slipping them under Kenny’s door or by submitting them electronically via email to . If submitting electronically, an electronic signature (ie, type your name) is sufficient for the bullet above.
Reminders:
- Read questions completely before beginning your response. This exam has quite a lot of reading because part of the test is whether or not you are able to read and understand formal inference rules (typing rules and operational rules).
- Always state your proof methodology clearly and explicitly before writing down the details of a proof (eg: “Proof by induction on the derivation of G |- e : t”). Points are automatically deducted from anyone who does not do this. Points will also be deducted for proofs that are unclear or poorly structured.
- Always use the exact syntax of expressions, types, judgments, etc. that you are given in a question, or clearly define the abbreviations that you're using. When in doubt, avoid abbreviations. Definitely do not just start using some new, informal notation without defining it -- graders will not be able to figure out your intent.
- When defining a new type system, set of operational rules, etc., be sure to state the form of the new judgments in question before laying out the details of the rules (unless, of course, the question specifies the form of the judgment you should use).
- Even if you can't come up with the correct solution for a question, write down as clear and concise an explanation of your thought process and partial work as you can to get partial credit. Do not leave a question entirely blank unless you know nothing about the topic.
- When writing out your proofs, use plenty of space (either electronically or on paper) to make them easy to read. One of the best ways is to format each line with one true statement (judgment) on the left and the justification for that statement on the right (in terms of earlier statements and inference rules, etc.).
- The exam will be graded out of 25.
Good luck!
(Questions begin on the next page.)
1. Consider the following syntax of trees and lists of numbers:
natural numbers n ::= 0 | 1 | 2 | ...
lists l ::= nil | n :: l
trees t ::= leaf n | node (t1,t2)
For example, “7::5::2::nil” is a list and“node(leaf 7,node(leaf 5,leaf 2))” is a tree. The judgement “|-- listmem n l” defines membership of a number n in a list l. The judgement “|-- append l1 l2 l3 defines what it means to append list l2 onto the end of list l1, creating list l3. The judgement “|-- treemem n t” defines membership of a number n in a tree t. Here are the rules:
|-- listmem n1 l
------(listmem0) ------(listmem1)
|-- listmem n (n::l) |-- listmem n1 (n2::l)
|-- append l1 l2 l3
------(append1) ------(append2)
|-- append nil l2 l2 |-- append (n1::l1) l2 (n1::l3)
------(treemem0)
|-- treemem n (leaf n)
|-- treemem n t1
------(treemem1)
|-- treemem n (node (t1,t2))
|-- treemem n t2
------(treemem2)
|-- treemem n (node (t1,t2))
Questions:
a) [3 points] Prove that if |-- append l1 l2 l3 and |-- listmem n l2 then
|-- listmem n l3. Hint: Do induction on the derivation of “|-- append l1 l2 l3”
b) [3 points] Prove that if |-- append l1 l2 l3 and |-- listmem n l1 then
|-- listmem n l3.
c) [3 points] Define a judgement with the form “|-- convert t l” that converts any tree t in a list l. You may perform the conversion in any way you choose. The only caveat is that you must convert all trees into some list and you must be able to prove the theorem in part d. You may use the append judgement above. You may define auxiliary judgments to help you with the conversion if you want.
d) [3 points] Prove that if |-- convert t l and |-- treemem n t
then |-- listmem n l. State and prove any auxiliary lemmas you need. You may use lemmas from parts a and b (even if you weren’t able to prove them).
(more midterm questions on the next page)
2. Here is the syntax of the untyped lambda calculus:
e ::= x | x.e | e1 e2
a) [2 points] Show the sequence of expressions you get when you evaluate the following expression usingthe left-to-right, call-by-value evaluation order, one step at a time. Evaluate it until you can’t evaluate it any more (according to call-by-value evaluation rules).
(x.y.z.y x z) (u.u) (w.w)
b) [1 point] Give an example of an untyped lambda calculus term that is “stuck.”
c) [4 points] Here are the multi-step evaluation rules:
e1 --> e2 e2 -->* e3
------(reflex) ------(trans)
e -->* e e1 -->* e3
Prove: If e -->* e’ and e’ -->* e’’ then e -->* e’’.
Prove this yourself on this exam directly from the rules above -- Don’t cite lemmas proven in class or in the textbook in order to prove this theorem.
(more questions on the next page)
3. Here is the syntax and typing rules of the call-by-value typed lambda calculus with only functions and unit:
t ::= unit | t1 -> t2
e ::= x | () | x.e | e1 e2
G ::= . | G, x:t
------(T-var)
G |-- x : G(x)
------(T-unit)
G |-- () : unit
G, x:t1 |-- e : t2
------(T-fun)
G |-- x.e : t1 -> t2
G |-- e1 : t1 -> t2 G |-- e2 : t1
------(T-app)
G |-- e1 e2 : t2
e1 --> e1'
------(E-app1)
e1 e2 --> e1' e2
e2 --> e2'
------(E-app2)
v e2 --> v e2'
------(E-app3)
(x.e) v --> e[v/x]
a) [1 point] Give an example of an expression e that:
- is not “stuck” and
- will not type check in any valid typing context at all.
b)[1 point] Give an example of an expression e that:
- will not type check in an empty initial typing context.
- but when you evaluate it for one step, the result willtype check in the empty context.
ie,: . |-- e : t is not a valid judgement for any t, but e --> e’ and for some t’, . |-- e’ : t’ is valid.
4. In this question, we will be using the following definition of the lambda calculus with booleans and recursive functions (LBR from now on):
Syntax:
(types) t ::= bool | t1 -> t2
(expressions) e ::= x | true | false | if e1 then e2 else e3 | fun f (x:t1):t2 = e | e1 e2
(values) v ::= true | false | fun f (x:t1):t2 = e
(contexts) G ::= . | G,x:t
Call-by-value Evaluation:
e --> e'
------(E-if0)
if e then e1 else e2 --> if e' then e1 else e2
------(E-if1)
if true then e1 else e2 --> e1
------(E-if2)
if false then e1 else e2 --> e2
e1 --> e1'
------(E-app1)
e1 e2 --> e1' e2
e2 --> e2'
------(E-app2)
v e2 --> v e2'
------(E-app3)
(fun f(x:t1):t2 = e) v --> e[v/x][(fun f(x:t1):t2 = e)/f]
Typing:
------(T-var)
G |-- x : G(x)
------(T-true) ------(T-false)
G |-- true : bool G |-- false : bool
G |-- e : bool G |-- e1 : t G |-- e2 : t
------(T-if)
G |-- if e then e1 else e2 : t
G, f:t1->t2, x:t1 |-- e : t2
------(T-fun)
G |-- fun f (x:t1):t2 = e : t1 -> t2
G |-- e1 : t1 -> t2 G |-- e2 : t1
------(T-app)
G |-- e1 e2 : t2
Now, consider extending LBR with types for integers and natural numbers. ie:
types t ::= ... (as before) ... | int | nat
integers n ::= ... | -2 | -1 | 0 | 1 | 2 | ...
operators op ::= + | -
expressions e ::= ... (as before) ... | n | e1 op e2
values v ::= ... (as before) ... | n
e1 --> e1'
------(E-op1)
e1 op e2 --> e1' op e2
e2 --> e2'
------(E-op2)
v op e2 --> v op e2'
------(E-op3)
n1 + n2 --> n3
(where n3 is the integer that results from adding integer n1 to integer n2)
(eg: 5 + 6 --> 11)
------(E-op4)
n1 - n2 --> n3
(where n3 is the integer that results from subtracting integer n2 from integer n1)
(eg: 5 - 6 --> -1)
n >= 0
------(T-nat)
G |-- n : nat
------(T-int)
G |-- n : int
G |-- e1 : nat G |-- e2 : nat
------(T-op1)
G |-- e1 op e2 : nat
G |-- e1 : nat G |-- e2 : int
------(T-op2)
G |-- e1 op e2 : int
G |-- e1 : int G |-- e2 : nat
------(T-op3)
G |-- e1 op e2 : int
G |-- e1 : int G |-- e2 : int
------(T-op4)
G |-- e1 op e2 : int
Now answer these questions:
a) [2 points] Is the standard Progress lemma true or false for LBR extended as above with ints and nats? If true just say “true” (don’t give a proof). If false, then say “false” and give a counter-example (ie: give a simple example expression and show that the progress lemma doesn’t hold for that expression).
b) [2 points] Is the standard Preservation lemma true or false for LBR extended as above with ints and nats? If true just say “true” (don’t give a proof). If false the say “false”and give a counter-example (ie: give a simple example expression and show that the preservation lemma doesn’t hold for that expression).