2008 Fiscal Year Annual Research Report
| Project/Area Number |
19540156
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 National Institute of Informatics, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Keywords | 置換簡約 / 型理論 |
|---|
| Research Abstract |
置換簡約の強正規化可能性は近年活発に研究されている。また、定理自動証明システムCoqは、フランスで研究開発されている証明システムで、基本理論と応用の両面で成功している。本研究では、これらの研究成果を深化発展させることにより、置換簡約の型理論の研究を行う。特に、(1)置換簡約やその関連概念を用いて論理体系および型付ラムダ計算を拡張した体系について、それを構築し、その基本性質を明らかにする。(2)Coq理論を置換簡約などにより拡張する。本年度は次の研究成果があった。
(1)遺伝的置換子を特徴付ける型が存在しないという定理を証明した。また、可算無限個の型を与え、これが遺伝的置換子を特徴付けるという定理を証明した。第一の定理は、遺伝的置換子全体が枚挙不可能であることを示すことにより証明された。第二の定理は、共通型型理論を用い、レベルnに対する型同型nを定義し、それにより深さnまでは遺伝的置換子であることが特徴付けられる型pnを定義し、そのような型pn全体を用いることにより、証明した。
(2)型簡約と等号理論を与え、これらが共通型の型同形を特徴付けるという定理を証明した。共通型の型同形は代入にたいして安定ではないことを示し、他の型理論のように合同関係による特徴づけができないことを示した。次に型簡約を導入し、与えられた型を同形であるがより単純な型に変形できることを示した。最後に、等号理論を与え、この簡約に関して正規である型に関する同形がこの等号理論におり特徴つけられることを証明した。
|
Research Products
(2 results)
