| 研究課題/領域番号 |
19K20211
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 千葉大学 (2020-2021)
東京大学 (2019) |
|---|
研究代表者 |
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2021年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | π計算 / 圏論的意味論 / 計算論的ラムダ計算 / 線形論理 / η則 / 計算効果 / 並行計算 / Freyd圏 |
|---|
| 研究開始時の研究の概要 |
並行計算とは、複数のプロセスが相互作用しながら同時に実行される計算である。例えば、ネットワークを介したサーバとクライアントの協働や、複数のコアやプロセッサを持つ計算機でのタスクの実行などが挙げられる。並行計算にはデッドロック・競合状態や命令実行順序の非決定性などの厄介な問題があり、逐次処理に比べて、正しい設計を行うことや正しさの検証が特別難しい。こうした課題へのアプローチとして、本研究では、並行計算の本質的な部分を抽象化した筋の良い計算モデルを与え、これを用いて設計や検証を行うことを狙いとする。本研究の特徴は、道具として圏論的意味論や論理学の研究の蓄積を知見を利用することにある。
|
| 研究成果の概要 |
本研究はπ計算という計算体系の圏論的意味論を与えるものである。複数の計算機が同時に協働して計算を行うことを並行計算といい、その本質的部分を取り出して抽象化した計算体系のひとつがπ計算である。π計算は並行計算の研究で広く使われている重要な言語であるにも関わらず、圏論的意味論が知られていなかった。
本研究の主な成果は次のようにまとめられる。(1) 標準的なπ計算の圏論的意味論を与えることへの本質的困難を指摘し、 (2)その本質的困難を回避したπ計算の変種に対する簡潔な圏論的意味論を与えた。また (3) 標準的なπ計算と我々の変種の関連を議論した。
|
| 研究成果の学術的意義や社会的意義 |
ネットワークを介して複数の計算機が協働して働くようなソフトウェアの設計・検証は、重要であるが難しい課題である。専門用語を使って言えば、並行システムの設計・検証である。本研究はこの課題への、プログラミング言語を通じた解決策のための基礎的な研究である。人間の持つプログラムの振る舞いに関する直観に数学的に厳密な背景を与えるものが意味論であるが、これまでは（圏論的）意味論を持つ並行システム（具体的にはπ計算）が存在していなかった。本研究はπ計算にはじめての圏論的意味論を与えるもので、今後の並行システム用プログラミング言語の設計や検証への応用が期待される。
|
