Midterm 2 concepts review

March 1, 2024
All notes are expanded based on

MP4

MP4.2: Continuation Passing Style, $quadk$

Write a function $quadk : int * int * int \to (int \to ’a) \to ’a$ that takes three interger arguments a, b, c and returns the result of the expression $(2 * (a^{2}) + 4 * b) + c$ .

# let quadk (a, b, c) k = ...;;
val quadk : int * int * int -> (int -> `a) -> `a = <fun>

# quadk (1, 1, 1) report_int;;
Result: 7
- : unit = ()

Useful things to know before starting is understanding the way the expression is evaluted when writing the CPS version.

Common.ml

let mulk(a, b) k = k (a * b);;
let addk(a, b) k = k (a + b);;

Solution:

let quadk (a, b, c) k =
    mulk(4, b) (fun e1 -> 
        mulk(a, a) (fun e2 -> 
            mulk(2, e2) (fun e3 -> 
                addk(e2, e2) (fun e4 -> 
                    addk(e4, c) k))))

MP4.3: Continuation Passing Style, $three_freeze$

Write a function $three_freezek: string * string \to (string \to ‘a) \to ‘a$ that takes two strings arguments s and p and calculates the string formed by concatenating them as sp. The function will then return the string made by repeating this string, and then on its left, repeating it once more. In the end, sp wil be repeated three times in a row, but you should only calcualte sp once.

# let three_freezek (s, p) k = ...;;
val three_freezek : string * string -> (string -> `a) -> `a = <fun>

# three_freezek ("muda", "plop") (fun s -> (s, String.length s));;
- : stirng * int = ("mudaplopmudaplopmudaplop", 24)

Solution:

let three_freezek (s, p) k = 
    concatk(s, p) (fun first -> concatk(first, first) (fun second -> concatk(first,second) k))

Sample Questions for Midterm 2

1. Put the following function in full continuation passing style: Use $addk, subk, mulk, leqk,$ for the CPS forms of the primitive opeartions (+, -, *, <=).

let rec sum_odd n = 
    if n <= 0 then
        0 
    else ((2 * n) - 1) + sum_odd (n - 1);;

Solution:

let sum_oddk n k = 
    leqk (n, 0) (fun is_less -> 
        if is_less k 0 
        else subk (n, 1) (fun one_less -> 
           sum_oddk one_less (fun e1 -> 
                mulk (2, n) (fun e2 -> 
                    subk (e2, 1) (fun e3 -> 
                        addk (e3, e1) k)))))

2. Given the following OCAML datatype: $type int_seq = Null | Snoc of (int_seq * int)$ write a tail-recursive function in OCAML all_pos : $int_seq \to bool$ that returns true if every integer in the input $int_seq$ to which all_pos is applied is strictly greater than 0 and false otherwise. Thus $all_pos (Snoc(Snoc(Snoc(Null, 3), 5), 7))$ should returns true, but $all_pos (Snoc(Null, -1)) and all_pos (Snoc(Snoc(Null, 3),0))$ should both return false.

Solution:

let rec all_pos s = 
    (match s with Null -> true
    | Snoc(seq, x) -> if x <= 0 then false else all_pos seq)

3. Write the definition of an OCAML variant type $reg_exp$ to express abstract syntax trees for regular expressions over a base character set of booleans. Thus, a boolean is a $reg_exp$ , epsilon is a $reg_exp$ , a paranthesized $reg_exp$ is a $reg_exp$ , the concatenation of two $reg_exp$ ’s is a $reg_exp$ , the choice of two $reg_exp$ ’s is a $reg_exp$ , and the Kleene star of a $reg_exp$ is a $reg_exp$ .

Solution:

type reg_exp = 
    Char of bool 
    | Epsilon 
    | Paren of reg_exp
    | Concat of (reg_exp * reg_exp)
    | Choice of (reg_exp * reg_exp)
    | Kleene_star of reg_exp

4. Given the following rules for CPS transformation:

$[[x]]_{κ} = κ x$

$[[c]]_{κ} = κ c$

$[[let x = e_{1} in e_{2}]]_{κ} = [[e_{1}]] (FN x \to [[e_{2}]]_{κ})$

$[[e_{1} \oplus e_{2}]]_{κ} = [[e_{2}]] (FN a \to [[e_{1}]] (FN b \to κ (b \oplus a)))$

where $e_{1}$ and $e_{2}$ are ocaml expressions, $κ$ is any continuation, $x$ is a varibale and $c$ is a constant, give the step-by-step transformation of

$[[let x = 2 + 3 in x - 4]] REPORTk$

Solution:

$[[let x = 2 + 3 in x - 4]] REPORTk \Rightarrow$

$[[2 + 3]] (FN x \to [[x - 4]] REPORTk) \Rightarrow$

$[[2 + 3]] (FN x \to [[4]] (FN n \to [[x]] (FN m \to REPORTk (m - n)))) \Rightarrow$

$[[2 + 3]] (FN x \to [[4]] (FN n \to (FN m \to REPORTk (m - n)) x)) \Rightarrow$

$[[2 + 3]] (FN x \to (FN n \to (FN m \to REPORTk (m - n)) x) 4) \Rightarrow$

$[[3]] (FN u \to [[2]] (FN v \to (FN x \to (FN n \to (FN m \to REPORTk (m - n)) x) 4) (v + u))) \Rightarrow$

$[[3]] (FN u \to (FN v \to (FN x \to (FN n \to (FN m \to REPORTk (m - n)) x) 4) (v + u)) 2) \Rightarrow$

$(FN u \to (FN v \to (FN x \to (FN n \to (FN m \to REPORTk (m - n)) x) 4) (v + u)) 2) 3$

5. MP5: Continuation Passing Style (CPS) Transformation cps_exp

Solution:

let rec cps_exp e k = 
    match e with 
    (* [[x]]k = k x *)
    | VarExp x -> VarCPS (k, x)
    (* [[c]]k = k c *)
    | ConstExp c -> ConstCPS (k, c)
    (* [[~e]]k = [[e]]_(FN v -> k (~v)) *)
    | MonOpAppExp (m, e) -> 
        let v = freshFor freeVarsInContCPS k 
        in cps_exp e (FnContCPS(v, MonOpAppCPS(k, m, v)))
    (* [[e1 + e2]]k = [[e2]]_(FN v2 -> [[e1]]_(FN v1 -> k (v1 + v2))) *)
    | BinOpAppExp (b, e1, e2) -> 
        let v2 = freshFor (freeVarsInContCPS k @ freeVarsInExp e1) in
        let v1 = freshFor (v2::(freeVarsInContCPS k)) in 
        let cps_e2 = 
            cps_exp e1 (FnContCPS(v1, BinOpAppCPS(k, b, v1, v2))) 
        in cps_exp e2 (FnContCPS(v2, cps_e2))
    (* [[e1 e2]]k = [[e2]]_(FN v2 -> [[e1]]_(FN v1 -> k (v1, v2))) *)
    | AppExp (e1 ,e2) -> 
        let v2 = freshFor (freeVarsInContCPS k @ freeVarsInExp e1) in 
        let v2 = freshFor (v2::freeVarsInContCPS k) in 
        let cps_e1 = cps_exp e1 (FnContCPS(v1, AppCPS(k, v1, v2))) in 
        cps_exp e2 (FnContCPS(v2, cps_e1))
    (* [[fun x -> e]]k = k (FUN x kx -> [[e]]kx) *)
    | FunExp (x, e) -> 
        let ecps = cps_exp e (ConVarCPS Kvar) in 
        FunCPS(k, x, Kvar, ecps) 
    (* [[let x = e1 in e2]]k = [[e2]]_(FN x -> [[e2]]k) *)
    | LetInExp (x, e1, e2) -> 
        let e2cps = cps_exp e2 k in 
        let fx = FnContCPS(x, e2cps) in 
        cps_exp e1 fx
    (* [[let rec f x = e1 in e2]]k = (FN f -> [[e2]]k)(FIX f. FUN x -> FN kx -> [[e1]]kx) *)
    | LetRecInExp (f, x, e1, e2) -> 
        let e1cps = cps_exp e1 (ContVarCPS Kvar) in 
        let e2cps = cps_exp e2 in 
        FixCPS(FnContCPS(f, kvar), f, x, Kvar, e1cps)

6. Given a polynorphic type derivation for ${} | - let id = fun x \to x in id id true : bool$

$Let \frac{Fun \frac{Var \frac{}{{x :^{'} a} ⊢ x :^{'} a}}{{} ⊢ fun x \to x} App \frac{App \frac{Var \frac{Instance : ’a \to bool \to bool}{Γ ⊢ id : (bool \to bool) \to bool \to bool} Var \frac{Instance : ’a \to bool}{Γ ⊢ id : (bool \to bool)}}{Γ ⊢ id id : bool \to bool} Const \frac{}{Γ ⊢ true : bool}}{{id : \forall^{'} a .^{'} a \to^{'} a} ⊢ id id true}}{{} ⊢ let id = fun x \to x : in id id true : bool}$