チャーチ数でビット単位 XOR してみよう

どうも, ビット演算が好きなたぬきです。

最近は関数のみでデータと操作の両方を表現するラムダ計算についてにわかにハマっています。 というわけでチャーチ数に対するビット単位 XOR をラムダ計算で定義してみましょう。 四則演算といえば add, sub, mul, div, xor ですよね!

チャーチ数とは, ラムダ計算における標準的な自然数の定義です。

ラムダ計算の世界では, すべてが関数とその適用によって表現されます。 **真理値も数もリストもすべてが関数**という狂気の世界です。

初めてこんなことを聞くとそんな世迷い言を本当に実現できるのか信じられない方も多いでしょう。 実際に試してみましょう。

ラムダ計算の実行環境としてはより専門的なものもあるとは思いますが, 今回は Python を使用します。

## ラムダ式の記法

ラムダ計算では無名関数を扱います。 これまで数学で関数を扱う際はだいたい $f$ などの仮の名前を使って

```math
\def\coloneqq{\mathrel{\mathop:}\mathrel{\mkern-1.2mu}=}

\def\id{\mathop{\text{id}}}
\def\true{\mathop{\text{true}}}
\def\false{\mathop{\text{false}}}
\def\disj{\mathop{\text{disj}}}
\def\conj{\mathop{\text{conj}}}
\def\inv{\mathop{\text{inv}}}
\def\succc{\mathop{\text{succ}}}
\def\add{\mathop{\text{add}}}
\def\mul{\mathop{\text{mul}}}
\def\replace{\mathop{\text{replace}}}
\def\pred{\mathop{\text{pred}}}
\def\subb{\mathop{\text{sub}}}
\def\iszero{\mathop{\text{iszero}}}
\def\gee{\mathop{\text{ge}}}
\def\divv{\mathop{\text{div}}}
\def\fix{\mathop{\text{fix}}}
\def\twice{\mathop{\text{twice}}}
\def\half{\mathop{\text{half}}}
\def\parity{\mathop{\text{parity}}}
\def\xorr{\mathop{\text{xor}}}

\def\xor{\mathbin{\small \triangle}}
\def\paren#1{{\left({#1}\right)}}

f(x) = x
```

のように表記しました。 ラムダ計算では名前のない関数そのものを表現する必要があるため, 同様のことを以下のように表現します。

```math
\lambda x. \mathop{x}
```

$\lambda$ という記号に引き続いて引数の文字を宣言し, ピリオドで区切った先に引数に対する操作を記述します。 特に難しいことはないと思います。 Python では以下のように記述されます。

```python
lambda x: x
```

いま, この関数を名前 $\id$ で束縛したいとしたら,

```math
\id \coloneqq \lambda x. \mathop{x}
```

```python
identity = lambda x: x
```

のように書けます。 この関数 $\id$ は引数をただそのまま返す**恒等関数**というもので, I コンビネータとも呼びます。 一見無意味なように見えますが, 他の関数に渡されることで重要な性質を実現させることも多いです。

ただし, ラムダ計算における名前の束縛は簡潔さのためにあるのであり, その実態はあくまでも無名関数と同様であることを念頭に置いてください。 それらの名前は再度登場した各箇所に埋め込むことができ(引数の名前はかぶらないように変更する必要はあると思いますが), **循環的な参照は発生してはいけない**ということです。

これはつまり, **直感的な方法では再帰関数を記述できない**ことを意味します。 といっても再帰ができないわけではなく, のちのち現れる「不動点コンビネータ」というものを利用して実現できます。

ラムダ計算の世界では, 原則として**引数はひとつ**です。 複数の引数を与えるような関数を表現するにはどうすればいいでしょう? 答えは簡単で, **関数がまた関数を返せばいい**ということです。 返ってきた関数に順番に引数を渡すことで, 複数の引数を与えたいという欲求を充足します。

たとえば, 二項の和は $\lambda x. \lambda y. x + y$ のようにすればよいわけです。 この関数に $3$ を適用すると, $\lambda y. 3 + y$ という関数が返るというわけです。 これを $\lambda x y. x + y$ のように略記することも多いです。 ただし, Python ではこのように書いてしまうと「ほんとうの意味での多引数関数」になってしまうので略記はできません。

関数適用の際, 通常の数学では紛れの心配がない場合は $\sin x$ のように単に並置し, そうでない場合は $f{\left(x\right)}$ のようにカッコを使いますが, ラムダ計算では関数がすべてなので基本的には常に $\mathop{f} \mathop{x}$ のように並置し, 適用順序が左結合でないときのみカッコを使用します。

## 真理値と論理演算

### 真理値

自然数に行く前に, もう少し簡単な真理値の定義について見てみましょう。 基本的なアイデアは, **真理値そのものがいわゆる三項演算子のように働く**ということです。 つまり, 真理値 $\true$ と真理値 $\false$ は以下のように定義できます。

```math
\begin{aligned}
\true &\coloneqq \lambda t f. \mathop{t} \\
\false &\coloneqq \lambda t f. \mathop{f}
\end{aligned}
```

```python
true = lambda t: lambda f: t
false = lambda t: lambda f: f
```

面白いのが $\true$ で, この関数に一つだけ引数を渡してやると, 戻ってくる関数は**引数に関わらず最初に渡しておいた引数を返すような定数関数**となることです。 このような定数関数をつくる関数を K コンビネータとも呼びます。 ちなみに, $\false = \true\id$です。 気が向いたら確かめてみてください。

### 選言 / 連言

さて, 真理値が定義できたので論理演算も定義しておきたいところですね。 選言(論理和) $\disj$ と連言(論理積) $\conj$ はどうなるでしょう。 Python における`or`と`and`の定義は, 左辺が Truthy のとき`or`は左辺を, `and`は右辺を返し, 左辺が Falsy のとき`or`は右辺を, `and`は左辺を返すのでした。 これをそのまま落とし込んでしまえば簡単です。 すなわち,

```math
\begin{aligned}
\disj &\coloneqq \lambda p q. \mathop{p} \mathop{p} \mathop{q} \\
\conj &\coloneqq \lambda p q. \mathop{p} \mathop{q} \mathop{p}
\end{aligned}
```

```python
disj = lambda p: lambda q: p(p)(q)
conj = lambda p: lambda q: p(q)(p)
```

となります。

### 否定

つづいて否定 $\inv$ を考えます。 $\true$ なら $\false$ を, $\false$ なら $\true$ を返すのですから, 以下のように定義することもできます。

```math
\inv \coloneqq \lambda p. \mathop{p} \false \true
```

```python
inv = lambda p: p(false)(true)
```

一方で, より一般に以下のようにも定義できます。 $\inv \true$ は, 第一引数ではなく第二引数を返します。 逆もしかりです。 すなわち,

```math
\inv \coloneqq \lambda p. \lambda t f. \mathop{p} \mathop{f} \mathop{t}
```

```python
inv = lambda p: lambda t: lambda f: p(f)(t)
```

となります。 $\inv$ は, **ある関数の第一引数と第二引数を入れ替えた関数を返す**とみなせます。

## 自然数と代数演算

### 自然数

準備運動もすみましたので自然数…すなわちチャーチ数に入りましょう。 チャーチ数の基本的なアイデアは, **自然数 $n$ は, 操作 $s$ と初期値 $z$ を受け取って, $z$ に $s$ を $n$ 回行って返す関数とする**ということです。 すなわち,

```math
\begin{aligned}
0 &\coloneqq \lambda s z. \mathop{z} \\
1 &\coloneqq \lambda s z. \mathop{s} \mathop{z} \\
2 &\coloneqq \lambda s z. \mathop{s} \paren{\mathop{s} \mathop{z}} \\
\vdots
\end{aligned}
```

```python
zero = lambda s: lambda z: z
one = lambda s: lambda z: s(z)
two = lambda s: lambda z: s(s(z)))
```

こうなります。 余談ですが, $0$ が $\false$ に同値ですね。

すべての数をこのように書いていくのは手間です。 ペアノの公理によると, 自然数には必ず「次の数」があります。 それを求める後者関数 $\succc$ を考えましょう。 受け取った数に $s$ と $z$ を渡して, さらにもう一度 $s$ を作用させればよいのですから, 以下のように定義できるでしょう。

```math
\succc \coloneqq \lambda n. \lambda s z. \mathop{s} \paren{\mathop{n} \mathop{s} \mathop{z}}
```

```python
succ = lambda n: lambda s: lambda z: s(n(s)(z)))
```

確認用のヘルパー関数として, Python のネイティブな整数とチャーチ数を相互変換する関数を作っておきます。 チャーチ数 → 整数の変換にはチャーチ数の定義を利用しています。

```python
def church_of(n):
    return zero if n <= 0 else succ(church_of(n - 1))
def integer_of(n):
    return n(lambda x: x + 1)(0)

three = church_of(3)
four = church_of(4))
(integer_of(three), integer_of(four))
```

```:stdout
(3, 4)
```

### 加算

自然数の定義ができましたので, 演算についても考えていきましょう。 まずは加算 $\add$ です。 加算を定義するにあたって二つの考え方があります。

1. $\succc$ を繰り返すことによって定義する
2. $s$ を和の回数分適用する事によって定義する

考えやすいのは 1 です。 つまり,

```math
\add \coloneqq \lambda n m. \mathop{m}\succc\mathop{n}
```

```python
add = lambda n: lambda m: m(succ)(n)
```

チャーチ数では, 最初に与えた引数を次に与えられた引数に適用します。 初期値を $n$ にして, $m$ 回 $\text{suc}$ を適用すれば, まさしく $n + m$ といえるでしょう。

一見ややこしいですが無駄がないのは 2 です。 こちらは,

```math
\add \coloneqq \lambda n m. \lambda s z. \mathop{m} \mathop{s} \paren{\mathop{n} \mathop{s} \mathop{z}}
```

```python
add = lambda n: lambda m: lambda s: lambda z: m(s)(n(s)(z))
```

となります。 返る関数は, 初期値 $z$ に操作 $s$ を $n$ 回適用したあと, さらに $m$ 回適用するので, まさしく $n + m$ 回 $s$ を適用するわけですから, チャーチ数としてみると $n + m$ となっていることがわかります。

```python
seven = add(four)(three)
integer_of(seven)
```

```:stdout
7
```

正しく計算できていますね。

### 乗算

続いては乗算 $\mul$ です。 こちらも $\add$ の繰り返しとする方法と, $s$ を積の回数分適用する方法があります。 前者では

```math
\mul \coloneqq \lambda n m. \mathop{m} \paren{\add \mathop{n}} \mathop{0}
```

```python
mul = lambda n: lambda m: m(add(n))(zero)
```

となります。 後者では

```math
\mul \coloneqq \lambda n m. \lambda s z. \mathop{m} \paren{\mathop{n} \mathop{s}} \mathop{z}
```

```python
mul = lambda n: lambda m: lambda s: lambda z: m(n(s))(z)
```

となります。 $\mathop{n} \mathop{s}$ を一つの関数としてみると, 引数に対し $s$ を $n$ 回適用するという関数です。 それを $m$ 回適用すれば, 全体で見て $s$ が適用される回数は $n \times m$ 回となります。 $z$ に $s$ を $n \times m$ 回適用する関数とは, チャーチ数の $n \times m$ にほかなりません。

```python
twenty_one = mul(seven)(three)
integer_of(twenty_one)
```

```:stdout
21
```

正しく計算できています。

### 減算 (0 を下限とする)

ここから一気にややこしさが跳ね上がります。 減算 $\subb$ を定義するにはどのようにすればいいでしょう。 とはいっても, チャーチ数は負の数を表現できないので, $0$ を下限とします。

まず先に, $\succc$ の逆といえる前者関数 $\pred$ を考えます。 そのために, 以下のような関数 $\replace$ を定義します。

```math
\replace \coloneqq \lambda n. \lambda s z. \mathop{n} \paren{\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}} \paren{\true \mathop{z}}
```

```python
replace = lambda n: lambda s: lambda z: n(lambda x: lambda s2: s2(x(s)))(true(z))
```

チャーチ数に $\replace$ を適用するとどうなるでしょう。 まずは $0$ の場合です。 初期値が $\true \mathop{z}$ ですので,

```math
\begin{aligned}
\replace \mathop{0} &= \lambda sz. \true \mathop{z} \\
(&= \lambda sz. \lambda s'. \mathop{z})
\end{aligned}
```

一つ余計に引数を取るだけですね。 $1$ はどうでしょう。

```math
\begin{aligned}
\replace \mathop{1} &= \lambda s z. \paren{\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}} \paren{\true \mathop{z}} \\
&= \lambda s z. \lambda s'. \mathop{s'} \paren{\true \mathop{z} \mathop{s}} \\
&= \lambda s z. \lambda s'. \mathop{s'} \mathop{z}
\end{aligned}
```

$s$ が $s'$ にすり替わりました。 もしやすべての $s$ を $s'$ にすり替えてしまう関数? いえ, $2$ を見てください。

```math
\begin{aligned}
\replace \mathop{2} &= \lambda s z. \paren{\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}} \paren{\paren{\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}} \paren{\true \mathop{z}}} \\
&= \lambda s z. \paren{\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}} \paren{\lambda s'. \mathop{s'} \mathop{z}} \\
&= \lambda s z. \lambda s'. \mathop{s'} \paren{\paren{\lambda s'. \mathop{s'} \mathop{z}} \mathop{s}} \\
&= \lambda s z. \lambda s'. \mathop{s'} \paren{\mathop{s} \mathop{z}} \\
\end{aligned}
```

外側の $s$ だけが $s'$ にすり替わりました。 以下同様に,

```math
\begin{aligned}
\replace \mathop{3} &= \lambda s z. \lambda s'. \mathop{s'} \paren{\mathop{s} \paren{\mathop{s} \mathop{z}}}\\
\replace \mathop{4} &= \lambda s z. \lambda s'. \mathop{s'} \paren{\mathop{s} \paren{\mathop{s} \paren{\mathop{s} \mathop{z}}}}\\
\replace \mathop{5} &= \lambda s z. \lambda s'. \mathop{s'} \paren{\mathop{s} \paren{\mathop{s} \paren{\mathop{s} \paren{\mathop{s} \mathop{z}}}}}\\
\vdots
\end{aligned}
```

となっていきます。 $\lambda x. \lambda s'. \mathop{s'} \paren{\mathop{x} \mathop{s}}$ が今ある最も外側の操作を $s$ に戻したあと $s'$ を付け加えてくれるので, 常に**最も外側の操作ひとつだけを別の操作 $s'$ に置き換えることができる**んですね。

ここまでくると勘がいい人はわかったかもしれません。 この別の操作 $s'$ に, 「なにもしない」恒等関数 $\id$ を与えてやれば, それで前者関数 $\pred$ が定義できます。

```math
\pred \coloneqq \lambda n. \lambda s z. \replace \mathop{n} \mathop{s} \mathop{z} \id
```
```python
pred = lambda n: lambda s: lambda z: replace(n)(s)(z)(identity)
```

```python
twenty = pred(twenty_one)
integer_of(twenty)
```

```:stdout
20
```

正しく計算できています。

$\pred$ が定義できたため, 加算の 1 と同様の方式で減算 $\subb$ が定義できます。

```math
\subb \coloneqq \lambda n m. \mathop{m} \pred \mathop{n}
```

```python
sub = lambda n: lambda m: m(pred)(n)
```

```python
seventeen = sub(twenty)(three)
integer_of(seventeen)
```

```:stdout
17
```

正しく計算できていますね。

### 除算 (ユークリッド除法)

減算も難しかったですが, 除算 $\divv$ はさらに難しいです。 こちらも有理数はチャーチ数の範疇外ですので, ユークリッド除法(あまりつき除法)の商をとるものを定義します。 つまり $17 \div 3 = 5$ とします。

形式的には, 除算は以下のように定義できます。

```math
n \div m =
\begin{cases}
  \paren{n - m} \div m + 1, & n \ge m \\
  0, & n < m
\end{cases}
```

これは $n \ge m$ によって場合分けをすればいよいでしょう。 第一引数が第二引数以上であることを示す関数 $\gee$ を定義します。 これは簡単に言えば, $m - n$ が $0$ であることと同値です。

では, 引数が $0$ であることをどのように確かめればいいでしょう。 ここで, チャーチ数の性質を思い出してください。 チャーチ数 $n$ に操作 $s$ と初期値 $z$ を与えると, $z$ に対して $n$ 回 $s$ を適用するのでした。 つまり, 初期値を $\true$ にして, 一度でも適用されるとつねに $\false$ を返すような関数を $s$ にすれば, $0$ のときだけ $\true$ を返すはずです。 $0$ であるかどうかを調べる述語関数 $\iszero$ は以下のように定義できます。

```math
\iszero \coloneqq \lambda n. \mathop{n} \paren{\true \false} \true
```

```python
iszero = lambda n: n(true(false))(true)
```

$\true$ は定数関数を作り出す高階関数でもあるのでしたね。 これを用いて $\gee$ は以下のように定義できます。

```math
\gee \coloneqq \lambda n m. \iszero \paren{\subb \mathop{m} \mathop{n}}
```

```python
ge = lambda n: lambda m: iszero(sub(m)(n))
```

さて, 最初に示した形式的定義に従えば, 気持ち的には $\divv$ を下のように定義したいです。

```math
\divv' = \lambda n m. \gee \mathop{n} \mathop{m} \paren{\succc \paren{\divv' \paren{\subb \mathop{n} \mathop{m}} \mathop{m}}} \mathop{0}
```

しかし, この定義は**循環参照**となっており, 本来無名であるべき**ラムダ計算では不可能な定義**です。 では, ラムダ計算において再帰関数はどのように定義すればいいでしょう。

まず, 自分自身を参照していた部分を, **外から引数として持ってくる**形に書き換えます。 すなわち, 以下のようになります。

```math
\lambda f. \lambda n m. \gee \mathop{n} \mathop{m} \paren{\succc \paren{\mathop{f} \paren{\subb \mathop{n} \mathop{m}} \mathop{m}}} \mathop{0}
```

あくまでも外部から持ってきた引数 $f$ を適用しているだけなので, これは循環参照になっていません。

さて, ある関数に対し, 適用しても変化しないような引数をその関数の**不動点**とよびます。 たとえば, $\mul \mathop{2}$ の不動点は $0$ です。 この不動点という概念はラムダ計算における再帰と深い関わりがあります。

不動点が再帰関数とどのような関係にあるのでしょう。 先程の $\lambda n m. \gee \mathop{n} \mathop{m} \paren{\succc \paren{\mathop{f} \paren{\subb \mathop{n} \mathop{m}} \mathop{m}}} \mathop{0}$ のような $f$ を含むなんらかのラムダ項を一般化して $L\paren{f}$ と書くことにします。

```math
\lambda f. L\paren{f}
```

もう一度いいますが, これは外から得られる $f$ を内部で使っているだけで, **これ自体は循環参照していません**。 ここで, この無名関数全体が不動点 $F$ をもつとします。 不動点の定義より, 以下の関係が導けます。

```math
\begin{aligned}
F &= \paren{\lambda f. L\paren{f}} \mathop{F}\\
&= L\paren{F}
\end{aligned}
```

**なに, $F = L\paren{F}$ ですって**。 $L\paren{F}$ は $F$ を含むラムダ項なので, **突然再帰関数が現れた**ことになります。 再帰させたい関数の部分をより大きなラムダ式で囲い, 外から持ってくるふりをしながらそれの不動点を求めると, **名前を束縛しなくても元の関数の再帰形が得られる**のです。

任意の関数の不動点を得る関数が以下に示す $\fix$ 関数です。 Y コンビネータとも呼びます。

```math
\fix \coloneqq \lambda f. \paren{\lambda x. \mathop{f} \paren{\mathop{x} \mathop{x}}} \paren{\lambda x. \mathop{f} \paren{\mathop{x}\mathop{x}}}
```

ただし, Python での実装の際これをそのまま使用すると, Python は**正格評価である**ため引数を先に評価しようとし, **無限ループになってしまいます**。

ラムダ計算においては $f$ という関数と $\lambda x. \mathop{f} \mathop{x}$ は明らかに等価です。 この置き換えは専門的には η 変換によります。

Python ではラムダ式の評価は遅延されるので, **遅延したい部分を η 変換してあげることで無限ループを防ぐ**ことができます。 この理屈で先程の $\fix$ の $\mathop{x} \mathop{x}$ 部分を変換すると,

```math
\fix \coloneqq \lambda f. \paren{\lambda x. \mathop{f} \paren{\lambda y. \mathop{x} \mathop{x} \mathop{y}}} \paren{\lambda x. \mathop{f} \paren{\lambda y. \mathop{x}\mathop{x} \mathop{y}}}
```

```python
fix = lambda f: (lambda x: f(lambda y: x(x)(y)))(lambda x: f(lambda y: x(x)(y)))
```

これで Python でも使用できる $\fix$ が定義できました。 このバージョンを本来の Y コンビネータと区別して Z コンビネータと呼ぶこともあります。

さて, ここまで来たら先程作成したラムダ式の不動点を求めることで $\divv$ が定義できます。

```math
\divv \coloneqq \fix \paren{\lambda f. \lambda n m. \gee \mathop{n} \mathop{m} \paren{\succc \paren{\mathop{f} \paren{\subb \mathop{n} \mathop{m}} \mathop{m}}} \mathop{0}}
```

```python
div = fix(lambda f: lambda n: lambda m: ge(n)(m)(succ(f(sub(n)(m))(m)))(zero))
```

ただし, これを上のようにそのまま実装してしまうと, Python は遅延評価ではないので $\gee \mathop{n} \mathop{m}$ が $\false$ であっても第一引数を評価しようとし, 無限ループに陥ってしまいます。 そこで, $\true$ 節全体を η 変換するとよいでしょう。

```python
div = fix(lambda f: lambda n: lambda m: ge(n)(m)(lambda x: succ(f(sub(n)(m))(m))(x))(zero))
```

これで実装できました。

```python
five = div(seventeen)(three)
integer_of(five)
```

```:stdout
5
```

正しく計算できています。

## XOR

前置きがめちゃめちゃ長くなってしまいましたが, いよいよ本題のビット単位 XOR  です。 ビット単位 XOR は, 形式的には以下のように定義できます。

```math
n \xor m = 
\begin{cases}
  m, & n = 0 \\
  n, & m = 0 \\
  \paren{n \div 2 \xor m \div 2} \times 2 + b, & \text{otherwise}
\end{cases} \\
\text{where } b = \begin{cases}
  0, & n + m \equiv 0 \mod 2\\
  1, & n + m \equiv 1 \mod 2
\end{cases}
```

$2$ 倍する $\twice$ と $\frac{1}{2}$ 倍する $\half$ は先程までに定義してきた $\mul$ および $\divv$ を使って簡単に定義できます。

```math
\begin{aligned}
\twice &\coloneqq \mul \mathop{2} \\
\half &\coloneqq \inv \divv \mathop{2}
\end{aligned}
```

```python
twice = mul(two)
half = inv(div)(two)
```

$2$ で割った余りを求める関数 $\parity$ はどうでしょうか。 もちろん $\lambda n. \subb \mathop{n} \paren{\twice \paren{\half \mathop{n}}}$ とすることもできますが, よりスマートな方法があります。

以下のように, $0$ に対してのみ $1$ を返し, それ以外のチャーチ数には $0$ を返す関数 $\delta$ を定義します。 $\iszero$ と同様に定義できます。

```math
\delta \coloneqq \lambda n. \mathop{n} \paren{\true \mathop{0}} \mathop{1}
```

```python
delta = lambda n: n(true(zero))(one)
```

これをチャーチ数の $s$ として与え, 初期値 $z$ を $0$ にしてしまえば, 関数が適用されるたびに $0$ と $1$ が入れ替わるため, これだけで $\parity$ が定義できます。

```math
\parity \coloneqq \lambda n. \mathop{n} \mathop{\delta} \mathop{0}
```

```python
parity = lambda n: n(delta)(zero)
```

材料は揃いましたので, $\xorr$ を組み立てていきます。 気持ち的には,

```math
\xorr' = \lambda n m. \iszero \mathop{n} \mathop{m} \paren{\iszero \mathop{m} \mathop{n} \paren{\parity \paren{\add \mathop{n} \mathop{m}} \succc \paren{\twice \paren{\xorr' \paren{\half \mathop{n}} \paren{\half \mathop{m}}}}}}
```

と書きたいです。 これを $\fix$ を使用して無名再帰すると,

```math
\xorr \coloneqq \fix \paren{\lambda f. \lambda n m. \iszero \mathop{n} \mathop{m} \paren{\iszero \mathop{m} \mathop{n} \paren{\parity \paren{\add \mathop{n} \mathop{m}} \succc \paren{\twice \paren{\mathop{f} \paren{\half \mathop{n}} \paren{\half \mathop{m}}}}}}}
```

となります。 こちらも Python 実装時は内側の $\false$ 節を η 変換して,

```python
xor = fix(lambda f: lambda n: lambda m: iszero(n)(m)(iszero(m)(n)(lambda x: parity(add(n)(m))(succ)(twice(f(half(n))(half(m))))(x))))
```

として実装できます。

```python
six = xor(five)(three)
integer_of(six)
```

```:stdout
6
```

正しく計算できていますね。

## 検算

※ 先に言っておくとこの検算, **計算に死ぬほど時間がかかります**。 具体的には Google Colab で実行したとき 6 時間以上使っても計算が終わりませんでした。 どうも $\divv$ が足を引っ張っているようです。 ラムダ式で遅延評価させるかわりに, 以下のように Python における三項演算子である`if`式に差し替えて実行したほうがいいです。 これだと 3 秒くらいで終わります。 というか $\half$ のもっと計算量が少ない定義ないかな…。

```python
div = fix(lambda f: lambda n: lambda m: succ(f(sub(n)(m))(m)) if ge(n)(m)(True)(False) else zero)
```

100 個くらいサンプルケースを作って検算してみましょう。 きれいに表示させたいので Numpy および Pandas を使用するが許してくれよな。

```python
import numpy as np
import pandas as pd

np.random.seed(753)

lhs = np.random.randint(0, 100, 100)
rhs = np.random.randint(0, 100, 100)
data = np.asarray([lhs, rhs]).T

df = pd.DataFrame(data, columns=['LHS', 'RHS'])
df
```

|     | LHS |  RHS|
|----:|----:|----:|
|   0 |  76 |  29 |
|   1 |  58 |   2 |
|   2 |  65 |  47 |
|   3 |  27 |  46 |
|   4 |  10 |  28 |
| ... | ... | ... |
|  95 |  87 |  51 |
|  96 |  40 |   2 |
|  97 |  59 |  42 |
|  98 |  33 |  24 |
|  99 |  83 |  80 |

まずはネイティブな演算子で XOR を計算します。

```python
df['Native'] = df['LHS'] ^ df['RHS']
df
```

|     | LHS | RHS | Native |
|----:|----:|----:|-------:|
|   0 |  76 |  29 |     81 |
|   1 |  58 |   2 |     56 |
|   2 |  65 |  47 |    110 |
|   3 |  27 |  46 |     53 |
|   4 |  10 |  28 |     22 |
| ... | ... | ... |    ... |
|  95 |  87 |  51 |    100 |
|  96 |  40 |   2 |     42 |
|  97 |  59 |  42 |     17 |
|  98 |  33 |  24 |     57 |
|  99 |  83 |  80 |      3 |


次にチャーチ数を経由して XOR を計算する関数を定義し, それをユニバーサル関数化します。

```python
church_xor = lambda n, m: integer_of(xor(church_of(n))(church_of(m)))
np_church_xor = np.frompyfunc(church_xor, 2, 1)
df['Church'] = np_church_xor(df['LHS'], df['RHS'])
df
```

|     | LHS | RHS | Native | Church |
|----:|----:|----:|-------:|-------:|
|   0 |  76 |  29 |     81 |     81 |
|   1 |  58 |   2 |     56 |     56 |
|   2 |  65 |  47 |    110 |    110 |
|   3 |  27 |  46 |     53 |     53 |
|   4 |  10 |  28 |     22 |     22 |
| ... | ... | ... |    ... |    ... |
|  95 |  87 |  51 |    100 |    100 |
|  96 |  40 |   2 |     42 |     42 |
|  97 |  59 |  42 |     17 |     17 |
|  98 |  33 |  24 |     57 |     57 |
|  99 |  83 |  80 |      3 |      3 |


結果やいかに。

```python
print('すべて一致しています' if all(df['Native'] == df['Church']) else '一致していない組み合わせがあります')
```

```:stdout
すべて一致しています
```

正しく計算できていますね。

## これいる?

[ちょっと草植えときますね型言語 Grass](http://www.blue.sky.or.jp/grass/doc_ja.html) しか手元にない環境で Grundy 数を計算する必要に迫られる日がいつか来るかもしれないからいる(鋼の意志)(レース序盤に前が詰まったときに強い意志を保ち持久力が回復する)。