2020 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 | 関数型言語 / ラムダ計算 / 一級継続 / 例外処理 / 制御捕獲 / 一級環境 |
|---|
| 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”で研究したCPS変換による定式化の成果をベースとして，計算モデルを研究に取り組んだ。また，停止性定理等の基本的性質や型推論アルゴリズムの研究をはじめた。
一級継続（call/cc）と制御捕獲機能(dynamic-wind)による例外処理機構に対して新たなλ計算についても研究をはじめた。最初に述べた研究と並行し，一級継続と制御捕獲を有する新たなλ計算ベースの計算体系を検討している。単純型付きエフェクトシステムへのCPS変換により意味を与えることを研究をはじめ、副作用がないサブセットにおいて，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 |
大域脱出(catch&throw, try-catch)と制御捕獲機能(finally, unwind-protect)による例外処理機構に対する新たなλ計算の確立し、CPS変換による定式化の成果をベースとして，計算モデルの研究を更に進める。また，停止性定理等の基本的性質や型推論アルゴリズムの研究を継続する。
一級継続（call/cc）と制御捕獲機能(dynamic-wind)による例外処理機構に対して新たなλ計算についても研究を続ける。最初に述べた研究と並行し，一級継続と制御捕獲を有する新たなλ計算ベースの計算体系を確立する。単純型付きエフェクトシステムへのCPS変換により意味を与えることを研究をはじめ、副作用がないサブセットにおいて，CPS変換が意味を保存していることや，型がついているプログラム式において停止性が成り立つことなど，理論的性質を研究する。
|
| Causes of Carryover |
新型コロナウイルス感染症拡大による本務の大学の研究費（法人運営費）においても出張旅費の未執行が発生し、それにより本補助金で執行すべきであった研究に用いる機器の費用が充当することが起こり、それを用いて本研究課題を推進することができた。本年度の成果を次年度において、発表するための出張旅費等に充てることを想定し、そのために、次年度使用額を生じることになった。
|
