# Homework 3
## Team:
* Chiao Lu
* UID: 204848946
* Email: chiao@cs.ucla.edu
* Aishni Parab
* UID: 905526328
* Email: aishni@cs.ucla.edu
## Problem 1
Let <code>id = function x → x</code>
### (a)
<code>x0</code> is a variable name.
<code>t = x0 (id id)</code> is stuck.
### (b)
<code>(id id) x0 → id x0 → x0</code> is now stuck!
### (c\)
<pre>
---------------------------------------- (E-APPBETA)
id id → id
---------------------------------------- (E-APP2)
(id (id id)) → id id
---------------------------------------- (E-APP1)
(id (id id)) id → (id id) id
</pre>
## Problem 2
```ocaml=
exception ImplementMe
(* Problem 2 *)
(* Type t represents abstract syntax trees for the lambda calculus. A
variable name is represented as an OCaml string.
Example: the term ((function x -> x x) (function x -> x)) would be represented as follows:
FunCall(Function("x", FunCall(Var "x", Var "x")), Function("x", Var "x"))
*)
(* We also include the constant True, which is a value, to make testing easier. *)
type t = True | Var of string | Function of string * t | FunCall of t * t
(* 2a: Implement the subst function below, which substitutes a given
value v for all free occurrences of the variable named x in term t,
returning the resulting term. You may assume that v has no free
variables. *)
let rec subst (x:string) (v:t) (t:t) =
match t with
| True -> True
| Var var -> (if var = x then v else t)
| Function(arg, body) -> ( if arg = x then Function(arg, body) else Function(arg, (subst x v body)) )
| FunCall(t1, t2) -> FunCall((subst x v t1), (subst x v t2))
(* 2b: Implement the step function, which takes a term of type t above
and produces a new term that results from taking one step of
computation on t, following the operational semantics rules for the
lambda calculus. If t is a normal form, the step function should
raise the NormalForm exception declared below. *)
exception NormalForm
let rec step t =
match t with
| True -> raise NormalForm
| Var _ -> raise NormalForm
| Function(arg, body) -> raise NormalForm
| FunCall(t1, t2) -> (
match (t1, t2) with
| (Function(t1_arg, t1_body), Function(t2_arg, t2_body)) -> (subst t1_arg t2 t1_body)
| (Function(t1_arg, t1_body), True) -> (subst t1_arg t2 t1_body)
| (Function(_, _), _) -> FunCall(t1, (step t2))
| (True, _) -> FunCall(t1, (step t2))
| (_, _) -> FunCall((step t1), t2)
)
```
## Problem 3
```ocaml=
exception ImplementMe
(* Problem 3 *)
(* As you saw in Problem 1, implementing the lambda calculus, and any
other language that has variables, is annoying, because you have to
manually implement the means of binding variables to values, in our
case via a substitution function.
An alternative style, known as higher-order abstract syntax (HOAS), is
a clever way to use variables from the host language (in our case,
OCaml) to represent variables in the language being implemented (in
our case, the lambda calculus). That way, we get substitution for
free! You will explore this style below...
*)
(* Type t represents abstract syntax trees for the lambda calculus.
We are only representing the subset of *closed* terms in the lambda
calculus -- HOAS cannot handle terms with free variables in them.
Note that we no longer have a term for variables below. Instead,
variables are represented implicitly via the fact that a lambda
calculus function is represented as an OCaml function from terms to
terms (hence the notion of higher-order syntax -- the syntax tree
contains functions).
Example: the term ((function x -> x x) (function x -> x)) would be represented as follows:
FunCall(Function(function x -> FunCall(x, x)), Function(function x -> x))
*)
type t = True | Function of (t -> t) | FunCall of t * t
(* Implement the step function, which takes a term of type t above and
produces a new term that results from taking one step of
computation on t. If t is a normal form, the step function should
raise the NormalForm exception. *)
exception NormalForm
let rec step t = match t with
| True -> raise NormalForm
| Function _ -> raise NormalForm
| FunCall(t1, t2) -> (
match (t1, t2) with
| (Function f1, True) -> f1 True
| (Function f1, Function f2) -> (f1 t2)
| (Function f1, _) -> FunCall(t1, (step t2))
| (True, _) -> FunCall(t1, (step t2))
| (_, _) -> FunCall((step t1), t2)
)
```
## Problem 4
### (a)
<pre>
T1 = Bool
T = Bool → Int
</pre>
Derivation:
<pre>
------- (T-VAR) ------- (T-NUM) ------ (T-NUM)
x:Bool ⊢ x:Bool x:Bool ⊢ 0:Int x:Bool ⊢ 1:Int
---------------------------------------------------------------------- (T-IF)
x:Bool ⊢ if x then 0 else 1 : Int
---------------------------------------------------------------------- (T-FUN)
∅ ⊢ function x: Bool → if x then 0 else 1 : (Bool → Int)
</pre>
### (b)
<pre>
T1 = Int → Bool
T = (Int → Bool) → Int
</pre>
Derivation:
Let <code>Γ = f:(Int → Bool)</code>
<pre>
-------- (T-VAR) --- (T-NUM)
Γ ⊢ f:(Int→Bool) Γ ⊢ 0:Int
--------------------------------- (T-APP) ---- (T-NUM) ---- (T-NUM)
Γ ⊢ (f 0): Bool Γ ⊢ 0:Int Γ ⊢ 1:Int
---------------------------------------------------------------------- (T-IF)
Γ ⊢ if (f 0) then 0 else 1 : Int
---------------------------------------------------------------------- (T-FUN)
∅ ⊢ function f: (Int → Bool) → if (f 0) then 0 else 1 : ((Int → Bool) → Int)
</pre>
### (c\)
`function f: T1 -> function x: T2 -> if (f x) then (x 0) else 1`
<pre>
T1 = (Int → Int) → Bool
T2 = Int → Int
T = ((Int → Int) → Bool) → ((Int → Int) → Int)
</pre>
Derivation:
<pre>
----------------- (T-VAR) --------- (T-VAR)
f:T1,x:T2 ⊢ f:(T2 → Bool) f:T1,x:T2 ⊢ x:T2 OUTOFSPACE
---------------------------------------- (T-APP) ----- (T-APP) - (T-NUM)
f:T1,x:T2 ⊢ (f x):Bool (x 0):Int 1:Int
------------------------------------------------------------------------ (T-IF)
f:T1,x:T2 ⊢ if (f x) then (x 0) else 1 : Int
------------------------------------------------------------------------ (T-FUN)
f:T1 ⊢ function x:T2 → if (f x) then (x 0) else 1 : (T2 → Int)
------------------------------------------------------------------------ (T-FUN)
∅ ⊢ function f:T1 → function x:T2 → if (f x) then (x 0) else 1 : T
</pre>
The <code>OUTOFSPACE</code> subtree is shown below because there's no space left above.
<pre>
---------------------- (T-VAR) ------------- (T-NUM)
f:T1,x:T2 ⊢ x:(Int→Int) f:T1,x:T2 ⊢ 0:Int
------------------------------------------------------------------------ (T-APP)
(x 0): Int
</pre>
## Problem 5
```ocaml=
(* Problem 5 *)
(* T ::= Bool | T -> T *)
type typ = Bool | Arrow of typ * typ
(* t ::= x | function x:T -> t | t1 t2 *)
type t = True | Var of string | Function of string * typ * t
| FunCall of t * t
(* env is a **type alias** for a list of (string,typ) pairs
env is not a new type, like t above,
but rather just a name for an existing type.
a list of pairs is sometimes called an *association* list.
OCaml already has some useful operations for manipulating such lists.
In particular, the function List.assoc (in the List standard library)
looks up the value associated with a given key in a given association
list. e.g., List.assoc "y" [("x", Bool); ("y", Arrow(Bool,Bool))]
returns Arrow(Bool,Bool). List.assoc raises a Not_found exception
if the given key is not in the list.
*)
type env = (string * typ) list
exception TypeError
(* typecheck takes a term (of type t) and a type environment (of type env)
and it returns the type of the term, or raises TypeError if the term
cannot be given a type. this function should have the same behavior
as the typechecking rules on the cheat sheet. *)
let rec typecheck (t:t) (env:env) : typ = match t with
| True -> Bool
| Var var -> (
try
List.assoc var env
with Not_found -> raise TypeError
)
| Function(arg, arg_type, body) -> (
let body_type = (typecheck body (List.append [(arg, arg_type)] env)) in
Arrow(arg_type, body_type)
)
| FunCall(t1, t2) -> (
let t2_type = (typecheck t2 env) in
match (typecheck t1 env) with
| Bool -> raise TypeError
| Arrow(t1_arg_type, t1_ret_type) -> (
if t1_arg_type = t2_type then t1_ret_type else (raise TypeError)
)
)
```
## Problem 6
### (a)
**Theorem:** If <code>∅ ⊢ t:T</code>, then either <code>t</code> is a value or there exists some term `t'` such that <code>t → t'</code>.
```
Defn. Lemma [Canonical Forms]:
1. If v is a value of type Bool, then v is either true or false.
2. If v is a value of type T1 -> T2, then v = function x: T1.t2.
Proof: We will prove by induction on typing derivation of t: T.
IH: Consider sub-derivation where if null |- t0: T, then either t0 is a value or there exists some term t0' such that t0 -> t0'.
The T-TRUE and T-FUN cases t is a value so the proof is trivial. T-VAR is not applicable since t is closed form (since environment is empty, we cannot look up the type for x).
For the case T-APP:
t = t1 t2
|- t1 : T11 -> T12
|- t2 : T11
By induction hypothesis, for both terms t1 and t2, either the term is a value or else it steps.
Case 1: t1 takes a step
If the term t1 takes a step, then we can apply E-APP1 to t.
Case 2: t1 is a value, t2 takes a step
If t1 is a value and t2 takes a step, then we can apply E-APP2 to t.
Case 3: t1 and t2 are values
If both t1 and t2 are values then by the Canonical forms lemma, t1 is of form function x: T11.t12 to which we can apply E-APPBETA to step t.
QED.
Ref. Pg 105 of txtbook.
```
### (b)
**Theorem:** If <code>Γ ⊢ t:T</code>, then either `t` is a value or there exists some term <code>t'</code> such that <code>t → t'</code>.
No. Consider the following counter example.
Start with non-empty type environment <code>Γ = {x:T}</code>
<pre>
Γ(x) = T
------------ (T-VAR)
Γ ⊢ x:T
</pre>
`x` is a variable, and therefore not a value.
`x` cannot step.
Sign in with Wallet
Connect another wallet