2015 Fiscal Year Research-status Report
非古典論理の代数的証明論とラムダ計算の交差型システムの研究
| Project/Area Number |
25330013
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| Project Period (FY) |
2013-04-01 – 2018-03-31
|
| Keywords | 部分構造論理 / 代数的証明論 / 完備化 / エルブランの定理 / 共通型 / 整合空間 / 計算可能解析 / 多相型ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
本研究課題は(1)非古典論理の代数的証明論の推進、および(2)ラムダ計算における交差型（共通型）システムの意味論的基礎と応用の2点を眼目とするものである。
(1)の中心課題は、非古典論理の証明論におけるさまざまな証明変形の技法が、代数的にも意味を持つことを明らかにすることである。平成27年度は、証明論に由来する剰余フレームの基礎理論に着手した。すでに剰余フレームは、カット除去と代数的完備化、稠密規則除去と代数的稠密化などの関係を統一的に理解するのに有用なことがわかっているが、これをさらに敷衍し、代数的論理の根幹部分へと推し進めるのが目標である。P. Cintula氏との共同研究では、証明論におけるエルブランの定理と順序代数におけるコンパクト完備化の関係について考察を進めた。またそれと関連して、一階述語部分構造論理や無限積・無限和を伴う部分構造論理の完全性定理を証明するための新しい手法を考案した。
(2)の中心課題は、交差型の理論を線形論理の表示的意味論に沿って発展させること、また応用としてラムダ計算の様々な性質を見ていくことにある。平成27年度は、前年度に引き続き、線形論理の整合空間を計算可能解析に応用する研究を進めた（松本慧氏との共同研究）。とくに基幹部分を再構成し、整合空間に基づく実現可能性解釈として圏論的に定式化した。またこの圏がこれまでに考案された種々の実現可能性解釈とは異なることを証明した。最後に関連研究として、伝統的証明論をラムダ計算へ応用する研究に着手した。具体的にはBuchholzのオメガ規則を応用することにより、多相型ラムダ計算のパラメータフリーな部分体系について、強正規化定理を「可術的に」証明することに成功した（秋吉亮太氏との共同研究）。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(1)については、前年度までに投稿した論文が順次採択されており、目に見える実績となりつつある。またCintula氏との共同研究を通して、部分構造論理における無限積の完全性など、新たな課題も見えてきた。ただし前年度に残されていたいくつかの問題（ブラウワーの不動点定理の証明論的証明、解説論文の作成など）は未だ中途段階にあり、引き続き努力が必要である。
(2)については、整合空間意味論の計算可能解析への応用というテーマが集約しつつある。成果をまとめた論文を近日中に投稿する予定である。また、伝統的証明論のラムダ計算への応用は、前者の専門家である秋吉氏との共同研究によって初めて見えてきた興味深い課題であり、大きな潜在力を秘めていると思う。すでに論文一本が採択されており、今後の展開についてもある程度の見通しがある。一方で本来掲げていた目標の一部、たとえば交差型（線形論理の表示的意味論）を用いてラムダ計算における種々の問題の決定可能性を示すという目標は、やや滞っている。引き続き努力が必要である。
|
| Strategy for Future Research Activity |
今年度はまず、共通型を用いて高階マッチング問題の決定可能性を示す課題に再挑戦したい。その他はおおむね前年度の研究を継続する予定である。
|
| Causes of Carryover |
国内旅費が予定よりも少額で済んだため。
|
| Expenditure Plan for Carryover Budget |
国内外旅費に充填する。
|
