什么是“自由变量”？

Question

（我确定这个网站上已经有这个答案了，但是搜索被C中的一个变量调用free（）的概念所淹没。）我遇到了“eta还原”这个术语，如果x是“M中不空闲”，则定义为f x = M x ==> M。我的意思是，我认为我理解它要说的内容的要点，看起来就像你将一个函数转换为无点风格时所做的一样，但我不知道x是不是免费的限定词意味着什么。

Answer 1

下面是一个例子：

\f -> f x 

在这种拉姆达，x是自由变量。基本上一个自由变量是一个变量，用于不是lambda的参数（或变量let）之一的lambda中。它来自lambda的上下文之外。

埃塔减少意味着我们可以改变：

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

但是，只有当x不是免费的（即，它不使用或是一个参数）中g。否则，我们就可以创造它是指一个未知变量的表达式：

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

Answer 2

好，here's the relevant Wikipedia article，什么是值得。

简短的说法是，这样的定义使用像“M”这样的占位符消除了lambda表达式的主体，因此必须额外指定该lambda绑定的变量没有在占位符表示的任何地方使用。

所以，一个“自由变量”在这里是指大致在一些模糊的或未知的外范围内定义的变量 - e.g，在像\y -> x + y一个表达式，x是自由变量但y不是。

Eta减少是关于删除一个多余的绑定层，并立即应用一个变量，这是（如你可能想象的那样）只有在有问题的变量仅用于那个地方时才有效。