2015 Fiscal Year Annual Research Report
量子プログラミング言語のコンパイラ―線形論理の意味論から導かれる「正しい」実装
| Project/Area Number |
15J08509
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
由水 輝 東京大学, 情報理工学系研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2015-04-24 – 2017-03-31
|
| Keywords | プログラム意味論 / マルチトークン機械意味論 / Geometry of Interaction / proof net / 評価戦略 / 並行計算 |
|---|
| Outline of Annual Research Achievements |
ボローニャ大学の Ugo Dal Lago 氏, パリ第7大学の Claudia Faggian 氏, フランス CentraleSupelec の Benoit Valiron 氏と共同で研究を行い, 申請書に記載した研究実施計画において重要となる概念である Geometry of Interaction, 特にマルチトークン機械意味論の理論を通常のプログラミング言語を解釈するのに十分な程度まで拡張する結果が得られた. さらに, この拡張した意味論を用いて古典計算における名前呼び・値呼び戦略の区別を与えることが可能なことを示すことに成功した. これを論文としてまとめ, 理論計算機科学分野のトップ国際会議のひとつであるLICS 2015に投稿し採択された. この結果において, 申請者は再帰に対応する proof net のノードの簡約規則の提案やマルチトークン機械の諸性質の証明を担当している.
研究実施計画においては[蓮尾 & 星野, LICS'11]の結果を用いて再帰・高階関数を解釈するとしたが, 今回の結果は同じ Geometry of Interaction 意味論という概念を用いつつも別の観点から再帰・高階関数を解釈することが可能なものであり, 同意味論の特にプログラム意味論への応用における基礎付けとして重要なものであると位置づけられる.
同結果に関しては国内学会PPL 2016にて内容を紹介する発表も行った。
また, Ugo Dal Lago 氏の所属であるボローニャ大学を訪問し, 並行計算に対する同様の意味論を与える研究を行い, ある種の並行計算モデルに対する遷移規則の草案を得るなど一定の成果を得た. これは並行計算に対し新たな検証手法をもたらすフレームワークとして期待が持てるものであり, 今後論文としてまとめ査読付きの国際会議ないしは学術雑誌に投稿する予定である.
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
前年度の研究では, 当初の予定とは異なる方向にではあるが大きな進展が得られた.
研究計画では量子計算に対する意味論としての Geometry of Interaction の応用を目指していたが, 前年度の研究ではもともと量子計算を指向して設計した概念であるマルチトークン機械意味論を量子計算に限らない計算一般を解釈可能なものへと拡張する結果が得られ, 実際に量子計算ではなく古典計算における名前呼び・値呼びという異なる評価戦略をトークン機械意味論のレベルで区別するという新規な結果を得た. この結果は高階関数・再帰を持つ量子計算プログラミング言語に対し Geometry of Interaction 意味論を与え, そこからコンパイラ実装を導出するという研究計画に沿った応用も考えられる他, 古典計算, あるいはより顕著には並行計算に対するコンパイラや形式検証において応用が期待されるものであり, 特に並行計算への応用に関しては既に Ugo Dal Lago 氏らとの共同研究に着手し, 一定の成果を得つつある.
以上から, 前年度の研究実績は本研究課題を推進しつつもより広い応用が視野に入る進展であると考える.
|
| Strategy for Future Research Activity |
研究計画に沿った量子計算への応用の他, プログラミング言語を Geometry of Interaction によって解釈する際に用いる proof net を一般化した概念である interaction net, さらにその並行計算への拡張である multiport interaction net に関してもマルチトークン機械意味論を与え, より広い範囲の計算体系にトークン機械意味論による解釈とその実際的な応用を与えるための基礎付けを目指し研究を進める.
|
Research Products
(6 results)
