(1) 研究上の成果
図式をユーザインタフェイスとした 圏論のための証明支援システムの概念設計を次のようにした。
[図式とは]
図 --1 のような図式の一般的な定義をしよう。
有向グラフにおいて、
始点と終点の等しい空でないパスの二つ組を 面分という。
我々は 図式とは ラベル付き有向グラフと
その上のいくつかの面分が指定されたものと定義する。
ラベルは点と矢印に付ける事ができ、そのラベルは変数名だが、
後記「描画コマンド」 に説明するように、
全称記号あるいは存在記号を一つつけることができる。
図式において指定されている面分を特に 可換面分という。
二つのパスで囲われた面分に二重矢印をつけて可換面分を示す。
図 --1 は確かに図式になっている。
[描画コマンド]
図式を描くための描画コマンドとして図 --3 のようなものを用意した。
点を打つ、始点と終点を定めて矢印を書く、点、矢印にラベルをつ
ける、そして可換面分を作るための二重矢印を付けるというコマンドがある。
可換面分を作るコマンドは指定したセルが二つのパスに囲まれているという条件
を満たしている時のみ実行可能である。
|
我々の描画コマンドは図式を作るが、 それだけでなく同時に論理式もインクリメンタルに生成する。
[コマンド列、図式、論理式の間の関係]
前節で説明したとおり、描画コマンドを次々に実行していくと、
システムは図式を表示し、同時に論理式を作っていく。
いいかえると、描画コマンドを実行順に並べた有限列が図式を一つ定め、
かつまた論理式を一つ定めるわけである。
つまり我々はコマンド列の全体から図式の全体への関数と
論理式の全体への関数を作った。
しかし、図式と論理式の間にはこのような関数は存在しない。
あるのは、同じコマンド列からでてきたという「関係」だけである。
つまり図式を見ても一通りに論理式は決まらず、論理式の図式による表示も
一通りに決まらない。
図式は論理式に対する一つのビューを定めていると考える事ができる。 三次元物体を二次元表示する場合、 一つの物体を見る視点(ビュー)をかえる事によって、 二次元表示はかわるし、別の物体でも同じ二次元表示を持つ場合がある。 論理式の図式による表現の場合も、これと丁度同じ事が起こっている。
論理式を表す図式が一意に定まらないこと、また逆に図式によって表される 論理式が一意に定まらないことは ユーザにとって大きな欠点にならないと我々は考えている。 図式を作成する手順は無数にあるわけではなく、それが表す 論理式も限られた数しか無い。その限られた組合せを、 最初に図式を入力したユーザが忘れるとは考えにくい。 また、補助的に論理式を画面に表示する仕組みを入れておけばよい。 それよりも、ユーザの望む図式を表示させる事によって、 ユーザの得る直感を大切にすべきだと我々は考えた。 この方法がうまくいくかどうかは今後、システムの試用によって 評価しなければならない。
[証明コマンド]
描画コマンドはシステムに対して証明したい論理式を入力し、表示させるコマンド
だったが、これとは独立に証明を実行するためのコマンドがあり、
それを証明コマンドと呼んでいる。証明コマンドはたくさ
んあるが、そのうち貼り付けコマンドについて説明する。
[貼り付けコマンド −−− 等式の証明]
貼り付けコマンドは等式に基づく式の変形を図式の上で行うため
の仕組みである。 例えば
の四つの等式を仮定して f = g を証明することを考える。人間がこれを証明する時は、
のように式を変形していって証明する。 これを真似ようというわけである。
四つの仮定とゴールは図 --4 のように表される。 貼り付けコマンドはその名のとおり仮定の図式を証明したい図式に ペタッとはりつけるのだが、具体的にどうするか説明する。
|
最初は図 --4の仮定の図式を証明したい図式 に貼り付ける。仮定(1) の左のパスが証明したい図式の f に 一致するので、そこに沿って貼り付ける。貼り付けられた部分には 色が塗られる(図 --5(1))。 色の塗られなかった部分が新たに証明すべき可換面分になる。 この意味は f と ( id ; f ) が等しいから、 f = g を証明するかわりに ( id ; f ) = g を証明すればよいということである。 同じように id がマッチして、図 --5(2) のように貼り付け、 次に ( f ; g ) がマッチして、貼り付けて図 --5(3)になる。 最後に、仮定(図 --4(4))は証明すべき可換面分と 両辺とも完全に一致する。 つまり証明したい等式が仮定の等式と同じだということである。 この時は全部を貼り付けることができて、全体が塗り潰され 最初の図式が証明された事になる(図 --5(4))。 貼り付けコマンドはこのように貼り付けていって全体を塗り潰す事によって 証明するためのコマンドである。
|
貼り付けコマンドを実行するための条件を正確に述べる。 まず特殊な場合として両方のパスが完全に一致した時を考える。 この時は仮定がゴール全体にぴったり貼り付けられる。 一般には、仮定の図式の左のパス全体が、ゴールの左のパスの一部と一致した時に、 貼り付ける事ができる。その時、その仮定の図式が 図 --6のように貼り付けられ、 貼り付けられた部分に色が塗られる。 塗られていない部分はまた二つのパスに囲まれて、新たに証明すべき可換面分に なる。
|
我々の扱う式に関しては貼り付けコマンドは等式推論に対して健全かつ完全である。 我々の扱う式は f ; g ; … ; h という形に限っている。 式の一部を等価な式に置き換える等式推論は, その部分に対する貼り付けによって模倣する事ができる。 この意味で貼り付けコマンドは等式推論に対して完全である。 健全性に関しても同様である。
(2) ソフトウェアとしての成果
我々は、JAVA を用いてインプリメンテーションを行っている。
現在、描画コマンドによる入力は一部の機能を除き実現されている。
証明支援の部分については、最も重要だと思われる貼り付けによって証明を行
う部分はできている。論理記号に関する証明に関しては一部の機能を除き
実現している。プログラムサイズはソースで約 7000 行である。
ドキュメントとしては操作マニュアルを用意する。
(3) 残された課題
現在まだインプリメンテーションされていない部分、例えばカットと呼ばれる
推論規則等も使用可能にする必要がある。
また、圏論によく使われる函手や自然変換といったものを簡単に取り扱えるように
する必要がある。
(4) 外部発表論文リスト