Modelling of Control Capture and Its Applications

例外処理機構は、多くのプログラミング言語において重要な仕組みであり、大域脱出とfinallyブロックを通じてコントロールキャプチャが提供されている。大域脱出や一級継続は、意味論や数理論理学との関連性を含め、多くの研究成果が得られている。しかし、コントロールキャプチャに関する研究はまだ不十分である。本研究では、これまでの大域脱出・一級継続の研究結果を基盤として、コントロールキャプチャ機能を有する例外処理機構の計算モデルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして、命令形言語やオブジェクト指向言語など様々なプログラミングパラダイムに対して研究を進める。さらに、その計算モデルを基盤として、コントロールキャプチャ機能を有する例外処理機構に対する検証手法を確立する。研究成果によって、コントロールキャプチャ機能に対する新たな理解が深まり、導入されていない言語への指針が得られ、コントロールキャプチャや例外処理機構を用いたプログラムのシステム検証の構築が期待される。プログラミング言語における関数クロージャは、自由変数を含む関数本体と、それらの値との関連付け（環境）を伴う。従来の理論では、関数クロージャから環境部分を抽出することで、環境を第一級オブジェクトとして扱う必要があった。本研究では、ラムダ計算において関数クロージャの環境を別の関数クロージャの環境と置き換える方法を提案し、環境を直接第一級オブジェクトとして扱うことを避ける。新たな計算システム「環境移植を伴うラムダ計算」が導入され、構文・簡約規則で定義される。変換意味論により簡約の健全性が示され、簡単な型システムと主題簡約性が提供される。このアプローチは、関数クロージャの理解と扱いを改善する新たな方法を提案している。

例外処理機構は、多くのプログラミング言語において重要な仕組みであり、大域脱出とfinallyブロックを通じてコントロールキャプチャが提供されている。大域脱出や一級継続は、意味論や数理論理学との関連性を含め、多くの研究成果が得られている。しかし、コントロールキャプチャに関する研究はまだ不十分である。本研究では、これまでの大域脱出・一級継続の研究結果を基盤として、コントロールキャプチャ機能を有する例外処理機構の計算モデルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして、命令形言語やオブジェクト指向言語など様々なプログラミングパラダイムに対して研究を進める。さらに、その計算モデルを基盤として、コントロールキャプチャ機能を有する例外処理機構に対する検証手法を確立する。研究成果によって、コントロールキャプチャ機能に対する新たな理解が深まり、導入されていない言語への指針が得られ、コントロールキャプチャや例外処理機構を用いたプログラムのシステム検証の構築が期待される。プログラミング言語における関数クロージャは、自由変数を含む関数本体と、それらの値との関連付け（環境）を伴う。従来の理論では、関数クロージャから環境部分を抽出することで、環境を第一級オブジェクトとして扱う必要があった。本研究では、ラムダ計算において関数クロージャの環境を別の関数クロージャの環境と置き換える方法を提案し、環境を直接第一級オブジェクトとして扱うことを避ける。新たな計算システム「環境移植を伴うラムダ計算」が導入され、構文・簡約規則で定義される。変換意味論により簡約の健全性が示され、簡単な型システムと主題簡約性が提供される。このアプローチは、関数クロージャの理解と扱いを改善する新たな方法を提案している。