Final Exam
As stated in the course policies, this course includes a final examination. This is a written exam in which you will work out problems similar to those in the homework assignments. This semester, the final exam will be held in SCI 199 on May 16 from 02:00 PM until 05:00 PM.
Exam Protocol
You will be provided a copy of the exam as well as scratch paper at the beginning of the examination paper. Your responses will be due at the end of the examination period, giving you three hours to complete the work. You may not use the textbook, your course notes, or electronic devices during the exam (unless otherwise explicitly exempted by the instructor), nor may you communicate with anyone other than the proctor during the exam.
You may bring a single exam reference sheet: a single piece of 8.5” by 11” letter paper or A4 paper paper. You must build the contents of this reference sheet yourself; you may not copy anyone else’s reference material. To demonstrate that you are the author of the document, it must be handwritten and in your handwriting and you will submit it when you turn in your exam. Any alternative to this arrangement must be explicitly approved by your instructor. You are not required to use an exam reference sheet, but it is the only material that you may consult while taking the exam.
As always, be sure to reach out to your instructor well before the scheduled exam time if you require some form of academic accommodation.
Practice Exam
This practice exam is meant to be indicative of the sort of questions you might see on the final.
Problem 1
Let’s play Get the Point. In each of the parts below, write an expression \(e\) to be given to the provided context \(C\) such that \(C[e] \Rightarrow v\) for some number \(v\) between \(0\) and \(5\). Your expression \(e\) must not include any integers or integer operations (but may include booleans and boolean operations). You will receive a number of points on this part of the problem equal to \(v\). Values of \(v\) outside of this range or expressions \(e\) for which \(C[e]\) does not evaluate will be worth no points.
a. \(C = \texttt{$\bullet$ (Function f -> f 4 True)}\)
b. \(C = \texttt{(Function q -> q (Function r -> r (Function s -> s 4))) $\bullet$}\)
c. \(C = \texttt{$\bullet$ (Function z -> z - 2) (Function x -> 0 - x) 1}\)
d. \(C = \texttt{(Function a -> Function b -> b (Function x -> x + 1) a) 2 (Function z -> $\bullet$)}\)
Problem 2
Consider a language F♭M: F♭ with so-called “maybe” values. Maybe values are similar to the OCaml option
type: None
is a maybe value containing nothing while Some(v)
is a maybe value containing something (for some value v
). Similar to OCaml, we also need a syntax which, given a maybe value, allows us to write code for two cases: the case in which a value is None
and a case in which it is Some
. The latter case must bind to a variable the contents of the Some
value.
a. Give the syntax extensions to the F♭ expression and value grammar which define F♭M.
b. Give the operational semantics of the new F♭M expressions.
c. Now consider TF♭M: a type system for F♭M. Give a new grammar for \(\tau\) in this language.
d. Give type rules to extend the TF♭ type system to TF♭M. Note that you do not have to extend the expression grammar to do so!
e. Assume that we extend \(\tau\) above to include \(\alpha\) from EF♭. Give type rules, deductive closure modifications, and consistency checking rules to extend the EF♭ type system to EF♭M.
Problem 3
Self-passing allows us to define recursive functions in F♭. Most languages support mutual recursion: multiple functions defined in terms of each other. For instance, the following OCaml code defines two functions which call each other until the received parameter is either zero or one.
let rec foo x =
if x = 0 then 0 else
bar (x-1)
and bar x =
if x = 0 then 0 else
if x = 1 then 1 else
foo (x-2)
in
foo 5;;
With the above definition, foo 3
and foo 4
evaluate to 0
while foo 5
evaluates to 1
.
a. Translate the above code to F♭ without using Let Rec
. You must define both functions and then call the foo
function. You should not change how foo
is called; the programmer should still write foo 5
to call the foo
function. (Hint: you’ll need to use a variation of self-passing to accomplish this!)
b. Write a general mutual recursion combinator for two functions. The Y-combinator takes in a function of the form Function self -> Function x -> ...
and produces a function of the form Function x -> ...
which can call itself via self
. Likewise, your combinator should take in two functions of the form Function f1 -> Function f2 -> Function x -> ...
and produce a single function of the form Function x -> ...
. Both functions should be able to call the first function via f1
and the second function via f2
. The function returned by your combinator should be the mutually recursive version of the first function.
For instance, letting your combinator be y2
, the code
Let y2 = ... In
Let foo =
y2
(Function f1 -> Function f2 -> Function x ->
If x = 0 Then 0 Else
f2 (x-1)
)
(Function f1 -> Function f2 -> Function x ->
If x = 0 Then 0 Else
If x = 1 Then 1 Else
f1 (x-2)
)
In
foo 5
should evaluate to 1
.
Problem 4
Consider the subtyping relation \(\tau <: \tau’\). We can define a subtyping graph to be a graph in which each node is a type \(\tau\) and each edge is a subtyping relationship \(\tau <: \tau’\) where \(\tau\) is the source node and \(\tau’\) is the target node. For instance, considering just the three types \(\texttt{\{\}}\), \(\texttt{\{x:Int\}}\), and \(\texttt{\{x:Int;y:Int\}}\), we can build the following subtyping graph:
![](latex-eb4b2b7454d43a97f28913b25a6b936d.png)
This graph expresses that \(\texttt{\{x:Int\}} <: \texttt{\{\}}\), that \(\texttt{\{x:Int;y:Int\}} <: \texttt{\{\}}\), and that \(\texttt{\{x:Int;y:Int\}} <: \texttt{\{x:Int\}}\). We call this a closed subtyping graph because, for every pair of vertices \(\tau_1\) and \(\tau_2\) in the graph, an edge from \(\tau_1\) to \(\tau_2\) exists if and only if \(\tau_1 <: \tau_2\).
a. Draw a closed subtyping graph which includes all of the following types as nodes:
- \(\texttt{\{\}}\)
- \(\texttt{\{x:Bool\}}\)
- \(\texttt{\{x:Int\}}\)
- \(\texttt{\{f:\{y:Int\} -> Bool; x:Bool\}}\)
- \(\texttt{\{f:\{\} -> Bool; x:Bool\}}\)
- \(\texttt{\{x:Bool\} -> \{\}}\)
- \(\texttt{\{\} -> \{\}}\)
- \(\texttt{\{\} -> \{x:Bool\}}\)
b. Consider the following graph:
![](latex-65e73571e310093227dd2f592bc95ee3.png)
Is it possible for this to be a closed subtyping graph? If so, fill in the nodes with appropriate types to create an example. If not, explain why this is not possible.
Problem 5
Let the language ZRing be defined by the following syntax:
\[\begin{array}{r c l}e & ::= & v \mid e\ \texttt{+}\ e \mid e\ \texttt{*}\ e \\ v & ::= & \texttt{0} \mid \texttt{1} \mid \texttt{-1} \mid \ldots\end{array}\]
Suppose we define the operational semantics of ZRing in the following way:
\[ \text{Value Rule }\dfrac{ }{v \Rightarrow v} \hspace{1cm} \text{Plus Rule }\dfrac{e_1 \Rightarrow v_1 \hspace{0.5cm} e_2 \Rightarrow v_2 \hspace{0.5cm} v = \text{the sum of $v_1$ and $v_2$}}{e_1\ \texttt{+}\ e_2 \Rightarrow v} \hspace{1cm} \text{Times Rule }\dfrac{e_1 \Rightarrow v_1 \hspace{0.5cm} e_2 \Rightarrow v_2 \hspace{0.5cm} v = \text{the product of $v_1$ and $v_2$}}{e_1\ \texttt{*}\ e_2 \Rightarrow v} \hspace{1cm} \]
Prove that ZRing is a normalizing language.