15–312: Principles of Programming Languages
Final Examination
May 9, 2017 1pm to 4pm
• There are 18 pages in this examination, comprising 5 questions worth a total of 120 points.
• You may refer to your personal notes and to Practical Foundations of Programming Languages,
but not to any other person or source.
• You have 180 minutes to complete this examination.
• Please answer all questions in the space provided with the question.
• There are three scratch sheets at the end for your use.
Full Name:
Andrew ID:
Question: Trees Cont FF Exc Space Total
Points: 15 10 30 30 35 120
15–312 Final 1 of 18 May 9, 2017 1pm to 4pm
Question 1 [15]: Rose Trees in System F
Recall the definition of System F. For your convenience we repeat the syntax here.
type τ ::= t
exp e ::= x
λ (x : τ) e
A rose tree is a tree in which each node has a variable and unbounded number of children.
Rose trees with elements of type α can be implemented with the following recursive type.
R(α) = rec t is α× recu is unit + (t× u)
(a) (6 points) Translate the type R(α) as a polymorphic type R of the form ∀(α.τ) in System
Hint: First encode the inner recursive type in System F. Recall Church encodings.
(b) You will now define the singleton tree r0 that consists of a single node 0 as a term of type
R[nat] in System F.
i. (3 points) Define the term nil[t], that represents the empty list of element type t.
(Question continues on the next page)
15–312 Final 2 of 18 May 9, 2017 1pm to 4pm
ii. (6 points) Use nil[t] for an appropriate t to define the singleton tree r0 that consists
of node 0 as a term of type R[nat] in System F.
You can use the natural number 0 in your term as an abbreviation for the actual
encoding of natural numbers in System F.
15–312 Final 3 of 18 May 9, 2017 1pm to 4pm
Question 2 [10]: Continuations
For this question, you will work with a total language with continuations, products, and sums.
The syntax of the language is given below and the static and dynamic semantics is defined as
in lecture.
type τ ::= cont(τ)
exp e ::= letcc{τ}(x.e)
throw{τ}(e1; e2)
λ (x : τ) e
case e {l · x ↪→ e1 | r · y ↪→ e2}
As a reminder, the static semantics for continuations is given by the following rules:
Γ, x : τ cont ` e : τ
Γ ` letcc{τ}(x.e) : τ
Γ ` e1 : τ1 Γ ` e2 : τ1 cont
Γ ` throw{τ}(e1; e2) : τ
Exhibit terms of the following types.
(a) (4 points) (cont(τ2)→ cont(τ1))→ τ1 → τ2
(b) (6 points) cont(cont(τ1) + cont(τ2))→ (τ1 × τ2)
15–312 Final 4 of 18 May 9, 2017 1pm to 4pm
Question 3 [30]: Flip Flops
The following diagram depicts an RS Latch, a logic gate comprising two cross-coupled nor gates
whose inputs and outputs are all booleans. The A output of the latch is governed by the R
and S inputs, which may not be both false or both true at the same time. If the R input is set
to true, and the S input is set to false, then the A output is driven to false; the latch is reset.
If, on the other hand, the S input is set to true, and the R input to false, then the A output
is driven to true; the latch is set. The B output behaves exactly the opposite way around.
In this question you are to develop an implementation of an RS latch in PCF extended with
booleans and products, as they are defined in PFPL.
The purpose of the exercise is to test your knowledge of self-reference (fixed points), laziness
and eagerness, and your ability to define an extension to this language to account for the
expected behavior of the latch. Laziness is defined to mean that all constructors are evaluated
lazily, and that function applications are call-by-name; eagerness is defined to mean that all
constructors are eager, and that function applications are call-by-value.
Please use pattern matching notation for functions whose domain is a product type, it will
make your solution much clearer.
(a) (4 points) Give a definition of the function nor of type bool× bool → bool such that
nor exhibits under either a lazy or eager interpretation:
nor(〈false, false〉) 7−→∗ true
nor(〈false, true〉) 7−→∗ false
nor(〈true, false〉) 7−→∗ false
nor(〈true, true〉) 7−→∗ false
There are essentially two possible answers, which differ in the order in which the inputs
are considered; give both implementations, called nor1 and nor2, using the notation of
Section 11.3 of PFPL:
(Question continues on the next page)
15–312 Final 5 of 18 May 9, 2017 1pm to 4pm
(b) (4 points) By definition nor1 and nor2 behave the same on values, and so in an eager
setting there are no inputs that would cause one to behave differently from the other. But
that is not true in a lazy setting. Give a pair of inputs on which nor1 behaves differently
from nor2 in a lazy setting. Hint : one argument must be a divergent computation; do you
(c) (4 points) Give a definition of the function rsl of type bool× bool→ bool× bool whose
inputs are R and S, respectively, and whose outputs are A and B, respectively. Define
your answer using either version of the nor function, nor1 or nor2, but be clear about
which you are using. Hint : your code should implement the wiring diagram given above,
ensuring that the outputs are properly “fed back” as inputs.
(d) (4 points) Argue that under an eager evaluation strategy, your definition of rsl diverges
for any input values, and hence cannot be considered a valid implementation of the RS
15–312 Final 6 of 18 May 9, 2017 1pm to 4pm
(e) (4 points) Show that under lazy evaluation, your definition of rsl behaves properly on
some value inputs, but not others. More precisely, give one pair of boolean values v1 and
v2 such that rsl(〈v1, v2〉) · l evaluates properly, and another pair v′1 and v
2 such that
rsl(〈v′1, v
2〉) · l evaluates improperly. Notice that we are only considering the A output of
the latch, which is the first projection.
(f) (10 points) It can be proved, with considerable difficulty, that there is no solution to
the rsl problem in either eager or lazy PCF enriched with booleans and products. We
must instead enrich PCF with a special “built-in” form of nor whose evaluation is non-
deterministic in that there can be more than one next state of evaluation for a given use of
nor. Give a non-deterministic dynamics for nor(e1; e2) such your implementation of rsl
using this form of nor will behave properly on all inputs. Hint : your answer will require
five rules.
15–312 Final 7 of 18 May 9, 2017 1pm to 4pm
Question 4 [30]: Exceptions in Algol
Recall from class that an exception mechanism consists of two separable parts, the control
mechanism, which allows for transfers from the raiser to the handler, and the data mechanism,
which passes a value from the raiser to the handler. The control aspect was studied in the
context of a functional expression language; the data aspect, which we isolated as dynamic
classification, was studied in the context of an imperative language. In this question you are to
consider an integrated account of both the control and data aspects of exceptions within the
command language of Modernized Algol, taking into account both scoped and free assignables.
The syntax of commands in extended MA is defined as follows:
Cmd m ::= dcl(e; a.m) dcl a := e inm new assignable
| get[a] @ a fetch
| set[a](e) a := e assign
| ret(e) ret e return
| bndow(e;x1.m1;x2.m2) bndowx1 ↪→ e inm1 owx2 ↪→m2 sequence/handle
| cls{τ}(b.m) cls b of τ inm new class
| raise(e) raise(e) raise exception
The first four are as usual, but the sequencing construct has been extended to include both
normal and exceptional (“otherwise”) returns, with the following statics:
Γ `Σ e : τ cmd Γ, x1 : τ `Σ m1 ∼·· τ ′ Γ, x2 : clsfd `Σ m2 ∼·· τ ′
Γ `Σ bndow(e;x1.m1;x2.m2) ∼·· τ ′
The usual sequencing construct, bndx← e ; m, may be defined as bndowx ↪→ e inm ow y ↪→
raise(y), which just propagates exceptions. Analogously, an exception handler command,
try e owx ↪→m, may be defined dually by bndowx ↪→ e in ret(x) ow y ↪→m, which propagates
normal returns.
The declaration cls{τ}(b.m) introduces a new class (aka “exception”), b, with associated value
of type τ for use within the command m, analogously to the declaration of assignables. Classes
are used to build elements of type clsfd, which is the type of exception values. The command
raise(e) raises an exception with associated value e of type clsfd. This value is passed to
the exception return of the nearest enclosing bind, which may propagate it further, or dispatch
on the class using the machinery of dynamic classification given in Chapter 33 of PFPL, the
syntax of which is given by the following grammar:
Typ τ ::= clsfd clsfd classified
Exp e ::= in[b](e) b · e instance
isin[b](e;x.e1; e2) match e as b · x ↪→ e1 ow ↪→ e2 comparison
You are to consider a scoped dynamics for classes/exceptions in the sense that no class/exception
is allowed to escape the scope of its declaration by any means. The scoped dynamics for
commands in MA has transitions the form m ‖ µ 7−→
m′ ‖ µ′, and the scoped dynamics for
expressions has transitions of the form e 7−→
(Question continues on the next page)
15–312 Final 8 of 18 May 9, 2017 1pm to 4pm
(a) (8 points) Give the scoped dynamics for the class declaration command, following the
pattern of assignable declaration. Your solution will require three rules to account for
computing within the scope of the declaration and for exiting the scope of the declaration.
(b) (8 points) Give the scoped dynamics for the raise command, following the pattern of the
return command. Your solution will require three rules, two defining the execution and
completion of the command itself, and one defining its interaction with the bind/otherwise
(bndow) command.
(Question continues on the next page)
15–312 Final 9 of 18 May 9, 2017 1pm to 4pm
(c) (4 points) Give two examples of a class declaration command that that cannot safely
make progress when executed, one involving a return command and one involving a raise
command. Each example should take exactly one line, and should either be unable to
progress, or would progress to an ill-defined state.
(d) (3 points) Define the statics of the raise command so as to ensure type safety.
(e) (3 points) Define the statics of class declaration so as to ensure type safety. In particular,
the two counterexamples you gave should not be statically correct according to your rules!
(f) (4 points) Assuming that the class declaration and assignable declaration commands are
the only means by which new symbols are introduced, is it sound to permit the type clsfd
to be mobile, or must it be declared immobile?
15–312 Final 10 of 18 May 9, 2017 1pm to 4pm
Question 5 [35]: Space Semantics
In class, we introduced cost dynamics to characterize the time needed to evaluate an expression.
In this exercise, you will develop an analogous idea to study the stack space required during
evaluation. Our case study will be PCF. We will work with both its evaluation semantics and
its stack semantics. The various entities we need have the following (concrete) syntax:
type τ ::= nat
exp e ::= x
λ (x : τ) e
ifz(e; e0;x.e1)
fix τ : x is e
frame f ::= s(–)
ifz(–; e0;x.e1)
stack k ::= �
You may assume the usual static semantics and that all expressions in this exercise are well-
typed. The rules for the stack machine for the call-by-value version of PCF are defined as
k B z 7→ k C z
k B s(e) 7→ s(–); k B e
s(–); k C v 7→ k C s(v)
k B ifz(e; e0;x.e1) 7→ ifz(–; e0;x.e1); k B e
ifz(–; e0;x.e1); k C z 7→ k B e0
ifz(–; e0;x.e1); k C s(v) 7→ k B [v/x]e1
k B λ (x : τ) e 7→ k C λ (x : τ) e
k B e1(e2) 7→ ap(–; e2); k B e1
ap(–; e2); k C v1 7→ ap(v1; –); k B e2
ap(λ (x : τ) e; –); k C v2 7→ k B [v2/x]e
k B fixx : τ is e 7→ k B [fixx : τ is e/x]e
We define the stack size |s| of a state s of the form kCe or kBv as the number |k| of frames in the
stack k. Given a sequence s0 7→∗ sn of state transitions of the form s0 7→ s1 7→ . . . 7→ sn−1 7→ sn,
we define the stack space of this transition, written ‖s0 7→∗ sn‖, as the size of the largest stack
size in this sequence (i.e., the high-water mark). More precisely,
‖s0 7→ s1 7→ . . . 7→ sn−1 7→ sn‖ = max
(Question continues on the next page)
15–312 Final 11 of 18 May 9, 2017 1pm to 4pm
(a) (4 points) Describe the stack space that is used for evaluating the numeral n as a function
of n, that is, define the function σ1(n) = ‖�B n 7→∗ �C n‖ using a simple arithmetic
expression.
(b) (8 points) Now consider the usual definition of addition in PCF:
add , fix plus : nat⇀ nat⇀ nat isλ (x : nat)λ (y : nat) ifz(x; y;x
′.s(plus(x′)(y))),
Describe the stack space that is used for evaluating the expression add(m)(n) as a function
of m and n, that is, define the function σ2(n,m) = ‖�B add(m)(n) 7→∗ �Cm+ n‖ using
a simple arithmetic expression.
Hint: Write down the steps of the stack machine until you see a pattern. Use your answer
to the previous questions.
Hint: We are asking for an exact solution but you can earn partial points with an asymp-
totically correct solution (using big-O).
(c) (8 points) Next you will define the rules of a cost dynamics for stack space that correctly
reflects the (high-water mark) stack space that we defined for the stack machine. The
rules are based on the standard evaluation dynamics for PCF annotated with natural
numbers. The resulting judgement has the form
and intuitively means that expression e evaluates to value v using stack space s. The rules
for conditionals and fix are defined as follows.
e ⇓s z e0 ⇓s0 v0
ifz(e; e0;x.e1) ⇓max{s+1,s0} v0
e ⇓s s(v) [v/x]e1 ⇓s1 v1
ifz(e; e0;x.e1) ⇓max{s+1,s1} v1
[fixx : τ is e/x]e ⇓s v
fixx : τ is e ⇓s v
(Question continues on the next page)
15–312 Final 12 of 18 May 9, 2017 1pm to 4pm
Define the remaining rules of the cost dynamics. The missing cases are zero, successor,
abstraction, and applications.
(d) Consider the expression ω that is defined as follows.
ω , fix loop : nat is loop
i. (3 points) Describe the stack space that is used for evaluating the expression ω on an
empty stack �.
ii. (3 points) What does the cost dynamics state about the stack space usage of ω?
(Question continues on the next page)
15–312 Final 13 of 18 May 9, 2017 1pm to 4pm
(e) (9 points) We now show that the cost dynamics is sound and complete with respect to
the stack semantics: For any expression e and value v, it is the case that � B e 7→∗ � C v
iff e ⇓s v where s = ‖�B e 7→∗ �C v‖.
Here, you will only prove the soundness of the evaluation dynamics. We also need to
generalize the theorem to account for intermediate steps in the derivation. So the actual
property you will prove is the following:
Property 1. If e ⇓s v then for any k we have that kBe 7→∗ kCv and ‖k B e 7→∗ k C v‖ =
The proof proceeds by rule induction on e ⇓s v. We will develop one case in detail and
ask you to prove one more.
Case ev:ifzz:
e ⇓s z e0 ⇓s0 v0
ifz(e; e0;x.e1) ⇓max{s+1,s0} v0
(ev:ifzz).
Induction hypothesis 1: For any stack k′ there is a derivation of k′ B e 7→∗ k′ C z
such that ‖k′ B e 7→∗ k′ C z‖ = s+ |k′|.
Induction hypothesis 2: For any stack k′′ there is a derivation of k′′Be0 7→∗ k′′Cv0
such that ‖k′′ B e0 7→∗ k′′ C v0‖ = s0 + |k′′|.
To show: For any stack k, there is a derivation of kB ifz(e; e0;x.e1) 7→∗ kC v0 such
that ‖k B ifz(e; e0;x.e1) 7→∗ k C v0‖ = max{s+ 1, s0}+ |k|.
Assume k is given. Let k′ be ifz(–; e0;x.e1); k and k
′′ be k. Then |k′| = |k| + 1 and
|k′′| = |k| and, using IH 1 with k′ and IH 2 with k′′, we derive
kBifz(e; e0;x.e1) 7→ ifz(–; e0;x.e1); kBe 7→∗ ifz(–; e0;x.e1); kCz 7→ kBe0 7→∗ kCv0
Moreover, we have∥∥∥∥∥∥∥∥∥∥
k B ifz(e; e0;x.e1)
7→ ifz(–; e0;x.e1); k B e
7→∗ ifz(–; e0;x.e1); k C z
7→∗ k C v0
∥∥∥∥∥∥∥∥∥∥
|k B ifz(e; e0;x.e1)|,
‖ifz(–; e0;x.e1); k B e 7→∗ ifz(–; e0;x.e1); k C z‖,
‖k B e0 7→∗ k C v0‖
= max{|k|, s+ 1 + |k|, s0 + |k|} (by IH 1 and IH 2)
= max{s+ 1, s0}+ |k|
This completes the proof for the case ev:ifzz.
(Question continues on the next page)
15–312 Final 14 of 18 May 9, 2017 1pm to 4pm
Provide the induction proof for Property 1 in the case where the derivation of e ⇓s v ends
in rule ev:s.
Case ev:s:
s(e) ⇓s+1 s(v)
Induction hypothesis:
15–312 Final 15 of 18 May 9, 2017 1pm to 4pm
Scratch Work:
15–312 Final 16 of 18 May 9, 2017 1pm to 4pm
Scratch Work:
15–312 Final 17 of 18 May 9, 2017 1pm to 4pm
Scratch Work:
15–312 Final 18 of 18 May 9, 2017 1pm to 4pm