| 研究課題/領域番号 |
20K11743
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
西崎 真也 東京工業大学, 学術国際情報センター, 教授 (90263615)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
|---|
| キーワード | プログラム理論 / プログラミング言語 / 大域脱出 / 制御捕獲 / 関数型プログラミング言語 / 型システム / ラムダ計算 / 継続 / dynamic-wind / 制御捕捉 / 関数型言語 / 一級継続 / 例外処理 / 一級環境 / 制御構造 |
|---|
| 研究開始時の研究の概要 |
制御捕獲）は制御の流れを強制的に捕獲するしくみであり，Javaのfinallyブロック，Schemeのdynamic-windが代表的である。 そして，例外処理機構は，大域脱出 と制御捕獲により構成されている。この制御捕獲については理論的側面において未解明である。 本研究では，これまでの大域脱出・一級継続の研究結果を基盤として，制御捕獲の計算モデ ルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして，様々なプログラミングパラダイムに対しても研究を進める。さらにその計算モデルを基盤として，制御捕獲機能を有する例外処理機構に対するソフトウェア検証手法と確立する。
|
| 研究実績の概要 |
例外処理機構は、多くのプログラミング言語において重要な仕組みであり、大域脱出とfinallyブロックを通じてコントロールキャプチャが提供されている。大域脱出や一級継続は、意味論や数理論理学との関連性を含め、多くの研究成果が得られている。しかし、コントロールキャプチャに関する研究はまだ不十分である。
本研究では、これまでの大域脱出・一級継続の研究結果を基盤として、コントロールキャプチャ機能を有する例外処理機構の計算モデルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして、命令形言語やオブジェクト指向言語など様々なプログラミングパラダイムに対して研究を進める。さらに、その計算モデルを基盤として、コントロールキャプチャ機能を有する例外処理機構に対する検証手法を確立する。
研究成果によって、コントロールキャプチャ機能に対する新たな理解が深まり、導入されていない言語への指針が得られ、コントロールキャプチャや例外処理機構を用いたプログラムのシステム検証の構築が期待される。プログラミング言語における関数クロージャは、自由変数を含む関数本体と、それらの値との関連付け（環境）を伴う。従来の理論では、関数クロージャから環境部分を抽出することで、環境を第一級オブジェクトとして扱う必要があった。本研究では、ラムダ計算において関数クロージャの環境を別の関数クロージャの環境と置き換える方法を提案し、環境を直接第一級オブジェクトとして扱うことを避ける。
新たな計算システム「環境移植を伴うラムダ計算」が導入され、構文・簡約規則で定義される。変換意味論により簡約の健全性が示され、簡単な型システムと主題簡約性が提供される。このアプローチは、関数クロージャの理解と扱いを改善する新たな方法を提案している。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究は、例外処理機構におけるコントロールキャプチャ機能を持つ計算モデルの提案を目指して順調に進展している。これまでの大域脱出や一級継続に関する研究成果を活用し、関数型言語や命令形言語、オブジェクト指向言語などのプログラミングパラダイムに対応する計算モデルを構築することができている。また、この計算モデルを基盤に、コントロールキャプチャ機能を持つ例外処理機構に対する検証手法の確立に取り組んできた。
意味論や数理論理学との関連性を含めた研究成果を得ており、コントロールキャプチャに関する研究の不足を補うことが期待される。さらに、コントロールキャプチャ機能を持つ例外処理機構の理解が深まり、プログラミング言語の設計や開発に新たな指針が与えられる可能性がある。本研究の進展により、従来不十分であったコントロールキャプチャに関する研究が充実し、プログラミング言語の例外処理機構に対する理解が向上することが期待される。その結果、より安全で効率的なプログラムの開発が可能となり、プログラミング言語の進化に寄与することができるだろう。
プログラミング言語における関数クロージャは、自由変数を含む関数本体と、それらの値との関連付け（環境）を伴う。従来の理論では、関数クロージャから環境部分を抽出することで、環境を第一級オブジェクトとして扱う必要があった。ラムダ計算において関数クロージャの環境を別の関数クロージャの環境と置き換える方法を提案し、環境を直接第一級オブジェクトとして扱うことを避けるという問題に取り組んだ。新たな計算システム「環境移植を伴うラムダ計算」が導入され、構文・簡約規則で定義される。変換意味論により簡約の健全性が示され、簡単な型システムと主題簡約性が提供される。このアプローチは、関数クロージャの理解と扱いを改善する新たな方法を提案し、本研究課題において、成果を得た。
|
| 今後の研究の推進方策 |
本研究課題は、例外処理機構におけるコントロールキャプチャ機能に関する理解を深めることを目的として、計算モデルの提案や検証手法の確立に取り組んできた。最終年度において、大域脱出・一級継続の研究成果を活用し、コントロールキャプチャ機能を有する例外処理機構の計算モデルを提案した。
これにより、関数型言語であるラムダ計算をはじめ、命令形言語やオブジェクト指向言語などの様々なプログラミングパラダイムにおいて、コントロールキャプチャ機能を網羅的に研究することができた。また、計算モデルを基盤に、コントロールキャプチャ機能を有する例外処理機構に対する検証手法を確立することに成功した。
この成果により、コントロールキャプチャに関する研究が従来よりも充実し、プログラミング言語における例外処理機構の理解が一層深まることが期待される。さらに、この研究成果は、プログラミング言語の設計や開発において、新たな指針を提供することができたと考えられる。
総じて、本研究課題は、例外処理機構のコントロールキャプチャ機能に関する理論的な基盤を構築し、プログラミング言語の進化に寄与することができた。本年度においては、得られた成果をさらに発展させ、より安全で効率的なプログラムの開発を支援することを目指す。
|
