Simply write answer for one ocaml CPS transformation question:)

HW 4 – CSP Transformation; Working with Mathematical Specifications

CS 421 – Fall 2013 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.pdf (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