| 平成８年度 委託研究ソフトウェアの提案 |
定理証明系は, 高度な知識処理システムを実現するための, 重要な基盤技術である. 自然数を扱えるような体系では, すべての定理を自動証明することが不可能なことがわかっているので, 定理証明系は, Boyer-Moore 証明系のように, 限られた範囲の体系を対象として完全自動証明を行うものと, Lego, coq, Isabelle, HOL などのように, 体系は限定しないかわりに, 完全自動証明をあきらめ, 形式的証明をユーザが自分で書くのを手助けする (もちろん, ルーチンワークは計算機システムの方で引き受ける---その結果, ユーザが指定するのは, 主に帰納法のルールの選択である) 定理証明支援系とにわかれる.
定理証明支援系の場合, 会話的システムであるため, ディスプレイに表示された証明途中結果をユーザが理解した上で、帰納法などのルールを選択していく必要があるが, 長大な論理式がディスプレイに現れると, それを理解するのが困難となる場合が多い. 大きな式を人間にわかり易い形でうまく取り扱うというのが, 会話的システムとして実現される定理証明支援系を開発する上での重要課題となっている.
従来, この問題に対するアプローチは二種類あった. 一つは, 式のなかの冗長な情報は入力しなくともシステムの側で推測し, また, そのような冗長な情報は表示もせずに済ませるというものである. Lego などで見られる implicit polymorphism と呼ばれるものは, 型の自動推論を系統的に行うもので, このようなアプローチの例である.
もう一つは, 適当なユーザ・インターフェイスを設定するものである. 式を構文木に基づいて構造化した形で表示／入力する INRIA のCENTAUR などの構造エディタがその例である. CENTAUR は coq へのインターフェイスも持っている.
いずれのアプローチも, 一般の論理式に通用するものだが, それゆえに限界があった.
この研究は, 圏論とよばれる数学の理論のための証明支援系のユーザ・インターフェイスを設計, 試作して, そのフィージビリティを評価することを目的とする.
圏論における基本データは, 有向グラフを基本とする可換図式 (以後省略して単に図式と呼ぶ) によって自然に表現することができる.図式に基づく等式証明というのは, 有向グラフの領域を二つのパスが同等であることを表す等式だと考え, 証明済の領域を次々に塗り潰していくことによって等式を証明していくという方法である.
図式を用いて論理式を適当に定義しなおし, 従来のように論理式の入出力のために文字列を用いるのではなく, 図式を入出力の基本的対象とするようなインターフェイスを持つ圏論の証明支援系を設計,試作するのが第一段階である.
次に, 試作した証明支援系を用いて, 実際にいくつか証明を書き, 設計したインターフェイスが, 証明構築にどれだけ役にたったかを評価する. 長期的には, 評価に基づいてインターフェイスを設計しなおしまた評価するというサイクルを繰り返す計画である.
まず, 圏論の命題を図式にもとづいて表記する構文を形式的かつ厳格に定義する. 圏論のなかでは, インフォーマルな図式を用いて議論するのが普通だが, ここでの仕事は, それをフォーマルな定義に高め,計算機によって図式を直接扱えるようにすることである.
ここで注意しなければならないのは, ディスプレイに表示される図式と論理式の間には, どちらの向きにも, いかなる函数も存在しない ことである. もちろん, 図式をうまく定義して, そのような函数が存在するようにすることは可能だが, 通常圏論の議論で用いられる図式をそのまま用いるかぎり, そのような函数をつくることはできないようである.
そこで, 我々はさらに論理式を書くためのコマンドを設定する. このコマンドの列を一つ決めると, それが与えられたときに描画すべき図式は一つ決まるし, また, それが表わすべき論理式も一つ決まる.
さらに, 図式に対する証明コマンドも設定する.
これらのコマンド列の設計と, それに基づく描画規則および論理式の生成規則がシステムの設計の核となる. この設計に基づき, システムをＪＡＶＡを用いて試作する. ＪＡＶＡを用いる理由は, ネットワークを通して, どこででもデモを行なえることである.
システム試作が, ある程度の段階に達したところで, 圏論での定理を実際に証明してみる. 第一段階では中程度の大きさの定理を証明してみる. たとえば, 随伴函手のいくつかの定義の同等性を示す定理,米田の補題など. この経験に基づいて, 一度システム設計 (コマンド列の設計など) を反省し, 試作のやりなおしの材料とする.
長期的には, この後, 設計試作をやりなおし, さらに大きな定理, たとえば Beck の monadicity theorem や Freyd の adjoint functor theorem などを証明してみて, さらに設計の反省をおこなうが, この段階は, 本提案の範囲の外である.
研究者は、互いに密な連絡を取りつつ共同で開発を勧める。主な役割分担は、圈論に関して木下が、証明支援システムに関して坂井が、ユーザインタフェイスに関して高橋が、実装に関して中田、池田、藤田が中心に行い、坂井が全体を取りまとめる。まず初年度に評価用第０版を試作する。次年度に第0版の評価に基づく改良版として第1版を作成する。研究開発は、資料などを中心にした調査フェーズ、設計試作のフェーズ、評価改良などのフェーズからなるが、各フェーズからのフィードバックは随時行う。海外での類似システムには優れたものも多いので、出張調査などにより得た情報を常に参考にしながら開発を進める。
圏論証明支援システム
このシステムは圏論の一階の命題を、文字列ではなく、グラフィカルな図式によって表す。図式の上でのマウスのクリックなどによって命題の証明を進める。
証明支援システムは数多く存在するが、グラフィカルなユーザインタフェイスを持つものは皆無と言ってよい。グラフィカルなユーザインタフェイスを証明支援システムに導入する事による効果を調べるのがこのシステムの主目的である。
圏論の命題は図式によって説明を付ける事がよくあるので、圏論に馴染みのあるユーザにとって、図式による表示は大変わかりやすい。特に証明支援システムを使っていると、長い論理式が出て来る事があり、証明の可読性の点で問題となる。図式によってそれをコンパクトに表示する事ができると、直感的にわかりやすい。
命題を文字列で入力するかわりに、このシステムでは図式を描画する。また、図式はユーザによって変形する事もできる。
このシステムでは、大別して次の２種類のデータ
１. 表示されている図式、
２. 表示されず内部にある命題、
を持つ。ユーザの与えるコマンドがこれらのデータを更新する。
コマンドは
・図式の描画、変形、
・証明実行、
の２つに分類することができる。
図式の描画、変形は、主に１. のデータを更新するものだが、図式の描画によって命題を入力する際は２. のデータも更新する。
証明実行は、本質的に２. のデータを更新する。場合によっては図式の変更が必要になるので、１. のデータも更新する。
約１万行。
- このソフトウェアがどういった形で利用されるのか
- 利用者へのセールスポイント
評価用試作(第0版)を作る。圈論の簡単な命題の証明が実行可能になる予定である。
ソフトウェア仕様書、ユーザマニュアル、利用例集
www-admin@icot.or.jp