查询Lambda微积分中的布尔值

Question

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

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

谁能帮助我理解这种表现形式？

Answer 1

为了理解如何在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会表现得像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

这个表达式a如果两个m和n是true,和b其他.因为a是你的函数的第一个参数,并且b是第二个,并且true被定义为一个函数,它给出了它的两个参数中的第一个,那么if m和nboth都是true,整个表达式也是如此.否则就是false.这只是定义and!

所有这些都是由Alonzo Church发明的,他发明了lambda演算.

Answer 2

在lambda演算中,布尔值由一个函数表示,该函数接受两个参数,一个用于成功,一个用于失败.这些参数称为continuation,因为它们继续进行其余的计算; 布尔值True调用成功延续,布尔值False调用失败延续.这种编码称为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编码时,通常使用代数定律和等式推理更容易处理,然后在最后转换为lambdas.