研究課題
19世紀末に創始された数理論理学は、完成した集まりとして無限を扱う実在論と、際限なく続くプロセスとして無限を扱う反実在論という二つの立場に厳密な数学的定式化を与えた。特に、数理論理学の一分野である証明論は、順序数表記系と呼ばれる数体系を導入し、公理系の中の形式的証明を順序数に対応付けることで、その公理系がどの程度の反実在論を表現しているのかについての尺度を与えた。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの枠組みの中で捉える観点をもたらした。本研究の目的は、線形論理がもつゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的反実在論を反省し分析することである。本年度は、順序数とゲームを共存させることのできる枠組みとして型理論に着目し、それについて研究することで次年度以降の研究の準備を行なった。まず、項書換え系と呼ばれる計算規則を単純型付きラムダ計算に加えたときに計算の停止性が保存される条件について研究した。このことを通して、プログラミング言語の一種でもある型理論の計算的側面を探究した。次に、マーティン・レーフ型理論の中で、ユニバース型と呼ばれるデータ型の構成を際限なく繰り返すことのできる演算子を定式化した。ユニバース型からは順序数と類似した構造をもつデータを構成できるため、この演算子の定義を通して、型理論の中で順序数を際限なく構成するアプローチを模索した。
2: おおむね順調に進展している
前年度は線形論理におけるゲームの研究を進めることができたのに対し、本年度は、順序数表記系とゲームを共存させることのできる枠組みである型理論の研究に進捗があったことが主な理由である。特に、項書換え系を単純型付きラムダ計算に加える研究を、1本の査読付き英語論文にまとめることができた。また、マーティン・レーフ型理論についての研究を手がかりに、順序数表記系と線形論理の研究の統合に関してもアイデアを得ることができた。
次年度は、前年度と同様に、順序数表記系の研究と線形論理の研究を並行して進展させるという課題を主軸とする。さらに、本年度に得られた着想をもとに、これらの研究の統合を視野に入れて研究活動に従事する。
すべて 2022
すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (1件) (うち国際学会 1件)
27th International Conference on Types for Proofs and Programs (TYPES 2021), Leibniz International Proceedings in Informatics (LIPIcs)
巻: 239 ページ: 12:1--12:23
10.4230/LIPIcs.TYPES.2021.12
