| 研究課題/領域番号 |
25330013
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2018-03-31
|
| キーワード | 部分構造論理 / 代数的証明論 / 稠密化 / 共通型 / 整合空間 / 計算可能解析 |
|---|
| 研究実績の概要 |
本研究課題は(1)非古典論理の代数的証明論の推進、および(2)ラムダ計算における交差型（共通型）システムの意味論的基礎と応用の2点を眼目とするものである。
(1)の中心課題は、非古典論理の証明論におけるさまざまな証明変形の技法が、代数的にも意味を持つことを明らかにすることである。平成26年度は、まず前年度の研究を引き継ぎ、超シークエント計算における稠密規則の代数的解釈を行った。証明論で稠密化規則を除去することは、代数では全順序代数を稠密化することに相当する。このアイデアを応用し、uninorm logicをknotted axiomsで拡張した論理体系一般について、標準完全性定理を証明した。また、ブラウワーの不動点定理がヴカシェヴィッチ無限多値論理に不動点を加えた体系の無矛盾性と等価であることを証明した。それゆえもし後者の論理についてカット除去定理が証明できれば、ブラウワーの不動点定理の別証明（証明論による証明）が得られることになる。
(2)については、交差型と線形論理の表示的意味論（とくに整合空間意味論）との対応関係を念頭においた上で、計算可能解析における表現の理論へと応用する研究を始めた。実直線、ユークリッド空間、連続関数空間などは整合空間を用いて表現することができる。すると整合空間上の安定写像によって連続写像や連続作用素がぴったり表現できる。また興味深いことに、整合空間における線形写像は、実直線上では一様連続写像にちょうど対応することがわかった。このことからハイネの定理（実直線のコンパクト区間上で連続性と一様連続性が一致すること）の計算内容に当たる安定写像が存在することを示した。また別研究として、対数領域計算量を特徴づける論理（parsimonious logic）を非一様計算量へと拡張し、ラムダ計算の型システムとして整備を行った。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
非古典論理の代数的証明論の研究(1)は順調に進んでいる。前年度は2本の雑誌論文を投稿し、現在査読中である。また1本の論文が投稿準備中である。
一方でラムダ計算における交差型の研究(2)については、当初研究計画として挙げていた交差型と表示的意味論、ゲーム意味論との対応関係の確立には取り組むことができなかった。その代わり具体例として、交差型と整合空間の対応関係を計算可能解析へと応用する研究を始めた。平成27年度中には具体的成果が上がると思う。
また関連研究として、線形論理の亜種で、対数領域計算量を特徴づける論理（parsimonious logic）とラムダ計算の研究を行った（D. Mazza氏との共同研究）。さらに、当研究課題に関連する一般向け読み物も執筆した。
まとめると、必ずしも当初計画通りとは言えないものの、研究はさまざまな方向に有意義な拡がりを見せているといえると思う。
|
| 今後の研究の推進方策 |
前年度に始めた交差型と整合空間意味論を計算可能性解析に応用する研究を継続する予定である。また代数的証明論については、この10年間の成果を集大成した解説論文を書き上げたいと思っている。
その他にも散発的なテーマがいくつかある（ブラウワーの不動点定理、対数領域計算量の論理等）。これらについても研究を継続したい。
|
| 次年度使用額が生じた理由 |
平成26年度は5件の国外出張を行った。そのうち3件を本研究費から支出する予定であったが、2件で済ますことができたため余剰が生じた。
|
| 次年度使用額の使用計画 |
平成27年度より証明支援系を用いた研究を本格的に始める予定のため、平成26年度の余剰分はコンピュータの購入に充てる予定である。
|
