2016 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 / interaction net / 評価戦略 / 計算副作用 / 並行計算 |
|---|
| Outline of Annual Research Achievements |
１年度目に引き続きボローニャ大学の Ugo Dal Lago 氏, パリ第７大学の Claudia Faggian 氏, フランス CentraleSupelec の Benoit Valiron 氏と共同で研究を行い, 本研究の実施計画における中心概念である Geometry of Interaction の複数トークン機械意味論としての理論を更に拡張し, 再帰・高階関数に加えて種々の確率的分岐を含むようなプログラミング言語を解釈することに成功した. 特に研究計画において目標としていた量子的な分岐はこの枠組みに含まれている. この結果はプログラミング言語理論のトップ国際会議であるPOPL 2017に共著論文として採択された. また, 申請者はこの研究の途中経過に関してマルセイユで行われたJSPS日仏二国間プロジェクト CRECOGI のワークショップにおいて対外発表を行った.
さらに, 逐次的計算だけでなく並行計算に対し同様の意味論を与えることを考え, Ugo Dal Lago 氏および申請者の所属研究室の修士課程学生である田中諒氏と共同研究を行った. 結果として, multiport interaction net (MIN) と呼ばれるクラスのグラフ書換え系の妥当な意味論を複数トークン機械によって与えることに成功した. 同グラフ書換え系は並行計算における標準的な計算モデルのひとつである π 計算を埋め込めることが知られており, この結果は理論的には複数トークン機械によって並行計算プログラム一般の意味論を与えられることを示すものである. この結果は共著論文として理論計算機科学分野のトップ国際会議である LICS 2017 に投稿し採択された. さらに同結果を用いてプロセス計算系に対し望ましい性質を保証する型システムの構成を与える研究も進行中である. この進行中の研究には multiport interaction net の基礎理論を整備したパリ第13大学の Damiano Mazza 氏も既に加わっており, 今後より一層の進展が大いに期待できるものである.
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
Research Products
(5 results)
