1999 Fiscal Year Annual Research Report
| Project/Area Number |
10680334
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
古森 雄一 千葉大学, 理学部, 教授 (10022302)
辻 尚史 千葉大学, 理学部, 教授 (70016666)
|
|---|
| Keywords | 型理論 / 意味論 / モデル / カテゴリ理論 / 文法的性質 / 強正規化 / 部分構造理論 |
|---|
| Research Abstract |
前年度の研究により「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を持つ型付λ計算についての研究も行ない、強正規化性が成立するこを示した。この性質の証明は、元々の発想は意味論的なものであったが、完成した証明は今の所意味論的構造を離れている。
|
-
[Publications] Masahiko Sato: "Explicit Environments"Proc. of TLCA '99 (LNCS 1581). 340-354 (1999)
-
[Publications] Takafumi Sakurai: "Categorical Model Construction for Proving Syntactic Properties"Int. J. of Foundations of Computer Science. (Toappear).
-
[Publications] Sachio Hirokawa: "A lambda proof of the P - W theorem"The Journal of Symbolic Logic. (Toappear).
-
[Publications] Mitsuharu Yamamoto: "Evolution of Inductive Definitions"Proc. of IWPSE 99. 17-21 (1999)
-
[Publications] 山本 光晴: "モデル検査アルゴリズムの検証について"日本ソフトウェア科学会第16回大会論文集. (1999)
