2007 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 |
置換簡約の強正規化可能性は近年活発に研究されている。また、定理自動証明システムGoqは、フランスで研究開発されている証明システムで、基本理論と応用の両面で成功している。本研究では、これらの研究成果を深化発展させることにより、置換簡約の型理論の研究を行った。本年度は次の研究成果を得た。(1)より単純な飽和集合を選言と二階存在限量子に対して定義し、その健金性定理を証明し、それを用いて置換簡約を含む二階自然演繹の強正規化可能性定理のより単純な証明を与えた。この定義により、選言に対する飽和集合はPi-0-1内包により、二階存在限量子に対する飽和集合はSigma-1-1内包により定義できた。(2)ラムダミュー計算におけるミュー簡約と選言に対する置換簡約の最大簡約長を項の構成に関する帰納法により与えた。(3)選言とその置換簡約を含む二階自然演繹の強正規化可能性定理のCPS変換を用いる証明を与えた。このことは、従来知られていた不完全な証明を増加項の概念を用いて完成させることによりなされた。
|
