Simply write answer for one ocaml CPS transformation question:)

Simply write answer for one ocaml CPS transformation question:)

HW 4 – CSP Transformation; Working with
Mathematical Specifications

CS 4

2

1

– Fall 201

3

Revision 1.0

Assigned Wednesday, September 18, 2013
Due Wednesday, September 25, 2013, 19:59pm
Extension 48 hours (20% penalty)

1 Change Log
1.0 Initial Release.

2 Objectives and Background
The purpose of this HW is to help your understanding of:

• The basic CSP transformation algorithm

• How to use a formal mathematically recursive definition

3 Turn-In Procedure
Using your favorite tool(s), you should put your solution in a file named hw4 (the same name as this file has
on the website). If you have problems generating a pdf, please seek help from the course staff. Your answers to the
following questions are to be submitted electronically via the handin script as though an MP. This assignment is
named hw4.

4 Background and Definitions
Throughout this HW, we will be working with a (very) simple functional language. It is a fragment of MicorML (a
frgament of SML, an OCaml-like language), and the seed of the language that we will be using in MPs throughout
the rest of this semester. Using a mix of MicroML concrete syntax (expression constructs as you would type them
in MicroML’s top-level loop) and recursive mathematical functions, we will describe below the algorithm for CSP
transformation for this fragment. You should compare this formal definition with the description given on examples in
class.

The language fragment we will work with in this assignment is given by the following Context Free Grammar:

e → c | v | e⊕e
| if e then e else e
| fn v => ; | e e

The symbol e ranges recursively over all expressions in MicroML, c ranges over constants, v ranges over program
variables, and ⊕ ranges over infixed binary primitive operations. The MicroML construct fn v=> e corresponds the
OCaml’s construct fun v-> e. This language will expand over the course of the semester.

1

Mathematically we represent CPS transformation by the functions [[e]]κ, which calculates the CPS form of an
expression e when passed the continuation κ. The symbol κ does not represent a programming language variable, but
rather a complex expression describing the current continuation for e.

The defining equations of this function are given below. Recall that when transforming a function into CPS, it is
necessary to expand the arguments to the function to include one that is for passing the continuation to it. We will use
κ to represent a continuation that has already been calculated or given to us, and k, ki, k′ etc as the name of variables
that can be assigned continuations. We will use v, vi, v′ etc for the ordinary variables in our program.

By v being fresh for an expression e, we mean that v needs to be some variable that is NOT in e. In MP5, you will
implement a function for selecting one, but here you are free to choose a name as you please, subject to being different
from all the other names that have already been used.

• The CPS transformation of a variable or constant expression just applies the continuation to the variable or
constant, since during execution, when this point in the code is reached, both variables and constants are already
fully evaluated (except for being looked up).

[[v]]κ = κ v

[[c]]κ = κ c

Example: [[x]](FUN y -> report y) = (FUN y -> report y) x This may be read as “load reg-
ister y with the value for x, then do a procedure call to report”.

• The CPS transformation for a binary operator mirrors its evaluation order. It first evaluates its first argument
then its second before evaluating the binary operator applied to those two values. We create a new continuation
that takes the result of the first argument, e1, binds it to v1 then evaluates the second argument, e2, and binds
that result to v2. As a last step it applies the current continuation to the result of v1 ⊕v2. This is formalized in
the following rule:

[[e1 ⊕e2]]κ = [[e1]]FUN v1 -> [[e2]]FUN v2 -> κ (v1 ⊕v2)
Where

v1 is fresh for e1, e2, and κ
v2 is fresh for e1, e2, κ, and v1

Example: [[x + 1]](FUN w -> report w)
= [[x]](FUN y -> [[1]](FUN z -> (FUN w -> report w) (y + z)))
= [[x]](FUN y -> ((FUN z -> (FUN w -> report w) (y + z)) 1))
= (FUN y -> ((FUN z -> (FUN w -> report w) (y + z)) 1)) x

• Each CPS transformation should make explicit the order of evaluation of each subexpression. For if-then-else
expressions, the first thing to be done is to evaluate the boolean guard. The resulting boolean value needs to
be passed to an if-then-else that will choose a branch. When the boolean value is true, we need to evaluate
the transformed then-branch, which will pass its value to the final continuation for the if-then-else expression.
Similarly, when the boolean value is false we need to evaluate the transformed else-branch, which will pass its
value to the final continuation for the if-then-else expression. To accomplish this, we recursively CPS-transform
the boolean guard e1 with the continuation with a formal parameter v that is fresh for the then branch e2, the
else branch e3 and the final continuation κ, where, based on the value of v, the continuation chooses either
the CPS-transform of e2 with the original continuation κ, or the CPS-transform of e3, again with the original
continuation κ.

[[if e1 then e2 else e3]]κ = [[e1]]FUN v -> IF v THEN [[e2]]κ ELSE [[e3]]κ

Where v is fresh for e2, e3, and κ

2

With FUN v -> IF v THEN [[e2]]κ ELSE [[e3]]κ we are creating a new continutation from our old. This
is not a function at the level of expressions, but rather at the level of continuations, hence the use of a different,
albeit related, syntax.
Example:
[[if x > 0 then 2 else 3]](FUN w -> report w)
= [[x > 0]](FUN y -> IF y THEN [[2]](FUN w -> report w) ELSE [[3]](FUN w -> report w))

= (FUN y -> IF y THEN [[2]](FUN w -> report w) ELSE [[3]](FUN w -> report w)) (x > 0)
= (FUN y -> IF y THEN ((FUN w -> report w) 2) ELSE ((FUN w -> report w) 3)) (x > 0)

• A function expression by itself does not get evaluated (well, it gets turned into a closure), so it needs to be
handed to the continuation directly, except that, when it eventually gets applied, it will need to additionally
take a continuation as another argument, and its body will need to have been transformed with respect to this
additional argument. Therefore, we need to choose a new continuation variable k to be the formal parameter
for passing a continuation into the function. Then, we need to transform the body with k as its continuation,
and put it inside a continuation function with the same original formal parameter together with k. The original
continuation κ is then applied to the result.

[[fn x => e]]κ = κ (FN x k -> [[e]]k) Where k is new (fresh for κ)

Notice that we are not yet evaluating anything, so (FN x k -> [[e]]k) is a CPS function expression, not
actually a closure.
Example:
[[fn x => x + 1]](FUN w -> report w)
= (FUN w -> report w) (FN x k -> (FUN y -> ((FUN z -> k (y + z)) 1)) x)

• The CPS transformation for application mirrors its evaluation order. In MicroML, we will uniformly use left-to-
right evaluation. Therefore, to evaluate an application, first evaluate the function, e1, to a closure, then evaluate
e2 to a value to which that closure is applied. We create a new continuation that takes the result of e1 and binds
it to v1, then evaluates e2 and binds it to v2. Finally, v1 is applied to v2 and, since the CPS transformation makes
all functions take a continuation, it is also applied to the current continuation κ. This rule is formalized by:

[[e1 e2]]κ = [[e1]](FUN v1 -> [[e2]](FUN v2 -> v1 v2 κ))
Where

v1 is fresh for e2 and κ
v2 is fresh for v1 and κ

Example: [[(fn x => x + 1) 2]](FUN w -> report w)
= [[(fn x => x + 1)]](FUN y -> [[2]](FUN z -> y z (FUN w -> report w)))
= (FUN y -> [[2]](FUN z -> y z (FUN w -> report w)))

(FN x k -> (FUN a -> ((FUN b -> k (a + b)) 1)) x)

= (FUN y -> ((FUN z -> y z (FUN w -> report w)) 2))

(FN x k -> (FUN a -> ((FUN b -> k (a + b)) 1)) x)

5 Problem
1. (35 pts) Compute the following CPS transformation. All parts should be transformed completely.

[[fn f => fn x => if x > 0 then f x else f ((-1) * x)]](FUN w -> report w)

3