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 已经指出，λ在 lambda 演算中与 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"))

这里是这个很棒的地方，叫做 Stack Overflow！

于 2012-12-09T01:03:44.087 回答