| 研究課題/領域番号 |
10680334
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 理学部, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| キーワード | 型理論 / 意味論 / モデル / カテゴリ理論 / 文法的性質 / 強正規化 / 部分構造理論 |
|---|
| 研究概要 |
前年度の研究により「2階のλ計算におけるいくつかの文法的性質のモデル論的な証明」について、いくつかの知見を得ることができた。申請時の研究計画では、本年度はそれに引き続き上記の成果をCCに拡張しさらにPTSに拡張する予定であった。実際にその拡張を行うには、前年度に想定していた構造より一般的なbicategoryという構造のほうが適当であることがわかったが、型理論の文法的性質の意味論的な証明という本来の適用範囲を広げるために、PTSに関して詳細に検討することは後回しにして、別の論理体系について考察を行なった。具体的には、部分構造論理(複数の論理体系の総称)におけるcut-free provabilityが成立/不成立という文法的性質を、FL-algebraやso-monoidという部分構造論理の意味論の枠組を使って示した。部分構造論理については、いくつかの体系についてcut elimination定理が成立し、それ以外の体系については成立しないことが知られている。cut-free provabilityはcut eliminationより弱い性質であるが、意味論的枠組で証明することによりいくつかの体系でcut-free provabilityが成立しない理由がより明確になった。さらにこの構造を使ってKripke semanticsを定義し、直観主義的様相論理(部分構造論理のひとつとみなすことができる)に対して従来より定義されているKripke semanticsとの関連を考察したが、直観主義的様相論理のKripke semanticsは直観主義的様相論理特有の性質を使って構成されているので部分構造論理に一般化するのは容易ではないことが判明した。
またexplicit environmentを持つ型付λ計算についての研究も行ない、強正規化性が成立するこを示した。この性質の証明は、元々の発想は意味論的なものであったが、完成した証明は今の所意味論的構造を離れている。
|
