このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

証明検証系Mizarのジレンマと証明系の村

証明検証系Mizarを試した印象の続報です。

内容:

これはひどい!」が、「これは素晴らしい!!」

Mizarの解説にあるサンプルコードはほぼ動きません*1。僕が試した範囲ではひとつも動きませんでした。理由は簡単で、構文的に完全じゃないからです。特に、構文上必須であるenviron部はたいてい欠如してます。

environ部とは、当該の証明記述ファイル(.mizファイル)が依存しているライブラリファイル(コンパイルされているが、.mizファイルと同等)を列挙する部分です。モジュールのインポート宣言と思えばいいです。

このインポート宣言を書くのが尋常じゃなく難しいのです。なぜなら:

  • モジュールはグルーピングも階層化もされてなく、1257個がフラットに配置されている。
  • モジュール名は8文字までの英数字(アンダースコアは許す)に限定される。
  • モジュールから何をインポートするかにより、インポート宣言が10種類に分かれている。
  • 再帰的なインポートはサポートされない。関連するモジュールを明示的にすべて列挙する必要がある。
  • モジュールの依存関係を表示するツールはない
  • 定義や定理がどのモジュールに含まれるかの検索は、grepと目視による。

ちょっと信じられない仕様ですが、その悲惨さを感じるには実例を見るといいでしょう。自然数(natural number)に関する定理達は、数学のかなり基本的な部分ですが、それを記述しているモジュール(.mizファイル)nat_1.mizのenviron部は次です。

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;

列挙されている8文字以内の大文字の名前が、nat_1.mizが参照している他のモジュールの名前達です。これらのモジュール名をどうやって知ったのでしょうか? たぶん、nat_1.mizのケースでは、著者が他のモジュールの全貌(=MMLライブラリ)を熟知していた、ってことでしょう。

では、僕のようにMMLライブラリについて何も知らない者が、自分で新しく.mizファイルを書くときはどうすればいいのでしょうか? 僕が調べた範囲では、

  • 難しいけど頑張れ

という、言い訳だか精神論だか励ましだか分かんない文言しかなかったです。

他にも驚かされることがイッパイで:

  • 新しく定義した名前や記号のインデックス(一種のハッシュマップ)を、手動で作成・メンテナンスしなくてはならない。
  • ソースファイル(自分で書いた.mizファイル)と同じディレクトリに一時的中間ファイルが生成される。それも、1ソースファイルに対して2527中間ファイル。他の一時ディレクトリに書き出すオプションは見あたらない。
  • エラーレポートは、ソースファイルにエラー番号が埋め込まれる。タグジャンプは使えないし、毎回(エラーがあれば)ソースが書き換えられる。
  • エラー番号に対するテキストは、mizar.msg(Mizar Errors Explanation File)を見ないと分からない。(addfmsgというツールを使えば、ソースファイルのお尻にテキストメッセージを挿入してはくれるが。)

僕が「証明検証系Mizarを試してみる」で次のように書いた理由はこれでお分かりでしょう。

Mizarは20世紀で時間が止まってしまったような印象を受けます。


なにから何まで今風じゃなくて、MS-DOSの時代にタイムスリップしたみたい。

“地獄の使い勝手”です。しかし一方、

証明記述の可読性が高いのは本当で、構文の設計は優れたものだと思います。CoqやIsabelleとは比べものにならないくらい読みやすいです。

構文や意味モデルはホントに素晴らしいんですよ。ソフトウェアとしては「こんなもん使えるか!」と投げ出すレベルなんですが、CoqやIsabelleでは代替できない機能と用途を持っているので、フラストレーションに耐えながら調べたり試したりしています。

Mizarコミュニティ

Mizarは、1970年代初頭に、アンジェイ・トリブレッツ*2(Andrzej Trybulec 1941-2013)がMS-DOS上のTurbo Pascal*3で実装をはじめたものです*4。その当時の仕様をかなりの程度引き継いでいる(あるいは、引きずっている)ようです。例えば、“あのenvironの仕様”も、貧弱なCPUと少量のメモリ環境下では納得がいくものです。

しかしそれにしても、なんでそのままなの? と疑問に感じます。どうもこれは、Mizarコミュニティの性格によるのではないか、と思えます。ソフトウェアは、コミュニティの性格を色濃く反映するものですから。

2014年の岡崎裕之さんのスライドによると、2013年時点ですでに5万2千の定理がMMLライブラリに含まれていたそうです。この膨大な定理群を書いた人々に関しては:

  • 延べ200名を超える著者

とあります。えっ? 200? 「延べ」がどういう勘定か分からないですが、個人の数が300を超えることはありえないでしょう。多めで300人としても、一人平均173定理を書いています。仮に「80:20の法則」が成立するなら、60人ほどのアクティブメンバーが一人平均700個弱の定理を書いていることになります。

要するにMizarコミュニティはあまり大きくないのです。40年以上という時間方向の蓄積により、MMLという巨大なライブラリを構築したわけです。今風の、例えばNode.jsのnpmリポジトリのように、世界中のコントリビューターにより短期間で生成された大規模ライブラリとは全く性格が異なります。

Mizarシステムのソースコードは非公開(バイナリ配布)で、システムとMMLライブラリの開発を主導している組織である Association of Mizar Users (ポーランド語 Stowarzyszenie Uzytkownikow Mizara; http://mizar.org/sum/)も、事実上はビアリストーク大学(ポーランド)、アルバータ大学(カナダ)、信州大学の有志で構成されているようです。

小さく閉じたコミュニティ内であれば、「難しいけど頑張れ」は通用します。一子相伝とは言わないまでも徒弟制度的にコツを教えることが出来ます。ひょっとすると、非公開の内部ツールを持っているのかも知れません。緊密な関係性と情熱があれば、精神論・根性論でさえ効果を発揮します。多少の不満があっても「まー、頑張ろう」と。また、修正しようと思ってもソースコードへのアクセスが自由でないから「まー、頑張ろう」と。

僕は、J言語のコミュニティを思い出しました。

J言語の場合は、その構文がこの世のモノならざる超絶変態ですから、興味を持つ人がソモソモ特殊な嗜好・指向・志向の持ち主で、コミュニティも独自の閉じた文化を持つのは必然だと思います。

しかしMizarの場合は、言語自体は(証明記述言語の範疇では)癖がなくまっとうで、書くにも読むにも楽なものです。むしろ癖が凄く難読なのは、他の証明系のタクティク言語です。Mizarはもっと世に広まってよいものだと思います。Association of Mizar Usersのミッションにも、"popularizing, propagating and promoting the Mizar language"とあります。であるなら、システムの仕様もコミュニティの在り方も、もう少し現代の傾向に合わせたほうがいいんじゃないか、と(余計なお世話ですが)考えます。

Mizarの可能性

Isabelleの高水準証明記述言語はIsarといいます。公式には"Intelligible semi-automated reasoning"のアクロニムだということですが、おそらくはMizarへのリスペクトが込められているんじゃないかと思います。実際、Isar(の設計者のウェンツェル)はMizarにかなり影響を受けています。

ウェンツェルは、Isabelle/Isar(言語)とIsabelle/PIDE(フロントエンド・ソフトウェア)が教育に有効だろうと主張しているし、その方向で頑張ってもいるようです。しかし、「ちょっと無理なんじゃないか」と僕は思います。Isabelleは(そしてもちろんCoqも)無駄に難しいからです。タクティク言語の難読さは論外ですが、高水準なIsarにしても、その意味モデルや論理的概念が難しいので、教育に使うための事前の教育で息切れするでしょう。

Mizarの難しさは、言語仕様やモデルに起因するというよりは、システムの機能が古臭すぎて多大なストレスを強いる点にあります。「難しいけど頑張れ」を「楽になるように修正する」に方向転換すれば、事態は改善されるはずです。教育を含めて一般的な用途への適用可能性は、CoqやIsabelleよりはずっと大きいでしょう。

「もったいないなーー」と感じるんですよ。"MIZAR: the first 30 years"において、「Mizarプロジェクトは、アンジェイ・トリブレッツの最高傑作」(The MIZAR project is opus magnum of Andrzej Trybulec.)と評されています。Mizarには卓越したアイデアが含まれていると思います。それなのにあの使い勝手とは …… もったいない!

*1:[追記]「動く」は言葉としてふさわしくないですね。「動かない」は「コンパイルできない」です。[/追記]

*2:カタカナ表記は https://ja.wikipedia.org/wiki/Mizar に従いました。forvoでポーランド語発音を聞いてみると、アンジェイとアンドレイの中間くらいの音みたいです。無理に書くと「アンデュェイ」とかだけど、「アンジェイ」とします。

*3:現在の実装言語はfree pascal

*4:[追記]開発実行環境がIBM PCDOSに移行したのは80年代とのことです。また、短期間ですが、最初はAlgol言語を使っていたようです。[/追記]