church 布尔值

Question

本帖介绍 church 布尔值。

church 布尔值可以在 lambda 表达式中起条件分支的作用。比如 bfg，希望在 b 为真时得到 f，反之得到 g.

即：(true f) g=f, (flase f) g =g

于是有 (true f) = λy . f,   (flase f)=λy . y

不难看出，我们可以给出以下定义：

• true: λxy . x
• flase: λxy . y

接下来看布尔运算，先分析 &.

true true ? = true
true flase ? = flase
flase true ? = ?

可见 & 可以定义为 λxy . x y x，类似可以得到 | 的定义

• &: λxy . xyx
• |: λxy . xxy

取反：λx . x flase true 或者 λx . λab . x b a

有了 bool 值后，我们可以判断一个 church 数 n 是否为 0. 只要通过 n 把一个输出值为 flase 的函数 n 次作用在 true 上，如果 n 是 0，将得到 true，反之得到  flase.

0?: λn . n (λx . flase) true

[预告]： 下次将在 bool 值的基础上构造减法。

[ 本帖最后由 win_hate 于 2008-10-26 10:27 编辑 ]

Answer 1

是不是再多给点背景资料？

另外，我觉着 Wikipedia 上这篇文章不错： http://en.wikipedia.org/wiki/Church_encoding

[ 本帖最后由 MMMIX 于 2008-10-26 13:54 编辑 ]