| 研究課題/領域番号 |
19J11926
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
水野 雅之 東北大学, 情報科学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2019-04-25 – 2021-03-31
|
| 研究課題ステータス |
採択後辞退 (2020年度)
|
| 配分額 *注記 |
900千円 (直接経費: 900千円)
2020年度: 400千円 (直接経費: 400千円)
2019年度: 500千円 (直接経費: 500千円)
|
|---|
| キーワード | 遅延評価 / 必要呼び / 名前呼び / プログラム意味論 |
|---|
| 研究開始時の研究の概要 |
本研究は遅延評価をサポートするコンパイラに対して形式的検証の手法を明らかにし，そのような処理系の信頼性を向上するものである．
そのため，定理証明支援系Coqを用いて様々なメタ定理を証明することで，形式的検証に適した意味論の定式化を模索するほか，遅延評価を効率的に実行するための最適化に対して実際に形式的検証を行い，その手法を明らかにする．
遅延評価は言語機能として提供されるだけでなく，その特別な例であるストリーム処理としてライブラリに取り入れられてもいる．本研究が完成した際の影響はそのようなライブラリにも波及すると予想される．
|
| 研究実績の概要 |
形式的検証に適した意味論の定式化を模索するため，λ計算を相互再帰で拡張した言語の二種類の遅延評価の実装，必要呼び意味論と名前呼び意味論の，評価結果が対応することの形式的検証を行うことで評価を行なった．コンパイラを検証する際，意味論の定式化は複雑さを左右するため重要である．その際，遅延評価の効率的な実装である必要呼び意味論では簡約ごとに変数の依存関係を辿る必要があるため，相互再帰のような言語機能は考慮が必要である．
その過程で，定理証明支援系を用いた形式化に適するのみならず，既存の研究と比較しても簡潔な，必要呼び意味論と名前呼び意味論の対応の証明が得られた．この証明は，名前呼び意味論を表示的意味論として定義していた既存研究[Launchbury, POPL ‘93]と異なり，必要呼び意味論と名前呼び意味論の両方を操作的意味論として定義している点が特徴である．
必要呼び意味論においてシェアされていたメモリ領域が名前呼び意味論においては複製される点に注目し，過度に一般的過ぎない巧妙な命題に対して帰納法を回す点も本研究の特徴である．相互再帰を含むプログラムの実行時データには普通再帰的な構造が現れるが，シェアリングに注目し，帰納法や余帰納法を用いることなく実行時データ同士の対応を定義している．この成果はTPPミーティングにおいて口頭発表を行なったほか，APLASにおいても口頭発表しており，20ページの論文が査読を経て，Springerが出版しているLNCSに採録されている．
相互再帰のみならず，一部の無限ループを実行時に検出する言語機能や，関数型言語で一般的な，データコンストラクタとパターンマッチングで対象言語を拡張した場合においても，必要呼びと名前呼びの対応の証明が複雑にならないことも確かめた．この結果はJFPに投稿すべく，現在論文を執筆中である．
|
| 現在までの達成度 (段落) |
翌年度、交付申請を辞退するため、記入しない。
|
| 今後の研究の推進方策 |
翌年度、交付申請を辞退するため、記入しない。
|
