遅延評価を行うプログラミング言語の必要呼び意味論とコンパイラの形式的検証
| Project/Area Number |
19J11926
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
水野 雅之 東北大学, 情報科学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2019-04-25 – 2021-03-31
|
| Project Status |
Declined (Fiscal Year 2020)
|
| Budget Amount *help |
¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2020: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 2019: ¥500,000 (Direct Cost: ¥500,000)
|
|---|
| Keywords | 遅延評価 / 必要呼び / 名前呼び / プログラム意味論 |
|---|
| Outline of Research at the Start |
本研究は遅延評価をサポートするコンパイラに対して形式的検証の手法を明らかにし，そのような処理系の信頼性を向上するものである．
そのため，定理証明支援系Coqを用いて様々なメタ定理を証明することで，形式的検証に適した意味論の定式化を模索するほか，遅延評価を効率的に実行するための最適化に対して実際に形式的検証を行い，その手法を明らかにする．
遅延評価は言語機能として提供されるだけでなく，その特別な例であるストリーム処理としてライブラリに取り入れられてもいる．本研究が完成した際の影響はそのようなライブラリにも波及すると予想される．
|
| Outline of Annual Research Achievements |
形式的検証に適した意味論の定式化を模索するため，λ計算を相互再帰で拡張した言語の二種類の遅延評価の実装，必要呼び意味論と名前呼び意味論の，評価結果が対応することの形式的検証を行うことで評価を行なった．コンパイラを検証する際，意味論の定式化は複雑さを左右するため重要である．その際，遅延評価の効率的な実装である必要呼び意味論では簡約ごとに変数の依存関係を辿る必要があるため，相互再帰のような言語機能は考慮が必要である．
その過程で，定理証明支援系を用いた形式化に適するのみならず，既存の研究と比較しても簡潔な，必要呼び意味論と名前呼び意味論の対応の証明が得られた．この証明は，名前呼び意味論を表示的意味論として定義していた既存研究[Launchbury, POPL ‘93]と異なり，必要呼び意味論と名前呼び意味論の両方を操作的意味論として定義している点が特徴である．
必要呼び意味論においてシェアされていたメモリ領域が名前呼び意味論においては複製される点に注目し，過度に一般的過ぎない巧妙な命題に対して帰納法を回す点も本研究の特徴である．相互再帰を含むプログラムの実行時データには普通再帰的な構造が現れるが，シェアリングに注目し，帰納法や余帰納法を用いることなく実行時データ同士の対応を定義している．この成果はTPPミーティングにおいて口頭発表を行なったほか，APLASにおいても口頭発表しており，20ページの論文が査読を経て，Springerが出版しているLNCSに採録されている．
相互再帰のみならず，一部の無限ループを実行時に検出する言語機能や，関数型言語で一般的な，データコンストラクタとパターンマッチングで対象言語を拡張した場合においても，必要呼びと名前呼びの対応の証明が複雑にならないことも確かめた．この結果はJFPに投稿すべく，現在論文を執筆中である．
|
| Research Progress Status |
翌年度、交付申請を辞退するため、記入しない。
|
| Strategy for Future Research Activity |
翌年度、交付申請を辞退するため、記入しない。
|
Report
(1 results)
Research Products
(3 results)
