什么是"自由变量"？

Question

(我确信这个必须已经在这个网站上得到了解答,但搜索被C语言中的变量调用free()的概念所淹没.)

我遇到了"eta reduction"这个术语,它被定义为f x = M x ==> M如果x"不是M中的自由".我的意思是,我认为我理解它试图说的内容的主旨,看起来就像你将一个函数转换为无点样式时所做的那样,但我不知道关于x的限定符不是自由的意思.

Answer 1

这是一个例子:

\f -> f x

在这个lambda中,x是一个自由变量.基本上,自由变量是lambda中使用的变量,它不是lambda参数(或let变量)之一.它来自lambda的上下文之外.

减少意味着我们可以改变:

(\x -> g x) to (g)

但是,只有x不是免费的(即它没有被使用或是一个参数)g.否则我们将创建一个引用未知变量的表达式:

(\x -> (x+) x) to (x+) ???

轻微的挑剔:如果它被绑定,可以使用"x".Eta-减少`(\ x - >(\ x - > x + x)x)`到`(\ x - > x + x)`完全没问题,即使`(\ x - > x + x)`包含`x`的两种用法.这是一个极端的案例,在处理人工编写的代码时不会显得太多,但我想编译器会经常遇到这种情况. (2认同)

Answer 2

简短的版本是这样的定义使用像"M"这样的占位符来消除lambda表达式的主体,因此必须另外指定由lambda绑定的变量不用于占位符表示的任何内容.

因此,这里的"自由变量"大致意味着在一些模糊或未知的外部范围中定义的变量 - 例如,在表达式中\y -> x + y,x是一个自由变量但y不是.

Eta减少是关于删除多余的绑定层并立即应用变量,这是(正如您可能想象的)只有在相关变量仅用于该位置时才有效.