私たちは物理の世界に産まれました。
我々の世界で電子計算機が発明されたのは20世紀中ごろになってからです。
しかし我々と違い電子計算機の中に産まれ、かつそのハードウェアに直接触れ観測できるような知的存在であればそうはならなかったはずです。

数学と計算機

数学が産まれたのは先史時代のことです。
その後、いろんな有名な数学者によってなんやかんやだいたいずっと進歩してきました。
個人的に挙げたい成果はユークリッドとかペアノとかによる公理系、ゲーデルの不完全性定理あたりです。

論理学の始まりは古代エジプトだかバビロニアだかだそうですが、紀元前3世紀アリストテレスの論理学が長い間主流を作りました。
それからしばらく進展があり、14世紀から19世紀というとてつもない停滞があり、19世紀には記号論理学が産まれます。
その後フレーゲの仕事とかラッセルとホワイトヘッドによる『プリンキピア・マテマティカ』とかで論理学により数学がだいたい形式的に定義できそうだと示されました。

計算機科学はだいたい20世紀中頃のアラン・チューリングです。
チューリングマシンは計算機の数学的なモデルであり、停止性問題からはゲーデルの第一不完全性定理を示せます。
実際の計算機は物理学の中の電磁気学を基礎とする電子工学あたりで出来ています。
電子計算機が出来てから現在に至るまで、数多の技術者・経営者・企業が歴史を飾っていますがそれは今はどうでも良いです。

ですから、大雑把に言って論理学の上に数学があり、数学の上に計算モデルがある。
ただ実際には論理学が数学の基礎を作っているかといえばそういうことはない。発展もほぼ独立。
物理的な計算機自体はもちろん物理世界にあって物理法則が支配する。当然ですが。
そういう感じになります。

20世紀まで誕生しなかった計算機が数学・論理学・物理学の基礎だと考える人はそう多くはないでしょう。
もちろん現在のあらゆる学者、というより全人類がコンピューターを使っているわけで、諸学問はある程度計算機上で表現されています。

Wikipedia『数学史』
Wikipedia『論理学の歴史』
佐々木力 2010年『数学史』

計算機から始まる学問史

計算機の中で生まれた知的存在がどのような学問を形成するかを考えてみましょう。
これは稚拙なフィクションに過ぎませんが、普段と異なる視点で世界を見るのに役立つ思考実験でもあります。
「計算機の中で生まれた知的存在」は長いので以下「彼ら」とします。

博物学

彼らの最も素朴な学問は、様々なプログラム自体と、その実行記録です。つまりライブラリです。
多くの問題に利用できるライブラリがあり、極めて大規模なランタイムが存在します。
また先行の実行記録があり、それを利用することで計算資源の節約が可能です。

その中には多数の数学的問題も存在します。
プログラムにより直接的に表現可能な数学の定理はいくつかあり、特に有名なのは四色定理です(複雑な手続きで変換が必要だそうですが)。
数学系のライブラリも存在し、彼らは数学自体を発見する以前から、数学的な意味のある諸問題を解決してきました。

物理学

彼らはあっさりと世界における基礎的な命令セットを発見します。
我々が素粒子に到達するまでに比べれば羨ましい話ですが、それなりに大変かもしれません。
数学を持たない彼らは各命令の実行前と実行後による計算機の振る舞いを一覧表にして、「そういうものだ」と受け容れます。

最適化学

彼らは異なるプログラムが同じ振る舞いをすることに気付きました。
彼らが作り上げたのは「最適化学」とでも呼ぶべきでしょうか。

ちなみに「計算結果はあらかじめ決まっている？」の記事で述べた「繰り返し実行比較プログラム」はこの最適化学的なものが頭にあっての発想です。

初期

初期の最適化学はかなり博物学的で、二種類のプログラムを収集します。
彼らは手探りで条件を満たすプログラムを発見します。

最適化プログラム

(\forall n \in \Sigma^*,\forall a)  \bigl(\text{Optimize}(n)\bigr)(a)=n(a)

(この数式っぽい奴を書くのは久しぶりなので合ってるか自信がありません。)

これはプログラムnを入力に取り、全く同じ挙動(同じ入力に対し同じ答えを返す)をするプログラムを出力するものです。
入力と出力が同じ場合もある、というか大抵はそうでしょう。
要するに最適化とかリファクタリングをするプログラムです。逆に長く・遅くなる場合もあります。

例として「nopの挿入・削除(nopがあれば)」「空ループの除去」「計算結果のキャッシュ」「同じ計算による結果の比較をtrueに置き換える」「加算の繰り返しを積算に置き換える」のような操作があります。

同一挙動判定プログラム

\text{Equal}(n,m) = \left\{
\begin{array}{ll}
1 \lor 0 & \text{if}\bigl(\forall a\bigr)n(a)=m(a) \\
0 & otherwise.
\end{array}
\right.

これは二つのプログラムが同じ挙動をする場合にのみ1を返すプログラムです。判断できなければ0を返します。
最適化プログラムがプログラムの変形を行うのに対し、こちらは変形できるか否かを判定します。
なお、一般的な同一挙動判定プログラムは存在しません。

網羅性チェック

初期の最適化学は経験的で曖昧で、学問というより実用的なテクニックでした。
最適化や挙動の同一性判定を全ての場合に対し保証するのは容易ではありません。
最適化では入力がどんなプログラムでも、入力と出力のプログラムにどんな入力が与えても同じ挙動をしなければなりません。
同一挙動判定が1を返す場合は、2つの入力プログラムがどのような入力に対しても同じ挙動をしなければなりません。

入力プログラムに関しては対応するプログラムを限定すれば簡単です。
対象外の入力に対し、最適化なら入力と同じ出力を、同一挙動判定なら0を返せば良いだけです。
問題は入出力するプログラムが全ての入力に対し同じ挙動をしていることを保証・判断しなければならない点です。

素朴には最適化により変化する処理の部分の開始時、結果に影響する全ての入力(チューリングマシンではテープに移動範囲)で実行し、終了時の結果が全て同じであることを確認します。
より複雑な問題にはシンプルな仮想マシンでの最適化を考えるのが便利です。二進数ベースであれば網羅性チェックは比較的簡単です。

最適化学から見た論理学

我々の世界認識には「それ自体の真偽は分からないが、論理式では記述できる命題」が自然に存在します。
例えば1号室と2号室しかない建物にAさんが入っていくのを見た場合、『「Aさんが1号室に居る」または「Aさんが2号室に居る」』は真です。廊下は無視します。
恐ろしいことに我々の世界には素朴に「重ね合わせ」という論理式で示せるような状態が存在しますが、基本的に我々が個別の命題をその真偽ではなく論理式で表現しなければならないのは我々の都合です。

極めて高い観測能力を持つ彼らにとって論理学は我々ほど自然なものではありません。
我々がプログラミングや計算機設計の際に論理を用いて行う推論を、彼らは最適化学の知見を用いて行います。
ただ二進数のビット演算を用いたループを持たない計算機モデルにはほぼ間違いなく到達しますし、それはもう論理学です。
網羅性チェックという点で論理学に相当するモデルはかなり便利です。
論理学は歴史的にも定式化でも最適化学の派生学問となります。

一階述語論理計算機

ここで一階述語論理計算機と呼べるものを考えます。
これは単純に入力(テープの初期状態)として論理式と各命題の真偽を与え、論理式の評価を出力します。
一階述語論理計算機がチューリングマシンで実装できることは明らかですが、簡単に説明します。

一階述語論理計算機は多テープチューリングマシンです。
第0テープに論理式、第1テープは変数以外の真偽、第6テープ以降は変数の真偽が保持されます。
第0テープのヘッダは常に右に移動し、第1テープ以外は自由に移動、第1テープはスタックのように振る舞います。
スタックにしたのは一つテープが少なくて済むからです。
なお一階述語論理計算機は一般的な繰り返し処理が書けないのでチューリング完全ではありません。

要するに逆ポーランド記法です。

基本コマンド

論理記号	命令	説明
$x_n$	`var(n)`	第2テープのnの位置が示すテープ番号で、nの位置の値を、第1テープのスタックにプッシュする。
$\neg$	`neg();`	第1テープのヘッダ位置を、その否定に書き換える。
$\land$	`and();`	第1テープのスタックから値を2つポップし、その論理積をプッシュする。
$\lor$	`or();`	〃論理和〃
$\supset$	`imp();`	〃論理包含〃。
$\equiv$	`equiv();`	〃同値〃。
$\forall x_n$	`forall(n in a,b,c...);`	一種のループ。第2テープのnの位置にa,b,cと代入していく。 `end;`時に偽だった場合に中断。コールスタックは第3テープ。今のnがいくつめかは第4テープ。第1テープの位置は第5テープ(どうでも良い)。
$\exists x_n$	`exists(n in a,b,c...);`	上の真偽を入れ替えたもの。
	`end`	ループの終了。
	`true();`	真を出力し停止します。なくても良いが、`true()`一文に最適化すると考えた方がすっきりする。
	`false();`	偽を出力し停止します。
	`halt();`	第2テープのスタック先頭を出力し停止します。

まぁこんなこと書かずとも、真偽を入力に取り論理式の評価を出力するプログラムが書けることは自明です。
真理関数ともいうので当たり前です。
論理式がそのまま命令セットになったような雰囲気を伝えたかっただけです。結構怪しいですが(ループとか)、雰囲気です。
(命題論理で良いのに述語論理にしてしまい苦労しました。しかも命題論理で考えた方が直感的で分かりやすい気さえします。)
量化の対象が有限個でない場合は同じ組み合わせをグループでまとめて考えれば良いでしょう。

推論規則

一階述語論理の推論規則は最適化学における最適化プログラムとして表現できます。
ただし一つの計算機を最適化していく関係上、導出は論理式の最後に$\land$で繋いで追加するイメージです(あるいは複数テープで論理式を表現するような拡張でも良いです)。
網羅性チェックは真理値表を使うことで比較的容易にできると思います。
最終的にtrue();やfalse();一文に変換することができれば、入力によらず真や偽であることを分かりやすく証明できます。

考察

こうして考えると最適化学の一種として論理学を定式化した方が自然です。
普通に考えて論理式は各命題の真偽を入力値として持ち命題の真偽を出力する関数ですし、推論規則の適用は網羅性が補償された最適化ですし、入力値によらない議論を行っています。
論理学で数学を、数学で計算機モデルを、計算機モデルで最適化学を定式化するよりいくらか直感的な点はあります。
実際のところこれはどっちでも良いのですが、論理学や数学に関する哲学的な問いに答える時には時折便利です。
選択公理のような問題も最適化学はともかく、計算機による数学や論理学の定式化の優位性を示唆します。

ただ最適化学だけでは最適化の妥当性を保証するハードルは結構高いです。
いくつかの議論で暗黙に論理を使っています。
とはいえ例えば論理学の推論規則を論じる際の議論はある程度非形式的だったりするので、基礎が曖昧なのは同じようなものかもしれません。

数学

彼らはおそらく非形式的証明を持ちません。
もちろん「知的存在」である限りあり得ないとは言いませんが、計算機の中で計算機に直接触れられる彼らにとってはその方がはるかに自然です。
その為、論理学はともかく人類と似た形での数学の発見や発展はかなり難しいでしょう。
最適化学や単純なプログラムの問題として諸々の基礎をすっ飛ばしてある程度実現できるかもしれませんが。

しかし我々の世界で天才達が『プリンキピア・マテマティカ』で成し遂げたような仕事を彼らはいつか達成するでしょう。
そしてありとあらゆる定理を形式的に証明します。
それは我々の世界の数学者ですら実現できていないことですから、なかなか大変な道のりだと思います。

最適化と計算量

最適化は対象となる計算機自体を実行することなく実現できます。
これにより計算で消費する資源、計算時間やテープの長さ(メモリの消費量)が増減します。
考えてみるとこれは結構不思議なことです。

特に不思議なのは最適化の自然な拡張で停止しない問題の解を定義できそうなことです。
最適化を少し延長して「仮に停止するとした場合」のような推論が成り立ちます。

最適化の自然な(に見える)拡張例

	説明
無限ループの削除	単純な無限ループの削除。
唯一の停止	プログラム内で唯一の停止(`return`相当)からの逆実行。
繰り返し実行結果の比較	二度実行したプログラムの結果は無条件で一致すると仮定する。
冗長な計算の削除	部分プログラムの実行結果が全体の出力に影響しない場合、該当部分を削除する。

ただ冷静に考えれば、そうした状況で最適化が適用できないのは大抵当たり前です。説明も十分に可能です。
そうした推定にどのような意味があるのかの疑問はあります。

計算機科学

我々が最初に計算機を作り出したのは最近のことですが、彼らが計算機を作り出すのは極めて早いでしょう。
ここで言う計算機は外部から見れば仮想マシンのことです。
彼らは数多の仮想マシンを作り出し、万能チューリングマシンやチューリング完全のような概念を経験的に発見し、彼らの属する計算機自体を他の計算機内で実現します。
様々な計算機内で彼らが属する計算機を表現するのは、より良い理解と最適化学の発展に繋がるでしょう。

計算機Aで計算機Bを実装した時、計算機Aでの最適化は計算機Bの最適化としても表現できる場合があります。
それにより既存の最適化の正当性を検証したり、新たな最適化を発見することができます。
また近い手段を用い論理の適用もある程度可能です。

彼らが論理学なしで停止性問題や複雑性クラスを発見するかは断言しがたいですが、知的存在である限りはその内発見するでしょう。
ある程度は我々と似たような計算機科学をかなりの初期に完成させると期待します。

感想

元々は「計算機が数学・論理学に先立つ」というようなことを言いたかったのですが、なんだかよく分からない粗雑なSFみたいな記事になってしまいました。
ただともかく、こうして計算機科学から数学などを論じることはそれなりの意義があることです。
実際普通の論理学や数学ではまず問題となりませんが、その中で難しい哲学的な問いを見つけた時にはこうした考え方が役に立つこともある、気がします。

この記事の中では「最適化学から見ると論理学はどう見えるか？」という問いは二・三日考えました。
最初に考えたのは「定理検証プログラムをパスする命題があり、それがなぜか彼らの世界に適用できる」というイメージでした。
それもそんなに悪くはないのですが、「論理学の計算機への適用」という部分がなんだかよく分かりませんでした。
もちろん計算機にも論理学が適用できるはずなのですが、「明白な命令セットがある世界でどのように？」というのは妙でした。
単純に「述語論理計算機」の最適化で考えるモデルはそれよりかかなりマシだったと思います。
とはいえ命題論理でなく述語論理で考えた上、テープを使ってチューリングマシン風に書いたのでいくらか骨が折れました。

数学が最適化学でどう位置づけられるのかは最終的にも曖昧にしてしまいました。
多分、個別の最適化の組み合わせで大概の定理を表現できる気はします。
結局のところほとんどの定理証明は計算機の挙動で説明できるはずですし。
ただ我々が普段基礎的な数学の知識をプログラミングで使うのが、彼らから見るとどうなるのかは微妙です。

宣伝

GitHub Sponsorsをだいぶ前に開設したのですが、誰も寄付してくれません。
寄付を呼び掛けるのは規約違反だったりする気がするので、そこそこ整備したページを見るだけ見てください。

GitHub Sponsors