| 研究課題/領域番号 |
25330013
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2018-03-31
|
| キーワード | 部分構造論理 / 代数的証明論 / 正準拡大 / エルブランの定理 / ラムダ計算 / 共通型 |
|---|
| 研究概要 |
本研究課題は(1)非古典論理の代数的証明論の推進、および(2)ラムダ計算における交差型（共通型）システムの意味論的基礎と応用の2点を眼目とするものである。
(1)について、非古典論理の代数的証明論の根本にあるのは、証明論的技法は代数の文脈に直接適用可能であり、またその逆も成り立つという洞察である。平成25年度は、証明論における超シークエント計算と代数（双対性理論）における正準拡大のアイデアを融合し、「超正準拡大」の手法を確立した。これは、よい性質を保ちつつFL代数を完備化するための手法である。応用として、様々な非古典述語論理についてエルブランの定理を代数的に証明し、エルブランの定理の代数的本質をとらえることに成功した。また、超シークエント計算における稠密規則除去定理のアイデアを順序代数の文脈に応用し、与えられた全順序FL代数を稠密化するための統一的手法を開発した。応用として、ファジー論理の重要な体系の一つであるuninorm logicが標準意味論について完全であることの代数的証明をはじめて与えることに成功した。以上２件について国際学会の招待講演で発表した。
(2)について、単純型付きラムダ計算における交差型（共通型）は、ある種の文脈で高速なプログラム実行（つまりラムダ項の評価）に応用できること、また線形論理のスコットモデルと密接な関係のあることが過去の研究により明らかになっている。平成25年度は過去の研究を継承し、ラムダ計算の別のモデルであるエンゲラーモデルとの関係を明らかにした。また不動点演算子を含む単純型付きラムダ計算へと研究を広げた。未だ継続中であるが、現段階までの予備的成果を国際学会の招待講演で発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
平成25年度は、研究のみならず、教育・成果普及面にも力を入れた。実際、日本国内における数学基礎論サマースクールの主催・講義、およびグルジアにおけるサマースクールの講師役を務めた。高校生向けの合宿セミナーでも講義を行った。特にグルジアで行った講義は、本研究課題に密接に関係するものである。
他方で論文の執筆がやや遅れている。２本の論文に取り組んだが、一方は現在査読中、もう一方は投稿準備中である。
最後に、交差型研究から派生した別の研究課題（線形論理意味論を用いた計算可能解析の基礎づけ）に着手したため、当初の計画にあった交差型の研究目標が十分に達成されていない。次年度に出来る限り遅れを取り戻そうと思う。
|
| 今後の研究の推進方策 |
まずは平成25年度に挙げた成果をまとめあげ、それらに関して2本の論文を執筆する予定である。また、前年度に達成できなかった目標（交差型と表示意味論の対応に関する一般論、および交差型とゲーム意味論の関係の確立）に引き続き取り組む。さらに、前年度の研究を通して浮かび上がった新たなアイデアにも取り組みたい。すなわち線形論理意味論を用いて計算可能解析の基礎づけを行う研究である。
それ以外の点については、当初の研究実施計画通りに進める予定である。
|
| 次年度の研究費の使用計画 |
年度末時点で、平成26年度の海外出張予定がすでに３件入っていたため、研究費の一部を次年度に回すことにした。
下記３件の出張旅費に使用予定。
(1) Workshop on Higher Order Computation: Types, Complexity, Applications （パリ、6月16日－18日）および Workshop on Abstraction and Verification in Semantics (パリ、6月23日－27日)、 (2) Vienna Summer of Logic （ウィーン、7月9日－24日のうち一部参加）、(3) 21st Workshop on Logic, Language, Information and Computation （チリ、9月1日－4日）。
|
