Ocaml, implement freevars letrec using sets

Question

I'm trying to implement letrec using mathematical lambda notation for the function, but I'm having difficulty. My assignment says that let can be defined as

p(e1) U (p(e2) - {x})

and that letrec can be defined as

(p(e1) - {f x}) U (p(e2) - {f}) 

I've successfully implemented let to find freevars in an expression, but I'm struggling with letrec implementation:

let rec fv (e:expr) : S.t = match e with
  | Id name -> S.singleton name
  | Value x -> S.empty 
  | Lambda(name, body) ->  S.remove name (fv body)
  | Let(name, def, body) -> S.union (fv def) (S.diff (fv body) (S.singleton name))   

  | App (e1, e2) | Add (e1, e2) | Sub (e1, e2) | Mul (e1, e2) | Div (e1, e2) | Lt (e1, e2) | Eq (e1, e2) | And (e1, e2) -> S.union (fv e1) (fv e2)

Can someone please walk me through how to do this? Do I have to use Lambda? I'm pretty lost at this point and implementations just trying to follow the definition must have been done incorrectly on my part because I can't quite get it working.

Answer 1

After reading your question many times, I realized you're trying to calculate the free variables of an expression like this:

let rec x = e1 in e2

The essence of let rec is that appearances of x in e1 are taken to refer to the value of x that is being defined. So x is not free in e1. And like the non-recursive let, x is not free in e2 either. It's bound to the value e1.

So I would have thought the implementation would look like this:

(p(e1) - {x}) U (p(e2) - {x})

The definition you give doesn't make sense (to me), especially since there's no obvious meaning for f.

One could imagine restricting this form to cases where x is a function. Maybe that's what the assignment is telling you.

If you give a few more details, maybe someone a little more versed in these things can help.

Answer 2

I agree with Jeffrey that there isn't quite enough information here. I'll give an implementation anyway, since the problem is fairly easy:

type term =
  | Var of string
  | App of term * term
  | Lam of string * term
  | Let of string * term * term
  | Letrec of (string * term) list * term

module S = Set.Make (String)

let rec free = function
  | Var name -> S.singleton name
  | App (f, x) -> S.union (free f) (free x)
  | Lam (arg, body) -> S.remove arg (free body)
  | Let (name, term, body) ->
    S.union (free term) (S.remove name (free body))
  | Letrec (rec_terms, body) ->
    S.diff
      (List.fold_left (fun set (_, term) ->
           S.union set (free term))
          (free body) rec_terms)
      (S.of_list (List.map fst rec_terms))

Note that this places no restriction on rec bound terms. If you will only be allowing functions there, then you can modify term to reflect that easily enough.