研究課題
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)なプログラム等価性理論を初めて定義し、複数の自明でないプログラム等価性の例を証明した。本研究は博士前期課程学生との共同研究である。
2: おおむね順調に進展している
研究計画のとおり、call/ccに関する理論を定義した上、自明でない複数の例を証明することができた。
本年度の知見を対称λ計算(symmetric lambda-calculus)や、環境双模倣の改良に活用・応用していく。
すべて 2016
すべて 雑誌論文 (1件) (うち査読あり 1件、 謝辞記載あり 1件) 学会発表 (1件) (うち国際学会 1件)
Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Lecture Notes in Computer Science
巻: 10017 ページ: 171-186
10.1007/978-3-319-47958-3_10
