2009 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)非可換一階シーケント計算NCLKを構成した。まず、非可換positive fragmentを普通の一階シーケント計算で前件にグループがあり右交換規則のない論理体系LK-に拡張した。次のことを示した。(i)NCLKはLJに同等、(ii)NCLKに交換規則を追加するとLKに同等になる、(iii)LK-はLJに同等、(iv)LK-とNCLKの間の翻訳がある。
(3)否定、積、多相型、存在型から成るラムダ計算のinhabitation問題が決定可能であることを証明した。このため、対応する論理体系である含意と選言をとり除いた二階自然演繹について、その証明可能性が決定可能であることを証明した。
|
Research Products
(3 results)
