研究者詳細
2023/09/26 更新
基本情報
経歴
社会貢献活動・その他
特定課題制度(学内資金)
早稲田大学 基幹理工学部 助手
定理証明支援系によるグラフ書換え言語の形式化
2022年 上田和紀
概要を見る
グラフ書換え言語LMNtalは,複雑な接続構造とその安全な操作を簡潔に表現できる言語である.LMNtalの項は,そのプログラムに対応するグラフの図的表現と併記されることがあるが,グラフ理論ではなく,構文主導の意味論に基づいて定義されている.そのため,LMNtalの項とその図的表現との対応関係,特にLMNtal項上の構造合同関係と,図的表現の間のグラフ同型との対応関係は非自明な課題である.本研究では,まず証明対象となるデータ構造の定義と,証明の大まかな方針を定めた.また,その知見を活かし,データ構造としてハイパーグラフを採用し形式文法に基づいた型定義を行う関数型言語λGTの提案に参画した.