查询上布尔在演算

Question

这是AND运算的演算表示：

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

谁能帮助我理解这种表示？

Answer 1

要理解如何表示演算布尔值，它有助于考虑IF表达式，“如果一则b，否则c”。这是选择在第一分支，B，如果这是真的的表达，和第二，C，如果是假的。 Lambda表达式可以做到这一点很容易：

lambda(x).lambda(y).x

会给你第一它的参数，和

lambda(x).lambda(y).y

给你的第二个。因此，如果一个是这些表达式中的一个，然后

a b c

给任何b或c，这正是我们想要的如果要做。所以定义

 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已被定义为给人的第一它的两个参数，那么如果m和n都是true，所以是整个表达式的功能。否则，它是false。而这and的只是定义！

这一切都被邱奇，是谁发明了演算发明的。

Answer 2

在演算，布尔由采用两个参数，一个用于成功，一个用于失败的函数表示。这些参数被称为的延续的，因为他们继续计算剩余的部分。布尔真呼叫的成功延续和布尔值false调用失败延续。这种编码被称为教会编码，这种想法是，布尔是非常像的“if-then-else的功能。”

因此，我们可以说

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

其中s代表成功，f代表失败，反斜杠是一个ASCII拉姆达。

现在我希望你能看到这是怎么回事。我们如何代码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

BUT，三元构建体，在演算的编码时，仅仅是功能应用，所以我们有

(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表达式结尾。

Answer 3

其实这有点不仅仅是AND运算更多。这是if m and n then a else b的演算的版本。这里的解释是：

在演算真正被表示为函数取两个参数*和返回第一。假被表示为函数取两个参数*并返回第二

在以上表明该函数采用四个参数*。从外观上来看m和n应该是布尔值，a和b的一些其它值。如果m为真，将评估哪个是n a b第一个参数。这反过来将评估的，如果当n是假N是真和b。如果m为假，将评估到其第二自变量湾

因此，基本上该函数返回一个如果m和n都为真，和b否则。

（*）其中，“取两个参数”装置“服用参数，并返回一个函数服用另一种说法。”

编辑回应您的评论：

所看到的wiki页面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.λb. b)，即false（如λx.λy. y手段false）。