2003 Fiscal Year Annual Research Report
近似プログララムの計算論―古典論理の証明のテストにむけて―
| Project/Area Number |
15700001
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
|
|---|
| Keywords | 極限操作 / 部分組合せ代数 / 古典論理 / λμ計算 |
|---|
| Research Abstract |
プログラムと構成的数学の証明との対応であるCurry-Howardの対応は、林 晋氏により、近似プログラムと古典論理の証明との対応に拡張されたのだが、近似プログラムの計算系を与えることが必要になる。我々は、そこで、近似プログラムを、極限において正解を計算するプログラムと考え、極限操作を用いて計算するプログラムの意味論をまず考えたい。
そこで、我々は全ての部分組合せ代数Aから我々は別の部分組合せ代数a-lim(A)を構成した。その部分組合せ代数では、自然数上のどの表現可能な部分関数φ(n)もちょうど、Aで表現可能な自然数上の部分関数ξ(t,n)の極限部分関数lim t→∞ ξ(t,n)の形をしている。その表現可能部分関数を解析するために、計算論的学習理論のlimiting recursive functionの概念にならって特徴づけ、limiting partial r.e.setに関する[Gold 1965]の未解決問題のひとつの解答を得た。
部分組合せ代数a-lim(A)は適当な部分同値関係による商構造になっていて、それは、極限の構造を次の意味で持っている:a-lim(A)の各要素はAの要素による可算列の極限とみなせる。この論文では、我々はその極限構造をBarendregtの値域特性(もし組合せ演算の値域が有限ならばそれは一元集合である).さらに、我々はその構成法a-lim(-)を超限回繰り返すことにより、無限λ計算を解釈する.最後に,我々は型がないλμ計算を解釈するために、別の部分組合せ構造で並列極限操作を持つものを導入する。
|
