圏論的意味論に基づく並行プログラミング言語の分析

基于类别语义的并发编程语言分析

• 批准号: 20J13473
• 负责人: 酒寄 健
• 金额: $ 1.09万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-24 至 2022-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20J13473/
• 关键词: π計算; 圏論的意味論; 並行計算

今年度は、「πF計算の代数的性質と整合するようにπF計算の簡約を再定義できるか?」という問いに関する研究を行った。これは平易な言い方をすると、「プログラムの振る舞いを定める、簡約関係という最も基本的な関係を、πF計算の”数理的な扱いやすさ”を損なわないように調整する」という研究である。簡約関係を所望の性質を持つように再定義することには成功したが、新たに定義した簡約関係は技術的に扱いづらく、その簡約関係を直接用いてプログラムの振る舞いを議論することが難しいという問題が生じた。そのため、本研究では、新たに共通型に基づく証明手法も提案し、型を用いてプログラムの振る舞いを議論できるようにした。また、新たな簡約関係のもとでは、forwarderという特殊なプロセスの作用はある意味で観測不能であることを示した。Forwarderの作用は従来のπ計算では観測可能であるため、これは新たな簡約関係と従来の簡約関係が異なっていることの傍証である。しかし、本研究ではπF計算の構文に”遅延”を表す定数を追加すれば、観測可能なforwarderを新たな簡約関係のもとでも表現できることを示した。さらに、”遅延”を表す定数をπF計算に追加すれば、forwarderに限らず、従来のπ計算の振る舞いを新たな簡約関係を用いて模倣できることも示し、この意味で従来の簡約関係と新たな簡約関係のギャップは大きくないことを証明した。これらの研究内容をまとめた論文は国際会議FSCD2021に採択された。（厳密には、投稿をしたのが令和2年度であり、採択が決まったのは令和3年度になってからである。）

今年，我们对这个问题进行了研究：“我们可以重新定义πF计算的简化以与πf计算的代数特性一致吗？”简而言之，这是一项研究，“调整简化关系的最基本关系，以定义程序的行为，以免破坏πF计算的“数学便利性处理”。尽管我们成功地重新定义了简化的关系以使所需的属性重新定义了所需的属性，但在技术上很难进行技术的验证，因此我们将其直接提出了一个简化的关系，而我们的关系很困难，而这些关系的行为是在这些方案中进行的，并且这些关系的行为是如此。基于常见类型，可以使用类型进行讨论。可观察到的转发器可以在新的简化关系下表达，通过在πF计算中添加一个不断的“延迟”，这表明不仅是逆转器，而且传统的π计算的行为可以使用新的简化关系来模仿，并且在这种情况下，传统的简化关系与新的简化关系之间的差异。 FSCD2021。