2010 Fiscal Year Annual Research Report
| Project/Area Number |
21700014
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| Keywords | 情報基礎 / 数理論理学 / 線型論理 / 部分構造論理 / ルディクス / 国際研究者交流 / フランス:オーストリア:アメリカ:チェコ |
|---|
| Research Abstract |
本研究は1.部分構造論理の代数的証明論、および2.ルディクス理論への余代数的アプローチの二点を主眼としている。
1.については証明論的手法と代数的手法を融合することにより、独自に考案した部分構造階層の中でさまざまな論理的・代数的性質を特徴づけることを目標としている。本年度は、subdirect representation(普遍代数学における"素因数分解")と代数的証明論の手法を組み合わせることにより、部分構造階層レベルP3に属する等式が完備化により保存されることの簡潔な証明を与えた。これは代数的証明論の純代数的文脈における有効性を示す簡明な証左を与えるものである(A.Ciabattoni, N.Galatosとの共同研究)。また、R.Horcikと部分構造論理における推論の計算量的研究に着手し、推論の計算量的困難さの原因として選言特性を同定した。そして選言特性を証明するための一般的な代数的手法を考案し、それにより部分構造階層において下層(レベルM2)に属する論理が計算量的にPSPACE困難であることを体系的に示した。これは上記とは逆に、代数的手法の純証明論的文脈における有効性を示すものである。成果はTheoretical Computer Scienceより出版されることが確定している。
2.については昨年度に引き続き、M.Basaldellaとルディクスの対話的完全性についての共同研究を行った。これはゲーデルの古典的完全性とは対照的に、無限的・余代数的文脈でも意味をなすものであり、プログラミング理論における一般再帰型の一意的解釈という重要な応用につながることを指摘した。また、A.Saurin、M.Basaldellaと焦点化原理(線型論理の証明論における重要定理)理解に向けたルディクスの応用についての研究を継続し、特にこれまでのアイデアおよび成果を圏論的観点から再整備した。成果は「プログラム意味論の数理的基礎」国際会議(MFPS)にて発表され、Electric Notes in Theoretical Computer Science誌の特集号に掲載された。その他、過去の成果をまとめた論文2件を出版した。
|
