---
# System prepended metadata

title: Homework 4

---

# Homework 4
- Chiao Lu
    - UID: 204848946
    - Email: josephlu85@engineering.ucla.edu
- Aishni Parab
    - UID: 905526328
    - Email: aishni@cs.ucla.edu

## Problem 1
### (a)
<pre>
function p:((A &and; B) &and; C) &rightarrow;
    let a = fst (fst p) in
    let b = snd (fst p) in
    let c = snd p in
    (a, (b, c))
</pre>

### (b)
<pre>
function p:((A &or; B) &or; C) &rightarrow;
    match p with
    | left aorb &rightarrow;
        match aorb with
            | left a &rightarrow; left a
            | right b &rightarrow; right (left b)
    | right c &rightarrow; right (right c)
</pre>

### (c\)
<pre>
function p:((A &or; B) &rightarrow; C) &rightarrow;
    (
        function p1:A &rightarrow; p (left p1),
        function p2:B &rightarrow; p (right p2)
    )
</pre>

### (d)
<pre>
function p1:(A &rightarrow; B) &rightarrow;
    function p2:(B &rightarrow; False) &rightarrow;
        function p3:A &rightarrow;
            p2 (p1 p3)
</pre>

## Problem 2
### (a)
Reference: [https://piazza.com/class_profile/get_resource/h82u3exc6351np/h860gvgnm2e1dr](https://piazza.com/class_profile/get_resource/h82u3exc6351np/h860gvgnm2e1dr)

If we have this rule
<pre>
t1 &rightarrow; t1'
------------------------------
while t1 do t2 &rightarrow; while t1' do t2
</pre>

We would also need something like the following

<pre>
------------------------------
while true do t2 &rightarrow; ???
</pre>

This is basically telling us to keep evaluating `t1` until it is `true` or `false`, and then we must either enter an _infinite loop_ or _not enter the loop at all_, which is definitely not the desired behaviour of `while`. We need the `while` loop to keep looking at `t1` until it evaluates to `false`, instead of just once.

### (b)
Online reference above is suggesting something like <code>if t1 then (t2; while t1 do t2) else ()</code>. We convert the sequencing (`;`) to `let` as discussed in the lecture (`t1;t2 --> let x=t1 in t2`). After that, as pointed out in the Campuswire hint by Todd, we can't use `let` so we convert it further to function call (`E-LetSugar`).

<pre>
fresh x
------------------------------
while t1 do t2 &rightarrow;
    if t1 then ((function x:True &rightarrow; while t1 do x) t2) else ()
</pre>

### (c\)
<pre>
&Gamma; &RightTee; t1:Bool     &Gamma; &RightTee; t2:True
------------------------------
&Gamma; &RightTee; while t1 do t2:True
</pre>

### (d)
<pre>
function whileFun f1:(True &rightarrow; Bool) f2:(True &rightarrow; True) &rightarrow;
    let rec loop = 
        function p1:(True &rightarrow; Bool) p2:(True &rightarrow; True) &rightarrow;
            if (p1 ()) then (let x=(p2 ()) in (loop p1 p2)) else ()
        in
            (loop f1 f2)
</pre>

## Problem 3
### (a)
<pre>
                              ------------------ (I-Var) ------------------ (I-Var)
                              tinfer({f:X1,x:X2}, f) = &#10112; tinfer({f:X1,x:X2}, x) = &#10113;
-------------------- (I-Var)  --------------------------------------------- (I-App)
tinfer({f:X1,x:X2}, f) = &#10114;    tinfer({f:X1,x:X2}, f x) = &#10115;
--------------------------------------------------------------------------- (I-App)
tinfer({f:X1,x:X2}, f (f x)) = &#10116;
--------------------------------------------------------------------------- (I-Fun)
tinfer({f:X1}, function x &rightarrow; f (f x)) = &#10117;
--------------------------------------------------------------------------- (I-Fun)
tinfer({}, function f &rightarrow; function x &rightarrow; f (f x)) = &#10118;
</pre>

Where
<pre>
&#10112; = (X3, {X3=X1})
&#10113; = (X4, {X4=X2})
&#10114; = (X5, {X5=X1})
&#10115; = (X6, {X3=X1}&bigcup;{X4=X2}&bigcup;{X3=X4&rightarrow;X6})
&#10116; = (X7, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7})
&#10117; = (X8, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7}&bigcup;{X8=X2&rightarrow;X7})
&#10118; = (X9, {X5=X1}&bigcup;{X3=X1}⋃{X4=X2}⋃{X3=X4→X6}&bigcup;{X5=X6&rightarrow;X7}&bigcup;{X8=X2&rightarrow;X7}&bigcup;{X9=X1&rightarrow;X8})
</pre>

### (b)

<pre>
x:Int
f:Int&rightarrow;Int

X1=Int&rightarrow;Int
X2=Int
X3=Int&rightarrow;Int
X4=Int
X5=Int&rightarrow;Int
X6=Int
X7=Int
X8=Int&rightarrow;Int
X9=(Int&rightarrow;Int)&rightarrow;Int&rightarrow;Int
</pre>

Putting this into ocaml shell gives
```ocaml=
─( 05:13:55 )─< command 0 >────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # function f -> function x -> f (f x);;
- : ('a -> 'a) -> 'a -> 'a = <fun>
─( 05:13:55 )─< command 1 >────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # function (f:int->int) -> function (x:int) -> f (f x);;
- : (int -> int) -> int -> int = <fun>

```
## Problem 4
<pre>
tinfer(G, s) = (S1, C1)
fresh T2
fresh X
--------------------------- (I-Left)
tinfer(G, left s) = (X, C1 &bigcup; {X=S1&vee;T2})

tinfer(G, s) = (S2, C2)
fresh T1
fresh X
--------------------------- (I-Right)
tinfer(G, right s) = (X, C2 &bigcup; {X=T1&vee;S2})

fresh X
fresh X1
fresh X2
tinfer((G, x1:X1), s1) = (S1, C1)
tinfer((G, x2:X2), s2) = (S2, C2)
tinfer(G, s) = (S, C)
------------------------------------(I-Match)
tinfer(G, match s with left x1&rightarrow;s1 |
                       right x2&rightarrow;s2) 
    = (X, C &bigcup; C1 &bigcup; C2 &bigcup; {S=S1&vee;S2, X=S})
    
</pre>

                         