2014 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 |
本研究の最終目標である形式木言語および木トランスデューサに関する理論の定式化のため，平成26年度においては，その基礎となる形式(文字列)言語理論に対する定式化と木トランスデューサ理論の応用について取り組んだ．ここでの「定式化」とは，定理証明支援系である Coq などを用い，計算機で機械的に検証できる形の(構成的な)証明に基づいて理論を再構築することで，今後の形式言語理論および形式木言語理論における研究成果の正当性の証明を補助するものである．ただし，形式言語理論の歴史は古く，結果も多岐に渡っており，全ての定理を短期間で網羅的に定式化することはできないため，この研究で必要となる形式木言語理論のうち，特に現在注目されている等価性判定に関連する部分の定式化を行った．
また，木トランスデューサ理論の応用については，構造化文書 XML を処理する最も実用的な言語 XQuery の処理系の効率化について研究を行った．当該年度で扱った効率化手法は，メモリを大幅に節約できるストリーム処理と，不要な計算を省略できる関数融合の2つである．前者は，研究代表者がこれまでに開発した木トランスデューサのストリーム化手法に基づいており，後者はトランスデューサの合成手法を応用したものとなっている．いずれの手法に対しても，理論的な正当性だけでなく実際に実装を行い，一般的に用いられる XML 処理ベンチマークを利用してその有効性の検証を行った．その結果，どちらの手法においても既存の処理系に対する優位な点が観測された．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当該年度の目標である形式 (文字列) 言語理論は定式化を行う予定であったが，木トランスデューサ理論 (特に等価性判定に関連するもの) の定式化に必要な部分を明確にし，その構成的な証明に関する調査を進めた．必要なものを全て網羅するには至っていないものの，当初の計画では後の年度で行う予定であった理論の応用についても複数の結果が得られたため，順調に進んでいるものと判断した．
|
| Strategy for Future Research Activity |
今後は形式木言語理論で特に機械的な検証が必要となる木トランスデューサの等価性判定問題について定式化を進める予定である．また，形式 (文字列) 言語理論についてまだ定式化が不十分な点についても進めることが期待される．特に，これらの理論の基礎的な結果は代数的アプローチに基づいているため，Coq の拡張である ssreflect などを用いて定式化を進める．
|
| Causes of Carryover |
本研究課題に最も関連の深い国際ワークショップである Trends in Tree Automata and Tree Automata (TTATT 2015) が予定より遅く，来年度 (平成27年度) に4月に開催されることとなったため．
|
| Expenditure Plan for Carryover Budget |
国際ワークショップである Trends in Tree Automata and Tree Automata (TTATT 2015) にプログラム委員として参加し，現在進めている研究について多くの専門家と議論を行う．
|
