証明検証系Mizar試用報告、第三弾です。
Mizarの難しさは、言語仕様やモデルに起因するというよりは、システムの機能が古臭すぎて多大なストレスを強いる点にあります。[...snip...]
「もったいないなーー」と感じるんですよ。[...snip...] Mizarには卓越したアイデアが含まれていると思います。それなのにあの使い勝手とは …… もったいない！
僕はほんとに「もったいない」と思っています。システムとコミュニティがこのままだと、せっかく蓄積した膨大なライブラリもあまり活用されないままに朽ちていく懸念さえあります。それはあまりにも「もったいない」。
内容：
なぜシステムは進化を止めたのか
次の文書を読んでみました。
- "Mizar: An Impression" by Freek Wiedijk （PDF 42ページ）
最近の文書でないのは明らかですが、いつ書かれたものかハッキリとは分かりません。参照しているMizarマニュアル（"An Outline of PC Mizar"）が1993年版なので、1990年代に書かれたものだと思います。
その時点で既に、Mizarシステムは進化を止めた、あるいは進化を嫌っている様子が伺えます*1。Mizarコミュニティの興味と情熱の対象はソフトウェアではなくて、MML（the Mizar Mathematical Library）の規模の拡大と精度の向上にあるようです。ソフトウェアはとりあえず使えているのだから、MML構築にエネルギーを注ぎたい、ということでしょう。
MMLは相互参照の塊なので、全体として一枚岩のライブラリです。なまじソフトウェアの仕様を変更するとMMLの整合性を破壊しかねません。また、ライブラリの整合性と品質を維持するには中央管理方式がふさわしいと判断されたのでしょう。
Mizarのアーティクル（.mizファイル）がMMLに登録されるには、いったんFormalized Mathematicsという論文誌に掲載され、それが"library committee"の手により次回リリースMMLに反映される、という手順らしいです。
MMLのメンテナンスには、おそらく、リンカ／ライブラリアンに相当する非公開のツールが使われているでしょう。そうだとしても、作業は随分大変だろうと予想します。過去のアーティクルがフリーズされるわけではなくて、基本部分の構成が変更されたりもするようです。そうなると、全ファイルの検証し直しの事態も発生します。
MMLを構成するテキスト（生の.mizファイル）の総量はウン百万行の規模ですから、全ファイルの検証の負荷は相当なものです。処理系には効率も求められます。MS-DOS時代の処理方式を変えないのは、効率の問題もあるかも知れません。
処理効率は良さそう
以下の話は、正式な資料に基づくものではありません（正式な資料はない）。僕の感触と推測です。
MMLのソースファイル（生の.mizファイル）は、$MIZFILES/mml/の下に存在します（$MIZFILESはMizarのインストールディレクトリ）が、処理系はソースファイルを見てないでしょう。$MIZFILES/prel/にコンパイルされた形式があるので、処理系はこちらを参照していると思います。
$MIZFILES/prel/の直下にはアルファベット1文字の名前のディレクトリが並びます。この1文字はアーティクル名の最初の1文字です。多数のファイルへのアクセスを高速化するためによく採用される方式ですね。1文字ディレクトリの下に、アーティクルの内容を細切れにしたファイル達が配置されています。
この細切れファイルの拡張子が、environ部のインポート宣言のディレクティブ名とだいたい対応しています*2。ベース名はアーティクル名と同じです。
| ファイル拡張子 | environ部のディレクティブ名 |
|---|---|
| .dfr | vocabularies |
| .dno | notations, expansions |
| .dce | construtors |
| .dcl | registrations |
| .def | definitions |
| .the | theorems |
| .sch | schemes |
個々のファイルは構文解析済みなので高速にメモリに載せることが出来ます*3。
このメカニズムを支えるために、人間（ユーザー）が、コンパイル済みファイルの拡張子に対応したインポート宣言とアーティクル名を列挙してあげるわけです。
environ
vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
SETFAM_1, ZFMISC_1, BINOP_1;
registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
RELSET_1, FUNCT_2, PBOOLE;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SETFAM_1, TARSKI, XBOOLE_0, RELAT_1;
equalities ORDINAL1, XBOOLE_0, CARD_1;
expansions SETFAM_1, ORDINAL1, TARSKI, XBOOLE_0;
theorems AXIOMS, ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, TARSKI, ORDINAL2,
XBOOLE_0, CARD_1, FUNCT_2, FUNCT_1, FUNCOP_1, PBOOLE, RELSET_1, RELAT_1,
PARTFUN1, SUBSET_1, NUMBERS, ENUMSET1, XBOOLE_1;
schemes SUBSET_1, ORDINAL2, FUNCT_2, PBOOLE, BINOP_1;
処理系の負担を軽くするために、人間が頑張る／我慢するのはかつては普通でした。Mizarの開発がはじまった1970年代だと、これはしょうがなかったでしょう。
その後コンピュータの処理能力は格段に向上したのですが、MMLの規模も肥大していったので、巨大な一枚岩ライブラリであるMMLの高速一括処理のために、この方式をやめられなかったのでしょう。あるいは単に、変更するタイミングを見つけられなかった、という事情かも知れません。
生き残れるのか
僕はジイサンなので、grepだけで参照を辿ったこともあるし、エラー番号の意味を紙のマニュアルをめくって調べた経験もあります。ですから、なんとか我慢することも可能です（ギリギリだけど）。しかし、矢鱈に親切なIDEで育った世代が、この使用感に耐えられるとは思えません。使わせるには、上司と部下／教師と学生とかの関係性により強制するくらいしか手段が思い付きません。
いくらなんでもキビシイですよ、これは。ソフトウェアを「とりあえず使えるんだから」と捨ておくと、Mizarプロジェクトの存続もあやしい気さえします。そうなると、40年以上も育〈はぐく〉んできたMMLも忘れ去られるかも知れません。
モダンなMizar互換処理系を誰かが作るとか、Mizar-to-Xxxコンバータにより他の言語のライブラリに吸収されるとかのシナリオも考えられますが、今のMizarシステムがもう少し今風の仕様を取り込むのが望ましい道でしょう。
輝け、Mizar
僕がダメ出しするのは、腹を立てているからではありません。いや、ちょっと苛つきましたけど、ダメだと切り捨てているのではなくて、「いいんだけどな、これ」という気分なんです。
アンジェイ・トリブレッツのアイデアは素晴らしいし、Mizarの表現力と実用性はMMLにより実証済みです。前世紀の遺物として朽ち果てるのではなくて、今の時代に適合し将来も成長し続ける形に生まれ変わって欲しいな、と期待するのです。
