| 研究課題/領域番号 |
10680334
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| 研究分担者 |
西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615)
腰越 秀之 千葉大学, 工学部, 助教授 (70110294)
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 理学部, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| キーワード | 型理論 / 意味論 / モデル / カテゴリ理論 / 文法的性質 / 強正規化 |
|---|
| 研究概要 |
本研究の目的である「2階のλ計算におけるいくつかの文法的性質のモデル論的な証明」について、いくつかの知見を得ることができた。通常、2階のλ計算のモデルのカテゴリ理論的な構成では、関数空間および2階の量化子をadjointにより定義するが、adjointをsemi-adjointに弱めたモデルを考えるとそれが強正規化性とβ同値な項の正規形の唯一性の証明に共通する構造であることがわかった。また、既に知られているHyland-Ongの構成では、λ項の集合を適当な関係で割ったものがcpcaになりそのcpca上のPERを型の解釈としているが、本研究では、もっと直接的にλ項の集合上のある条件を満たすPERを型の解釈とすることにより、強正規化性の証明において使われる条件とモデルの構成のためだけに使われる条件を明確に区別することができた。以上のことについては“Categorical Model Construction for Proving Syntactic Properties"という論文として発表した。
そして現在さらにこれらの結果を拡張することを考えている。まず、2階のλ計算の拡張である型理論体系CCにおいても「型付け可能な項は強正規化性を持つ」という性質があることが知られているので、上記の結果をCCの場合に拡張した。拡張自体は可能であるが、既に知られているその性質の文法的証明を検討した結果、その証明の構造を素直にモデルの構成と見なすには、bicategoryと呼ばれるさらに一般的な構造を考えたほうかよいことがわかった。また、上記の種類の型理論だけではなくもっと広い範囲で文法的性質のモデル論的な証明ができるかどうかを調べるため、部分論理のカット無しでの証明可能性についてモデル論的証明ができることを示した。
|
