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

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

コンピュータの深淵において、「if」は二つの顔を持ちます。

コンピュータ科学の歴史とは、この「動作」としての if と「真理」としての if を統合するプロセスでした。

アラン・チューリングは、「あるプログラムがいずれ停止するかを判定する万能な if 文（アルゴリズム）は存在するか？」という問いに対し、それは論理的に不可能であることを証明しました。数学的「if」には、計算という物理的行為では決して辿り着けない深淵があるのです。

「このプログラムにバグがない」ことをどう保証するか。ホーア論理は、プログラムの各ステップを数学的な「if」として記述します。

${P} S {Q}$ （もし実行前の状態が $P$ ならば、プログラム $S$ の実行後は必ず $Q$ になる）プログラムを書くことは、数学的な「if」を物理的に実装することに他なりません。

20世紀、数学とコンピュータ科学の間に「命題は型であり、証明はプログラムである」という衝撃的な一致が発見されました。

数学： $P ⟹ Q$ （含意）
CS： $P \to Q$ （関数型）数学で「もし $P$ ならば $Q$ 」を証明することは、型 $P$ のデータを受け取り型 $Q$ のデータを生成する関数を書くことと、論理的に全く同じ作業なのです。

数学における「if」は、もはや紙の上の概念ではなく、世界を動かすアルゴリズムの正当性を支える骨組みです。次章では、このように厳密を極めた「数学的 if」と、私たちが日常使っている「曖昧な if」の間の、決定的で興味深い断絶について考察していきましょう。