| 研究課題/領域番号 |
17K00092
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
浜名 誠 群馬大学, 大学院理工学府, 准教授 (90334135)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | 書換え系 / 関数プログラム / 型理論 / 合流性 / 停止性 / ラムダ計算 / 自動証明 |
|---|
| 研究実績の概要 |
本年度は国際会議論文2本出版および3つの賞受賞の良好な成果を得た。
二階書換えの停止性、合流性自動判定のためのSOLシステムのソフトウェアの改良を進めConfluence Competitoin 2018に出場し、好成績を得た。またConfluence Competitoin 2018の開催方法とその内容についての報告論文を国際会議FSCD 2018で発表した。
さらに多相書換え規則の新しいフレームワークとその合流性の理論を提案した。様々なプログラミングの基礎計算系を定式化することができ、さらにそれら基礎体系の性質を調べることに適した体系となった。多相書換えのための型推論アルゴリズムを新しく設計し、SOLシステムに実装した。また多相書換えの弱合流性検証のための危険対チェック基準を明らかにした。そしてそれらの正当性を証明した。この論文は国際会議FLOPS 2018で発表し、Best Paper Awardを受賞した。
またこれまで困難と思われていた二階書換えの停止性のモジュラ性の証明に取組み、minimal non-terminating terms、predictive labellingの方法とGeneral Schema法を組み合わせる証明の見通しがたった。この証明の準備的報告を日本ソフトウェア科学会第35回大会にて発表し、優秀発表賞および高橋奨励賞を受賞した。
これらにより高階代数系を基礎とするプログラミング言語のための有用な決定手続きの研究成果が着実に揃いつつある。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
二階書換えの理論を拡張し、多相書換えのための合流性の自動チェック行うPolySOLシステムの実装ができた。プログラム言語のための計算体系や関数型プログラムの等式理論の決定可能性が自動チェックできるもので、特に値呼び体系の合流性の自動証明が可能となった。
|
| 今後の研究の推進方策 |
二階書換えの停止性のモジュラ性の証明の細部を詰めながら論文の執筆を行い、この技法をSOLシステム実装する。そして有効性を幅広い例に対して検証する。
|
| 次年度使用額が生じた理由 |
国際会議論文の開催場所が国内だったため予定していた海外旅費分を部分的に使用しなかった。来年度の海外旅費に当てる。
|
