定理証明支援系による形式木言語理論の定式化

2015 Fiscal Year Research-status Report

• Project/Area Number: 25730002
• Research Institution: The University of Electro-Communications
• Principal Investigator: 中野 圭介 電気通信大学, 情報理工学(系)研究科, 准教授 (30505839)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Keywords: 形式木言語理論 / 木オートマトン / 木トランスデューサ

Outline of Annual Research Achievements

本研究の最終目標である形式木言語および木トランスデューサ理論の定式化のため，平成27年度においては，木トランスデューサの等価性判定に関連する部分について定式化及び重要な定理の形式証明を行った．「木トランスデューサの等価性判定」とは，2つの木トランスデューサが関数として同じ振舞いをするかを決定することであり，ここでいう「定式化」は定理証明支援系Coqを用いて計算機で機械的に検証できる環境を構築することである．
木トランスデューサの等価性判定には，対象とする木トランスデューサに応じてさまざまな手法が提案されており，平成27年度においては入出力が文字列に近い単項木であるような木トランスデューサを対象とする等価性判定について定式化を進めた．本研究の対象は形式木言語理論であるが，このトランスデューサの等価性判定には，語 (文字列) を対象にした形式言語理論の内容についても定式化する必要があるため，Doczkalらの行った正規言語に関する定式化を参考にし，Coqの拡張であるSSReflectを利用した．特に，等価性判定で利用される語方程式の求解アルゴリズムであるマカニン法の定式化にも着手した．このアルゴリズムは，最も証明が困難なアルゴリズムの1つとされており，本年度内には証明が終わらなかったが，来年度には証明を完了させ，それを用いた木トランスデューサの等価性判定アルゴリズムを定式化する予定である．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本研究の発足時当初の予定では，木トランスデューサ理論の中から合成や逆像などのさまざまな性質について，定式化と形式証明を行うこととしていたが，従来の全ての結果をまとめるとなるとかなり膨大な定式化が必要であるため，平成27年度は，等価性判定についてのみ研究に取り組んでおり，来年度も引き続き等価性判定だけに的を絞って進める予定である．これは，マイクロソフトの研究グループが6年半かけて奇数位数定理を証明した前例から考えればある程度予想されたことであり，短期間単独で定式化を行っていることを考慮すれば許容できる範囲のものである．

Strategy for Future Research Activity

本研究の最終年度である平成28年度は，木トランスデューサの等価性判定アルゴリズムのうち，語方程式求解を利用したものについて引き続き定式化を行う．まず，語方程式求解アルゴリズムであるマカニン法の定式化について形式証明を与え，それを基に下降型トランスデューサや単項木トランスデューサなどの一部の木トランスデューサに対する等価性判定アルゴリズムの形式証明を行う．

Causes of Carryover

本研究課題における成果を年度内には発表することができず，予定より予算の利用が少なくなったため．

Expenditure Plan for Carryover Budget

国内での学会発表または学会誌への掲載料として利用する予定である．