Categorical Semantics and Logical Interpretation of the Pi-Calculus

2020 Fiscal Year Research-status Report

• Project/Area Number: 19K20211
• Research Institution: Chiba University
• Principal Investigator: 塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
• Project Period (FY): 2019-04-01 – 2022-03-31
• Keywords: π計算 / 圏論的意味論 / η則 / 計算効果

Outline of Annual Research Achievements

本研究は並行計算のモデルであるπ計算に圏論的意味論を通じて新しい洞察を与え、それを通じて既存の結果に首尾一貫した説明を与え、また並行プログラムの自動検証手法などの応用上重要な新しい結果を得ることを目指すものである。圏論的意味論の提案は既に前年度に行っており、本年度はその性質について詳しく調査した。
主に取り組んだ課題は、「強有刺双模倣性」や「弱有刺双模倣性」といった性質が圏論的モデルで特徴づけられるか、という問である。「強有刺双模倣性」や「弱有刺双模倣性」は操作的意味論を通じて定義される概念で、数あるπ計算で記述されたプログラムの等価性の中で最も重要なものである。「強有刺双模倣性」や「弱有刺双模倣性」によるプログラムの同値関係は素朴な形では圏論的意味論で捉えることができないことは我々が前年度に指摘しており、何らかの工夫が必要であることが分かっていた。
我々は圏論的意味論の分析を通じて、π計算における命令がアトミックに振る舞っているという新しい解釈を与え、この新しい解釈の元での双模倣性と圏論的意味論で捉えられることを示した。新しい解釈と古い解釈ではπ計算のプログラムの意味が変わってしまうが、古い解釈のプログラムに少しの変更を加えることで意味を保存しながら新しい解釈に移行できることを示した。本結果は論文の形にまとめられ、International Conference on Formal Structures for Computation and Deduction 2021 （計算と演繹の形式的構造に関する国際会議 2021）に採録された。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

「強有刺双模倣性」や「弱有刺双模倣性」を完全に特徴づける圏論的モデルは存在するかという問が当初の想定を超えて難しかったため。想定以上の時間がこの問に費やされた結果、予定していた別のテーマである線形論理との関係について当初の期待ほどには進展させられなかった。

Strategy for Future Research Activity

これまで続けてきた基礎的な研究を継続して推進するとともに、基礎的な結果を応用する研究を行う。特に重要なテーマとしては次の２つが挙げられる。(a) π計算と線形論理の関係について。特に線形論理にどのような変更を行うことでπ計算が得られるかと、逆にπ計算をどのように制限すれば線形論理を得られるかについて調査を行う。(b) 並行プログラムの検証技術への応用。これまでに得られた結果を踏まえて、振る舞いのいい並行プログラムのクラスを与え、このクラスについての検証手法を提案する。特に一定の制限の下での決定可能性を与えることを目指す。

Causes of Carryover

主に新型コロナウィルス感染症の影響で、国際会議などへの参加旅費が不要になったり、海外の研究者を訪問する予定がなくなったりしたため。こうした計画は翌年度に繰り越して実施することを計画している。