この記事は株式会社LIFULLの数学同好会あなぐま会のための発表資料です。

アナリストやデータサイエンティストが多いので、「彼らが普段使っているPythonで（普段あまりあまり触れないであろう）コンピュータ・サイエンスの数学とつながる話をしよう」という意図です。実は「圏論の初歩をPythonプログラミングで説明する」という資料も用意しつつあったのですが、夜の回（飲み会）の題材にしては重すぎたのと、Pythonでは説明しづらい概念（射の集合など）があったので断念しました。

自己紹介

名前: 二宮健（たけし）
所属: AI戦略室データサイエンスG（嶋村さんチーム）
　　→ PE3U4G（須藤さんチーム）

機械科学専攻（修士）から、2015年にLIFULLにエンジニアとして新卒入社。
広告運用自動化（MAM）やAIシステムの実装に従事。

プログラミングや情報科学は就職後に学んだことのほうが多い気がする。

チャーチ数について

関数（ラムダ式）で次のように整数を定義すると、（0を含む）自然数として計算できる。これをチャーチ数という。

zero = lambda f: lambda x: x
one = lambda f: lambda x: f(x)
two = lambda f: lambda x: f(f(x))
three = lambda f: lambda x: f(f(f(x))) 
...

Pythonでの実装例

加算、乗算、累乗が定義できることを確かめる。数値に変換するto_int以外では関数（lambda）しか登場していないことに注目。

church.py

from __future__ import annotations
from numbers import Number
from typing import Callable


class ChurchNumber(Number):
    def __init__(self, church: Callable):
        self.ch = church

    def to_int(self) -> int:
        """チャーチ数を組み込みのint型に変換する"""
        return self.ch(lambda n: n + 1)(0)

    def succ(self) -> ChurchNumber:
        """チャーチ数に+1する"""
        return ChurchNumber(lambda f: lambda x: f(self.ch(f)(x)))

    def __add__(self, other: ChurchNumber) -> ChurchNumber:
        """チャーチ数同士を足し算する"""
        return ChurchNumber(lambda f: lambda x: self.ch(f)(other.ch(f)(x)))

    def __mul__(self, other: ChurchNumber) -> ChurchNumber:
        """チャーチ数の掛け算(*)を定義する"""
        return ChurchNumber(lambda f: lambda x: other.ch(self.ch(f))(x))

    def __pow__(self, exponent: ChurchNumber) -> ChurchNumber:
        """チャーチ数の累乗(**)を定義する"""
        return ChurchNumber(lambda f: lambda x: exponent.ch(self.ch)(f)(x))

次のように動作します。

test.py

from church import ChurchNumber

zero = ChurchNumber(lambda f: lambda x: x)
assert zero.to_int() == 0

# succのテスト
one = zero.succ()
two = one.succ()
three = two.succ()
assert (one.to_int(), two.to_int(), three.to_int()) == (1, 2, 3)

# 加算、乗算、累乗の確認
assert (one + two).to_int() == three.to_int()
assert (two ** three).to_int() == 8
assert (two * three).to_int() == 6

説明のしやすさのためにChurchNumberクラスを導入していますが、ラムダ式だけを使って書ける。

zero = lambda f: lambda x: x
succ = lambda c: lambda f: lambda x: f(c(f)(x))
to_int = lambda c: c(lambda n: n + 1)(0)
# lambda c1, c2: ...ともできますが、λ計算の理論では全ての関数が1引数なので、それに合わせています
add = lambda c1: lambda c2: lambda f: lambda x: c1(f)(c2(f)(x))
...

ただ、コードを読んでも何をやってるか分からなくなって断念した😅

減算や除算は自然数に対して閉じてないので書いていないが、負の数まで拡張した記事も見つかった。

動作の説明

「関数をfをx回適用する」という形で数字を表現している
to_intでは「0に対して+1を行う関数」を適用して、int型に変換している
succではfを1つ増やしている
__add__では「otherの回数関数を実行した後、selfの回数実行する」関数を用意して合計している
後の実装は興味があったら調べてください

チャーチ数って何の役に立つの？

普段のプログラミングでチャーチ数を実行することはない
- データ量がでかい。intで数十バイトで済むのにわざわざ関数を使っている
- 「表現したい数だけ関数を実行する」なので、intに比べると非常に遅い
チャーチ数はλ計算の理論で重要。λ計算はチューリングマシンと同等の数学的モデルで、プログラミング言語理論ではλ計算の理論を使って解析されることが多いように思う。

ここでは、データ型さえ必要なく，すべて関数だけで（数値を）導入できることを説明しよう．（中略）これは，1940年代にλ算法（今日の関数プログラミングに関する研究の論拠となる形式的数学体系）に関する仕事の中でAlonzo Churchが目指した目論みの一部である．
―――『関数プログラミング入門』より。括弧内は追記

λ計算の理論の中で「関数だけの世界で様々なデータ型を導入できるか」という問題でチャーチ数が提案されたらしい（後述）。他にもチャーチ真理値などもある。

（参考）ペアノの公理

ペアノの公理は以下の様に定義される。

自然数は次の5条件を満たす。

自然数$0$が存在する。

任意の自然数$a$にはその後者 (successor)、$suc(a)$が存在する（$suc(a)$は$a + 1$の "意味"）。

$0$はいかなる自然数の後者でもない（$0$より前の自然数は存在しない）。

異なる自然数は異なる後者を持つ：$a \neq b$のとき$suc(a) \neq suc(b)$となる。

$0$がある性質を満たし、$a$がある性質を満たせばその後者$suc(a)$もその性質を満たすとき、すべての自然数はその性質を満たす。

5番目の公理は、数学的帰納法の原理である。

――― Wikipediaより

ペアノの公理を満たすものはノイマンの構成法という別の方法もある。

λ計算の軽い紹介

λ計算の構文は次の3つから成り立っている。

\begin{align}
t ::=&\qquad&項:\\ 
&x &変数\\
&\lambda x.\, t\qquad &ラムダ抽象\\
&t \, t &関数適用
\end{align}

見ての通り関数の宣言と適用だけで、数値や条件式やループの構文は無い。しかし、チャーチ数と同様に、チャーチ真理値で条件分岐を、不動点コンビネータで再帰（ループ）を導入できるので、任意のプログラムが実行できる。

ちなみに、Pythonを含む多くの言語では、具象構文が抽象構文木(AST)として解釈された上で実行されており、そのときにλ計算の理論が活かされているらしい。

Pythonのプログラマーとしての主張

同じ「自然数」の仕様を表現するためにも、複数の実装方法がある。目的にとって効率のよいデータ構造を選ばなくてはならない。
- メモリ上で2進数として表現されている（詳しくはWebで学ぶ情報処理概論）
- 実際のPythonのint型は自動でメモリ領域を増やしたり、小さい整数を共有していたりいろいろやってる
また『型システム入門』によると、λ計算でもブール値や数値を導入した拡張された体系を使うこともあるらしい

更に話すと面白そうな話題

ラムダ計算
- 不動点コンビネータ（Yコンビネータ）による無名関数の再帰
- 評価戦略
型理論
代数的データ型（Pythonでは未実装）を使うと一瞬でチャーチ数が宣言できること

参考

書籍

記事