2021 Fiscal Year Research-status Report
Modelling of Control Capture and Its Applications
| Project/Area Number |
20K11743
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
西崎 真也 東京工業大学, 学術国際情報センター, 教授 (90263615)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | 関数型プログラミング言語 / 型システム / ラムダ計算 / 継続 / dynamic-wind / 制御捕捉 |
|---|
| Outline of Annual Research Achievements |
大域脱出(catch&throw, try-catch)と制御捕獲機能(finally, unwind-protect)による例外処理機構に対する新たなλ計算の研究を進捗させた。
2020年度以前に，エフェクトシステムにより副作用を定式化した単純型付きλ計算上での，catch&throw/unwind-protectの定式化を論文“Effect System with Control Capturing”で研究してきた。この成果，及び，論文“Translation Style Semantics and Type System of Control Capturing”で研究した継続渡しスタイル変換による定式化の成果をベースとして，計算モデルを研究への取り組みを継続した。
一級継続（call/cc）と制御捕獲機能(dynamic-wind)による例外処理機構に対して新たなλ計算についても研究を継続し、最初に述べた研究と並行し，一級継続と制御捕獲を有する新たなλ計算ベースの計算体系を確立することに成功した。具体的には、エフェクトシステムにより副作用を定式化した単純型付きラムダ計算において、call-with-crrent-continuation・dynamic-windを導入し定式化したような体系となっている。そして、この他系において理論的な性質を示した。
また、当該年度においては、単純型付きエフェクトシステムへのCPS変換により意味を与えることを研究を継続し、副作用がないサブセットにおいて，ＣＰＳ変換が意味を保存していることや，型がついているプログラム式において停止性が成り立つことなど，理論的性質の研究も引き続き取り組んでいる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
コロナ禍のため、コロナ禍以前よりも研究者間でのコミュニケーションは低調となったものの、リモート実施の国際会議参加を通して、研究交流を行なうことにより補完している。
それ以外の点については概ね順調である。
|
| Strategy for Future Research Activity |
CPS変換（継続渡しスタイル変換）を用いたcall-with-current-continuationとdynamic-windの意味論の定式化を完成することを今後の推進方策とする。そこでの具体的な課題として、CPS変換意味論と、エフェクトシステムと単純型付きラムダ計算という枠組みのもとでの操作的意味論と、継続渡しスタイル変換による意味論との等価性を証明することがあげられる。さらに実践的な課題としては、理論的な成果からの言語処理系における設計や実装に対する貢献があげられる。
|
| Causes of Carryover |
コロナ禍により、国内旅費及び外国旅費の支出が抑制されることにより、設備備品費や消耗品費は、運営費交付金を始めとする別の研究費により充当されたため。
次年度使用については、新型コロナウイルス感染症拡大措置の緩和による、国内研究集会及び国外研究集会の実施の再開が見込まれる。それらの研究集会に参加することにより、情報交換、特に、これまでの研究成果に関する情報交換を通して、本研究課題の研究を一層推進していくことを予定している。情報交換については、プログラミング言語Schemeの制御捕獲の形式化に関する国際的な動向や、制御捕獲に関連する理論、例えば、代数的エフェクト等の研究についての情報交換について焦点を当てることを予定している。
|
