π計算の圏論的意味論と論理的解釈

2021 年度 研究成果報告書

• 研究課題/領域番号: 19K20211
• 研究種目: 若手研究
• 配分区分: 基金
• 審査区分: 小区分60010:情報学基礎論関連
• 研究機関: 千葉大学 (2020-2021); 東京大学 (2019)
• 研究代表者: 塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
• 研究期間 (年度): 2019-04-01 – 2022-03-31
• キーワード: π計算 / 圏論的意味論 / 計算論的ラムダ計算 / 線形論理

研究成果の概要

本研究はπ計算という計算体系の圏論的意味論を与えるものである。複数の計算機が同時に協働して計算を行うことを並行計算といい、その本質的部分を取り出して抽象化した計算体系のひとつがπ計算である。π計算は並行計算の研究で広く使われている重要な言語であるにも関わらず、圏論的意味論が知られていなかった。
本研究の主な成果は次のようにまとめられる。(1) 標準的なπ計算の圏論的意味論を与えることへの本質的困難を指摘し、 (2)その本質的困難を回避したπ計算の変種に対する簡潔な圏論的意味論を与えた。また (3) 標準的なπ計算と我々の変種の関連を議論した。

自由記述の分野

プログラム意味論

研究成果の学術的意義や社会的意義

ネットワークを介して複数の計算機が協働して働くようなソフトウェアの設計・検証は、重要であるが難しい課題である。専門用語を使って言えば、並行システムの設計・検証である。本研究はこの課題への、プログラミング言語を通じた解決策のための基礎的な研究である。人間の持つプログラムの振る舞いに関する直観に数学的に厳密な背景を与えるものが意味論であるが、これまでは（圏論的）意味論を持つ並行システム（具体的にはπ計算）が存在していなかった。本研究はπ計算にはじめての圏論的意味論を与えるもので、今後の並行システム用プログラミング言語の設計や検証への応用が期待される。