第9章：コンピュータ科学と数学的「if」――アルゴリズムと型理論

――実行される論理、真理としての計算

9.1 二つの「if」の遭遇：命令と真理の交差点

現代文明を根底から支えているコンピュータの深淵において、「if」という言葉は二つの全く異なる、しかし表裏一体の顔を持っている。

第一の顔は、プログラミングにおける「条件分岐（Conditional Branching）」としての if である。これは「もし条件 $P$ が成り立つならば、処理 $A$ を実行せよ。さもなくば処理 $B$ を実行せよ」という、時間軸に沿った命令（Imperative）である。 第二の顔は、本稿でこれまで探求してきた「論理含意（Logical Implication）」としての $P⟹Q$ である。これは「命題 $P$ が真であれば、命題 $Q$ も真である」という、時間を超越した恒久的な真理関係の記述である。

プログラマがキーボードで打ち込む if は、回路の中を走る電気信号を切り替える物理的なスイッチの操作であり、数学者が紙の上に書く $⟹$ は、イデアの世界における真理の道を指し示す標識である。一見すると、この「物理的な行動」と「論理的な関係」の間には、深い溝があるように見える。

しかし、コンピュータ科学の歴史とは、まさにこの二つの「if」を統合していくプロセスであった。ライプニッツが夢見た「計算（Calculemus）による紛争の解決」は、現代において「型理論」や「形式検証」という形で結実し、プログラムが「正しく動くこと」と、数学的に「正しいこと」を、論理の言葉で一つに結びつけたのである。本章では、この計算機の「if」が、いかにして数学的「if」という高貴な魂を得るに至ったのか、その劇的な物語を解剖していく。

9.2 チューリングの「if」と知の限界：停止性問題という断崖

コンピュータ科学の父、アラン・チューリングが1936年に発表した論文は、人類の知性に衝撃を与えた。彼は「万能チューリングマシン」という抽象的な計算モデルを構築したが、その動作の基本は、驚くほど単純な「if」の連鎖であった。

9.2.1 状態遷移としての「if」

チューリングマシンの定義において、計算とは次のようなルールの積み重ねである。 「もし、現在の内部状態が $q$ で、テープから読み取った記号が $s$ であるならば、記号 $s^{\prime }$ を書き込み、ヘッドを $d$ 方向に動かし、状態を $q^{\prime }$ に移行せよ。」

このミクロな「ならば」の連鎖によって、人類が行うあらゆる「計算」が再現可能であることが示された。ここでは、数学的な「if」は、ステップ・バイ・ステップの具体的な「動作」へと完全に分解されている。

9.2.2 停止性問題：判定不可能な「if」の発見

チューリングはこのモデルを用いて、論理学的な究極の問いに挑んだ。 「あるプログラム $M$ に入力 $x$ を与えたとき、そのプログラムがいずれ計算を終えて停止するかどうかを判定する『万能な if 文（プログラム）』は存在するか？」

もしそのような判定プログラム $H(M,x)$ が存在するならば、私たちはすべてのアルゴリズムの運命を事前に予見できることになる。しかしチューリングは、背理法（第5章）を用いて、そのようなプログラム $H$ は論理的に存在し得ないことを証明した。

ここにあるのは、数学的「if」の暴力的なまでの限界である。「もし～ならば」をどれほど積み重ねても、計算という物理的行為のすべてを事前に予測し、判定することはできない。チューリングの発見は、コンピュータという「論理の権化」の中に、論理そのものでは捉えきれない「深淵」があることを浮き彫りにしたのである。

9.3 ホーア論理：バグという「偽」を許さない数学的規律

1960年代、ソフトウェアが巨大化し、人間の手に負えなくなったとき、アントニー・ホーアは「プログラムの動作を数学的な証明として記述する」という革命的なアイデアを提唱した。これがホーア論理（Hoare Logic）である。

9.3.1 ホーア三つ組：$\{P\}S\{Q\}$

ホーアは、プログラムの各ステップに、数学的な「if」を組み込んだ「ホーア三つ組」という形式を与えた。 $\{P\}S\{Q\}$ これは次のように読み解かれる。「もし、実行前の状態が条件 $P$（事前条件）を満たしているならば、プログラム $S$ を実行した後、その状態は必ず条件 $Q$（事後条件）を満たしている。」

この構造において、プログラムのコード $S$ は、もはや単なる命令の羅列ではない。それは、前提 $P$ から結論 $Q$ を導き出すための、物理的な「証明」そのものとなったのである。

9.3.2 ループ不変量：時間を超える「恒久的な if」

特に、プログラムにおける繰り返し（ループ）構造を証明するために、ホーアは「ループ不変量（Loop Invariant）」という概念を導入した。 「もし、繰り返しが始まる前に条件 $I$ が真であり、かつ繰り返しの一回一回がその真実を壊さないならば、何万回繰り返した後でも $I$ は真である。」

これは第5章で学んだ「数学的帰納法」のコンピュータ科学的実装である。プログラミングにおける if 分岐やループの中に、数学的な不変性を持ち込むことで、ホーアは「テスト（実際に動かしてみること）」ではなく「証明（論理的な保証）」によってソフトウェアの正しさを保証する道を開いた。数学的「if」は、ここでは混沌としたコードを支配する「法」としての役割を担っている。

9.4 チャーチ・ブーリアン：関数という「if」の構成

コンピュータ科学のもう一人の巨人、アロンゾ・チャーチは、チューリングとは異なるアプローチで計算を定義した。彼のラムダ計算（Lambda Calculus）は、現代の関数型プログラミング（Lisp, Haskell, OCamlなど）の聖典である。

9.4.1 if を使わずに if を作る

驚くべきことに、チャーチの世界には、最初から用意された if 文は存在しない。彼は、純粋な「関数」だけを使って、論理的な「if」をゼロから構築してみせた。

• True := $\lambda x.\lambda y.x$ （二つの引数のうち、一つ目を選ぶ関数）
• False := $\lambda x.\lambda y.y$ （二つの引数のうち、二つ目を選ぶ関数）

この定義において、if Condition then A else B は、単なる関数の適用 Condition A B となる。もし Condition が True であれば $A$ が返り、False であれば $B$ が返る。

ここにあるのは、物理的な条件分岐としての if ではなく、純粋な「選択」という論理的な本質としての「if」である。チャーチ・ブーリアンは、私たちが当たり前のように使っているコンピュータの命令が、その実体においては、純粋数学的な「関数の適用」という高度に抽象化された行為に還元できることを示している。数学的「if」は、ハードウェアのスイッチを離れ、純粋な「情報の型」へと昇華されたのである。

9.5 カリー＝ハワード同型対応への序曲：命題と型の結婚

20世紀後半、数学とコンピュータ科学の間に、ある「奇跡的な一致」が発見された。それが、本章の後半で詳述するカリー＝ハワード同型対応（Curry-Howard Isomorphism）である。

これまでの章で学んできた数学的な「もし $P$ ならば $Q$」という命題。 そして、コンピュータ科学における「型 $P$ のデータを受け取り、型 $Q$ のデータを返す関数」。

この二つが、実は論理的な構造において完全に同一であるというこの発見は、知の歴史における最大の衝撃の一つであった。数学で証明を綴ることは、コンピュータで関数を書くことと同じであり、コンピュータでコードがコンパイルを通ることは、その背後にある論理的な「if」の正しさが証明されたことを意味する。

数学的「if」は、ここにおいてついに、紙の上の沈黙を破り、計算機の中で鼓動し、実行され、世界を書き換える「プログラム」としての実体を得ることになったのである。

---

9.6 カリー＝ハワード同型対応：命題は型であり、証明はプログラムである

20世紀後半、数学者ハスケル・カリーと計算機科学者ウィリアム・アルヴィン・ハワードによって、人類の知の歴史を塗り替える驚くべき発見がなされた。それが「カリー＝ハワード同型対応（Curry-Howard Isomorphism）」である。この理論は、一見すると全く別個のものに見えていた「数理論理学」と「計算型理論」が、実は数学的な構造において完全に同一であることを示した。

9.6.1 「ならば（$⟹$）」の正体としての「関数型（$\to$）」

本稿のテーマである「もし $P$ ならば $Q$」という論理含意を、カリー＝ハワード同型対応の視点から再定義してみよう。

• 論理学の世界： $P⟹Q$ は、命題 $P$ が真であれば命題 $Q$ も真であることを主張する「命題」である。
• 計算機科学の世界： $P\to Q$ は、型 $P$ のデータを受け取り、型 $Q$ のデータを返す「関数の型」である。

この二つは、単に似ているのではない。論理学において命題 $P⟹Q$ を証明するという行為は、計算機科学において型 $P$ から型 $Q$ への変換を行う関数プログラムを記述することと、論理的に一対一に対応しているのである。ここにおいて、「ならば」という言葉は、静的な真理の記述から、ある情報を別の情報へと変換する「動的な変換プロセス（プログラム）」へとその姿を変えた。

9.6.2 直観主義論理：構成的な「if」

この同型対応が真に威力を発揮するのは、第1章でも触れた直観主義論理の文脈である。直観主義において、命題 $P⟹Q$ が「真である」とは、「もし $P$ の証明（証拠）が与えられたなら、それを使って $Q$ の証明を組み立てる具体的な方法が存在する」ことを意味する。

これは、計算機科学における「関数の実行」そのものである。関数とは、入力（前提の証拠）を受け取り、計算という手続きを経て、出力（結論の証拠）を生成する機械である。数学における「if」は、カリー＝ハワード同型対応を通じて、ただの抽象的な主張であることをやめ、実際に「実行可能」な、実体を持った手続きへと進化したのである。

9.7 依存型と述語論理の統合：定理証明支援系のメカニズム

第6章で学んだ「述語論理（$\forall$ や $\exists$）」もまた、型理論の世界では「依存型（Dependent Types）」という高度な概念として再解釈される。

9.7.1 全称記号 $\forall$ は「依存積型」である

「すべての $x$ について、もし $P(x)$ ならば $Q(x)$ である」という全称命題を考えてみよう。これを型理論で解釈すると、「任意の入力 $x$ を受け取り、その $x$ に応じた型 $Q(x)$ のデータを返す関数」（$\Pi$型、依存積型）となる。

ここでの「if」は、さらに柔軟で強力なものとなる。入力 $x$ の値に応じて、返される出力の「型」そのものが変化する。数学における普遍的な法則は、プログラミングにおける「高度に一般化されたジェネリックな関数」として実装されるのである。

9.7.2 定理証明支援系（Lean, Coq, Agda）の台頭

この依存型理論を基盤として、現代数学の最前線では Lean, Coq, Agda といった「定理証明支援系（Proof Assistants）」が活用されている。 数学者が紙の上に書く証明は、時として論理的な飛躍や誤りを含む。しかし、定理証明支援系において、数学者は証明を「プログラム」として記述する。コンピュータの型チェッカー（コンパイラ）は、その「プログラム」が論理的に正しいかどうかを、一文字のミスも許さず機械的にチェックする。

「もしコンパイルが通るならば、その定理は数学的に正しい」。 数学的「if」は、ここにきて、人間の曖昧な納得に頼ることをやめ、機械による冷徹かつ完璧な検証の対象となった。現在、フィールズ賞受賞者らを含むトップクラスの数学者たちが、数学の全体系を Lean などの言語で記述し直す「数学のデジタル化」プロジェクトを進めている。数学的「if」は、人類共通の「実行可能な知のデータベース」へと蓄積されつつある。

9.8 形式検証（Formal Verification）：バグを「不条理」に変える力

コンピュータ科学における「if」の厳密性は、私たちの現実世界の安全性と直結している。航空機の制御システム、原子力発電所の管理、心臓ペースメーカーのソフトウェア。これらの領域において、バグ（論理的な誤り）は文字通り「死」を意味する。

9.8.1 「テスト」から「証明」へ

従来のソフトウェア開発では、膨大な数のテストケースを入力し、バグがないかを確認していた。しかし、第6章で学んだ通り、$\forall x$（すべての入力）に対してテストを行うことは、組み合わせ爆発のために不可能である。 ここで形式検証が登場する。形式検証は、プログラムが仕様を満たしていることを、数学的な「証明」として構成する。

「もし、プログラムのソースコードが数学的な仕様 $S$ を満たすことが証明されたならば、どのような入力 $x$ が与えられたとしても、バグは絶対に発生しない。」

これは、バグを「単なるミス」から、論理的な「矛盾（第5章）」へと昇華させる作業である。矛盾が含まれないことが証明されたプログラムは、宇宙が崩壊しない限り、仕様通りに動くことが保証される。インテル社のCPU設計や、Amazonのクラウドシステムの基幹部分など、現代のインフラの最重要部は、この数学的「if」による鉄壁の証明によって守られている。

9.9 関数型プログラミングのエレガンス：純粋な「if」の追求

現代のプログラミング言語の中でも、特に Haskell のような純粋関数型言語は、数学的な「if」の美しさを最も色濃く受け継いでいる。

9.9.1 副作用の排除と論理的一貫性

多くの言語では、if 文の中で「画面に文字を出す」「変数の値を書き換える」といった、論理学とは無関係な「副作用」が許されている。しかし、純粋関数型言語では、関数は数学的な関数と同じく、入力を出力に変えるだけである。

ここでの if は、第1章で学んだ真理値表に限りなく近い。 if P then A else B は、単なる条件分岐ではなく、一つの「値」を表現する数式となる。この純粋性があるからこそ、プログラムを代数方程式のように変形し、最適化することが可能になる。数学的な「if」の厳密性は、プログラミングにおける「保守性」や「予測可能性」という実利的な価値へと直接結びついているのである。

9.9.2 パターンマッチング：洗練された「場合分け」

関数型言語で多用される「パターンマッチング」は、第5章で学んだ「場合分けの証明」の直接的な実装である。 「もしデータがこの形（$P_1$）ならば、この処理をせよ。もしこの形（$P_2$）ならば……」 プログラムがすべてのケース（if）を網羅していることを型システムが保証することで、抜け漏れによるエラーを未然に防ぐ。数学における「尽挙法」という泥臭い戦術は、コンピュータサイエンスにおいて「型による安全なプログラミング」という洗練された芸術へと進化した。

9.10 第9章の結語：論理が現実を計算する時代

本章では、数学的「if」がコンピュータ科学という新たな肉体を得て、いかにして「実行される知能」へと進化したかを詳述した。

• 命題論理の「含意（$⟹$）」は、型理論の「関数（$\to$）」として実体化された。
• チューリングの「停止性問題」は、論理だけでは捉えきれない計算の深淵（限界）を示した。
• 定理証明支援系は、数学の証明をプログラムの検証へと統合した。
• 形式検証は、社会の安全を「数学的必然（if）」によって担保する道を開いた。

数学における「if」は、もはや紙の上の概念ではない。それは、この世界を動かすアルゴリズムの正当性を支える、目に見えない骨組みである。論理的に「正しい」ことは、計算機によって「実行可能である」ことと結びつき、人類の知性は、かつてないほどの確実性を持って未来を構築し始めている。

しかし、このように厳密を極めた数学的・計算機的な「if」の世界を知れば知るほど、私たちは一つの大きな謎に直面することになる。それは、私たちが日常的に、あまりにも軽やかに使いこなしている「もし～ならば」という言葉の、底知れない曖昧さと豊かさである。なぜ数学の「if」はこれほどまでに冷徹であり、日常の「if」はこれほどまでに人間的なのか。次章では、この「論理と心理」の決定的断絶を掘り下げ、数学的厳密性が人類の思考に何をもたらしたのか、その光と影を考察していく。

---