| 研究概要 |
本年度は,高階項書換え系にもとづいたXML変換のための具体的な枠組みを作り上げた.この枠組みでは,項と型の両方に特別な表現□の存在を許す.項に現れる□はλ項の束縛変数に相当し,□を含む項はトップレベルだけにλバインダをもつ二階のλ抽象に相当する.また,□を含む項に引数を与えることは,λ項のリデックスをβ簡約することに相当する.すなわち,我々の枠組みは制限された二階のλ計算に相当するが,XML文書そのものが一階の項なので,XML文書の変換はこの制限のもとで表せることを我々は見いだした.また,λ計算よりも制限された理論的枠組みを与えることで,理論的な扱いを容易にすることができた.
XML文書の変換では,変換前と変換後で同じタグがまったく異なる型をもつことがよくある.このようなタグへの型付けは,通常の型変数を用いたのでは対応できない.我々の枠組みでは,型に現れる□を他の型で置き換えることで新たな型を生成できる.□を置き換える型は任意なので,□を含む型をもつ(二階の)変数に,変換の前後で異なる型をもつ引数を与えるような変換パターンを記述できる.このような変換パターンにより,同じタグに異なる型付けをするような変換が可能になった.我々の体系は,上記のような柔軟な型体系をもつが,すべての変換パターンに対して静的な型チェックを行うことができる.
また,我々の枠組みでは,通常の高階パターン照合で生じるような求解の非決定性はまったく生じない.これは枠組みの理論的取り扱いのみならずパターン照合アルゴリズムの設計と実装をも容易にするという利点がある.
我々は,この枠組みの型理論的な性質を明らかにし(研究業績2),パターン照合アルゴリズムを提案した(研究業績1).今年度提案したパターン照合アルゴリズムはいくつかの制限をもつので,次年度でこの制限をなくしていく.また,提案したパターン照合アルゴリズムにもとづいて,プロトタイプシステムの実装を行う.
|
