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

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

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

［参照用 記事］

フォワード・リーズニングとバックワード・リーズニング

雑記／備忘

現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。

内容：

証明ソフトウェアの進歩は遅い

「プログラミング言語Lean 4の現状」に書いたように、証明ソフトウェアの開発は膨大な時間と手間がかかるもので、Coq, Isabelle, Mizar は30年から50年ほどの開発期間を経ています。新しいソフトウェアであるLeanでも、もう10年になります。どの開発チームも最優秀の人材を揃えています。それでも「使いものにならない」事実が、証明ソフトウェアの開発が極めて困難であることを物語っています。

「使いものにならない」に対して、「何言ってるんだ、十分実用になっているぞ」と反論する人もいるでしょう。「使いものになる／使いこなしている」と言う人は、十分な技量とありあまる情熱を持っているかたでしょう。僕が意図している「使いものになる」は：

  1. 特別な資質や膨大なトレーニングを要求しないで使える。
  2. 使うにあたって、心理的障害や認知負荷が特に大きくはない。
  3. ユーザー数が多いポピュラーな対話的ソフトウェアと同程度のUIを備えている。

この基準は、クリアするには厳しすぎる無茶な基準かも知れません。が、ひとつの物差しとして考えると、現存のメジャー証明ソフトウェアはこの基準にはまったく手が届きません。

UIに関して言えば、ウィンドウシステムを使っているにしても、本質的にはキャラクタUI／コマンドUIです。前世紀からこれといって変わってない（良くも悪くも）クラシックなものです。理論的観点／技術的観点から内部の視点で見れば、めざましく進歩しているのかも知れませんが、外部からみると「なかなか使えるようにならないなー」。

バックワード・リーズニング

現存の証明支援系が対話的にサポートしている証明手法はバックワード・リーズニングです。「何かを作る」状況で例え話をすると、バックワード・リーズニングとは次のような考え方です。

  1. Xを作りたいな。
  2. Xを作るには、素材に何が必要だろう？
  3. AとBがあれば、Xを作れるな。
  4. Aは今ここにある、ヨシ。しかし、Bはないな。
  5. Bを作るには、素材に何が必要だろう？
  6. Cがあれば、Bを作れるな。
  7. Cは今ここにある、ヨシ。
  8. これでもう、Xを間違いなく作れるじゃん、あーメデタイ。

この考え方では、まず目的物を決めて、目的から逆向きにたどって素材に至ります。素材がすべて手元にあることが確認できたらメデタイわけです。逆算して計画を立てているだけで実際には作っていません -- そこは目くじらを立てないことにします。

バックワード・リーズニングでは、最初から目的がハッキリしているし、逆向きにたどるステップも比較的明確なので、ソフトウェアによる支援がしやすいのです。

フォワード・リーズニング

フォワード・リーズニングでは、手元にある素材から出発して目的のモノを作り出します。

  1. Cが今ここにある。
  2. CからBが作れるな。
  3. ヨシ、CからBを作った。
  4. Aが今ここにある。
  5. AとBからXが作れるな。
  6. ヨシ、AとBからXを作った。メデタイ。

この方法だと、CやBをいじっているときに、必ずしもXが作れると確信してないかも知れません。最初に、DやEをゴニョゴニョしていて、Xを作れないかも知れません。しかし、DやEからXとは別なYが作れた、なんて事もあります。

フォワード・リーズニングだと、作業のはじめの段階で何から手を付けていいかはよく分からないのです。作業工程も試行錯誤が入る発見的なものになるでしょう。ソフトウェアによる支援（次に何をすべきかのアドバイスとか）は、やりにくいでしょう。

しかし人間は、目的から逆向きにたどるバックワード・リーズニングだけで証明（やその他のこと）をやっているわけではありません。フォワード・リーズニングとバックワード・リーズニングを、けっこう複雑に混ぜて使っているのです。なので、バックワード・リーズニングしか使うな、と言われると途方に暮れたりツラい気持ちになります。

フォワード・リーズニングの対話的サポート

現存の証明支援系で、フォワード・リーズニングに基づく証明が一切書けないわけではありません。書けるのですが、一人で／自分だけでエディタでモクモク・ツラツラと書きくだすだけです。バックワード・リーズニングのときのように、ソフトウェアと一緒に作業する環境ではありません。ツラい、寂しい、つまらない。

一人で／自分だけでする作業でも、定形作業・機械的操作はけっこうあるので、ソフトウェアが介入・支援する余地はあると思います。証明支援系がフォワード・リーズニングをまったく手伝う気がないのは、歴史的惰性にすぎないかも知れません。やればできる子なのに、習慣で何もやらない、と。

「愚痴と文句」を言ってみても、どうこうなるとは期待してませんが、仮にソフトウェア実装が出現しなくても、フォワード・リーズニングの対話的コマンド（いわば、逆タクティク）がどうあるべきかを考えるのは有意義だと思います。