A simple implement of the Church Numbers

A simple implement of the Church Numbers

前几天做了一下 Codewars 上面的一点水题熟悉一下 fp, 然后碰到了与 邱奇数(Church Number) 相关的一系列题目。

感觉挺有意思,对我这种新手也有一定的思考难度。

维基上面有相关的资料 ,但我看起来还是感觉挺吃力,中文版也仅仅翻译了其中一小部分。

这里就写一点我自己的理解

The definition of Church Number

邱奇数给了我们一种新的形式去理解自然数。(这里我们不使用原始的 lambda 表达式,这里我们把多个参数写在一起)

在邱奇计数 (Church Numerals) 中我们令 $0$ 表示为 $\lambda f x . x$ , 用函数来描述的话是 $\text{zero}\space f \space x = x$。

这个 zero 接收一个函数和一个参数,函数 $f$ 的输入输出的类型都与参数 $x$ 相同。

有了 $0$ 自然要有后继 (successor) ,这里我们对后继的定义为 $\lambda n. \lambda fx.f(n \space f\space x)$ , 用函数来描述的话是 $\text{succ}\space n \space f \space x = f(n\space f \space x ) $.

例如我们可以定义 1 = succ 0 :
$$
\begin{align}
0 &= \lambda fx. x \
\text{succ} \space n \space f \space x &= \lambda nfx.f(n \space f \space x) \
1 = \text{succ} \space 0 &=\lambda fx. f(0\space f \space x) \
&= \lambda fx.f\space x \
&= f \space x
\end{align}
$$
所以邱奇数 1 所干的事就是把给自己的函数和参数调用一次并返回结果

同理我们有 2 = succ 1 :
$$
\begin{align}
1 &= \lambda f x. f\space x \
2 = \text{succ} \space 1 &= \lambda fx.f (1\space f \space x) \
&= \lambda f x.f (f\space x) \
&= f f \space x
\end{align}
$$
所以对应于自然数 $n$ 的邱奇数所做的事就是对参数调用 $n$ 次传给自己的函数。

基于这一点,我们可以轻松地写出邱奇数到自然数的转换——只需要让 $x = 0 ,f = \lambda x.x + 1$ 就行了。

而自然数到邱奇数的转换则更加显然,只需要递归调用 $\text{succ}$ 直到需要转换的自然数为 $0$ 就可以了。

有了零和后继,我们就能得到所有的邱奇数,正如我们是如何得到自然数一样。

下面我们来定义邱奇数的一些运算:

首先是加法,我们需要知道邱奇数的加法该如何定义才能保持原本的性质不变。

邱奇数 $n$ 对 $x$ 调用了 $n$ 次 $f$ ,邱奇数 $m$ 对 $x$ 调用了 $m$ 次 $f$ ,那么 $\text{plus}\space n\space m$ 应该对 $x$ 调用了 $n+m$ 次 $f$.

所以我们给出如下定义
$$
\begin{align}
\text{plus } n \space m &= \lambda fx.f(n\space f \space (m \space f \space x)) \
\end{align}
$$
可以看出,我们相当于先把 $x$ 代换为 $m\space f \space x$ 再使用 $n$ 进行求值,所以 $f$ 一共迭代了 $n + m$ 次。

然后是乘法与幂运算,这两个的定义与加法类似
$$
\begin{align}
\text{mul} \space n\space m &= \lambda fx. m \space (n \space f) x \
n ^m &= \lambda fx.(m \space n) f \space x
\end{align}
$$
乘法相当于用 $(n\space f)$ 替代 $f$ ,而幂则是把$n, m$复合起来再对 $f, x$ 进行调用。

减法需要我们先定义前驱。

前驱相对复杂得多,但理解原理之后结论就很显然了。

我们定义邱奇数的前驱 (predecessor) 满足
$$
\text{pred} \space 0 = 0 \
\text{succ pred } n = n
$$
如果 $n$ 是对 $x$ 调用 $n$ 次 $f$ ,那么它的前驱 $\text{pred }n$ 应该是对 $x$ 调用 $n -1$ 次 $f$ .

维基上面给出了两种思路,但原理是类似的。

考虑到我们无法求出 $f$ 的反函数 (如果能的话就方便了) ,这减少的一次 $f$ 的调用我们必须得用其它的方式来抵消。

我们可以构造一个容器来保存我们的数据 $x$ , 并使用一些技巧来抵消这 $n$ 次调用中的一次,这样就能得到 $n$ 的前驱。

考虑到 $\text{pred }0 = 0$ ,我们可以把这个需要抵消的一次调用挪到第 $1$ 层,这样对所有情况就都能适用了。

维基上给出的两种包装方案分别是用 Pair 和函数来保存。

使用函数来包装的话,我们可以用下面的表达式来计算 $\text{pred }n$ ,(为了方便我添加了一些括号)
$$
\begin{align}
\text{pred } &n = \lambda fx. (n \space(\lambda gh.h(g\space f)) (\lambda u.x)) (\lambda x.x)
\end{align}
$$
这个式子或许有一点复杂,我们一点点地拆开来看。

首先看当 $n=0$ 时,原式子相当于
$$
\begin{align}
\text{pred } 0 &=\lambda fx.(0\space (\lambda gh.h(g\space f)) (\lambda u.x))(\lambda x .x) \
&=\lambda fx.(\lambda u.x) (\lambda x.x) \
&=\lambda fx. (x) \
&= x =0
\end{align}
$$
当 $n = 1$ 时 :
$$
\begin{align}
\text{pred }1 &= \lambda fx.(1 \space (\lambda gh.h(g\space f)) (\lambda u.x))(\lambda x .x) \
&= \lambda fx.(\lambda gh.h(g\space f) (\lambda u.x))(\lambda x.x) \
&= \lambda fx.(\lambda h. h((\lambda u .x) \space f ) )(\lambda x.x) \
&= \lambda fx.(\lambda h. h \space x) (\lambda x. x) \
&= \lambda fx. x \
&= x = 0
\end{align}
$$
再举一个例子,当 $n=2$ 时:
$$
\begin{align}
\text{pred }2 &= \lambda fx.(2 \space (\lambda gh.h(g\space f)) (\lambda u.x))(\lambda x .x) \
&= \lambda fx.((\lambda gh.h(g\space f))(\lambda gh.h(g\space f)) (\lambda u.x))(\lambda x.x) \
&= \lambda fx.((\lambda gh.h(g\space f))(\lambda h. h((\lambda u .x) \space f ))(\lambda x.x) \
&= \lambda fx.((\lambda gh.h(g\space f))\lambda h. h \space x) (\lambda x. x) \
&= \lambda fx.(\lambda h.h((\lambda h.h\space x) f) )(\lambda x.x) \
&= \lambda fx.(\lambda h.h (f\space x)) (\lambda x.x) \
&= \lambda fx.(f\space x) \
&= f \space x = 1
\end{align}
$$
这个式子里面最核心的部分就是 $n \space (\lambda gh.h(g\space f)) (\lambda u.x)$ ,这也是打包操作的核心所在。

我们可以发现
$$
\begin{align}
\text{samesum } n &= \lambda fx. (n \space(\lambda gh.h(g\space f)) (\lambda u.u\space x)) (\lambda x.x) \
&= \lambda fx.(n\space (\lambda h.h\space x))(\lambda x.x) \
&= \lambda fx. (n \space f\space x) = n
\end{align}
$$
所以这种表示方法是与原定义等价的,那么我们可以观察 $\text{samenum}$ 和 $\text{pred} $ 的区别。

注意到我们把 $\lambda u. u\space x$ 换成了 $\lambda u . x$ , 这也就是少的那一次调用所在。

我们把 $x$ 封装在一个函数里,每次调用的是对封装的函数进行处理的函数,也就是 $\lambda gh. h(g\space f)$ ,每次调用相当于把一个 $f$ 压入我们封装好的函数里,如此重复 $n$ 次。

最后我们需要的不是一个函数而是一个值,所以我们需要把封装在函数中的值取出来,所以我们要用到 $\text{id} = \lambda x. x$ 函数来得到最后的结果。

同样我们也可以用 $\text{pair}$ 来封装数据,原理基本类似,都是在第一次调用时避开。

有了后继我们就能定义减法:
$$
n - m = (n \text{ pred}) \space m
$$

下面是用函数式语言的实现

Implement of Church Number in Javascript

为什么是 Js 呢, 因为做的第一道题是 Js 的。

等会再贴 Haskell 的代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
function zero(f, x) {
return x;
}

function succ(church) {
return (f, x) => f(church(f, x));
}

const one = succ(zero);
const two = succ(one);
const three = succ(two);

function churchToInt(church) {
return church(x => x + 1, 0);
}

function intToChurch(int) {
return int === 0 ? zero
: succ(intToChurch(int - 1));
}

function add(church1, church2) {
return (f, x) => church1(f, church2(f, x));
}

function mul(church1, church2) {
return (f, x) => church1((x2) => church2(f, x2), x);
}

function pow(church1, church2) {
return (f, x) => church2(x2 => mul(church1, x2), one)(f, x)
}

function pre(church) {
return (f, x) => church(g => h => h(g(f)), y => x)(xs => xs);
}

function sub(church1, church2) {
return (f, x) => church2(pre, church1)(f, x);
}

function print(church) {
console.log(churchToInt(church));
}

const eight = pow(two, three);

print(eight); // 8
print(add(two, three)); // 5
print(add(zero, one)); // 1
print(sub(eight, two)); // 6
print(pre(eight)); // 7
print(mul(eight, two)); // 16
print(pow(eight, two)); // 64

Implement of Church Number in Haskell

这个实际上就是 Codewars 里面的代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
module Haskell.Codewars.Church where

import Prelude hiding (succ, pred, fst, snd)

newtype Pair a b = Pr (forall c . (a -> b -> c) -> c)

instance (Show a, Show b) => Show (Pair a b) where
show (Pr p) = p (\ a b -> "(" ++ show a ++ "," ++ show b ++ ")")

pair :: a -> b -> Pair a b
pair f s = Pr (\ b -> b f s)

fst :: Pair a b -> a
fst (Pr p) = p const

snd :: Pair a b -> b
snd (Pr p) = p (\ _ b -> b)

newtype Number = Nr (forall a. (a -> a) -> a -> a)

instance Show Number where
show (Nr a) = a ("1+" ++) "0"

instance Eq Number where
a == b = eval a == eval b

fold :: Number -> (a -> a) -> a -> a
fold (Nr n) = n

eval :: Number -> Integer
eval (Nr a) = a (+1) 0

zero :: Number
zero = Nr (\ _ z -> z)

one = succ zero

succ :: Number -> Number
succ (Nr a) = Nr (\ s z -> s (a s z))

add :: Number -> Number -> Number
add (Nr a) = a succ

mult :: Number -> Number -> Number
mult (Nr a) b = a (add b) zero

pow :: Number -> Number -> Number
pow x (Nr n) = n (mult x) one

pred :: Number -> Number
pred (Nr n) = Nr(\ f x -> (n (\ g h -> h (g f)) (const x) id))

subt :: Number -> Number -> Number
subt a (Nr b) = b pred a

代码还是挺短的。。

Implement of Church Number in C++

然后又手贱,写了个 C++ 版本的

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
#include <iostream>
using namespace std;

auto zero = [](auto f)
{
return [=](auto x)
{
return x;
};
};

auto succ = [](auto church)
{
return [=](auto f)
{
return [=](auto x)
{
return f(church(f)(x));
};
};
};

auto add = [](auto church1)
{
return [=](auto church2)
{
return [=](auto f)
{
return [=](auto x)
{
return church1(f)(church2(f)(x));
};
};
};
};

auto mul = [](auto church1)
{
return [=](auto church2)
{
return [=](auto f)
{
return [=](auto x)
{
return church1([=](auto x2)
{
return church2(f)(x2);
})(x);
};
};
};
};

auto powc = [](auto church1)
{
return [=](auto church2)
{
return [=](auto f)
{
return [=](auto x)
{
return (church2([=](auto x2)
{
return mul(church1)(x2);
})(succ(zero)))(f)(x);
};
};
};
};

auto pred = [](auto church)
{
return [=](auto f)
{
return [=](auto x)
{
return (church([=](auto g)
{
return [=](auto h)
{
return h(g(f));
};
})([=](auto y)
{
return x;
}))([=](auto xs)
{
return xs;
});
};
};
};

auto sub = [](auto church1)
{
return [=](auto church2)
{
return [=](auto f)
{
return [=](auto x)
{
return (church2(pred)(church1))(f)(x);
};
};
};
};

auto one = succ(zero);

int main(int argc, char* argv[])
{
auto temp = [](int x) { return x + 1; };

auto two = add(one)(one);
auto three = add(two)(one);

auto six = mul(two)(three);
auto c64 = powc(two)(six);
auto c63 = pred(c64);
auto c60 = sub(c63)(three);

cout << zero(temp)(0) << endl; // 0
cout << one(temp)(0) << endl; // 1
cout << two(temp)(0) << endl; // 2
cout << six(temp)(0) << endl; // 6
cout << c64(temp)(0) << endl; // 64
cout << c63(temp)(0) << endl; // 63
cout << c60(temp)(0) << endl; // 60




int x;
cin >> x;

return 0;
}