2021 Fiscal Year Annual Research Report
Categorical Semantics and Logical Interpretation of the Pi-Calculus
| 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 |
前年度までに行ってきた基礎的な結果を背景に、今年度は隣接分野との関係や応用を目指した研究を行った。
隣接分野としては、特に線形論理との関連を調べた。π計算と線形論理との関連についてはセッション型システムを背景に持つものが知られており、これは構文的な直感に基づくものである。一方で本研究で与えられた圏論的意味論は、構文論ではなく意味論に基づく新しい関係を与えていることが意味論的考察から分かる。数学的にいうと、本研究で与えたπ計算の構文モデルは線形非線形モデルの例になっている、ということである。この関係に基づいて、線形論理の論理式で型が付くπ計算の項という概念を得ることができた。こうして得られた型付け関係の直感的解釈や応用については、今後の研究を要するところである。
応用として、プログラム検証への応用について検討した。本研究で得た成果に、強い意味で競合およびデッドロックのないπ計算については逐次的計算の検証手法である交差型システムが利用できる、というものがあった。しかしながら、強い意味で競合およびデッドロックのないπ計算が豊富に現れる領域が見つかっておらず、この結果の応用的価値が低い状態であった。本年度の成果としては、近年注目を集めているプログラミング言語である Rust のプログラムと強い意味で競合およびデッドロックのないπ計算の関係の議論が挙げられる。証明の細部が完成していないものの、それが完成すれば本研究は重要な応用先を得ることになる。
|
