| 研究課題/領域番号 |
21700014
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| キーワード | 情報基礎 / 数理論理学 / 線型論理 / 部分構造論理 / ルディクス / 国際研究者交流 / オランダ:オーストリア:アメリカ |
|---|
| 研究概要 |
本研究は1.部分構造論理の代数的証明論、および2.ルディクスをはじめとするゲーム意味論一般への余代数的アプローチを主眼とするものである。
1.については、剰余束論や様相代数の文脈で代数的証明論の手法を応用し、自由代数の特徴づけや「間マクニールー正準拡大」による代数の拡大の研究を行った(Y.Venemaとの共同研究)。とりわけ「間マクニールー正準拡大」を体系的に取り扱う方針を示し、また興味深い具体例をいくつか発見した。成果は第二回順序・代数・論理国際会議における招待講演で発表した。また、部分構造論理の代数的証明論の第一主論文をまとめ上げ、Annals of Pureand Applied Logic誌にて公表した(A.Ciabattoni、N.Galatosとの共同研究)。
2.については、ルディクス理論よりもやや研究範囲を拡大し、ゲーム意味論に基づくラムダ項(プログラム)の実行方法の研究を行った。計算量理論的に実証可能な形で、最適なプログラム実行方法を求めるのが研究の目的である。結局、標準的なβ簡約と、線型論理のスコットモデル上での解釈、それからクリヴィン機械(これはゲーム意味論と関連が深い)の3種を混合したハイブリッドな実行方法が最適であるという結果が得られた。それにより、ラムダ項正規化に関して「オーダーが1上がるごとに時間計算量クラスと領域計算量クラスが交代してあらわれる」という非常に興味深い現象を捉えることに成功した。成果は第23回「リライティング技法とその応用」国際会議にて発表予定である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
代数的証明論およびルディクス理論の研究については、意義のある成果を複数挙げ、一定の評価を得ているものと自負している(これは当該期間中に5回招待講演の依頼を受けたことにより裏付けられる)。前者については、すでに第一主論文を出版し、また興味深い課題が次々に出てきており、活発な状況である。後者についても、当初計画の半分程度は遂行できたものと思う。ただし前者の代数的発想と後者の余代数的発想の融合を模索する研究については、未だ発表可能な成果は出ておらず、達成度は不十分である。
|
| 今後の研究の推進方策 |
上に述べた代数的発想と余代数的発想の融合について集中的に研究を行う必要がある。また代数的証明論の第二主論文を今年度中にまとめ上げる予定である。ルディクス理論については、当初計画の後半に取り組むとともに、(すでに前年度から試みていることであるが)やや研究範囲を拡大し、ゲーム意味論一般およびそれに基づくプログラム実行方法についての諸問題に取り組みたい。前年度の成果であるラムダ項(プログラム)の最適な実行方法に関する研究は、多くの関連研究を持ち、将来的発展を十分に見込めるものである。それゆえ本研究課題から派生した重要課題として、集中的に取り組みたい。
|
