丘奇数
2022/05/25
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)
这里有几件事需要注意：
- f 的类型是
a -> a（因为类型 a 的后继也是类型 a) - 丘奇数的类型是
(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 \times n = 0 + \underbrace{n + \dots + n}_{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 = \lambda f.\lambda x.f^nx\] \[n\ f = \lambda x.f^nx\]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 操作