2015 Fiscal Year Annual Research Report
| Project/Area Number |
25540001
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / プログラム等価性 / 継続演算子(call/cc) / 環境双模倣 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は研究代表者らの環境双模倣を発展させた非単調な再帰的定義の理論である。主な成果として研究協力者との共同研究により、代表的な継続演算子の一つであるcall/ccを持つ値呼び型無しλ計算のための新たな等価性証明手法を定式化し、その健全性・完全性を証明した。以下にその詳細の一部を記述する。Eは評価文脈である。値の上の二項関係Rがadquate up-to contextであるとは、以下の条件を満たすことと定義する。(1) (λx.M) R (λx.M') ならば、任意のW = [~V/~x]C, W' = [~V'/~x]C, E = [~V/~x]E0, E' = [~V'/~x]E0, ~V R ~V' に対し、E[[W/x]M] ～_R E'[[W'/x]M']。ただし～_R は以下の条件をすべて満たす最大の対称な関係と定義する。(2) M ～_R M' かつ M → N ならば、M' →* N' なる N' が存在し、N ～_R N' または N = [~V/~x]C, N' = [~V'/~x]C, ~V R ~V' の形。(3) V ～_R M' ならば M' →* V' なる V' が存在する。従来の環境双模倣との大きな違いは、簡約の途中でcall/ccにより継続が取り出される可能性があるため、条件(1)において任意のEを考慮する必要がある一方、条件(3)においてR に(V, V')を追加する必要がない点にある。任意のEを考慮することは一見すると重い条件のように思われるが、(2)の後半のup-to contextによりEをキャンセル（吸収）することが可能なため、証明の負担は大きく変わらない（特にcall/cc を用いない場合）。この大きな特徴はcall/ccがないλ計算等における環境双模倣にも応用可能であり、今後のさらなる理論の発展が期待できる。
|
