Mizarは、集合論と一階述語論理を組み込みで持っています。何もない所から（from scratch）、集合論＋一階述語論理により意味のある定理を記述するのは労力がかかり過ぎて現実的ではありません。付属のライブラリMML（Mizar Mathematical Library）に頼らざるを得ないのです。
MMLは、ソース行で約2百8十万行、ファイル数は1257です。コンパイルにより1ファイルが10種類（たぶん）の概念的構成素に分割されます。仮に、分割された構成素をモジュールと呼ぶなら。モジュール数は1万2千7百です。それらが無構造フラットに配置され、モジュールを識別する名前は8文字以内です。
構造的モジュール編成や再帰的インポートをサポートしてないので、どのモジュールをインポートすべきかの判断は人手、grepと目視です。findvocというツールがありますが、結局はソースファイルをエディタで開いて目で探すので利便性はgrepと大差ないです。
今までの記事で「これは地獄だ」とか「若い者が使うわけない」とか書いたので、ネガティブキャンペーンみたいになっちゃいましたが、僕の真意は「輝け、Mizar」に書いたとおりです。
アンジェイ・トリブレッツのアイデアは素晴らしいし、Mizarの表現力と実用性はMMLにより実証済みです。前世紀の遺物として朽ち果てるのではなくて、今の時代に適合し将来も成長し続ける形に生まれ変わって欲しいな、と期待するのです。
さて、朗報です。地獄のような検索＆ブラウズの作業に疲弊しているとき、次の論文を見つけました。
- Title: Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- Authors: Kazuhisa Nakasho, Yasunari Shidama
- URL: https://arxiv.org/abs/1505.01577
比較的最近（2015年）の論文で、HTMLとブラウザによるMML検索＆ブラウズ・ツールの話です。
Motivation
[...snip...]
the increased volume of the libraries makes it difficult for users to grasp what and where symbols and theorems are defined.動機
[...snip...]
ライブラリの規模は増大しているので、どこにどんな記号や定理が定義されているかをユーザーが把握するのは困難になっている。
そう、そう、そう、そう。そうなのよ。困難なのよ、すっごく。
そこでツールを作ったよ、ということで、オンラインで公開されています。
あーー、これは助かります。非常に助かります。
今後もこのツールが維持されることを願います。というのも、このテのツールへの言及やリンクはあるのですが、リンク切ればっかり。論文が残っているがソフトウェア実体はない、という状況が多いからです。せっかく作ったツールも、なんらかの事情で公開が中止されて永久に消えてなくなってしまう、という。オフラインでも使えるように、Mizar配布物に同梱されるか、できればソースが公開されると嬉しいです。
[追記]
喜んだのもつかの間、さっそく壁にぶち当たってしまった。関数、述語、型などは名前や記号を持つので、その名前・記号をキーにして検索できます。しかし、Mizarの定理は名前を持ってないのでした、クーッ。定理はなんと出現順通し番号で識別するのです。だから無名。
「自然数nに対して n + 0 = n」という定理が必要なのだけど、どこにあるのか分からない。名前が付いていれば、"unit", "neutral", "zero"とかのキーワードで引っかかるので検索も可能でしょうが、名前がないので検索のしようがありません。ハーーッ（溜め息）。
8文字（ほぼ意味不明）の名前をたよりにそれらしいファイルを見当付けて、目で眺め回して、みつからなかったら次のファイル…… を繰り返すしか手段がなさそうです。正式な名前じゃなくても、コメントにタグとかキーワードが書いてあればgrepで引っ掛けることも可能ですが、そんな情報もない。
そもそも定理を通し番号で参照していると、定理の追加削除があると、番号が狂って参照が破綻するんですよね。40年間これでやってきて、40年間誰も直そうとしなかった、ってのが信じられないよ。って、また愚痴になってしまった。
[/追記]
