2016 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 | 部分構造論理 / 不動点定理 / Lukasiewicz論理 / 素朴集合論 / 多相型ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
本研究課題は（１）非古典論理の代数的証明論の推進、および（２）ラムダ計算における交差型（共通型）システムの意味論的研究と応用の２点を眼目とするものである。
（１）については、非古典論理の証明論をブラウワー流の不動点定理と関連付ける研究を集中的に行った。Lukasiewiczの無限多値論理（およびその下位論理）は自己否定を始めとする不動点演算子を加えても無矛盾なことが知られており、その証明には普通ブラウワーの不動点定理が用いられる。本年度はその逆方向、つまりLukasiewicz論理＋不動点演算子の無矛盾性を証明論的に示すことにより、ブラウワーの定理に別証明を与える可能性を追求した。成功すれば非古典論理証明論の純数学的応用としての意義がある。未だ完全証明には至っていないものの、関連成果として不動点演算子と矛盾しない部分構造論理の範囲確定に一定の成果を挙げた。また密接に関連する事柄として、ファジー論理の基礎であるMTL論理上の素朴集合論が無矛盾であることを証明した。最後に別方向の研究として、伝統的証明論における３値意味論を用いたカット除去定理証明法と矛盾許容論理の関連性に着目し、部分構造論理へと一般化する研究を行った。
（２）については、前年度に引き続き、伝統的証明論とラムダ計算の型理論を関連づける研究を進めた。具体的には可術的・帰納的な体系と非可術的な体系の比較という伝統的証明論以来の課題を取り上げ、そのための技法（BuchholzのΩ規則）ごとラムダ計算の文脈にもたらす研究である。本年度はまずシステムTを一般化し、反復帰納的データ型を持つ体系を考え、それがシステムFのパラメータフリーな部分体系と表現力において一致することを明確にした。さらに二階多相型から高階多相型へと研究を発展させ、強正規化性定理の可術的証明を進めた。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
（１）について：本年度は、ブラウワー不動点定理の証明論的分析に専念したため、代数的証明論の他の課題にはあまり手がつけられなかった。不動点定理そのものについても最終的解決には至らず、いま少し工夫が必要なようである。
（２）について：本年度は共通型そのものではなく、その派生的な研究を主に進めた。共通型自体については、他研究者の研究により線形論理との関係がより深いレベルで明らかになりつつあるが、筆者自身はその動向をフォローするにとどまっている。
|
| Strategy for Future Research Activity |
（１）については、ブラウワー不動点定理の証明論的分析を継続する。（２）については、当初の目的に立ち返り、共通型に基づいて高階マッチング問題に明快証明を与えることに集中したい。
|
| Causes of Carryover |
本科研費より支出予定だった海外出張の一部が先方負担に変わったため。
|
| Expenditure Plan for Carryover Budget |
国内外出張旅費に充てる。またプレゼンテーション用のノートパソコンを購入する。
|
