2018 Fiscal Year Research-status Report
Principles of Higher-Order Universal Algebraic Datatypes
| Project/Area Number |
17K00092
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院理工学府, 准教授 (90334135)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 書換え系 / 関数プログラム / 型理論 / 合流性 / 停止性 / ラムダ計算 / 自動証明 |
|---|
| Outline of Annual Research Achievements |
本年度は国際会議論文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回大会にて発表し、優秀発表賞および高橋奨励賞を受賞した。
これらにより高階代数系を基礎とするプログラミング言語のための有用な決定手続きの研究成果が着実に揃いつつある。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
二階書換えの理論を拡張し、多相書換えのための合流性の自動チェック行うPolySOLシステムの実装ができた。プログラム言語のための計算体系や関数型プログラムの等式理論の決定可能性が自動チェックできるもので、特に値呼び体系の合流性の自動証明が可能となった。
|
| Strategy for Future Research Activity |
二階書換えの停止性のモジュラ性の証明の細部を詰めながら論文の執筆を行い、この技法をSOLシステム実装する。そして有効性を幅広い例に対して検証する。
|
| Causes of Carryover |
国際会議論文の開催場所が国内だったため予定していた海外旅費分を部分的に使用しなかった。来年度の海外旅費に当てる。
|
-
-
[Journal Article] Confluence Competition 20182018
Author(s)
T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and Harald Zankl
-
Journal Title
Leibniz International Proceedings in Informatics (LIPIcs)
Volume: 108
Pages: 32:1--32:5
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
