(* Search for "FIX" to find all the places where you must make changes
in this file. *)
(* Your first task in this problem is to implement a function fv
that takes a lambda-calculus term and returns the set of variables
that appear free in that term.
We will represent variables using strings.
That means that the function fv must return a set of strings.
You do not have to implement sets (and operations on sets) yourself.
Instead we will use the set implementation in the standard library.
The standard library defines a Set module that we first "specialize"
to get sets of strings. That is the first line below. It's okay if
you don't quite undertand what this line is doing yet; see below. *)
module String_set = Set.Make (String)
(* Now we open the String_set module we've created. The module provides
us with a value "empty" that is the empty set of strings. It also
provides us with a number of operations that we can use to manipulate
sets of strings, such as adding an element (add), removing an element
(remove), set union (union), checking if a set is empty (is_empty),
checking if a given element is in a set (mem), and many more.
To see the full list of operations provided, start the ocaml
interactive system and type "#use "lambda.ml";;" and take a look at
the signature of our String_set module.
Recall that once we have opened a module, we can just say "empty"
when we want the empty set of strings, rather than typing out
"String_set.empty", and similarly for all the other operations
provided by String_set*)
open String_set
(* define var to be the string type *)
type var = string
(* define a type for "sets of variables" *)
type var_set = String_set.t
(* define terms of the lambda-calculus *)
type term =
| Var of var
| Lam of var * term
| App of term * term
(****************************************************************)
let id : term = Lam ("x",Var "x")
let selfapp : term = Lam ("x",App (Var "x",Var "x"))
let loop : term = App (selfapp,selfapp)
let eg1 : term = Lam ("x", Lam ("x", App (Var "x",Var "x")))
let eg2 : term = Lam ("x", Lam ("y", App (Var "x",Var "y")))
(****************************************************************)
(* Your first task is to define the function that computes the set of
free variables of a term. The function takes a term and returns
a set of variables.
Currently, the function is pretty useless; it always returns an
empty set of variables, no matter what the term. But notice that
this was sufficient to get the function fv to typecheck. *)
let fv (e:term) : var_set = empty (* FIX *)
(****************************************************************)
(* Next, define a function that prints a set of variables
(i.e., a set of strings)
You must change this function to properly print members of
the set s. The desired format is: {x, y, z}. *)
let print_varset (s:var_set) : unit = (* FIX *)
print_string "FOO\n"
(* make sure you test your implementation of fv; here is one simple
test case to start, though it won't work right until you get
print_varset working as it should *)
let _ = print_varset (fv (Lam ("x", App (Var "y", Var "z"))))
(****************************************************************)
(* a function for printing lambda-calculus terms *)
let print_term e =
let rec aux e =
match e with
Lam (x,e) -> "lam " ^ x ^ "." ^ (aux e)
| App (e1, e2) -> "(" ^ (aux e1) ^ ") (" ^ (aux e2) ^ ")"
| Var v -> v
in
print_string (aux e); print_string "\n"
(****************************************************************)
(* a useful function for creating fresh variable names x1, x2, ... *)
let count : int ref = ref 0
let freshvar () =
let c = !count in
(count := c + 1; "z"^(string_of_int c))
(****************************************************************)
(* Your next task is to implement capture-avoiding substitution.
In class, we wrote "e{e1/x}" for "subst e e1 x"
You will probably want to use the function freshvar (defined above)
to generate fresh variables names *)
let subst (e:term) (e1:term) (x:var) : term = id (* FIX *)
(* Write a function that determines whether a term e is a value.
"isval e" returns true if e is a value (i.e., a lambda-term \x.e)
and returns false otherwise *)
let isval (e:term) : bool = true (* FIX *)
(* Finally, implement the CBV big-step operational semantics for
lambda calculus. Note that "eval" stands for big-step.
Here "eval e" takes a closed term e (i.e., a term with no free
variables). If e is not closed, the function should raise the
exception TermNotClosed. Given a closed term e, "eval e" should
return a value (i.e., a lambda-term \x.e' ) if e terminates;
otherwise it should diverge. (Note that if it diverges, you
will have to enter Control C to interrupt the execution.) *)
(* Before you implement eval, make sure you write down the big-step
CBV operational semantics for the lambda calculus on paper. *)
(* Raise exception Term NotClosed if the argument is not a
closed expression *)
exception TermNotClosed
let eval (e:term) : term = id (* FIX *)
(****************************************************************)
(* if e evaluates to e' then "evalsto e" returns e'' where e''
is alpha-equivalent to e' *)
let evalsto (e:term) : unit =
(print_string "The term:\n\t\t";
print_term e;
print_string "Evaluates to:\n\t\t";
print_term (eval e))