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

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

• 批准号: 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 计算的语法中添加表示“延迟”的常量，可以在新的约简关系下表达可观察的转发器。此外，通过在 πF 计算中添加一个表示“延迟”的常数，我们表明可以使用新的约简关系来模拟传统 π 计算的行为，而不仅仅是转发器。事实证明，约简关系中的差距并不存在。大的。总结这些研究内容的论文被国际会议 FSCD2021 接收。 （严格来说，2020年提交，2023年决定采纳。）