遅延評価を行うプログラミング言語の必要呼び意味論とコンパイラの形式的検証

形式的検証に適した意味論の定式化を模索するため，λ計算を相互再帰で拡張した言語の二種類の遅延評価の実装，必要呼び意味論と名前呼び意味論の，評価結果が対応することの形式的検証を行うことで評価を行なった．コンパイラを検証する際，意味論の定式化は複雑さを左右するため重要である．その際，遅延評価の効率的な実装である必要呼び意味論では簡約ごとに変数の依存関係を辿る必要があるため，相互再帰のような言語機能は考慮が必要である．その過程で，定理証明支援系を用いた形式化に適するのみならず，既存の研究と比較しても簡潔な，必要呼び意味論と名前呼び意味論の対応の証明が得られた．この証明は，名前呼び意味論を表示的意味論として定義していた既存研究[Launchbury, POPL ‘93]と異なり，必要呼び意味論と名前呼び意味論の両方を操作的意味論として定義している点が特徴である．必要呼び意味論においてシェアされていたメモリ領域が名前呼び意味論においては複製される点に注目し，過度に一般的過ぎない巧妙な命題に対して帰納法を回す点も本研究の特徴である．相互再帰を含むプログラムの実行時データには普通再帰的な構造が現れるが，シェアリングに注目し，帰納法や余帰納法を用いることなく実行時データ同士の対応を定義している．この成果はTPPミーティングにおいて口頭発表を行なったほか，APLASにおいても口頭発表しており，20ページの論文が査読を経て，Springerが出版しているLNCSに採録されている．相互再帰のみならず，一部の無限ループを実行時に検出する言語機能や，関数型言語で一般的な，データコンストラクタとパターンマッチングで対象言語を拡張した場合においても，必要呼びと名前呼びの対応の証明が複雑にならないことも確かめた．この結果はJFPに投稿すべく，現在論文を執筆中である．

形式的検証に適した意味論の定式化を模索するため，λ計算を相互再帰で拡張した言語の二種類の遅延評価の実装，必要呼び意味論と名前呼び意味論の，評価結果が対応することの形式的検証を行うことで評価を行なった．コンパイラを検証する際，意味論の定式化は複雑さを左右するため重要である．その際，遅延評価の効率的な実装である必要呼び意味論では簡約ごとに変数の依存関係を辿る必要があるため，相互再帰のような言語機能は考慮が必要である．その過程で，定理証明支援系を用いた形式化に適するのみならず，既存の研究と比較しても簡潔な，必要呼び意味論と名前呼び意味論の対応の証明が得られた．この証明は，名前呼び意味論を表示的意味論として定義していた既存研究[Launchbury, POPL ‘93]と異なり，必要呼び意味論と名前呼び意味論の両方を操作的意味論として定義している点が特徴である．必要呼び意味論においてシェアされていたメモリ領域が名前呼び意味論においては複製される点に注目し，過度に一般的過ぎない巧妙な命題に対して帰納法を回す点も本研究の特徴である．相互再帰を含むプログラムの実行時データには普通再帰的な構造が現れるが，シェアリングに注目し，帰納法や余帰納法を用いることなく実行時データ同士の対応を定義している．この成果はTPPミーティングにおいて口頭発表を行なったほか，APLASにおいても口頭発表しており，20ページの論文が査読を経て，Springerが出版しているLNCSに採録されている．相互再帰のみならず，一部の無限ループを実行時に検出する言語機能や，関数型言語で一般的な，データコンストラクタとパターンマッチングで対象言語を拡張した場合においても，必要呼びと名前呼びの対応の証明が複雑にならないことも確かめた．この結果はJFPに投稿すべく，現在論文を執筆中である．