| 研究概要 |
本研究は,高階ナローイング(higher-order narrowing)に基づくパターン照合およびユニフィケーションの手法を活用することで,従来困難であったXMLデータの統合処理の記述に適したプログラミング言語環境を構築することを目的としている.研究計画にしたがい,平成17年度(初年度)には言語設計の基盤となる理論面の整備を行った.その概要は以下の通りである.まず,XMLデータの処理に十分な記述力を有しつつ効率的な処理が見込める高階のデータ型として「不完全正則表現型(incomplete regular expression (RE) type)」と呼ぶ静的な型付けのシステムを新たに提示し,その型付け規則を形式化した.現在までに,不完全RE型に関する以下の性質を明らかにした.(1)型検査(type check)問題は型の包含関係の検査に帰着される.(2)型の包含関係は決定可能(decidable)である.(3)極小な型付けが存在する.すなわち型付け可能な式に対しては型の包含関係を順序関係とする極小な型付けが常に可能である.(4)極小な型付けを行うアルゴリズムが存在する.以上の性質を用いて,不完全RE型の型検査および型付けを行うアルゴリズムを構築した.さらに,不完全RE型の式のパターン照合アルゴリズムを与えた.このアルゴリズムの定式化には疑似言語ではなく変換規則を用いた.現在までに,関数記号の型が個体型(individual type)の場合について,本アルゴリズムの求解の健全性(soundness)と完全性(completeness)について考察を進め,その証明をほぼ完了した.本アルゴリズムのユニフィケーションへの拡張については現在進行中であり,次年度前半にかけて行う.
|
