Lambda 演算中布尔值的查询
这是 AND 运算符的 lambda 演算表示形式：
lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b
任何人都可以帮助我理解这种表示形式吗？
This is the lambda calculus representation for the AND operator:
lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b
Can anyone help me in understanding this representation?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
要理解如何在 lambda 演算中表示布尔值，考虑一下 IF 表达式“if a then b else c”会有所帮助。这是一个表达式，如果为真，则选择第一个分支 b，如果为假，则选择第二个分支 c。 Lambda 表达式可以非常轻松地做到这一点：
将为您提供第一个参数，并
为您提供第二个参数。因此，如果 a 是这些表达式之一，则
给出
b或c，这正是我们希望 IF 执行的操作。因此，define和
ab c的行为类似于if a then b else c。查看
(nab)的表达式，这意味着if n then a else b。那么
m (nab) b表示如果
m和n都为true，则此表达式的计算结果为，否则为ab。由于a是函数的第一个参数，而b是第二个参数，并且true已被定义为一个函数，该函数给出其第一个参数两个参数，那么如果m和n都为true，则整个表达式也是如此。否则为假。这就是and的定义！这一切都是由 Alonzo Church 发明的，他发明了 lambda 演算。
To understand how to represent Booleans in lambda calculus, it helps to think about an IF expression, "if a then b else c". This is an expression which chooses the first branch, b, if it is true, and the second, c, if it is false. Lambda expressions can do that very easily:
will give you the first of its arguments, and
gives you the second. So if a is one of those expressions, then
gives either
borc, which is just what we want the IF to do. So defineand
a b cwill behave likeif a then b else c.Looking inside your expression at
(n a b), that meansif n then a else b.Then
m (n a b) bmeansThis expression evaluates to
aif bothmandnaretrue, and tobotherwise. Sinceais the first argument of your function andbis the second, andtruehas been defined as a function that gives the first of its two arguments, then ifmandnare bothtrue, so is the whole expression. Otherwise it isfalse. And that's just the definition ofand!All this was invented by Alonzo Church, who invented the lambda calculus.
在 lambda 演算中，布尔值由一个带有两个参数的函数表示，一个表示成功，一个表示失败。这些参数被称为延续，因为它们继续进行其余的计算；布尔值 True 称为成功延续，布尔值 False 称为失败延续。这种编码称为 Church 编码，其思想是布尔值非常类似于“if-then-else 函数”。
所以我们可以说
其中
s代表成功，f代表失败，反斜杠是一个 ASCII lambda。现在我希望你能明白事情的发展方向。我们如何编码
和？好吧，在 C 中我们可以将其扩展为只有这些是函数，所以
但是，当在 lambda 演算中编码时，三元构造只是函数应用，所以我们有
所以最终我们到达
如果我们重命名成功和失败延续对于
a和b，我们返回到原始值与 lambda 演算中的其他计算一样，尤其是在使用 Church 编码时，使用代数计算通常更容易定律和方程推理，然后最后转换为 lambda。
In the lambda calculus, a Boolean is represented by a function that takes two arguments, one for success and one for failure. The arguments are called continuations, because they continue with the rest of the computation; the boolean True calls the success continuation and the Boolean False calls the failure continuation. This coding is called the Church encoding, and the idea is that a Boolean is very much like an "if-then-else function".
So we can say
where
sstands for success,fstands for failure, and the backslash is an ASCII lambda.Now I hope you can see where this is going. How do we code
and? Well, in C we could expand it toOnly these are functions, so
BUT, the ternary construct, when coded in the lambda calculus, is just function application, so we have
So finally we arrive at
And if we rename the success and failure continuations to
aandbwe return to your originalAs with other computations in lambda calculus, especially when using Church encodings, it is often easier to work things out with algebraic laws and equational reasoning, then convert to lambdas at the end.
实际上它不仅仅是 AND 运算符。这是 lambda 演算的
if m and n then a else b版本。解释如下：在 lambda 演算中，true 表示为接受两个参数* 并返回第一个参数的函数。 False 表示为接受两个参数*并返回第二个参数的函数。
上面显示的函数需要四个参数*。从表面上看，m 和 n 应该是布尔值，a 和 b 应该是其他值。如果 m 为真，它将计算其第一个参数，即
na b。如果 n 为真，则计算结果为 a；如果 n 为假，则计算结果为 b。如果 m 为 false，它将计算其第二个参数 b。所以基本上，如果 m 和 n 都为 true，则该函数返回 a，否则返回 b。
(*) 其中“采用两个参数”表示“采用一个参数并返回采用另一个参数的函数”。
编辑以回应您的评论：
and true false如维基页面上所示，工作原理如下：第一步是将每个标识符替换为其定义，即
(λm.λn.mnm ）（λa.λb.a）（λa.λb.b）。现在应用函数(λm.λn.mnm)。这意味着mn m中每次出现的 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表示假）。Actually it's a little more than just the AND operator. It's the lambda calculus' version of
if m and n then a else b. Here's the explanation:In lambda calculus true is represented as a function taking two arguments* and returning the first. False is represented as function taking two arguments* and returning the second.
The function you showed above takes four arguments*. From the looks of it m and n are supposed to be booleans and a and b some other values. If m is true, it will evaluate to its first argument which is
n a b. This in turn will evaluate to a if n is true and b if n is false. If m is false, it will evaluate to its second argument b.So basically the function returns a if both m and n are true and b otherwise.
(*) Where "taking two arguments" means "taking an argument and returning a function taking another argument".
Edit in response to your comment:
and true falseas seen on the wiki page works like this:The first step is simply to replace each identifier with its definition, i.e.
(λm.λn. m n m) (λa.λb. a) (λa.λb. b). Now the function(λm.λn. m n m)is applied. This means that every occurrence of m inm n mis replaced with the first argument ((λa.λb. a)) and every occurrence of n is replaced with the second argument ((λa.λb. b)). So we get(λa.λb. a) (λa.λb. b) (λa.λb. a). Now we simply apply the function(λa.λb. a). Since the body of this function is simply a, i.e. the first argument, this evaluates to(λa.λb. b), i.e.false(asλx.λy. ymeansfalse).