|
本研究の目標は形式木言語および木トランスデューサに関する理論を定理証明支援系Coqを利用して定式化することであったが，最終年度である平成28年度においては，木トランスデューサ理論のうち，特に合成や等価性判定に関して定式化を行った．これらの問題は，木トランスデューサ理論のみならず木オートマトン理論を暗に利用しているため，木オートマトンの定式化も必要となる． 既存の形式 (文字列) 言語理論に対する定式化において利用されていた通常の (文字列) オートマトンを応用し，目的とする合成や等価性判定に必要な部分のみ木オートマトンの定式化を行った． 木オートマトン理論全体の定式化を少人数・短期間の研究プロジェクトとして行うことは困難であるため，これは今後の課題とする． 今回は木オートマトンの構成に関する基本的な定理のみを必要とした．
木トランスデューサの合成については，トップダウン木トランスデューサとよばれる比較的簡素な木トランスデューサの合成を中心に進めたが，その簡素さに反して決定性や全域性とよばれる制約に応じて正当性に影響があるため，緻密な場合分けが必要であった．また，より表現力の高い属性付き木トランスデューサを利用した融合変換については，定式化に関連した実装も進めた．
木トランスデューサの等価性判定については，語方程式におけるマカニン法の定式化や，Seidlらが新たに提案した等価性判定アルゴリズムの定式化と実装を進めた． マカニン法は停止性の証明が煩雑であり，構成的な証明を必要とする定理証明系を用いた定式化には至らなかった．また，Seidlらの等価性判定アルゴリズムは一部の定式化と実装を行い，手法の有効性について検証を行った．
|
