玩一玩丘奇数

• church 数的定义
• 后继
• 加法
• 乘法
• 乘方/前继/减法

church 数的定义

zero = λf.λx.x

one = λf.λx.f x

two = λf.λx.f (f x)

怎么理解丘奇数$C_n$呢？
首先理解什么是自然数：首先 0 是自然数，每个自然数都有一个后继，后继也是自然数。
这里其实是一个有「零」和「一元运算」的集合，且这个运算对该集合封闭。

这里我们把参数 f 看成是这个一元(后继)运算，参数 x 看成是这个集合的「零」：

• λf.λx.x 表示，如果你告诉我后继函数是 f，零元是 x，那么我就知道 zero 是 x
• λf.λx.f x 表示，如果你告诉我后继函数是 f，零元是 x，那么我就知道 one 是 f x
• λf.λx.f (f x) 表示，如果你告诉我后继函数是 f，零元是 x，那么我就知道 two 是 f (f x)

以此类推。

用 Haskell 写出来，让 church 变得清晰一些

zero :: (a -> a) -> a -> a
zero = \f -> \x -> x

one :: (a -> a) -> a -> a
one = \f -> \x -> f x

two :: (a -> a) -> a -> a
two = \f -> \x -> f (f x)

这里有几件事需要注意：

1. f 的类型是 a -> a（因为类型 a 的后继也是类型 a)
2. 丘奇数的类型是 (a -> a) -> a -> a

后继

如果我们定义后继运算为 (+1),零元为0, 那么:

• zero (+1) 0 的值为 0
• one (+1) 0 的值为 1
• two (+1) 0 的值为 2

为了方便后面的描述，我们把确定了后继运算和零元的自然数称为「特化的自然数」，没有确定后继运算和零元的上述定义的自然数叫「丘奇数」。

我们可以使用给定的后继运算对特化的自然数做后继运算，但是能否直接对丘奇数进行后继运算呢？

即我们需要实现一个 succ 函数：

• succ (λf.λx.x) == λf.λx.f x
• succ (λf.λx.f x) == λf.λx.f (f x)

succ 可以给定一个丘奇数，能够返回这个丘奇数的后继丘奇数。

考虑到丘奇数的类型是 (a -> a) -> a -> a，用 haskell 来描述 succ 的类型签名就应该是:

succ :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a)

去掉第二个丘奇数类型的括号，就得到

succ :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a

现在尝试实现它

succ :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
succ n = \f -> \x -> undefined

回到丘奇数的定义，丘奇数是一个函数，如果你给我一个后继运算，给我一个零元，我就能给出任何特化的自然数。

也就是说 undefind 这里我们需要一个特化的自然数，但最好不要随便给，因为我们希望丘奇数与特化的自然数是同构的，如果我们能给出丘奇数 n 的特化的自然数的后继，就可以让丘奇数和特化的自然数比较自然的一一对应起来。

所以先通过 n f x，可以把丘奇数 n 变为一个特化的自然数，然后求出其后继 f (n f x)，于是

succ :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
succ n = \f -> \x -> f (n f x)

这时候我们可以使用 zero 和 succ 来搞出特化的自然数：

• zero (+1) 0 => 0
• (succ zero) (+1) 0 => 1
• (succ (succ zero)) (+1) 0 => 2

加法

plus :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a
plus = \m -> \n -> \f -> \x -> undefind

可以先用 m f x 和 n f x 搞出两个特化的自然数 i 和 j，这个时候要在 i 的基础上对 i 应用 j 次 f，但这里的 j 不是整数，但是如果把 j 作为 n 的零元，这样定义出的 i 就有了 i + j 的效果

plus :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a
plus = \m -> \n -> \f -> \x -> m f (n f x)

乘法

mul :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a
mul = \m -> \n -> \f -> \x -> undefined

定义加法的时候，我们在零元上动了手脚，乘法我们对后继函数动手脚，下面介绍操作思路。

首先对 m * n 作如下等价变形：

所以 m * n 是对 0 作 m 次 (+n) 运算。

然后我们再次观察丘奇数的类型定义:

(a -> a) -> a -> a

把后面的 a -> a 用括号括起来

(a -> a) -> (a -> a)

丘奇数 $C_n$ 其实可以看做这样的一个函数：输入一个后继函数 f，得到一个 $Z$ -> $C_n$ 的函数(Z 为特化的零元)

任何一个丘奇数 $C_n$，在应用一个后继函数 f 后，都得到一个把零元应用n次f的函数

n f 就是我们要的每次 (+n) 的后继函数，于是我们可以写出乘法了

mul :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a
mul = \m -> \n -> \f -> \x -> m (n f) x

m (n f) x 的意思是，对零元 x 进行 m 次 n f 操作

乘方/前继/减法

暂时还不知道如何 reasonable 的得到