形式論理に基づくXML処理システム

本年度は昨年度に引き続き、形式論理によるXML処理言語の理論的なモデルである"Macro Tree Transducer"を基に、既存手法では難しかった巨大なXML文書を扱う複雑なXML変換処理に関しても、その実行および正当性の検証を効率的に行うための研究を行った。具体的な成果は以下の通りである。実際の応用に際し使用されるXML変換は、単一の処理だけで完結するものではなく、通常、いくつかの処理を合成することで複雑な変換を実現しており、高効率な変換処理や正当性検査を実現するには、「合成」の取り扱いが本質的である。本年度の研究成果としては、まず、個々の処理が比較的単純なものである場合には、記述上は「合成」として記述されていても自動的に単一の処理へと畳み込み、簡易な処理/検査を可能とするモデルMulti-Return Macro Tree Transducerを提案し、国際学会CIAA 2008で発表した。さらに、個々の処理を単純なものと限らない一般の場合に関しても考察を進め、XML変換プログラムは、複数の処理の途中で無駄な中間結果を決して生成しない"Garbage-Free Form"と呼ばれる最適化された形式へと常に変形可能であることを証明した。この形式を用いることで、従来計算量の上界が明らかになっていなかったいくつかの問題(期待される入出力XMLを与えてプログラムがその通りの処理を行うか否かを検査する『変換メンバシップ問題』、エラーやセキュリティ上の問題を含むような特定の出力が決してプログラムから生成され得ないことを検査する『出力言語メンバシップ問題』、等)に関してNPおよびDSPACE(n)と呼ばれる計算量を示し、具体的なアルゴリズムを設計した。この成果は、理論計算機科学に関する国際学会FSTTCS 2008にて発表を行った。また、変換メンバシップ問題については特に、Multi-Return Macro Tree Transducerによって単一の処理へ畳み込むことによってPTIMEと呼ばれる非常に効率的な計算量で検査が可能であることを示し、XML処理言語に関する国際学会PLAN-X2009にて発表を行った。

本年度は昨年度に引き続き、形式論理によるXML処理言語の理論的なモデルである"Macro Tree Transducer"を基に、既存手法では難しかった巨大なXML文書を扱う複雑なXML変換処理に関しても、その実行および正当性の検証を効率的に行うための研究を行った。具体的な成果は以下の通りである。実際の応用に際し使用されるXML変換は、単一の処理だけで完結するものではなく、通常、いくつかの処理を合成することで複雑な変換を実現しており、高効率な変換処理や正当性検査を実現するには、「合成」の取り扱いが本質的である。本年度の研究成果としては、まず、個々の処理が比較的単純なものである場合には、記述上は「合成」として記述されていても自動的に単一の処理へと畳み込み、簡易な処理/検査を可能とするモデルMulti-Return Macro Tree Transducerを提案し、国際学会CIAA 2008で発表した。さらに、個々の処理を単純なものと限らない一般の場合に関しても考察を進め、XML変換プログラムは、複数の処理の途中で無駄な中間結果を決して生成しない"Garbage-Free Form"と呼ばれる最適化された形式へと常に変形可能であることを証明した。この形式を用いることで、従来計算量の上界が明らかになっていなかったいくつかの問題(期待される入出力XMLを与えてプログラムがその通りの処理を行うか否かを検査する『変換メンバシップ問題』、エラーやセキュリティ上の問題を含むような特定の出力が決してプログラムから生成され得ないことを検査する『出力言語メンバシップ問題』、等)に関してNPおよびDSPACE(n)と呼ばれる計算量を示し、具体的なアルゴリズムを設計した。この成果は、理論計算機科学に関する国際学会FSTTCS 2008にて発表を行った。また、変換メンバシップ問題については特に、Multi-Return Macro Tree Transducerによって単一の処理へ畳み込むことによってPTIMEと呼ばれる非常に効率的な計算量で検査が可能であることを示し、XML処理言語に関する国際学会PLAN-X2009にて発表を行った。