0

我正在尝试使用函数的数学 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 吗？在这一点上我很迷茫，只是试图遵循定义的实现对我来说一定是错误的，因为我不能让它工作。

4

2 回答 2

1

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

let rec x = e1 in e2

的本质let rec是，xin的出现被认为是指正在定义e1的值。x所以x不是免费的e1。和 non-recursive 一样let，x也不是免费的e2。它绑定到 value e1。

所以我会认为实现看起来像这样：

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

您给出的定义（对我来说）没有意义，特别是因为f.

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

如果您提供更多细节，也许更精通这些事情的人会有所帮助。

于 2017-03-25T02:16:41.117 回答
0

我同意 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以足够容易地反映这一点。

于 2017-03-25T04:45:40.480 回答