表題番号:2024C-436
日付:2025/03/20
研究課題グラフ文法に基づくグラフマッチングの記述および型検査
研究者所属(当時) | 資格 | 氏名 | |
---|---|---|---|
(代表者) | 理工学術院 基幹理工学部 | 助手 | 山本 直輝 |
(連携研究者) | 理工学術院 基幹理工学部 | 教授 | 上田和紀 |
- 研究成果概要
- 本研究は、形式文法に基づいて複雑なグラフ構造を抽象化することにより、グラフ構造を扱う大規模なプログラムに関するプログラマの理解を助け、またプログラムの実行および安全性検証の効率化を図るものである。なお本研究は、学部および修士課程において行った、グラフ書換え言語LMNtalの形式文法に基づいた型検査手法LMNtal ShapeTypeに関する研究に端を発する。2024年度は、JSSST 2023にて発表した局所的な接続関係の整合性に着目した型検査手法であるLMNtypeの着想を基に、定式化を洗練させていった。その成果として、LMNtal上のグラフ文法であるLMNtalGGと、それに基づくグラフ型とその差分からなる差分グラフ型の概念を確立し、査読付き国際会議で発表した[1]。また、10月には同内容を国際ワークショップAPLAS-NIER 2024にて発表した。従来、LMNtal ShapeTypeやLMNtypeといった静的な型定義・検査手法と、書換え規則の発火条件としてユーザが定義したグラフ型による制約を課すことができる拡張言語であるCSLMNtalとは、双方ともにグラフ文法に基づいているため共通する部分が多いにもかかわらず、独立に研究が進められてきた。一方で、今回提案したLMNtalGGではその垣根を取り払い、相互の技術交流・融合を行うことを目指している。実際、論文[1]においてもLMNtalGGの主要な応用として上記の2点を挙げている。加えて、従来のLMNtal ShapeTypeでは、リスト型とその差分である差分リスト型とを独立に定義する必要があり、「差分リストにリストを繋いだものはリストである」といった一見自明な性質を示すのが困難であったが、今回のLMNtalGGに基づく差分グラフ型では、差分リスト型を既存のリスト型に基づいてその差分として定義することで、この問題を回避している。また、上記の成果および従来のLMNtal ShapeTypeに関する成果(2022年IEEE ACCESS論文)をもとに、博士論文を執筆・提出し、博士(工学)の学位を拝領した。