2009 Fiscal Year Annual Research Report
計算とルディクス: 論理・計算・複雑さのための一般的フレームワーク構築に向けて
Project/Area Number |
08F08803
|
Research Institution | Kyoto University |
Principal Investigator |
照井 一成 Kyoto University, 数理解析研究所, 准教授
|
Co-Investigator(Kenkyū-buntansha) |
BASALDELLA Michele 京都大学, 数理解析研究所, 外国人特別研究員
|
Keywords | linear logic / ludics / completeness theorem |
Research Abstract |
2009年度は下記の研究を行った。 1.線形論理証明論において重要な役割を果たす焦点化原理について、ルディクス理論の観点から分析を行った。焦点化原報は証明探索・論理プログラミングなどの操作的な観点から説明されるのが常であるが、本研究ではある種代数的な定式化を与えることに成功した。成果はワークショップ『ゲーム・対話・相互作用』、および国際学会MFPS'10に投稿し、受理された(Basaldella, Saurin,照井の共同研究)。 2.昨年度に引き続き、伝統的なゲーデル完全性とゲーム意味論的な対話的完全性の関係性をルディクスの枠組みで確立する研究を行った。昨年度の研究が伝統的な有限的・帰納的観点に根ざしていたのに対し、本年度の研究は、無限的・余帰納法的観点からそれを補完するものであり、数理論理学におけるラッセル・パラドックス、プログラミング理論における一般再起型の解釈、実現可能性理論における直交性の概念など、多くの重要概念を統合するものとなった。成果は論理・理論計算機科学分野に おいて最も権威のある学会の一つであるLICS'10に投稿し、受理された(Basaldella,照井の共同研究)。
|
Research Products
(6 results)