2021 Fiscal Year Annual Research Report
Development of software foundation based on certified formal tree language theory
| Project/Area Number |
17K00007
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
中野 圭介 東北大学, 電気通信研究所, 教授 (30505839)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | 形式木言語理論 / 等価性判定問題 / 計算モデル |
|---|
| Outline of Annual Research Achievements |
本研究の目的は定式化された形式木言語理論をソフトウェア基盤技術へ応用することであった． 最終年度にあたる令和二年度において，形式木言語理論における木構造データ変換のモデルであるストリーム型の木トランスデューサに着目して研究を進めていたが，予期しない成果発表の延期や関連する意外な応用の発見もあったため，期間を延長して研究を進めた． 発見した応用の一つは双方向変換の一貫性の判定方法に関するものであったが，引き続き研究を進めることで判定方法の精査を行った．
具体的には，双方向変換の満たすべき性質として知られていた12個の規則に対し，組合せによる含意関係や同値関係を網羅的に確認し，それ以外に関係があり得ないことも併せて証明した． この事実については，さらに定理証明支援系Coqにより機械的に検査できる形で形式的に証明を行っており，その結果を強固なものとしている．
また，この成果を得る過程において，既存の双方向変換言語がもつ表現力が自明でないことを発見し，その精査も進めた． 双方向変換言語はその名の通り双方向変換を実現するための言語であるが，その一貫性を自動で保証するためにさまざまな制約が課されているため，表現力が制限されている可能性がある． これを明らかにするために双方向変換のための計算モデルの設計に着手した． まだ，完全なものはできていないものの，双方向変換のもつべき一部の性質について，計算モデルの作成に成功した．
|
