functional-programming - 在 Lambda 演算中查询布尔值

Question

这是 AND 运算符的 lambda 演算表示：

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

任何人都可以帮助我理解这种表示吗？

Answer 1

要了解如何在 lambda 演算中表示布尔值，考虑一个 IF 表达式“if a then b else c”会有所帮助。这是一个表达式，如果为真则选择第一个分支 b，如果为假则选择第二个分支 c。Lambda 表达式可以很容易地做到这一点：

lambda(x).lambda(y).x

会给你它的第一个论点，并且

lambda(x).lambda(y).y

给你第二个。因此，如果 a 是这些表达式之一，那么

a b c

给出bor c，这正是我们希望 IF 做的事情。所以定义

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

并且a b c会表现得像if a then b else c.

看着你的表情里面(n a b)，那意味着if n then a else b。那么m (n a b) b意味着

if m then (if n then a else b) else b

此表达式的计算结果为aif bothm和nare true，b否则为 else 。因为ais 是你的函数的第一个参数并且b是第二个参数，并且true被定义为一个函数，它给出了它的两个参数中的第一个，那么 ifm和nare both true，整个表达式也是如此。否则就是false。这只是and!

这一切都是由发明 lambda 演算的 Alonzo Church 发明的。

Answer 2

在 lambda 演算中，布尔值由一个接受两个参数的函数表示，一个代表成功，一个代表失败。参数称为continuations，因为它们继续进行其余的计算；布尔 True 调用成功延续，布尔 False 调用失败延续。这种编码称为 Church 编码，其思想是布尔值非常类似于“if-then-else 函数”。

所以我们可以说

true  = \s.\f.s
false = \s.\f.f

wheres代表成功，f代表失败，反斜杠是一个 ASCII lambda。

现在我希望你能看到这是怎么回事。我们如何编码and？好吧，在 C 语言中，我们可以将其扩展为

n && m = n ? m : false

只有这些是函数，所以

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f

但是，当在 lambda 演算中编码时，三元结构只是函数应用程序，所以我们有

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f

所以最后我们到达

&& = \n . \m . \s . \f . n (m s f) f

如果我们将成功和失败的延续重命名为a，b我们将返回您原来的

&& = \n . \m . \a . \b . n (m a b) b

与 lambda 演算中的其他计算一样，尤其是在使用 Church 编码时，通常更容易使用代数定律和等式推理来解决问题，然后在最后转换为 lambdas。

Answer 3

实际上，它不仅仅是 AND 运算符。这是 lambda 演算的版本if m and n then a else b。这是解释：

在 lambda 演算中，true 表示为一个接受两个参数*并返回第一个参数的函数。False 表示为接受两个参数*并返回第二个参数的函数。

您在上面显示的函数需要四个参数*。从外观上看，m 和 n 应该是布尔值，而 a 和 b 应该是其他一些值。如果 m 为真，它将评估其第一个参数，即n a b。如果 n 为真，这反过来将评估为 a，如果 n 为假，则评估为 b。如果 m 为假，它将评估其第二个参数 b。

所以基本上函数返回 a 如果 m 和 n 都为真，否则返回 b 。

(*) “采用两个参数”意味着“采用一个参数并返回一个采用另一个参数的函数”。

编辑以回应您的评论：

and true false如维基页面上所见，工作方式如下：

第一步是简单地将每个标识符替换为其定义，即(λm.λn. m n m) (λa.λb. a) (λa.λb. b). 现在该功能(λm.λn. m n m)已应用。这意味着每次出现的 m inm n m都被第一个参数 ( (λa.λb. a)) 替换，每次出现的 n 都被第二个参数 ( (λa.λb. b)) 替换。所以我们得到(λa.λb. a) (λa.λb. b) (λa.λb. a). 现在我们简单地应用函数(λa.λb. a)。由于此函数的主体只是 a，即第一个参数，因此 this 的计算结果为(λa.λb. b), ie false（λx.λy. y表示false）。