4
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 3 years have passed since last update.

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

Last updated at Posted at 2021-04-24

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

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

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

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

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

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

ラムダ式の記法

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

\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

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

\lambda x. \mathop{x}

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

lambda x: x

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

\id \coloneqq \lambda x. \mathop{x}
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$ は以下のように定義できます。

\begin{aligned}
\true &\coloneqq \lambda t f. \mathop{t} \\
\false &\coloneqq \lambda t f. \mathop{f}
\end{aligned}
true = lambda t: lambda f: t
false = lambda t: lambda f: f

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

選言 / 連言

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

\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}
disj = lambda p: lambda q: p(p)(q)
conj = lambda p: lambda q: p(q)(p)

となります。

否定

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

\inv \coloneqq \lambda p. \mathop{p} \false \true
inv = lambda p: p(false)(true)

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

\inv \coloneqq \lambda p. \lambda t f. \mathop{p} \mathop{f} \mathop{t}
inv = lambda p: lambda t: lambda f: p(f)(t)

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

自然数と代数演算

自然数

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

\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}
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$ を作用させればよいのですから, 以下のように定義できるでしょう。

\succc \coloneqq \lambda n. \lambda s z. \mathop{s} \paren{\mathop{n} \mathop{s} \mathop{z}}
succ = lambda n: lambda s: lambda z: s(n(s)(z)))

確認用のヘルパー関数として, 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 です。 つまり,

\add \coloneqq \lambda n m. \mathop{m}\succc\mathop{n}
add = lambda n: lambda m: m(succ)(n)

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

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

\add \coloneqq \lambda n m. \lambda s z. \mathop{m} \mathop{s} \paren{\mathop{n} \mathop{s} \mathop{z}}
add = lambda n: lambda m: lambda s: lambda z: m(s)(n(s)(z))

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

seven = add(four)(three)
integer_of(seven)
stdout
7

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

乗算

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

\mul \coloneqq \lambda n m. \mathop{m} \paren{\add \mathop{n}} \mathop{0}
mul = lambda n: lambda m: m(add(n))(zero)

となります。 後者では

\mul \coloneqq \lambda n m. \lambda s z. \mathop{m} \paren{\mathop{n} \mathop{s}} \mathop{z}
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$ にほかなりません。

twenty_one = mul(seven)(three)
integer_of(twenty_one)
stdout
21

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

減算 (0 を下限とする)

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

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

\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}}
replace = lambda n: lambda s: lambda z: n(lambda x: lambda s2: s2(x(s)))(true(z))

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

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

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

\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$ を見てください。

\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'$ にすり替わりました。 以下同様に,

\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$ が定義できます。

\pred \coloneqq \lambda n. \lambda s z. \replace \mathop{n} \mathop{s} \mathop{z} \id
pred = lambda n: lambda s: lambda z: replace(n)(s)(z)(identity)
twenty = pred(twenty_one)
integer_of(twenty)
stdout
20

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

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

\subb \coloneqq \lambda n m. \mathop{m} \pred \mathop{n}
sub = lambda n: lambda m: m(pred)(n)
seventeen = sub(twenty)(three)
integer_of(seventeen)
stdout
17

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

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

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

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

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$ は以下のように定義できます。

\iszero \coloneqq \lambda n. \mathop{n} \paren{\true \false} \true
iszero = lambda n: n(true(false))(true)

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

\gee \coloneqq \lambda n m. \iszero \paren{\subb \mathop{m} \mathop{n}}
ge = lambda n: lambda m: iszero(sub(m)(n))

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

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

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

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

\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}$ と書くことにします。

\lambda f. L\paren{f}

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

\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 コンビネータとも呼びます。

\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}$ 部分を変換すると,

\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}}}
fix = lambda f: (lambda x: f(lambda y: x(x)(y)))(lambda x: f(lambda y: x(x)(y)))

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

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

\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}}
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$ 節全体を η 変換するとよいでしょう。

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

これで実装できました。

five = div(seventeen)(three)
integer_of(five)
stdout
5

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

XOR

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

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$ を使って簡単に定義できます。

\begin{aligned}
\twice &\coloneqq \mul \mathop{2} \\
\half &\coloneqq \inv \divv \mathop{2}
\end{aligned}
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$ と同様に定義できます。

\delta \coloneqq \lambda n. \mathop{n} \paren{\true \mathop{0}} \mathop{1}
delta = lambda n: n(true(zero))(one)

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

\parity \coloneqq \lambda n. \mathop{n} \mathop{\delta} \mathop{0}
parity = lambda n: n(delta)(zero)

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

\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$ を使用して無名再帰すると,

\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$ 節を η 変換して,

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))))

として実装できます。

six = xor(five)(three)
integer_of(six)
stdout
6

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

検算

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

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 を使用するが許してくれよな。

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 を計算します。

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 を計算する関数を定義し, それをユニバーサル関数化します。

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

結果やいかに。

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

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

これいる?

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

4
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
4
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?