2018 Fiscal Year Annual Research Report
Algebraic Proof Theory for Nonclassical Logics and Intersection Types for Lambda Calculus
| Project/Area Number |
25330013
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| Project Period (FY) |
2013-04-01 – 2019-03-31
|
| Keywords | 二階述語論理 / 代数的証明論 / MacNeille完備化 / 線形論理 / 証明ネット |
|---|
| Outline of Annual Research Achievements |
前年度に引き続き、順序数解析における重要技法の1つであるΩ規則について、代数的観点から研究を行った。Ω規則は可術的なカット除去証明に用いられる構文論的な手法であるが、ブール代数・ハイティング代数の文脈で解釈するとMacNeille完備化と密接な関係にあることがわかる。後者の完備化は、代数的なカット除去証明のエッセンスでもある。そこでこの発見に基づいてΩ規則の代数版・Ω解釈の概念を導入し、二階述語論理の部分体系に対して可術的かつ代数的なカット除去の証明を与えた。
二階算術Z2の１無矛盾性が二階述語論理全体のカット除去と同値であることは竹内外史以来よく知られている。上記の応用として、同様の対応関係が帰納的定義の算術理論IDｎ（ω未満）と二階述語論理のパラメータフリーな部分体系LIPｎについて成り立つことを、代数的意味論を用いて証明した。以上の成果については、概要を国際学会CSL2018にて発表し、詳細を雑誌論文にまとめ上げ投稿済みである。
その他に行った研究として、(i)線形論理の証明ネットと量子計算に関する基礎研究、(ii)線形論理の有限表示意味論を用いた証明ネットの高速評価の研究が挙げられる。(i)については、過去に調べたブール回路との正確な対応関係を量子回路へと拡げる可能性を模索した。(ii)については、過去の研究で線形論理のスコットモデルを用いてラムダ項の意味論的評価を行う手法を考案したが、代わりに（集合版）整合空間モデルを用いることにより、意味論的評価を（証明ネットの意味での）「実験」とみなし、証明ネットへと適用範囲を拡げる研究を行った。
|
