6

私は次のOCamlテストのために宿題をしていましたが、何の問題もありませんでした。

次の抽象構文（xは変数）で定義されたλ項の言語を考えてみましょう。 

t ::= x | t t | λx. t

λ項を表す型項を記述します。変数が文字列として表されていると仮定します。

わかりました、男の子。

# type t = Var of string | App of (t*t) | Abs of string*t;;
type t = Var of string | App of (t * t) | Abs of (string * t)

項tの自由変数fv（t）は、帰納的に次のように定義されます。 

fv(x) = {x}  
fv(t t') = fv(t) ∪ fv(t')  
fv(λx. t) = fv(t) \ {x}

確実なこと。

# let rec fv term = match term with
Var x -> [x]
  | App (t, t') -> (List.filter (fun y -> not (List.mem y (fv t'))) (fv t)) @ (fv t')
  | Abs (s, t') -> List.filter (fun y -> y<>s) (fv t');;
      val fv : t -> string list = <fun>

例えば、 

fv((λx.(x (λz.y z))) x) = {x,y}.

それを確認しましょう。

# fv (App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"));;
- : string list = ["y"; "z"; "x"]

私は何百万回もチェックしましたが、結果には「z」変数が含まれているはずです。それについて私を安心させていただけませんか？

4

1 に答える 1

4

OPへのコメントでは、@ PasqualCuoqの種類によって、ラムダ計算ではOCamlλと同じように関連付けられていることが指摘されています。funつまり、用語t in λx.tは貪欲に評価されます（http://en.wikipedia.org/wiki/Lambda_calculus#Notationを参照）。

これが意味するのは、(λz.y z)実際に(λz.(y z))はであり、上記の関数は正しいが、サンプル式に提供された変換は、本来(λx.(x (λz.y z))) xあるべきものではないということです。

(App(Abs("x", App(Var "x", Abs("z", App(Var "y", Var "z")))), Var "x"))

代わりに

(App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"))

これがStackOverflowと呼ばれるこの素晴らしい場所です！

于 2012-12-09T01:03:44.087 に答える