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

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

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

参照用 記事

Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。

内容:

Isabelleの独自な世界

Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より:

PIDE構想は、Isabelleプロジェクト/コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか? なかなかに興味深いですな。

Isabelleが世の趨勢と離れるのか? という話をしてますが、有り体に言えば、もともとIsabelleは独特の文化を持った癖の強い処理系で、利用者は特殊な人々です。証明支援系を使いたくても、Isabelleを避ける人はいるでしょう。僕自身、Isabelleは「ダメだこりゃ」と思った1人です。

2005年の夏に、証明支援系を動かしたくなったことがあるのですが、そのとき僕が選んだのは Poly/ML + Isabelle ではなくて、 Moscow ML + HOL でした。当時のメモが残っています*1

Isabelleの何がそんなに嫌だったのかというと、余りにも不格好で気持ち悪い構文です。例えば、SML(Standard ML言語)で次のように書ける関数定義が、

fun conc [] ys = ys
  | conc (x :: xs) ys =  x :: (conc xs ys);

Isabelleでは次のように書きます。

fun conc :: "'a list => 'a list => 'a list"
where
  "conc [] ys = ys"
| "conc (x # xs) ys = x # (conc xs ys)"

Isabelleには外部構文(outer syntax)と内部構文(inner syntax)の区別があり、内部構文は引用符のなかに書きます。それがまるで文字列に見えてしまい、sh(シェル)スクリプトでevalを使っているような気持ち悪さです。「これは生理的に耐えられない」と思いました*2

今でも外部構文/内部構文の区別はそのままで、ソースコード気持ち悪さはパワーアップしています。

とあるIsabelleソースの一部*3 :

    from \<open>\<exists>!y. ?R m y\<close>
    obtain y where y: "?R m y"
      and yy': "\<And>y'. ?R m y' \<Longrightarrow> y = y'" by blast
    show "\<exists>!z. ?R (succ m) z"

TeXコントロールシークエンス/XMLタグのような書き方は、特殊文字を表現するマークアップです。もはや、ソースコードを直接目視することやテキストエディタでの入力は考えてないようです。Isabelle/jEditで見れば:

そして、特殊文字の入力はシンボルパレットからどうぞ。

プログラミング言語APLでは、専用のキーボードや印字装置が必要だった、という話がありますが、IsabelleはAPL的方向に進んでいるようです。現代では、専用ハードウェアは不要で、ソフトウェアで入出力(編集と表示)をサポートできます。そのソフトウェアがIsabelle/jEditというわけです。

Isabelleのチュートリアルなどで、サンプルコードとして次のようなテキストが載っていたりします。

面食らいますよね。「いやっ、擬似コードじゃなくて、実際のソースコードサンプルを載せてくれよ」と。これが、実際のソースコードサンプルなんですよね。ただし、Isabelle/jEditじゃないと入出力(編集と表示)が出来ませんけど。

Isabelleの未来

「いったいどこへ向かう気なんだよ? Isabelle」、「それが正しい方向なのかい? Isabelle」と問いたくなります。

汎用の編集系Emacsや広く普及したSML処理系SML/NJを切り捨てたことは、より独自な閉じた世界へと向かっている印象を受けます。

しかし、ウェンツェルの意図はそうじゃないようです。むしろ逆で、証明支援系をより広い用途でより多くの人々に使って欲しい、だから古臭くて低機能なEmacsやSML/NJとは決別した、ということみたい。

ウェンツェルの2010年のスライド(のPDF)を見ると、PIDEという言葉こそ使っていませんが、この時点で既にIsabelle/jEditのアイディアは確立されていたことが分かります。

このスライドの冒頭には、次の2つの目標が掲げられています。

  1. 我々の証明エンジンをそこら辺にいる人々に使ってもらおう。(Make our provers accessible to many more people out there.)
  2. 証明エンジンのフロントエンドを作るのをうんと簡単にしよう。(Make building front-ends for provers really easy.)

証明エンジン/フロントエンドの用途のひとつとして、例えば教育が想定されています。

PIDEアーキテクチャは、Isabelleに限らず、他の証明支援系のUI構築にも使えるものです。実際ウェンツェルは、頼まれもしないのに(たぶん)、CoqのPIDEフロントエンドを試作したりしています。

現状のCoqのフロントエンドは、証明コマンド(タクティク)を実行して証明状態を遷移させていくものです。つまり、対話的スクリプティング環境なんです。これに対してPIDEのフロントエンドは、スクリプティング環境ではなくてドキュメント作成編集環境です。

「証明スクリプトから証明ドキュメントへ」 -- PIDEのキャッチフレーズのひとつです。動作記述である証明スクリプトでは、人がそれを読んで理解するのは困難です。宣言的で人が読める証明、それがウェンツェルの言う証明ドキュメント(proof document)です。

と、ここ数年のウェンツェルの主張を追ってみると、Isabelleの世界を広げようと尽力しているのが分かります。証明支援系の利用が広がらないネックは、「難読な証明記述言語と貧弱なユーザーインターフェースだ」との認識のもと、Isar(Isabelleの宣言的証明記述言語)とIsabelle/jEditにより障壁を取り除く戦略のようです。

この戦略が功を奏するのか? 僕には予測できません。が、このような戦略と方向性の文脈のなかで、11年前に抱いた悪印象はだいぶ緩和されました。広がりゆく(であろう)Isabelleの世界にちょいと入り込んでみようかな。


独白的余談:「ソースコードはプレーンテキストで書くべきで、プレーンテキストとして十分に読みやすくあるべき」だと僕は思っています。けど、プレーンテキストで見たときに気持ち悪いIsabelleコードは、Isabelle/jEditが綺麗に見せてくれたほうが助かります。引用符は見せないでくれ、型変数 'a もイタリックのaにしてくれ。

*1:結局このときは、MoscowML+HOLがビルド出来ず、Prolog処理系で推論計算しました。

*2:[追記]今見たら、HOLでもけっこう引用符を使ってますね。|- や [ ] を使うと引用符を省けるので「多少はマシ」という判断だったのでしょう、覚えてないけど。[/追記]

*3:~~/HOL/ex/Abstract_NAT.thy lemma Rec_functional: 50行目