量子プログラミング言語のコンパイラ―線形論理の意味論から導かれる「正しい」実装

量子编程语言编译器：源自线性逻辑语义的“正确”实现

• 批准号: 15J08509
• 负责人: 由水 輝
• 金额: $ 1.09万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-24 至 2017-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15J08509/
• 关键词: プログラム意味論; 複数トークン機械意味論; Geometry of Interaction; proof net; interaction net; 評価戦略; 計算副作用; 並行計算; マルチトークン機械意味論

１年度目に引き続きボローニャ大学の 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 氏も既に加わっており, 今後より一層の進展が大いに期待できるものである.

从第一年开始，他与博洛尼亚大学，巴黎大学的克劳迪娅·法吉安（Claudia Faggian）以及中央supelec的贝诺伊特·维龙（Benoit Valiron）合作进行了研究递归和高阶功能。特别是，该框架中包括针对研究计划中的量子分支。该结果是在2017年POPL 2017年的最高国际编程语言理论会议上合着的。申请人还解释了这项研究在Marseille举行的JSP双边项目Crecogi中的进展。此外，我们与申请人实验室的硕士学生Ugo Dal Lago和Tanaka Ryo进行了联合研究项目。结果，我们成功地提供了一个合理的语义理论，用于使用多个令牌机器使用多个令牌机器的图形重写系统称为多端子交互网（min）。众所周知，相同的图形重写系统可以嵌入π计算，这是平行计算的标准计算模型之一，该结果表明，从理论上讲，可以由Multitoken Machines作为共同撰写的论文给出并行计算程序的语义理论，并被选为在2017年共同创作的纸张2017年的著名论文，这是该领域的最佳国际会议。此外，目前正在进行研究以提供一种类型系统，以保证过程计算系统的所需属性。这项正在进行的研究已经与巴黎第13大学的达米亚诺·马扎（Damiano Mazza）一起加入了，他发展了多个互动网的基本理论，我们可以期望将来会有更多的进步。

项目成果

ボローニャ大学(イタリア)

博洛尼亚大学（意大利）

Some comparison between SMLL and Amida

SMLL 和 Amida 之间的一些比较

• 发表时间: 2015
• 作者: Ugo Dal Lago;Claudia Faggian;Benoit Valiron;Akira Yoshimizu;Akira Yoshimizu;Akira Yoshimizu;Akira Yoshimizu
• 通讯作者: Akira Yoshimizu

The geometry of parallelism: classical, probabilistic, and quantum effects

并行性的几何：经典效应、概率效应和量子效应

• DOI: 10.1145/3009837.3009859
• 发表时间: 2017
• 期刊: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM
• 作者: Ugo Dal Lago;Claudia Faggian;Benoit Valiron;Akira Yoshimizu
• 通讯作者: Akira Yoshimizu

The Geometry of Probabilistic Parallelism

概率并行的几何

• 发表时间: 2016
• 作者: Ugo Dal Lago;Claudia Faggian;Benoit Valiron;Akira Yoshimizu;Akira Yoshimizu;Akira Yoshimizu
• 通讯作者: Akira Yoshimizu

Parallelism and Synchronization in an Infinitary Context

无限上下文中的并行性和同步

• DOI: 10.1109/lics.2015.58
• 发表时间: 2015
• 期刊: 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2015
• 作者: Ugo Dal Lago;Claudia Faggian;Benoit Valiron;Akira Yoshimizu
• 通讯作者: Akira Yoshimizu