表題番号：2022C-435
日付：2023/04/07
研究課題定理証明支援系によるグラフ書換え言語の形式化
| 研究者所属（当時） | 資格 | 氏名 | |
|---|---|---|---|
| （代表者） | 理工学術院 基幹理工学部 | 助手 | 山本 直輝 |
| （連携研究者） | 理工学術院 基幹理工学部 | 教授 | 上田和紀 |
- 研究成果概要
- グラフ書換え言語LMNtalは，複雑な接続構造とその安全な操作を簡潔に表現できる言語である．LMNtalの項は，そのプログラムに対応するグラフの図的表現と併記されることがあるが，グラフ理論ではなく，構文主導の意味論に基づいて定義されている．そのため，LMNtalの項とその図的表現との対応関係，特にLMNtal項上の構造合同関係と，図的表現の間のグラフ同型との対応関係は非自明な課題である．
本研究では，まず証明対象となるデータ構造の定義と，証明の大まかな方針を定めた．また，その知見を活かし，データ構造としてハイパーグラフを採用し形式文法に基づいた型定義を行う関数型言語λGTの提案に参画した．