lambda 表达式的自由变量列表 [英] Free variables list of a lambda expression

问题描述

我正在为即将到来的 OCaml 测试做一些功课，但遇到了一些麻烦.

I was just doing some homework for my upcoming OCaml test and I got into some trouble whatnot.

考虑由以下抽象语法(其中 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"变量.你能就此让我放心吗?

I've checked a million times, and I'm sure that the result should include the "z" variable. Can you please reassure me on that?

推荐答案

在对 OP 的评论中，@PasqualCuoq 指出，λ 在 lambda 演算中与 λ 相关联OCaml 中的代码>乐趣.也就是说，术语 t in λx.t 被贪婪地评估(参见 http://en.wikipedia.org/wiki/Lambda_calculus#Notation).

In the comments to the OP it has been pointed out by the kind @PasqualCuoq that λ in lambda calculus associates the same as fun in OCaml. That is, the term t in λx.t is evaluated greedily (see http://en.wikipedia.org/wiki/Lambda_calculus#Notation).

这意味着(λz.yz)实际上是(λz.(yz))，上面的函数是正确的，但是提供的翻译对于示例表达式 (λx.(x (λz.yz))) x 不是，因为它应该是

What this is means is that (λz.y z) is actually (λz.(y z)), and that the function above is correct, but the translation provided for the sample expression (λx.(x (λz.y z))) x isn't, as it should've been

(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！

Here's to this awesome place called Stack Overflow!

这篇关于lambda 表达式的自由变量列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！