2002 Fiscal Year Annual Research Report
| Project/Area Number |
13680411
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, 電子・情報工学系, 助教授 (10195000)
|
|---|
| Keywords | 継続 / 公理化 / CPS変換 / コントロールオペレータ |
|---|
| Research Abstract |
本研究では,control delimiter(制御限定子)を持つ継続の体系,すなわち,限定継続の制御演算子の妥当な定式化を目的としている.前年度の研究では限定継続機構の動的側面にフォーカスを当てるため、より簡単な「動的例外」機構について厳密な理論的解析を行い、自然な型理論の枠組みにおさまるという結果を得た。今年度の研究では、限定継続機構そのものの研究にもどり、最も広く使われているshift/reset演算子を取りあげ、これに対する健全かつ完全な公理化を行った。shift/reset演算子の意味は、既にCPS変換に基づくものが与えられていたが、CPS変換は項をかなり大きくする変換であるため、変換後の項についての推論はかなり困難である。そこで、shift/reset演算子を使ったプログラムに対する推論を効率的に行うためには、直接の公理化が必要である。従来、このような公理化としては健全な規則がいくつか与えられていたのみであり、完全な公理化は与えられていなかった。我々は、CPS変換の逆変換というアイディアを援用することにより、完全な公理化が得られることを示し、具体的に12個の公理を得ることに成功した。これは、従来得られていなかった健全かつ完全な公理化を与えたという意味で大きな成果である。さらに、この公理系は、Computational Lambda Calculusの公理系、call/ccに対する公理系、shift/resetに固有の公理系の3種類の分類することができ、shift/resetに固有の公理系についてはほとんど最適(他の公理から導出できるものはない)であることを示すことができ、この未解決の問題に対する決着を付けた。
|
