本年度は、線形論理上の集合論の計算機科学への応用に関して、二つの面で進展があった。 一つは、理論的な側面で、線形集合論の意味論に関するものである。線形集合論に対する自然な表示意味論は、これまで知られていなかったが、報告者は昨年の一月に命題線形論理の源泉ともいえるcoherence spaceを、型なしランダム計算のスコット意味論の手法と組み合わせることで、線形集合論の表示意味論を構成することに成功した。しかし、その意味論はそのままでは限量記号を扱えないという問題があった。本年度に入って、この意味論の拡張を研究した結果、帰納的定義の理論で良く知られているcardinality argumentを使うことで、もともとの意味論を段階的に拡張していった際の不動点として、限量記号を含んだ表示意味論が得られることがわかった。 もう一つは、実践的な側面で、形式システムのインターフェイスに関するものである。論理学での証明図はbinary treeの形で与えられることが多いが、計算機上では、通常それを文字列として表現することになる。しかし視覚的なユーザインターフェイスをつかうことで、binary treeをそのまま画面上で操ることも可能となった。さらに、ネットワーク上での使用を考えるとWebのブラウザ経由で使えるものが望ましい。こうしたアイデアの実現として、click and dragでマウスにより視覚的かつ自由に証明図を構成するシステムPierをJawaのアプレットとして開発した。これは、http://fbc.keio.ac.jp/^〜 sirahataにおいて公開されている。
|