2019 Fiscal Year Research-status Report
Categorical Semantics and Logical Interpretation of the Pi-Calculus
| Project/Area Number |
19K20211
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 並行計算 / π計算 / 圏論的意味論 / Freyd圏 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、並行計算のモデルであるπ計算の理論を、圏論的意味論を通じて整理・深化することであった。初年度である本年度には、π計算の圏論的意味論の提案とその基本的な性質の調査を行った。
はじめにπ計算の圏論的意味論として、コンパクト閉フライド圏を提案した。コンパクト閉フライド圏は、並行計算の圏論的モデルとして使われることもあったコンパクト閉圏と、副作用のある関数型言語のモデルである閉フライド圏の２つ構造を併せ持った圏である。我々はコンパクト閉フライド圏によるπ計算の解釈とを与え、同時に対応するπ計算の型理論を定式化した。これによってπ計算の圏論的意味論としてコンパクト閉フライド圏が適切であることを示した。
圏論的意味論の応用として、π計算と関数型プログラミング言語の間の相互の翻訳を与えた。コンパクト閉フライド圏は副作用のある関数型プログラミング言語のモデルである閉フライド圏の特殊な場合であるため、特殊な関数型プログラミング言語として理解することもできる。すると (π計算) = (コンパクト閉フライド圏) = (特殊な関数型プログラミング言語) というコンパクト閉フライド圏を介した対応関係によって、π計算と特殊な関数型プログラミング言語の相互翻訳が与えられる。この翻訳は純粋に数学的な考察のみで定まることに注意する。こうして得られる翻訳は、実は Sangiorgi らによって提案されていたものに一致する。この意味で、我々の圏論的意味論は Sangiorgi らの翻訳を数学的に説明することに成功した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
初年度の目標であったπ計算の圏論的意味論を与えることについて、当初の予定通りに達成したため。
|
| Strategy for Future Research Activity |
本年度に与えた圏論的意味論を基盤として、発展的な課題に取り組む。特に重要な課題として、研究計画にも上げた次の２つに取り組む。(a) 広く用いられている重要な性質である「強有刺双模倣性」や「弱有刺双模倣性」を完全に特徴づける圏論的モデルは存在するか。(b) 線形論理とπ計算の関係、特に線形論理にどのような公理を追加するとπ計算を得ることができるのか。
|
| Causes of Carryover |
当初予定していた海外の研究者の元への訪問が、事情により延期されたため。
|
