1997 Fiscal Year Annual Research Report
| Project/Area Number |
09780300
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
白旗 優 慶應義塾大学, 商学部, 専任講師 (00286618)
|
|---|
| Keywords | 線形論理 / 集合論 / プログラム意味論 |
|---|
| Research Abstract |
本年度は、線形論理上の集合論の計算機科学への応用に関して、二つの面で進展があった。
一つは、理論的な側面で、線形集合論の意味論に関するものである。線形集合論に対する自然な表示意味論は、これまで知られていなかったが、報告者は昨年の一月に命題線形論理の源泉ともいえるcoherence spaceを、型なしランダム計算のスコット意味論の手法と組み合わせることで、線形集合論の表示意味論を構成することに成功した。しかし、その意味論はそのままでは限量記号を扱えないという問題があった。本年度に入って、この意味論の拡張を研究した結果、帰納的定義の理論で良く知られているcardinality argumentを使うことで、もともとの意味論を段階的に拡張していった際の不動点として、限量記号を含んだ表示意味論が得られることがわかった。
もう一つは、実践的な側面で、形式システムのインターフェイスに関するものである。論理学での証明図はbinary treeの形で与えられることが多いが、計算機上では、通常それを文字列として表現することになる。しかし視覚的なユーザインターフェイスをつかうことで、binary treeをそのまま画面上で操ることも可能となった。さらに、ネットワーク上での使用を考えるとWebのブラウザ経由で使えるものが望ましい。こうしたアイデアの実現として、click and dragでマウスにより視覚的かつ自由に証明図を構成するシステムPierをJawaのアプレットとして開発した。これは、http://fbc.keio.ac.jp/^〜 sirahataにおいて公開されている。
|
-
[Publications] Masaru Shirahata: "Linear Set Theory with Strict Comprehension" The Proceedings of the Sixth Asian Logic Conference. (1998)
-
[Publications] Masaru Shirahata: "The Strong Normalization of Intcitionistic Set Theory Without Equality" 慶應義塾大学日吉紀要・自然科学. (1998)
-
[Publications] Masaru Shirahata: "A Coherence Space Semantics for Linear Set Theory" 数理解析研究所講究録. 1010. 101-112 (1997)
-
[Publications] Masaru Shirahata: "A Coherence Space Semartics for Linear Set Theory With Quantifiers(Abstract)" Proceedings of the 31st MLG meeting at Miho,Shimizu,Japan 1997. 45-47 (1998)
