这是AND运算符的λ演算表示：
lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b
有人能帮我理解这个表示吗？
Lambda演算中布尔值的查询
12
- name_masked
3个回答
13
要理解如何在lambda演算中表示布尔值，可以考虑一个IF表达式，“如果a则为b否则为c”。这是一个表达式，如果为真，则选择第一个分支b，如果为假，则选择第二个分支c。Lambda表达式可以很容易地完成这个任务：
lambda(x).lambda(y).x
将返回其参数中的第一个参数。
lambda(x).lambda(y).y
给你第二个。所以如果a是这些表达式之一，那么
a b c
返回 b 或 c，这正是我们想要的 IF 函数的作用。因此定义：
true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y
并且 a b c 的行为类似于 如果 a 那么 b 否则 c。
在你的表达式中查看 (n a b)，那意味着 如果 n 那么 a 否则 b。
然后 m (n a b) b 意味着
if m then (if n then a else b) else b
如果m和n都为true，则该表达式将评估为a，否则为b。由于a是函数的第一个参数，b是第二个参数，而true被定义为一种给出其两个参数中的第一个参数的函数，因此如果m和n都为true，则整个表达式也为true。否则，它就是false。这就是and的定义！
所有这些都是由阿隆佐·邱奇发明的，他发明了lambda演算。
- Peter Westlake
6
8
在λ演算中，布尔值由一个接受两个参数的函数表示，一个用于成功，一个用于失败。这些参数被称为“continuations”，因为它们继续执行剩余的计算; 布尔值True调用成功continuation，而布尔值False调用失败continuation。这种编码被称为Church编码，其思想是布尔值非常类似于“if-then-else函数”。
因此，我们可以说：
所以，最终我们到达了
因此，我们可以说：
true = \s.\f.s
false = \s.\f.f
这里的s表示成功，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 编码时，与其他计算一样，通过代数定律和等式推理来解决问题通常更容易，然后在最后将其转换为 lambda 表达式。
- Norman Ramsey
4
实际上，这不仅仅是AND运算符。这是lambda演算中的版本，即
在lambda演算中，true表示为一个接受两个参数并返回第一个参数的函数。false表示为一个接受两个参数并返回第二个参数的函数。
您上面展示的函数接受四个参数。从外观上看，m和n应该是布尔值，a和b是其他值。如果m为true，则将计算其第一个参数，即
因此，基本上该函数在m和n都为true时返回a，在其他情况下返回b。
(*)其中，“接受两个参数”表示“接受一个参数并返回一个接受另一个参数的函数”。
针对您的评论进行编辑：
如维基百科页面所示，
第一步只需用其定义替换每个标识符，即
if m and n then a else b。以下是解释：在lambda演算中，true表示为一个接受两个参数并返回第一个参数的函数。false表示为一个接受两个参数并返回第二个参数的函数。
您上面展示的函数接受四个参数。从外观上看，m和n应该是布尔值，a和b是其他值。如果m为true，则将计算其第一个参数，即
n a b。这将根据n是true还是false而分别计算为a或b。如果m为false，则计算其第二个参数b。因此，基本上该函数在m和n都为true时返回a，在其他情况下返回b。
(*)其中，“接受两个参数”表示“接受一个参数并返回一个接受另一个参数的函数”。
针对您的评论进行编辑：
如维基百科页面所示，
and true false的工作原理如下：第一步只需用其定义替换每个标识符，即
(λm.λn. m n m) (λa.λb. a) (λa.λb. b)。现在应用函数(λm.λn. m n m)。这意味着在m n m中的每个出现都将替换为第一个参数（(λa.λb. a)），并且在n的每个出现都将替换为第二个参数（(λa.λb. b)）。因此，我们得到(λa.λb. a) (λa.λb. b) (λa.λb. a)。现在只需应用函数(λa.λb. a)。由于此函数的主体仅为a，即第一个参数，因此此计算为(λa.λb. b)，即false（因为λx.λy. y表示false）。- sepp2k
1
@sepp：如果可以的话，你能帮我处理一下我在下面给Peter发的第二条评论吗？ - name_masked
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接
(λm.λn. m n m) (λa.λb. a) (λa.λb. b)中，括号中的第一部分是一个函数，第二部分和第三部分被替换为m和n：(λa.λb. a) (λa.λb. b) (λa.λb. a)。然后再次执行相同的操作，记住每个括号中的a和b是完全独立的。第一部分(λa.λb. a)返回其两个参数中的第一个。因此，它返回(λa.λb. b)，这是false的Church表示形式。 - Peter Westlake