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

具有惰性求值和编译器形式化验证的编程语言的必要调用语义

• 批准号: 19J11926
• 负责人: 水野 雅之
• 金额: $ 0.58万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-25 至 2021-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19J11926/
• 关键词: 遅延評価; 必要呼び; 名前呼び; プログラム意味論

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

The formalization of the formal evaluation of the meaning theory is modeled, and the calculation of λ is repeated. The evaluation of the two kinds of speech is carried out, and the necessary meaning theory is called, and the meaning theory is called, and the evaluation result is carried out. When it comes to evidence, it means that the formulation of the theory is important. In the meantime, it is necessary to consider the speech function of the delay evaluation rate. The proof of theorems is supported by formalization, comparison, simplicity and proof of existing theories. This is a proof of the existence of the theory of meaning before the name is called.[Launchbury, POPL '93] The theory of meaning before the name is called. The theory of meaning before the name is called. The characteristics of this study are as follows: (1) The essential meaning theory is called in the middle,(2) The essential meaning theory is called in the middle,(3) The essential meaning theory is called in the middle,(4) The essential meaning theory is called in the middle,(5) The essential meaning theory is called in the middle,(6) The essential meaning theory is called in the middle,(7) The essential meaning theory is called in the middle,(8) The essential meaning theory is called in the middle,(9) The essential meaning theory is called in the middle,(9) The essential meaning theory is called in the middle,(10) The essential meaning theory is called in the middle,(10) The essential meaning theory is called in the middle,(11) The essential meaning theory is called in the middle,(10) The essential meaning theory is called in the middle,(11) The essential meaning theory is copied in the middle,(10) The essential meaning theory is called in the middle,(11) The essential meaning theory is called in the middle,(10) The essential meaning theory is called in the middle The structure of mutual re-entry, including re-entry, re-entry and re-entry, can be found in the actual operation time, and the structure of common re-entry can be found in the actual operation time, re-entry and re-entry. The results of this study were published by Springer and published by LNCS. The speech function of the speech function is detected when the speech function is executed, and the speech function of the relevant number type is ordinary. The speech function of the speech type is ordinary. The speech function of the speech type is ordinary. The speech function of the speech type is ordinary. The speech function of the speech type is simple. The speech function of the speech type is simple. The result is JFP submission.

项目成果

Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion

使用相互递归的 Call-by-Need 和 Call-by-Name 评估的形式验证

• DOI: 10.1007/978-3-030-34175-6_10
• 发表时间: 2019
• 期刊: Lecture Notes in Computer Science
• 作者: Masayuki Mizuno;Eijiro Sumii
• 通讯作者: Eijiro Sumii