| 研究課題/領域番号 |
18K11156
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
浅田 和之 東北大学, 電気通信研究所, 助教 (00570251)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2022-03-31
|
| キーワード | ゲーム意味論 / ゲーム理論 / モデル検査 |
|---|
| 研究実績の概要 |
2020年度では高階プログラム検証に用いられる高階木文法（非決定性のあるラムダ計算）に関して2本の論文が採録された．これらの論文の内容は2019年度に行ったものであり，前年度の報告のとおりである．
2020年度では高階プログラムのモデル検査の意味論の研究を行った．高階プログラムのモデル検査はゲーム意味論を用いた手法が知られているが，そのゲーム意味論とはことなるゲーム理論の意味論を用いてモデル検査の意味論を与える共同研究を行った．このゲーム理論ではゲームをインターフェースで拡張子，構成的にゲームを表現したり，その意味を計算したりできるようになった．この構成性はコンパクト閉圏の構造を持ち，これはプログラミング言語の意味論と相性のいいものであり，今後多くの発展的研究が期待される．
この成果の論文は現在執筆中であり，近く投稿予定である．
また，この成果と2018年度に発表した交差型ベースの意味論的変換のモデルとを組み合わせて，従来のゲーム意味論をより細かい技術により再構成するような意味論が与えられないか研究を進めている．特に，これにより高階プログラムのモデル検査の意味論を与えられないか研究を進めている．高階プログラムのモデル検査の意味論はこれまでに比較的多くの種類が与えられてきたが，意味論の定義は新規手法で与えられているものの，その正当性定理の証明は既存研究に頼っているものが大多数となっている．その証明手法も含めて，上記手法での研究を進めている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究は普遍的モデルによるプログラム推論の研究を推し進めるものであるが，プログラム推論の主要な手法であるモデル検査の基盤技術であるゲーム理論について，プログラミング言語と相性のいい形の意味論を与えることに成功し，多くの将来研究の可能性を生み，分野の発展に寄与できた．
|
| 今後の研究の推進方策 |
当年度に得られたゲーム理論の意味論と，2018年の成果を用いて，高階モデル検査の意味論を解析する研究を進める．
本研究においてはプログラムの意味の不連続性が問題になる．プログラム自体は連続関数であるがモデル検査の性質が不連続であるため，実無限を直接捉える必要があり，そのためにゲーム理論の意味論を戦略そのものを見るようなモデルに拡張することを検討している．
また多相型理論について，パラメトリシティと定義可能性の関係の研究を進め，またパラメトリシティの圏論的再構成の研究を進める．
パラメトリシティは内的な定義可能性であり，既存の定義可能性と関連する意味論との関係を調べる．またパラメトリシティを項生成規則を拡張することと圏論的普遍性を持たせることの関係を分析しつつ研究を進める．
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染症のまん延により学会参加や他研究者との研究打ち合わせの機会がなくなり，成果発表における交流・議論や共同研究の機会の減少が生じ，研究へも若干影響が出ており，その分使用されなかった経費を次年度に使用し研究を継続・完成させる予定である．
|
| 備考 |
研究者代表者のホームページ
|
