2013 Fiscal Year Research-status Report
Haskellコアの意味論－先端的ソフトウェア検証基盤へ向けて
| Project/Area Number |
25540002
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 理工学研究科, 助教 (90334135)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | プログラム意味論 / 操作的意味論 / Haskell / 情報学基礎 |
|---|
| Research Abstract |
本年度は、Haskellコアの操作的意味論へのアプローチとして以下の三つの成果を得た。
(1)高階関数のモデルである遺伝単調高階関数類 が Σモノイド を成すことを明らかにした。これを元にした高階書換え系の代数的停止性証明へと応用した。
(2)多相型付きλ計算の停止性証明を代数化し、Reduciblity の概念が、多相代数理論のモデルの一つである事を明らかにできた。GiradによるReducibility という極めてトリッキーな型付き集合の構成よる証明が、多相代数理論のモデルの一例になることを明らかにし、これまで知られていなかったReducibility 証明の本質とその代数的な性質のよさを初めてを明らかにした興味深い結果といえる。Haskellプログラムの停止性推論に有効である。
(3)seqコンビネータのあるHaskellコア言語を考察し、それをMoggiの計算メタ言語に共有付きlet文を追加したものへの変換方法を考案した。ここでの等式推論体系は、seqによる値呼びも加味した必要呼び計算をモデル化するものとなった。
またプログラム言語と意味論の間の連携を押し進める最新の研究結果を報告する、 関数型言語、プログラム意味論、Haskellに関連する領域の研究会 Semantic Methods in Haskell and Functional Programming Seminarを浜名が企画し、国立情報学研究所にて開催した。研究代表者と分担者も成果について発表した。研究会は外部からも多数の参加者があり好評を博した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
計算モナドを用いれば、部分値や値呼びの計算を表示的に表せるため、計算メタ言語を元にコア言語を設定する方向性はよいアプローチである。次年度以降にはこれとグラフ書換え計算、Call-by-need計算との対応を調べる事が必要である。
|
| Strategy for Future Research Activity |
本年度は、The European Joint Conferences on Theory and Practice of Software (ETAPS)併設の国際ワークショップMathematically Structured Functional Programming 2014のプログラム委員、および国内プログラミング言語会議PPLのプログラム委員を務め、型理論および関数型プログラミングの最新進展状況を把握し、関連研究者から有用な研究推進の情報を得た。今後はこれを参考にし、Haskellの操作的意味論の研究へ進める。特にHaskellの代表的実装であるGHCの内部言語と仮想機械の構成について調べることも今後の研究の促進に必要であることを認識した。
|
| Expenditure Plans for the Next FY Research Funding |
各所からの研究訪問があったために旅費を使う必要がなかった。
次年度以降に旅費と謝金に用いる。
|
