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 128 on December 14 from 07:00 PM until 10: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)}\)

Show Answer

b. \(C = \texttt{(Function q -> q (Function r -> r (Function s -> s 4))) $\bullet$}\)

Show Answer

c. \(C = \texttt{$\bullet$ (Function z -> z - 2) (Function x -> 0 - x) 1}\)

Show Answer

d. \(C = \texttt{(Function a -> Function b -> b (Function x -> x + 1) a) 2 (Function z -> $\bullet$)}\)

Show Answer

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.

Show Answer

b. Give the operational semantics of the new F♭M expressions.

Show Answer

c. Now consider TF♭M: a type system for F♭M. Give a new grammar for \(\tau\) in this language.

Show Answer

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!

Show Answer

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.

Show Answer

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 argument 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!)

Show Answer

Let fooPart =
  Function foo -> Function bar -> Function x ->
    If x = 0 Then 0 Else
    bar foo bar (x-1)
In
Let barPart =
  Function foo -> Function bar -> Function x ->
    If x = 0 Then 0 Else
    If x = 1 Then 1 Else
    foo foo bar (x-2)
In
Let foo = fooPart fooPart barPart In
foo 5

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.

Show Answer

(Function f1 -> Function f2 ->
  Let wrapper =
    Function self -> Function f -> Function x -> f (self self f1) (self self f2) x
  In
  wrapper wrapper f1
)

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:

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\}}\)

Show Answer

b. Consider the following graph:

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.

Show Answer

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.

Show