YSMull
<-- home

丘奇数

church 数的定义

zero = λf.λx.x

one = λf.λx.f x

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

怎么理解用 church encoding 定义的自然数呢?
首先理解什么是自然数:首先 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 xn 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)

丘奇数n 其实可以看做这样的一个函数:输入一个后继函数 f,得到一个 零元 -> 丘奇数n 的函数

也就是说,任何一个丘奇数n,在应用一个后继函数 f 后,都得到一个把零元应用n次f的函数

\[n = \lambda f.\lambda x.\underbrace{f( \dots (f}_{n个f} x)\dots)\] \[n\ f = \lambda x.\underbrace{f( \dots (f}_{n个f} x)\dots)\]

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 进行 mn f 操作