| Project/Area Number |
20J13473
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
酒寄 健 東京大学, 情報理工学系研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2020-04-24 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2020: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | π計算 / 圏論的意味論 / 並行計算 |
|---|
| Outline of Research at the Start |
本研究は、πF計算というπ計算の部分体型に関する研究である。π計算とは並行プログラムに関する理論的研究をする際に対象言語としてが広く行われている計算体型であるが、π計算には数理的に扱いにくいという問題がある。申請者は、現在までにπ計算の適切な部分体型（πF計算）に着目すれば、この部分体型は特定の代数構造を持つという点で数理的な性質の良いということを発見した。本研究では、πF計算の性質をより詳しく調べる。具体的には、(1）πF計算が代数構造を持つことが、πF計算の解析にどのように役立つのか、(2)πF計算の長所を保ったまま追加の言語機構を足す方法は存在する方法はあるのかを調査する。
|
| Outline of Annual Research Achievements |
今年度は、「πF計算の代数的性質と整合するようにπF計算の簡約を再定義できるか?」という問いに関する研究を行った。これは平易な言い方をすると、「プログラムの振る舞いを定める、簡約関係という最も基本的な関係を、πF計算の”数理的な扱いやすさ”を損なわないように調整する」という研究である。簡約関係を所望の性質を持つように再定義することには成功したが、新たに定義した簡約関係は技術的に扱いづらく、その簡約関係を直接用いてプログラムの振る舞いを議論することが難しいという問題が生じた。そのため、本研究では、新たに共通型に基づく証明手法も提案し、型を用いてプログラムの振る舞いを議論できるようにした。また、新たな簡約関係のもとでは、forwarderという特殊なプロセスの作用はある意味で観測不能であることを示した。Forwarderの作用は従来のπ計算では観測可能であるため、これは新たな簡約関係と従来の簡約関係が異なっていることの傍証である。しかし、本研究ではπF計算の構文に”遅延”を表す定数を追加すれば、観測可能なforwarderを新たな簡約関係のもとでも表現できることを示した。さらに、”遅延”を表す定数をπF計算に追加すれば、forwarderに限らず、従来のπ計算の振る舞いを新たな簡約関係を用いて模倣できることも示し、この意味で従来の簡約関係と新たな簡約関係のギャップは大きくないことを証明した。これらの研究内容をまとめた論文は国際会議FSCD2021に採択された。（厳密には、投稿をしたのが令和2年度であり、採択が決まったのは令和3年度になってからである。）
|
| Research Progress Status |
翌年度、交付申請を辞退するため、記入しない。
|
| Strategy for Future Research Activity |
翌年度、交付申請を辞退するため、記入しない。
|
