Ocaml、セットを使用してフリーレックletrecを実装する

Question

私は関数のための数学ラムダ記法を使用してletrecを実装しようとしているが、私は困難を抱えている。私の割り当ては、私が成功した表現でfreevarsを見つけるために聞かせて、私はletrecに苦しんだ実装しましたLETが

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

として定義することができ、そのletrecが

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

として定義することができることを言います実装：

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) 

誰かがこれを行う方法を私に歩いてもらえますか？私はラムダを使用する必要がありますか？私はこの時点でかなり失われています。定義に従っている実装は、私がそれを正しく動作させることができないため、私のところで間違って行われているに違いありません。

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

私はここで十分な情報がないとジェフリーに同意します。

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を修正することができます。