| 配分額 *注記 |
3,600千円 (直接経費: 3,600千円)
2005年度: 1,100千円 (直接経費: 1,100千円)
2004年度: 1,000千円 (直接経費: 1,000千円)
2003年度: 1,500千円 (直接経費: 1,500千円)
|
|---|
| 研究概要 |
本研究の目的は,XMLテキストの変換に高階項書換え系の技術を取り入れることで,XML変換技術の強化と理論的整備をはかることである.
本研究の成果の一つは,XML文書変換に適した高階項書換え系を与え,その型理論的な性質を解明したことである.我々はXML文書に対する二階のパターン照合に対する考察から,項にホールを導入した文脈を高階の項として用いるのが適当であることを見出した.また,文脈の考え方を項だけでなく型にも適用した不完全正則表現型という新たな型システムを導入した.XML文書からのパターンの抽出と合成のときにホールを任意の型で具体化することで,型の利点をいかしつつ柔軟な高階パターン照合が可能になる.本研究では,上記の項と型システムにもとづきXML文書変換のための高階項書換え系を設計するとともに,例を用いてこの書換え系がXML変換に対して有用であることを示した.また,不完全正則表現型システムのもとで書換え規則に対する静的な型検査が可能であることを理論的に示した.
もう一つの成果は,XML文書の項表現と二階のパターンとの間の高階パターン照合アルゴリズムを設計し,その理論的性質を明らかにしたことである.我々は,パターン照合問題を与える等式の列の変換を行う推論規則の集合によりパターン照合アルゴリズムを設計した.その結果,変換にもとづく形式を用いると,一階のパターン照合の推論規則と対応する形で,二階のパターン照合の推論規則が与えられることを見出した.このようにして得られたアルゴリズムに対して理論的な検討を加えた結果,それが健全性と完全性をもつことを示せた.
本研究成果は,XML変換の理論的性質を書換え技術を用いて解明するときの基礎を与える.書換え技術は,合流性や停止性といった性質を解明するのに適しているので,XML変換におけるこれらの性質を検討する際に本研究成果を役立てることができる.
|
