| 研究課題/領域番号 |
10680334
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 理学部, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615)
腰越 秀之 千葉大学, 工学部, 助教授 (70110294)
|
|---|
| 研究期間 (年度) |
1998 – 1999
|
| 研究課題ステータス |
完了 (1999年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
1999年度: 900千円 (直接経費: 900千円)
1998年度: 1,400千円 (直接経費: 1,400千円)
|
|---|
| キーワード | 型理論 / 意味論 / モデル / カテゴリ理論 / 文法的性質 / 強制規化 / 部分構造論理 / 強正規化 / 部分構造理論 |
|---|
| 研究概要 |
平成10年度は、「2階のλ計算におけるいくつかの文法的性質のモデル論的な証明」について、いくつかの知見を得ることができた。通常、2階のλ計算のモデルのカテゴリ理論的な構成では、関数空間および2階の量化子をadjointにより定義するが、adjointをsemi-adjointに弱めたモデルを考えるとそれが強正規化性とβ同値な項の正規形の唯一性の証明に共通する構造であることがわかった。
申請時の研究計画では、11年度はそれに引き続き上記の成果をCCに拡張しさらにPTSに拡張する予定であった。実際にその拡張を行うには、前年度に想定していた構造より一般的なbicategoryという構造のほうが適当であることがわかったが、型理論の文法的性質の意味論的な証明という本来の適用範囲を広げるために、PTSに関して詳細に検討することは後回しにして、別の論理体系について考察を行なった。具体的には、部分構造論理(複数の論理体系の総称)におけるcut-free provabilityが成立/不成立という文法的性質をFL-algebraやso-monoidという部分構造論理の意味論の枠組を使って示した。これによりいくつかの体系でcut-free provabilityが成立しない理由がより明確になった。さらにこの構造を使ってKripke semanticsを定義し、直観主義的様相論理(部分構造論理のひとつとみなすことができる)に対して従来より定義されているKripke semanticsとの関連を考察したが、直観主義的様相論理のKripke semanticsは直観主義的様相論理特有の性質を使って構成されているので部分構造論理に一般化するのは容易ではないことが判明した。
またexplicit environmentを持つ型付λ計算についての研究も行ない、強正規化性が成立することを示した。この性質の証明は、元々の発想は意味論的なものであったが、完成した証明は今の所文法的な証明である。
|
