lambda表达式的自由变量列表

Question

我刚刚为即将到来的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"变量.你能安慰我吗？

Answer 1

在对 OP 的评论中，@PasqualCuoq 指出，\xce\xbb在 lambda 演算中与 OCaml 中的关联相同fun。也就是说，该术语t in \xce\xbbx.t被贪婪地求值（参见http://en.wikipedia.org/wiki/Lambda_calculus#Notation）。

\n\n

这意味着(\xce\xbbz.y z)实际上是(\xce\xbbz.(y z))，并且上面的函数是正确的，但是为示例表达式提供的翻译(\xce\xbbx.(x (\xce\xbbz.y z))) x不是，因为它应该是

\n\n

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

\n\n

代替

\n\n

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

\n\n

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

\n