| Project/Area Number |
19K20211
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Chiba University (2020-2021)
The University of Tokyo (2019) |
|---|
Principal Investigator |
Tsukada Takeshi 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2021: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | π計算 / 圏論的意味論 / 計算論的ラムダ計算 / 線形論理 / η則 / 計算効果 / 並行計算 / Freyd圏 |
|---|
| Outline of Research at the Start |
並行計算とは、複数のプロセスが相互作用しながら同時に実行される計算である。例えば、ネットワークを介したサーバとクライアントの協働や、複数のコアやプロセッサを持つ計算機でのタスクの実行などが挙げられる。並行計算にはデッドロック・競合状態や命令実行順序の非決定性などの厄介な問題があり、逐次処理に比べて、正しい設計を行うことや正しさの検証が特別難しい。こうした課題へのアプローチとして、本研究では、並行計算の本質的な部分を抽象化した筋の良い計算モデルを与え、これを用いて設計や検証を行うことを狙いとする。本研究の特徴は、道具として圏論的意味論や論理学の研究の蓄積を知見を利用することにある。
|
| Outline of Final Research Achievements |
This research project aims to develop a categorical semantics of the pi-calculus. Concurrent computing is a form of computation in which many computers are executed concurrently and work together to perform a computation, and the pi-calculus is a formal calculus modelling the essence of concurrent computing. Despite the importance of the pi-calculus, which has been widely used in the research of concurrent computing, no categorical semantics has been given for the pi-calculus.
The contributions of this research project can be summarised as follows: (1) we pointed out a fundamental difficulty in developing a categorical model of the conventional pi-calculus, (2) we proposed a variant of the pi-calculus, which avoids the difficulty, and gives a simple categorical semantics for the valiant, and (3) we discuss the relationship between the conventional pi-calculus and our variant.
|
| Academic Significance and Societal Importance of the Research Achievements |
ネットワークを介して複数の計算機が協働して働くようなソフトウェアの設計・検証は、重要であるが難しい課題である。専門用語を使って言えば、並行システムの設計・検証である。本研究はこの課題への、プログラミング言語を通じた解決策のための基礎的な研究である。人間の持つプログラムの振る舞いに関する直観に数学的に厳密な背景を与えるものが意味論であるが、これまでは（圏論的）意味論を持つ並行システム（具体的にはπ計算）が存在していなかった。本研究はπ計算にはじめての圏論的意味論を与えるもので、今後の並行システム用プログラミング言語の設計や検証への応用が期待される。
|
