ゲーム意味論と交差型システムによるプログラム検証

2018 年度 研究成果報告書

• 研究課題/領域番号: 16K16004
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 情報学基礎理論
• 研究機関: 東京大学
• 研究代表者: 塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
• 研究期間 (年度): 2016-04-01 – 2019-03-31
• キーワード: ゲーム意味論 / 交差型システム / generalised species / 線形論理

研究成果の概要

ソフトウェアの信頼性の確保は重要な社会的課題であり、この観点から強力な型システムを持つ関数型プログラミング言語が注目を集めている。型システムごとに検出できるエラーの種類や検出精度は異なるため、目的に応じて適切な型システムを設計する必要がある。本研究では交差型システムと呼ばれる種類の型システムについて研究し、従来では研究者の経験と試行錯誤に依存していた交差型システムの設計プロセスに、ゲーム意味論と呼ばれる分野の数理が利用できることを示した。

自由記述の分野

プログラム意味論

研究成果の学術的意義や社会的意義

本研究成果は、経験と試行錯誤が頼りであった交差型システムの設計に、数理的な背景を見出したことである。数理的な背景とは、具体的には、ゲーム意味論と組合せ論である。ゲーム意味論は多くの研究があるものの、成果を理解し利用できる研究者の数が少ないという問題があったが、本研究成果によってゲーム意味論の知見を交差型システムの形で幅広い研究者に理解できる形で提供できる道が拓けた。また組合せ論との関わりを示したことで、交差型システムに新しい見方を提供し、例えば母関数などといった組合せ論の概念を交差型システムについて考えることを可能にした。