位相空間とコンピュータサイエンス
1947年の月曜の朝、ベル研究所のリチャード・ハミングを待っていたのは、週末に流したバッチの計算結果ではなく、エラーの報告だった。リレー式計算機はパリティチェックで「どこかが誤っている」と気づき、そこで停止していた。機械は誤りに気づけた。気づいたうえで何もせず、週末を丸ごと捨てていた。
ハミングは考えた。誤りを検出できるなら、その位置まで特定して直せるはずだ。この問いに答えるため、彼はビット列の間の「距離」を持ち出した。
これがコンピュータサイエンスと位相数学の最初の接点になる。そして同じことが、その後も繰り返し起きた。プログラムが止まるかどうかを判定したい人、while ループの意味を数式で書きたい人、分散システムが合意できない理由を知りたい人。彼らは全員、行き詰まったところで同じ問いに立ち返っている。この対象にとって、「近い」とは何なのか。
この記事は、その6つの場面を時代順にたどる。距離で足りた場面、距離では足りず開集合が要った場面、近さが順序に変わった場面、近さが図形になった場面。位相空間論は抽象的な理論として最初からあったのではない。必要に迫られて、そのたびに輸入された道具だった。
結論
- コンピュータサイエンスが位相の言葉を借りたのは、抽象化のためではない。具体的な問題で行き詰まり、「近さ」を定義し直す必要に迫られたからだ
- 1947年・誤り訂正符号: ビット列の近さをハミング距離で測ると、符号の設計は「球が重ならないように詰め込む」幾何の問題になる
- 1936年から1980年代・停止性問題: プログラムの性質に距離は入らない。「有限時間で肯定できる」を開集合と読むと、半決定可能=開、決定可能=開かつ閉という地図が引ける
- 1969年・再帰の意味: 値を「どこまで分かったか」に置き換えると、情報の順序に位相が入る。再帰の意味は近似列の果て(最小不動点)として定まる
- 1977年・静的解析: 抽象解釈は具体と抽象をガロア接続で結び、同じ不動点の骨格を解析器の実装に持ち込んだ
- 1993年・分散合意: 起こりうる実行を図形として描くと、コンセンサスの不可能性が「連結な図形は切り離せない」という位相の事実になる
- 2002年・データ解析: スケールを決め打ちせず全部のスケールを持ち歩くことで、点群の「形」が特徴量になる
- 距離で足りるなら距離のまま済ませる。位相まで上がるのは、距離を入れられない対象に出会ったときだけでよい
前提
- 対象読者: 集合と写像の記法が読め、計算可能性・型・静的解析・分散システムのいずれかに触れたことがある人
- ねらい: 定理を証明することではなく、各分野が位相の言葉を借りた経緯と、それによって何が言えるようになったかをつかむこと
- 前提知識: 集合、写像、極限の初歩。代数的位相幾何(ホモロジーなど)は概要だけ扱う
- 操作できる図を6つ置いた。読み飛ばしても本文だけで筋は通る
通しの問い: 「近い」とは何か
物語に入る前の準備として、この記事で繰り返し出てくる道具を3つ用意する。どれも「近い」を言葉にするための道具になる。
1つ目は距離。集合 $X$ と関数 $d: X \times X \to \mathbb{R}_{\geq 0}$ の組が距離空間であるとは、次の3条件を満たすことをいう。
- $d(x, y) = 0 \iff x = y$(同一性)
- $d(x, y) = d(y, x)$(対称性)
- $d(x, z) \leq d(x, y) + d(y, z)$(三角不等式)
対象が実数である必要はない。ビット列や文字列であっても、この3条件を満たす $d$ を作れれば距離空間になる。第1章はこの一般性だけで話が終わる。
2つ目は開集合。距離が決まると、点 $x$ を中心とする半径 $\varepsilon$ の開球 $B(x, \varepsilon) = \{ y \in X \mid d(x, y) < \varepsilon \}$ が定義できる。ふだんの言葉なら「$x$ の近所」だ。そして部分集合 $U$ が開集合であるとは、$U$ のどの点についても、その点の十分小さい開球が $U$ に収まることをいう。どの点も「近所ごと」入っている集合、と読めばよい。
定規を取り替えると球の形は変わる。次の図で確かめられる。
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
ここに最初の発見がある。ユークリッド・マンハッタン・チェビシェフの3つは、球の形がまるで違うのに、開集合の集まりとしては完全に一致する。どの球の中にも別の距離の小さい球が入るからだ。つまり距離は開集合を決めるが、開集合は距離を1つに決めない。距離には余分な情報が含まれている。
3つ目は位相空間。そこで距離という数値を捨て、開集合の集まり $\mathcal{O}$ だけを構造として持たせる。
- $\emptyset \in \mathcal{O}$ かつ $X \in \mathcal{O}$
- $\mathcal{O}$ の元の任意個(無限個でもよい)の和集合は $\mathcal{O}$ に属する
- $\mathcal{O}$ の元の有限個の共通部分は $\mathcal{O}$ に属する
和は無限個を許すのに、共通部分は有限個までしか許さない。この非対称さは第2章で意味を持つ。
連続写像も距離なしで定義できる。$f: X \to Y$ が連続とは、$Y$ の任意の開集合 $V$ について逆像 $f^{-1}(V)$ が開集合になることをいう。「出力について知りたいことが決まったとき、入力について何を知れば足りるか」を問うのが連続性だ。この向きは、計算の依存関係とそのまま重なる。
道具は以上になる。ここからは時代順に6つの場面をたどる。
1947年、週末が消えた話とハミング距離
この章の「近い」: 2つのビット列が何ビット違うか。距離で測れる、いちばん素直な場面だ。
「検出できるなら、直せるはずだ」
冒頭の場面に戻る。当時のベル研究所のリレー式計算機はパリティチェックを備えていて、誤りを検出すると停止した。検出しかできない機械は、週末をまるごと無駄にする。ハミングは後年、このときの苛立ちを「機械が誤りを検出できるのなら、なぜその位置を特定して直せないのか」という趣旨で振り返っている。
素朴な解は「パリティビットを増やす」だ。では、何ビット足せばよいのだろうか。どう配置すれば検出ではなく訂正まで届くのか。そして、どこまで足せば十分なのか。その場しのぎの工夫を積み上げても、この3つには答えられない。
ビット列に定規を当てる
ハミングは視点を変えた。符号語の集合を $\{0, 1\}^n$ の部分集合と見て、2つの語が何ビット違うかを距離として測ったのだ。
これがハミング距離になる。異なる位置を数えるだけの素朴な定義だが、距離の公理をきちんと満たす。
- 違う位置が1つもなければ同じ語(同一性)
- 違う位置の個数は、どちらから数えても同じ(対称性)
- $x$ から $z$ へ直接変えるビット数は、$y$ を経由するビット数以下(三角不等式)
$\{0, 1\}^n$ は $2^n$ 個の点からなる有限の距離空間になった。連続や極限がいっさい出てこない、純粋に離散的な空間だ。
設計が幾何になる
距離が入った瞬間、誤り訂正の意味が幾何になる。$t$ ビットの誤りとは、受信語が送信した符号語から距離 $t$ 以内へずれることだ。したがって、
- 各符号語を中心とする半径 $t$ の球が重ならなければ、受信語がどの球に入るかで元の語を1つに決められる(訂正できる)
- 球が重なれば、どちらに戻すべきか決められない(訂正できない)
符号の最小距離を $d$ とすると、球が重ならない条件は $d \geq 2t + 1$、すなわち次になる。
$$t = \left\lfloor \frac{d - 1}{2} \right\rfloor$$符号を設計することは、有限の距離空間に球を詰め込むことに等しい。実際に頂点を選んで確かめてほしい。
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
球の体積を数えれば限界も出る。半径 $t$ の球に入る語は $\sum_{i=0}^{t} \binom{n}{i}$ 個なので、符号語を $M$ 個置くなら次の条件が要る。
$$M \cdot \sum_{i=0}^{t} \binom{n}{i} \leq 2^n$$これがハミング限界(球充填限界)だ。図の反復符号 $\{000, 111\}$ は $2 \times (1 + 3) = 8 = 2^3$ で等号を満たす。すき間なく詰まった完全符号の最小例になっている。ハミングが1950年の論文で示した $(7, 4)$ 符号も $16 \times (1 + 7) = 128 = 2^7$ で完全符号だ。
要点
- ハミング距離は距離の公理を満たす。だからビット列の全体は有限の距離空間になる
- 訂正できる条件は「半径 $t$ の球が交わらない」。設計は球の詰め込みに変わる
- 「情報量を増やす」と「誤りに強くする」は、球を増やすか大きくするかという1つの綱引きになる
そしてこの章には位相が出てこない。有限集合の上の距離をそのまま使えば足りるからだ。距離で足りるなら距離のまま済ませる。話が変わるのは、距離を入れようがない対象と出会ったときだ。
この章の参考
- ハミング符号 - Wikipedia
- Hamming bound - Wikipedia
- Richard W. Hamming, “Error Detecting and Error Correcting Codes”, Bell System Technical Journal, 1950(原典)
- F. J. MacWilliams, N. J. A. Sloane, “The Theory of Error-Correcting Codes”, North-Holland(符号理論の定番書)
「止まらない」は永遠に確かめられない話と開集合
この章の「近い」: プログラムの性質どうしの近さ。何メートルとは言えない対象に、初めて位相が要る。
決定不能では言い足りない
チューリングが1936年に示したように、任意のプログラムが停止するかを判定するアルゴリズムは存在しない。停止性問題は決定不能だ。
ただ、実際に手を動かすとこの結論は少し粗く感じる。停止する場合と停止しない場合で、扱いがまるで対称ではないからだ。
- 停止するなら、実行を続ければいつか必ず「止まった」と分かる
- 停止しないなら、いつまで待っても「止まらない」とは確定しない
「止まる」は有限時間で肯定できるが、否定はできない。計算可能性理論はこれを半決定可能(帰納的可算)と呼ぶ。決定可能か決定不能かという二分法では、この非対称さが表現されない。では、この非対称さを扱える言葉はどこにあるのだろうか。
観測の非対称を位相と読む
1980年代、マイケル・スミスやスティーヴン・ヴィッカーズは、この非対称さを位相の言葉として整理した。性質 $P$ について「$P$ が成り立つなら有限時間で肯定できる」とき、$P$ を観測可能と呼ぶ。すると次が分かる。
- 有限個の観測可能な性質は、順に確かめて合わせればよい。だから有限個の共通部分も観測可能
- 無限個のうちどれか1つが成り立てばよいなら、成り立つものが有限時間で見つかる。だから無限個の和集合も観測可能
- 無限個すべてが成り立つことは、有限時間では確かめられない。だから無限個の共通部分は許されない
準備で見た位相の公理と、一字一句同じ形をしている。和は無限個を許すのに共通部分は有限個まで、というあの非対称さは、「有限個の観測なら待てるが、無限個は待てない」という機械の制約そのものだった。ヴィッカーズの本の題名が Topology via Logic であるのは、この一致を指している。
対応はこうなる。
- 半決定可能な性質 = 開集合
- 反証だけが半決定可能な性質 = 閉集合
- 決定可能な性質 = 開かつ閉(clopen)
「停止する」は開集合、「停止しない」は閉集合。そして開かつ閉ではないので決定可能ではない。決定不能性が「開いてはいるが、閉じていない」という図形の言葉になった。
実際に1ビットずつ観測してみると、この違いは体で分かる。同じ列を見ていても、性質によって答えの出るタイミングがまるで違う。
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
コンパクト性が探索を終わらせる
舞台をもう少し具体的にする。無限のビット列全体の集合 $2^{\omega}$ を考える。プログラムの出力ストリームや、終わらない観測の履歴だと思えばよい。ここでの基本的な開集合は「先頭 $n$ ビットが決まった値である」という筒集合で、有限の接頭辞だけで判定できる性質にあたる。
この空間はコンパクトだ。そこから計算の事実が1つ落ちてくる。コンパクト空間の開かつ閉な集合は有限個の筒集合の和に限られるので、決定可能な性質は必ず有限の接頭辞だけで判定できる。「無限に読み進めないと決まらないが、それでも決定可能」という都合のよい性質は存在しない。
マーティン・エスカルドはこの構造を逆手に取った。無限のビット列の集合に対する全探索を、有限時間で終える Haskell のプログラムを示したのだ。無限個の候補を「全部試す」コードが本当に終了する。理由は、空間がコンパクトだからになる。
要点
- 開集合=有限時間で肯定できる性質、閉集合=有限時間で否定できる性質、開かつ閉=決定可能
- 位相の公理の非対称さは、「有限個の観測しか待てない」という計算の制約と一致する
- コンパクト性は「全探索が有限で終わる」ことに対応する
距離では測れない対象に、開集合が構造を与えた。次の章では、この「有限の観測」という発想が、プログラムの意味そのものを定義しにいく。
この章の参考
- 停止性問題 - Wikipedia
- 位相空間 - Wikipedia
- Alan M. Turing, “On Computable Numbers, with an Application to the Entscheidungsproblem”, 1936(原典)
- Steven Vickers, “Topology via Logic”, Cambridge University Press(開集合を観測として読む立場を通した本)
- Martín Escardó, “Infinite Sets That Admit Fast Exhaustive Search”, LICS 2007(無限集合の全探索が終わる話)
while ループの意味が書けない話とスコット位相
この章の「近い」: 計算の途中状態どうしの近さ。近さが順序に変わる場面だ。
反対していた本人がモデルを作った
1960年代後半、オックスフォードのクリストファー・ストレイチーは、プログラムの意味を数学的な対象として定義しようとしていた。表示的意味論と呼ばれる試みだ。代入や条件分岐は関数として書ける。ところが再帰と while で止まる。
1fact n = if n == 0 then 1 else n * fact (n-1)
fact を fact で定義している。「この等式を満たす関数 $f$」を意味と定めたいが、そんな $f$ が存在するのか、複数あるならどれを選ぶのかがはっきりしない。しかも入力によっては停止しないので、「すべての入力に値を返す関数」としては書けない。
λ計算のモデルを作ろうとすると壁はもっと硬い。λ計算は関数を関数に適用できるので、意味の集合 $D$ には $D \cong D \to D$ が要る。ところがカントールの対角線論法から、2要素以上の集合では $\lvert D^D \rvert > \lvert D \rvert$ になる。ふつうの集合と関数の世界に、そんな $D$ は存在しない。
1969年にオックスフォードへ来たダナ・スコットは、この点を根拠に「型のないλ計算に数学的な意味は与えられない」と考えていた。ところが同じ年の秋、彼は自分でそのモデルを作ってしまう。何が壁を壊したのだろうか。
値を「どこまで分かったか」に置き換える
値を完成品ではなく、どこまで分かったかの記録として捉え直す。
- $x \sqsubseteq y$ を「$x$ の情報は $y$ に含まれる($y$ のほうが詳しい)」と読む
- 何も分かっていない状態を $\bot$(ボトム)と書く。停止しない計算の意味がこれになる
- 無限リストの先頭10要素まで確定した状態は、20要素まで確定した状態より情報が少ない
この順序集合が有向完備(任意の有向部分集合が上限を持つ)なら、有向完備半順序集合(dcpo)と呼ぶ。有向とは「どの2つの途中状態にも、その両方より詳しい状態がある」こと、有向完備とは「情報を増やし続けた行き先が必ず存在する」ことを指す。上限 $\bigsqcup$ が「計算を続けた果て」にあたる。
ここに位相が入る。次の2条件を満たす集合を開集合とするのが、スコット位相だ。
- 上に閉じている($x \in U$ かつ $x \sqsubseteq y$ ならば $y \in U$)
- 有向上限では飛び越えられない($\bigsqcup D \in U$ なら、ある $d \in D$ が既に $U$ に属する)
条件1は「情報が増えても真であり続ける」、条件2は「極限で真になるなら、有限の途中段階で既に真になっている」を意味する。前の章の言葉に訳すと、スコット開集合とは有限の情報だけで肯定できる性質になる。停止性問題で見つけた読み替えが、そのまま意味論の土台になった。
連続写像も、この位相のもとで具体的な形を取る。
$$f \text{ がスコット連続} \iff f \text{ が単調} \ \wedge \ f\left(\bigsqcup D\right) = \bigsqcup f(D)$$「入力の情報が増えれば出力の情報も増える」かつ「極限を先に取っても後に取っても同じ」ということだ。有限の情報から有限の出力を作る計算は、この性質を満たす。無限の情報を一度に見なければ計算できない関数は満たさず、実装もできない。
再帰の意味は近似の果て
$\bot$ を持つ dcpo 上のスコット連続関数 $f$ には最小不動点が存在する(クリーネの不動点定理)。
$$\mathrm{fix}(f) = \bigsqcup_{n \geq 0} f^n(\bot)$$fact の意味は、$\bot$ から出発して定義を1回ずつ展開した近似列の極限として定まる。$n$ 回展開した段階では入力 $n$ 未満だけが正しく、その果てがプログラムの意味になる。停止しない入力の値は $\bot$ のまま残る。
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
$D \cong D \to D$ の壁も同じ発想で崩れる。関数空間をすべての関数ではなくスコット連続な関数だけに制限すれば、濃度の矛盾は起きない。スコットはこうして $D_\infty$ を構成した。「計算できる関数だけを関数と呼ぶ」という制限が、位相の連続性として書けたことになる。
要点
- 情報の順序に位相を入れると、停止しない計算を $\bot$ として意味論の中に置ける
- 再帰的な定義には、最小不動点という一意で自然な解が与えられる
- 遅延評価や無限リストは、有向上限として素直に扱える
ただし距離の直感は捨てる必要がある。スコット位相はハウスドルフではない。$\bot$ を含む開集合は上に閉じているため空間全体しかありえず、$\bot$ とほかの点を開集合で分離できない。「まだ何も返していない計算」を有限の観測で他と区別できないという事実が、分離公理の破れとして現れている。
この章の参考
- 領域理論 - Wikipedia
- Scott continuity - Wikipedia
- Dana S. Scott, “Outline of a Mathematical Theory of Computation”, 1970(原典)
- Dana S. Scott, Christopher Strachey, “Toward a Mathematical Semantics for Computer Languages”, 1971
- Samson Abramsky, Achim Jung, “Domain Theory”, Handbook of Logic in Computer Science(通読向けサーベイ)
嘘をつかない近似の話と抽象解釈
この章の「近い」: 近似の粗さの順序。第3章の枠組みが、実務のツールに降りてくる。
正確に答えれば決定不能、雑に答えれば嘘になる
「この変数がゼロになることはあるか」「この配列アクセスは範囲内か」を、実行せずに知りたい。しかし実行の可能性は無限にあり、全部は試せない。第2章のとおり、正確に答えようとすれば決定不能にぶつかる。
だから近似する。ここで新しい怖さが出てくる。近似が嘘をつけば、保証にならない。「安全側に外す」ことをどう担保するかが問題になる。
ガロア接続が健全性を担保する
パトリック・クザとラディア・クザが1977年に整理した抽象解釈は、この近似を順序と不動点の言葉で定式化した。
- 具体的な意味(すべての実行の集合)と、抽象的な意味(符号、区間、型など)を、それぞれ順序集合として用意する
- 両者をガロア接続 $\alpha: C \to A$、$\gamma: A \to C$ で結ぶ。$\alpha(c) \sqsubseteq a \iff c \sqsubseteq \gamma(a)$ を満たす対で、抽象化しても健全性が失われないことを保証する
- 解析は、抽象領域上の単調関数の最小不動点を求める操作になる。静的解析器がループの解析でやたらと時間を使う場面を見たことがあるだろうか。あれは、この不動点を近似列で求めているところだ
骨格は第3章とまったく同じになる。違いは目的だけで、あちらは意味を定義するため、こちらは解析器を作るために使っている。
順序と位相の関係もここで効く。有限集合の上の位相は前順序と1対1に対応する。アレクサンドロフが1937年に示した対応だ。位相から $x \leq y$ を「$x$ を含むどの開集合も $y$ を含む」と定義すると前順序になり(特殊化順序)、逆に前順序の「上に閉じた集合」を開集合とすると位相になる。位相の $T_0$ 分離公理は、前順序の反対称性に対応する。
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
抽象領域の格子も、部分型関係も、依存関係も、因果順序も、すべて順序構造だ。この対応により、それらはすでに位相空間でもある。「上に閉じた集合が開集合」という規則は、計算の言葉では「いったん成り立てば、情報が増えても成り立ち続ける性質」になる。
要点
- ガロア接続は「粗くしても嘘にならない」ことを保証する枠組み
- 解析の停止性は、順序の高さ(鎖の長さ)の問題になる
- 高さが無限の領域では反復が止まらないので、収束を強制する演算(widening)を入れる
widening は「極限に到達するのを待たず、有限の観測で打ち切る」操作にあたる。有限時間で肯定できることしか扱えないという第2章の制約に対する、実装側からの回答だといえる。
この章の参考
- Abstract interpretation - Wikipedia
- ガロア接続 - Wikipedia
- Patrick Cousot, Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”, POPL 1977(原典)
- P. S. Alexandroff, “Diskrete Räume”, Matematicheskii Sbornik, 1937(有限位相と前順序の対応)
誰も合意できない理由は形にあった話と単体複体
この章の「近い」: 起こりうる実行どうしの近さ。ここで近さは図形になる。
1985年の不可能性
複数のプロセスが1つの値に合意する(コンセンサス)のは、分散システムの基本的な仕事だ。ところがフィッシャー、リンチ、パターソンは1985年、非同期でプロセスが1つでも停止故障しうるなら、確実に合意へ到達するアルゴリズムは存在しないと証明した。FLP 不可能性と呼ばれ、2001年のダイクストラ賞を受けている。
証明は「まだ結果が確定していない状態を保ち続けられる」ことを追う議論で、結論は明快だ。しかし、なぜそうなるのかという直感は残りにくい。しかも「3プロセス中2つまでの故障」のような設定に変えるたび、議論を組み直す必要があった。もっと見通しよく、問題ごとに解けるかどうかを判定できないのだろうか。
1993年、3組が同じ図形にたどり着く
1993年の STOC で、3組の研究者が独立に同じ発想を持ち込んだ。ハーリヒとシャヴィット、ボロフスキーとガフニ、サックスとザハログルー。彼らは実行の全体を図形として描いた。
- 頂点は「あるプロセスが、ある局所状態にある」という事実
- 単体(頂点の組)は「それらの局所状態が同時に起こりうる」という両立関係
- こうしてできる単体複体をプロトコル複体と呼ぶ
すると次が示せる。
- 非同期で停止故障がありうるモデルでは、プロトコル複体は実行が進んでも連結なまま保たれる。隣り合う実行は「あるプロセス1つの見え方」しか違わないため、状態が滑らかにつながっている
- 一方、2値コンセンサスの出力複体は連結ではない。$0$ に決める世界と $1$ に決める世界が離れているからだ
- 連結な複体から非連結な複体への連続写像(単体写像)は存在しない
この図は JavaScript で描画する。JavaScript を有効にすると、図を操作しながら確認できる。
つまり、コンセンサスが解けない理由は「連結な図形を連続写像で切り離せない」という位相の事実だった。実装の工夫で越えられない理由が、形として目に見える。メッセージパッシングモデルについては、ビラン・モラン・ザクスが1990年に連結性による特徴づけを与えている。
要点
- プロトコル複体の連結性が、そのまま合意の不可能性を決める
- 問題ごとに議論を組み直さず、統一的に扱える。$k$-set agreement の不可能性はスペルナーの補題(三角形分割の彩色に関する組合せ的な補題で、ブラウワーの不動点定理と本質的に同値)から従う
- 「何が解けるか」は、入力複体から出力複体への単体写像が存在するかという問題になる
この一連の結果には2004年のゲーデル賞が贈られた。離散的な数え上げが位相の定理を経由して、分散システムの限界を決めている。
この章の参考
- Consensus (computer science) - Wikipedia
- スペルナーの補題 - Wikipedia
- Michael J. Fischer, Nancy A. Lynch, Michael S. Paterson, “Impossibility of Distributed Consensus with One Faulty Process”, Journal of the ACM, 1985(FLP の原典)
- Maurice Herlihy, Nir Shavit, “The Topological Structure of Asynchronous Computability”, Journal of the ACM, 1999
- Maurice Herlihy, Dmitry Kozlov, Sergio Rajsbaum, “Distributed Computing Through Combinatorial Topology”, Morgan Kaufmann(この分野の教科書)
点の集まりに穴を見る話と永続ホモロジー
この章の「近い」: 点群の中の近さ。ただし1つの尺度に決め打ちしない。
スケールを決められない
センサの配置、時系列を埋め込んだ点群、高次元の特徴ベクトル。これらについて「クラスタがいくつあるか」だけでなく「輪になっているか」「穴が空いているか」を知りたい場面がある。しかし点の集まりそのものに、穴という構造はない。
半径 $\varepsilon$ 以内の点を結んで図形を作れば穴は現れる。ところが $\varepsilon$ を小さくすればバラバラの点に、大きくすれば1つの塊になる。適切な $\varepsilon$ を決められないという壁がここにある。
全部のスケールを持ち歩く
エーデルスブルンナーらが2002年に示した答えは明快だった。1つに決めず、全部のスケールを持ち歩けばよい。
- 点群に距離を入れる(第1章と同じく、対象に応じた距離でよい)
- 半径 $\varepsilon$ 以内の点を結んで単体複体を作る(ヴィートリス・リップス複体)
- $\varepsilon$ を $0$ から増やしながら、穴が生まれては埋まる様子を記録する
flowchart LR points["点群<br/>距離空間"] --> complex["単体複体<br/>ε でつなぐ"] --> homology["ホモロジー<br/>穴の個数"] --> barcode["バーコード<br/>いつ生まれ、いつ埋まったか"]
この記録が永続ホモロジーだ。長く生き残る特徴は本質的な構造、すぐ消える特徴はノイズとみなせる。スケールを決め打ちしないことが、そのままノイズ耐性になっている。
要点
- センサネットワークの被覆判定: 通信範囲から複体を作り、穴の有無で隙間を検出できる(デ・シルヴァとグリスト、2007年)
- 時系列の周期性検出: 遅延埋め込みで点群にし、円状の構造(1次元の穴)を見る
- 機械学習の特徴量: 永続ホモロジーの要約統計量を、通常の特徴量に加える
距離から複体を作り、複体から不変量を計算する。この記事でたどった距離・離散・位相の3つを、そのままの順で使う応用になる。
この章の参考
- Persistent homology - Wikipedia
- 単体複体 - Wikipedia
- Herbert Edelsbrunner, David Letscher, Afra Zomorodian, “Topological Persistence and Simplification”, Discrete & Computational Geometry, 2002(原典)
- Vin de Silva, Robert Ghrist, “Coverage in Sensor Networks via Persistent Homology”, Algebraic & Geometric Topology, 2007
- Herbert Edelsbrunner, John Harer, “Computational Topology: An Introduction”, American Mathematical Society
6つの物語が示すもの
並べ直すと、1本の線が見えてくる。どの章も「この対象にとって近いとは何か」を問い直し、答えが出た瞬間に壁が崩れている。そして問い直しのたびに、近さの表現が数値から離れていった。
| 年代 | 分野 | 何と何の近さか | 使った道具 |
|---|---|---|---|
| 1947 | 誤り訂正符号 | ビット列どうし | ハミング距離、球の詰め込み |
| 1936-1980s | 停止性問題 | プログラムの性質どうし | 開集合、コンパクト性 |
| 1969 | 再帰の意味 | 計算の途中状態どうし | 情報の順序、スコット位相 |
| 1977 | 静的解析 | 近似の粗さどうし | ガロア接続、最小不動点 |
| 1993 | 分散合意 | 起こりうる実行どうし | 単体複体、連結性 |
| 2002 | データ解析 | 点群の中の点どうし | 永続ホモロジー |
flowchart LR n1["近さを<br/>数値で測る"] --> n2["近さを<br/>開集合で表す"] --> n3["近さが<br/>順序になる"] --> n4["近さが<br/>図形になる"] n1 -.- c1["誤り訂正符号"] n2 -.- c2["停止性問題"] n3 -.- c3["意味論・静的解析"] n4 -.- c4["分散合意・データ解析"]
用語の対応も表にしておく。左の位相の言葉が、右の計算の言葉としてどう読めるかという対照表だ。
| 位相の概念 | コンピュータサイエンスでの読み替え | 主に登場する章 |
|---|---|---|
| 距離・球 | ハミング距離、編集距離、埋め込みベクトルの近さ | 第1章 |
| 開集合 | 有限時間で肯定できる性質(半決定可能な述語) | 第2章、第3章 |
| 閉集合 | 反証だけが半決定可能な性質 | 第2章 |
| 開かつ閉 | 決定可能な性質 | 第2章 |
| コンパクト性 | 有限時間で終わる全探索 | 第2章 |
| 連続写像 | 有限の出力が有限の入力だけで決まる計算 | 第2章、第3章 |
| 収束・極限 | 近似列の果て、再帰の意味、不動点 | 第3章、第4章 |
| 特殊化順序 | 情報の多さ、部分型、抽象度の順序 | 第4章 |
| 連結性 | 状態を2つの世界に分離できない | 第5章 |
| ホモロジー(穴) | データの形、被覆の隙間、周期構造 | 第6章 |
その他の接点
章として立てるほどの分量はないが、同じ系譜にある話題を短くまとめておく。
- ストーン双対性と型・論理: ブール代数はストーン空間、分配束はスペクトル空間、フレームはロケールと、それぞれ互いを決め合う関係にある。「性質を並べた代数」と「性質を満たすものの空間」は裏表だ。アブラムスキーの
Domain theory in logical formは、意味論の領域と観測可能な性質の論理を対応づけた。第2章の「開集合=観測可能な性質」を、代数の側から見た姿にあたる - ホモトピー型理論: 型を空間、項を点、等式型を道の空間とみなす見方。証明支援系(Cubical Agda など)として動く形式体系になっている
- 三角不等式による枝刈り: $d(q, x) \geq \lvert d(q, p) - d(p, x) \rvert$ を使えば、距離を1回測るだけで候補を捨てられる。BK-tree や VP-tree の枝刈りはこれを根拠にしている。逆に、余弦類似度のように三角不等式を満たさない量を距離として扱うと、索引が静かに誤る
- バナッハの不動点定理: 完備な距離空間で $d(f(x), f(y)) \leq c \cdot d(x, y)$($c < 1$)を満たす写像には一意な不動点がある。第3章が「順序と最小不動点」で再帰を扱ったのに対し、こちらは「距離と一意不動点」で同じ役割を果たす。数値反復の収束や、並行プロセスのメトリック意味論で使われる
- ネットワークトポロジー: こちらの「トポロジー」はグラフの形状の話で、位相空間論の定理を使っているわけではない。語が共通するだけで、この記事の内容とは直接つながらない
おまけ: 実務にどう持ち帰るか
ここまで読んで「面白いが、明日の仕事とは関係ない」と思われたかもしれない。実際、位相の定理を実装に埋め込む機会はほとんどない。それでも、判断の材料としては持ち帰れるものがある。
1. 「距離」を名乗る量には公理を確認する。埋め込みベクトルの類似度、独自に定義した近さのスコア、ドメイン固有の差分。索引や枝刈りに使う前、三角不等式が成り立つかを一度は確かめたい。成り立たない量で枝刈りをすると、落ちるはずのない候補が静かに落ちる。壊れ方が静かなぶん、あとから気づきにくい。
2. 仕様を「肯定が有限で終わるか」で分ける。ヘルスチェック、リトライ、タイムアウトの設計は、結局のところ「YES はいつか分かるが NO は分からない」という非対称さの扱いだ。第2章の言葉でいえば、開集合しか観測できない世界で、どこに打ち切りを置くかという設計になる。「NO を確定できない項目に、確定を前提とした分岐を書いていないか」は見直す価値がある。
3. 近似には順序と不動点を用意する。第4章の骨格は静的解析に限らない。段階的に情報を増やす処理(キャッシュの温まり、再試行つきの収束、段階的ロールアウトの判定)は、順序と単調性を決めておくと設計が安定する。そして高さが無限なら、widening にあたる打ち切りを最初から用意しておく。
4. 不可能性は、早めに知るほど得をする。第5章が示すのは「実装の工夫では越えられない壁がある」という事実だ。非同期のモデルで完全な合意を目指す設計は、始める前に止められる。銀の弾丸がないと分かっていること自体が、設計上の判断材料になる。
5. 分からない対象は、まず距離が入るかを問う。距離が入るなら第1章の道具立てがそのまま使える。入らないなら、何が有限時間で観測できるかを列挙する。この2択で切り分けるだけでも、扱いあぐねている対象の輪郭が見えてくる。
用語ミニ辞典
本文で使った言葉をかみ砕いておく。厳密な定義は本文と参考文献に譲り、ここでは「だいたいこういうもの」という感覚を示す。
| 用語 | かみ砕くと |
|---|---|
| 開球 | ある点から距離 $r$ 未満の点を全部集めた「近所」 |
| 開集合 | どの点も「近所ごと」入っている集合。ふちギリギリの点がない |
| 閉集合 | 開集合の補集合。ふちを含んでいる集合 |
| 開かつ閉(clopen) | 開集合でも閉集合でもある集合。計算では「決定可能」にあたる |
| 近傍 | ある点を内側に含む範囲。有限の観測で区別できない範囲のこと |
| 連続写像 | 出力の近さを保証するために、入力の近さだけを見ればよい写像 |
| ハウスドルフ | どの2点も、互いに交わらない近傍で引き離せるという性質 |
| コンパクト | 「無限に広がっていない」という性質。全探索が有限で終わることに対応する |
| 連結 | 2つの離れた塊に分けられないという性質 |
| 半決定可能 | 成り立つときは有限時間で確かめられるが、成り立たないときは答えが出ないこと |
| 前順序 | 「$x \leq x$」と「$x \leq y$ かつ $y \leq z$ なら $x \leq z$」だけを満たす関係 |
| 単体複体 | 点・辺・三角形・四面体などを貼り合わせた図形を、頂点の集合の組合せで表したもの |
| dcpo | 情報の順序が入っていて、情報を増やし続けた行き先が必ず存在する集合 |
| $\bot$(ボトム) | 何の情報も持たない値。停止しない計算の意味 |
| 最小不動点 | $f(x) = x$ を満たすもののうち、情報がいちばん少ないもの |
| ガロア接続 | 詳しい世界と粗い世界を、意味を壊さずに行き来させる写像の組 |
| ホモロジー | 図形にあいた「穴」の個数などを、代数の言葉で数えたもの |
注意点
- 各章の物語は要点だけを取り出しており、実際には多くの研究者による積み重ねがある。年号は主要な論文が出た時期の目安として読んでほしい
- ハミングの逸話は本人の回想にもとづく要約であり、発言をそのまま引用したものではない
- スコット位相はハウスドルフ性を満たさず、距離からは生成できない。「近い点は分離できる」という距離空間の直感を持ち込むと誤る
- 位相的な議論が強いのは、意味論の基礎づけと不可能性の証明であり、日々の実装を直接高速化するものではない。第1章や第6章のほうが実装には近い
- 永続ホモロジーの計算量は素朴な実装で点数の3乗規模になりやすく、大規模データにそのまま適用するのは難しい
- 「開集合=半決定可能」「コンパクト=全探索が終わる」という対応が成り立つのは、適切な位相を入れた場合に限られる
まとめ
- 6つの場面はどれも、行き詰まったところで「近いとは何か」を定義し直し、その定義が壁を壊している
- 第1章: ハミング距離が距離の公理を満たすと気づくと、符号設計は球の詰め込みに変わり、訂正能力と情報量の綱引きを1つの幾何で表せる
- 第2章: 「有限時間で肯定できる」を開集合と読むと、半決定可能=開、決定可能=開かつ閉となり、コンパクト性から「決定可能なら有限の接頭辞で判定できる」が従う
- 第3章: 値を情報の順序に置き換えると位相が入り、停止しない計算を $\bot$ のまま含めて再帰の意味を最小不動点として定義できる
- 第4章: 抽象解釈はガロア接続と最小不動点で近似の健全性を保証する。順序はそのまま位相でもある
- 第5章: 実行の全体を単体複体として描くと、合意の不可能性が「連結な図形を切り離せない」という位相の事実になる
- 第6章: スケールを1つに決めず全部持ち歩けば、点群の形がノイズに強い特徴量として取り出せる
- 距離で足りるなら距離のまま済ませ、距離を入れられない対象に出会った段階で位相まで上がる。この使い分けが、6つの章に共通する判断だといえる
さらに読む
各章の原典と論文は「この章の参考」に置いた。ここでは全体を通して読む本を挙げる。
- James R. Munkres, “Topology”, Prentice Hall(位相空間論の定番の教科書)
- 内田伏一『集合と位相』裳華房(日本語で読める入門書)
- G. Gierz et al., “Continuous Lattices and Domains”, Cambridge University Press(順序と位相の関係を体系的に扱う)
- Steven Vickers, “Topology via Logic”, Cambridge University Press(この記事の第2章・第3章の視点そのもの)
- Maurice Herlihy, Dmitry Kozlov, Sergio Rajsbaum, “Distributed Computing Through Combinatorial Topology”, Morgan Kaufmann(第5章を本格的に追う場合)
- Richard W. Hamming, “The Art of Doing Science and Engineering”, Gordon and Breach(第1章の背景にある本人の回想)
- Samson Abramsky, “Domain Theory in Logical Form”, Annals of Pure and Applied Logic, 1991(意味論と論理の双対性)
- Peter T. Johnstone, “Stone Spaces”, Cambridge University Press(ストーン双対性)
- The Univalent Foundations Program, “Homotopy Type Theory: Univalent Foundations of Mathematics”, 2013(型と空間の対応)