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

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

• 批准号: 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 氏も既に加わっており, 今後より一層の進展が大いに期待できるものである.

从第一年开始，我们与博洛尼亚大学的Ugo Dal Lago先生、巴黎第七大学的Claudia Faggian先生、法国Centrale Supelec的Benoit Valiron先生进行了联合研究，进一步扩展了理论。通过令牌机器语义，我们成功地解释了除了递归和高阶函数之外还包括各种概率分支的编程语言。特别是，作为研究计划目标的量子分支被包含在这个框架中，该成果在编程语言理论顶级国际会议 POPL 2017 上被接受为合着论文。在马赛举行的 JSPS 日法双边项目 CRECOGI 研讨会上介绍了该项目的进展情况。此外，我们考虑不仅为顺序计算赋予类似的语义，还考虑为并行计算赋予相似的语义，以及 Ugo Dal Lago我们与申请人实验室的硕士生 Ryo Tanaka 进行了联合研究。结果，我们成功地为一类使用多个令牌机的称为多端口交互网络（MIN）的图重写系统开发了有效的语义。已知能够嵌入 π 演算，这是并行计算中的标准计算模型之一，并且该结果理论上可以应用于一般使用多令牌机的并行计算程序，这表明可以给出。的语义该结果作为共同撰写的论文提交给理论计算机科学领域的顶级国际会议LICS 2017，并被接受。此外，利用相同的结果，正在研究构建一个保证所需属性的类型系统。巴黎第十三大学的 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