In this assignment you will model the lambda calculus
1. Define an OCaml data type lc for the pure lambda calculus
2. Define functions ht, size, fv that give the height, size (number of atomic terms) and free variables in a given lambda term.
3. Define a function subst that given a lambda term e, a variable x and another lambda term e' , returns e[e'/x].
4. Define a function subterm_occ which returns all the occurrence positions (given as sequences over {L, R} of all occurrences of a given term e_1 inside another given term e_2.
5. Implement closures, using type and data type definitions,and write a functions isValueClosure that checks whether a given closure is a value closure or not.
6. Define functions that implement the big-step closure semantics for both call-y-value and call-by-name parameter passing.
7. For closed lambda terms, implement the SECD machine that defines execution under call-by-value.
8. For closed lambda terms, implement the Krivine machine that defines execution under call-by-name semantics.
Show that your abstract machine implementations are correct with respect to the semantics you have coded in part 6.
For 7&8, define suitable functions to initialize the machine, and (in 8) to unload the machine.
For (7), show that the closure that is obtained as the answer corresponds in a formal sense to the value closure that the call-by-value semantics of (6) returns.