| 研究課題/領域番号 |
17K00092
|
|---|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
浜名 誠 群馬大学, 大学院理工学府, 准教授 (90334135)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | 書換え系 / 関数プログラム / 型理論 / 合流性 / 停止性 / ラムダ計算 / 自動証明 |
|---|
| 研究実績の概要 |
本年度は国際ワークショップ論文1本、学術論文誌2本の出版の良好な成果を得た。
国際ワークショップUNIF'17ではFunction-as-Constructor Higher-Unifictionを初めて関数的に実装したことを報告した。これにはPruningとDischargingという操作を実装する必要があるが、Haskellを用いて効果的に実装できることを示した。
新しい国際論文誌ACM on Programming Languagesで発表した論文では、近年その重要性が高まる関数型プログラミング言語を高機能化する8つの異なる計算体系の決定性可能性(decidability)の証明を一度に解決した。これはFunction-as-Constructor Higher-Unifictionを用いた危険対チェックとGeneral Schema方式による強停止性の判定を２階書換えに対して精密に定式化し、さらにそのためのSOLシステムのソフトウェアを開発し、公開した。同内容を国際会議ICFP 2018で発表した。
また、プログラム理論の国際論文誌Mathematical Structures in Computer Scienceにおいて、グラフデータベースのための質問言語UnCALの圏論的意味論を初めて与えた。これはBloomとEsikによるイテレーション圏を用いることで、グラフ間の双模倣を完全に等式によって公理化することに成功した。この意味論からグラフ上の構造再帰がイテレーション関手として自然にモデル化できることも示した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
二階書換えの理論を精密化させ、二階書換えのための合流性と停止性の自動チェック行うSOLシステムの実装ができた。多数のプログラム言語のための計算体型や関数型プログラムの決定可能性が自動チェックできるもので、特にFunction-as-constructorパターンを許すため、これまでつくられたことない新規な二階書換えの自動証明が可能となった。
|
| 今後の研究の推進方策 |
SOLシステムの実装により、各種の例を検討したために明らかになった事項は、書換え系の多相化と、二階の停止性証明機構をさらに強力する事である。特にFunction-as-constructorのための停止性手法はこれまで行われてないため、推し進める。
|
| 次年度使用額が生じた理由 |
前倒し申請をしたがそれを実際は使用しなかったため、当初の研究計画通りに使用する。
|
