2016 Fiscal Year Research-status Report
継続と文脈の概念にもとづく新しい関係的プログラム意味論
| Project/Area Number |
16K12409
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | Call/cc / 継続演算子 / 環境双模倣 / プログラム等価性 |
|---|
| Outline of Annual Research Achievements |
Call/cc（call-with-current-continuationの略）とは、「残りの計算」を表す「継続」を取り出して変数に束縛（代入）し、後で呼び出せるようにする言語機能である。具体的構文は言語によって異なるが、例えば42 + (callcc k. k(777) + 13)というプログラムを考えると、callcc kによって取り出される「残りの計算」すなわち「継続」はk(x) = abort(42 + x)なる関数kによってあらわされる。ただしabortはその時点での残りの計算（継続）を捨てて、中の式の計算のみを続ける演算子である。したがって、前述のプログラムはk(777) + 13（ただしkは上述の関数）すなわちabort(42 + 777) + 13すなわち42 + 777と計算される。
このように、call/ccは大域脱出(global exit)や命令型言語のgotoないしC言語でいうsetjmp/longjmpのような制御構文を表すことができる強力な演算子であるが、その強力さのため、call/ccを用いたプログラムに関する理論、特にプログラム等価性は困難な問題であった。本研究では研究代表者らによる環境双模倣の理論を発展させ、call/ccを持つλ計算の、文脈等価性(contextual equivalence)に対して健全(sound)かつ完全(complete)なプログラム等価性理論を初めて定義し、複数の自明でないプログラム等価性の例を証明した。本研究は博士前期課程学生との共同研究である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画のとおり、call/ccに関する理論を定義した上、自明でない複数の例を証明することができた。
|
| Strategy for Future Research Activity |
本年度の知見を対称λ計算(symmetric lambda-calculus)や、環境双模倣の改良に活用・応用していく。
|
