Ocaml，使用集合实现freevars letrec

Question

我正在尝试使用函数的数学lambda表示法来实现letrec，但我遇到了困难。我的赋值说明let可以定义为

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

而letrec可以定义为

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

我已经成功地实现了let来查找表达式中的freevars，但我正在为letrec实现而苦苦挣扎：

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)

有没有人能教我怎么做？我必须使用Lambda吗？在这一点上，我相当迷茫，只是试图遵循定义的实现一定是我做得不正确，因为我不能完全让它工作。

Answer 1

在多次阅读您的问题后，我意识到您正在尝试计算表达式的自由变量，如下所示：

let rec x = e1 in e2

let rec的本质是将e1中的x的外观视为引用正在定义的x的值。所以在e1中x不是免费的。与非递归let一样，x在e2中也不是免费的。它绑定到值e1。

所以我认为实现应该是这样的：

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

您给出的定义(对我来说)没有任何意义，特别是因为f没有明显的含义。

可以想象将这种形式限制在x是函数的情况下。也许这就是作业告诉你的。

如果你给出更多的细节，也许更精通这些东西的人可以提供帮助。

Answer 2

我同意Jeffrey的观点，这里没有足够的信息。无论如何，我都会给出一个实现，因为这个问题相当简单：

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))

请注意，这对rec约束术语没有限制。如果你只允许那里的函数，那么你可以修改term来很容易地反映这一点。