2021 Fiscal Year Annual Research Report
Universal models of programming languages and program reasoning
| Project/Area Number |
18K11156
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
浅田 和之 東北大学, 電気通信研究所, 助教 (00570251)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | ゲーム理論 / 高階プログラム検証 / 高階不動点論理 / 圏論的意味論 / 線形論理 / 線形代数 / 量子プログラミング |
|---|
| Outline of Annual Research Achievements |
昨年度の報告に記載した投稿予定の論文を投稿し，国際会議MFPS 2021に採択された．これはゲーム理論に関するものであり，パリティゲームをコンパクト閉圏の構造で構成的（要素還元的）に解く方法を与えたものである．
2021年度では他に3つの研究を行なった．いずれも共同研究である．
一つは上記の研究と同じ方向性のもので，Mean-Pay-Offゲームを構成的に解く方法を得た．現在論文を投稿予定である．
もう一つは高階不動点論理の表現力に関するもので，高階プログラムの検証に応用できる．詳しく述べると，最大不動点が除かれた整数を扱える（n階の）高階不動点論理μHFL(Z)と，それから連言を除いた（n+1階の）体系とで，表現力に違いがない（一方の論理体系の任意の論理式を他方の論理式に真偽を変えずに翻訳できる）ことを示した．論文は投稿予定で，またarxivにて公開済みである．
最後の一つは線形論理・線形プログラミング言語の意味論に関するものであり，国際会議LICS 2022に採択された．古典線形論理のモデルとして，コヒーレンス空間・有限性空間・確率的コヒーレンス空間・関係モデル・重み付き関係モデルなど，多くのモデルが知られているが，本研究では線形論理のモデルを（圏論的）加群理論として与える一般的なフレームワークを与えた．これにより上述したモデルを統一的に同じ形式で与えることができ，またこれら古典線形論理のモデルを直観主義線形論理のモデルとして拡張する方法も実現した．また本研究の量子プログラミング言語の意味論への応用も研究しており，論文を投稿予定である．
|
| Remarks |
研究者代表者のホームページ
|
