型理論とその周辺

点击翻译按钮获取中文摘要

型理論の研究で明らかにしたい事柄の一つに,与えられた型システムで型付け可能な項全体を適当な同値関係(例えば,β同値,βη同値,またはその他の同値関係)の下で同値類に分類したとき,その全体がどのような数学的構造を成すかを知ることが上げられる.これは本来,意味論の中心的な研究課題であると言えるが,型理論の場合,この問題に対して構文論(または証明論)的なアプローチの可能性が考えられる.本研究では,構文論的アプローチによって,単純型理論における型付き項全体を,同値関係βηで割った商集合を,ある種の文法的手法を用いて表現することに成功した.ここで用いた手法は,文脈自由文法の名で親しまれている概念を,この目的のために拡張したもので,述語論理における項や,これを拡張した種々の型理論の項から成る集合を端的に表現できる一般的な枠組みであり,今後,単純型以外の種々の体系に対しても,有用性を発揮することが期待される.この,新たに導入した文法的方法の一つの応用として,型理論の型付き項を用いて,自由代数構造の上のどのような関数が表現可能かを調べる問題が上げられる.型のないラムダ計算の項を用いて表現可能な自然数関数はちょうど計算可能関数と一致し,単純型理論の場合はそれが拡張多項式と一致することが知られているが,これを一般の自由代数構造上の関数に拡張すると,単純型理論の場合でも議論が非常に複雑になり,その結果,表現可能な関数についてある種の特徴付けがすでに得られているものの,満足のいく結果とは言い難い.この問題に対して,我々の文法的手法を用いて,既存の結果とは異なる見通しの良い新しい特徴付けを得ることができた.この結果を更に単純型以外の型理論に拡張する試みを今後続けたいと計画している.