2010 Fiscal Year Annual Research Report
| Project/Area Number |
19540156
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Keywords | 置換簡約 / 型理論 |
|---|
| Research Abstract |
置換簡約の強正規化可能性は近年活発に研究されている。また、定理自動証明システムCoqは、フランスで研究開発されている証明システムで、基本理論と応用の両面で成功している。本研究では、これらの研究成果を深化発展させることにより、置換簡約の型理論の研究を行う。本年度は次の研究成果があった。
(1)multiple quantifierとは、任意個数の複数個のquantifierを導入または除去で.きる規則をもつquantifierである。否定、直積と存在に関するmultiple quantifierをもつ型付ラムダ計算の型推論が非決定可能であることを証明した。また、任意に関するmultiple quantifierと含意をもつ型付ラムダ計算の型推論が非決定可能であることを証明した。
(2)型理論Fの項として、型理論Fのある単射解釈の像に対するecompiler-normalizerを与えた。これらの項、評価による正規化、および型理論Fのベータイータ完全モデルの関係を明らかにした。
(3)マルチステージ言語のレコード計算への翻訳を与え、型をもつという性質が保たれることを証明し、また、翻訳が簡約に関して模倣であることを証明した。この翻訳により、マルチステージ言語のプログラム検証をレコード計算のプログラム検証に帰着した。
|
