XMLは木構造データのための単純でかつ柔軟性のある汎用データ形式である。またXMLは、そのサブセットをスキーマを用いて定義することができ、それを個別のアプリケーションのデータ交換形式として用いることができる。近年XMLが次世代Webアプリケーションへ急速に採用されてきているに従い、XMLを用いたソフトウェア開発に助けとなるようなよりよいプログラミング言語機能のサポートが求められている。特に、強い要望のある機能は、(1)出力データが、与えられたスキーマに必ず従うことを保証する静的プログラム解析、(2)木構造を操作するために便利な言語機能である。

　本論文では、XML処理言語の核となる機能を2つ、すなわち「正規表現型」と「正規表現パターンマッチ」を提案する。正規表現型は、スキーマ言語によく見られる「繰り返し(*)」や「選択(l)」などの正規表現の記法を型システムに採り入れる。さらに、「意味論」的に定義された部分型をサポートする。本研究では、この部分型がもつ柔軟性が、XMLを用いたソフトウェアをスムーズに進化させるのに必要であることを論じる。正規表現パターンマッチは、従来の(関数型言語にあるような)パターンマッチ機構に、上記の繰り返しや選択の演算子を追加したものである。これら演算子を使うことによって、任意の長さを持つ部分木「列」をマッチすることができるようになるので、列の中の任意の位置に一挙に飛んで、そこから欲しいデータを抽出するようなパターンが簡潔に記述できる。本研究ではさらに、これら2つの機能を使った言語の例としてXDuce言語を設計し、その核言語を定式化し、型健全性を証明する。

　さらに本研究では、上記の機能を実現する上で発生するアルゴリズム上の問題にも取り組む。部分型の判定問題は、正規ツリーオートマトンの包含判定問題に簡単に帰着できるが、この問題自体が指数時間完全という高い計算量をもつことが分かっている。この問題点に対し本研究では実際の入力に対しては効率的に動作するアルゴリズムを開発する。まず出発点としてAikenとMurphyの集合制約の解消アルゴリズムを用いる。本研究での追加点は(1)完全性の証明、(2)XML処理で発生する典型例に対応した実装技法、(3)予備実験である。予備的実験では、ある程度現実的な例をいくつか試した結果、実用的な効率で動作することを確認した。

　正規表現パターンマッチを型付きプログラミング言語に用いる際、パターンマッチに出現する変数の型を自動的に計算し、過度な型注釈をユーザに要求しないようにすると言うことが重要である。そのために本研究では、パターンマッチを取り巻く文脈からパターンの変数へ、型情報を伝播するような型推論アルゴリズムを開発する。このアルゴリズムは、まず型とパターンをツリーオートマトンへ変換し、ツリーオートマトンの閉包演算(和・積・差)を使って型情報の伝播を行なう。技術的に困難な点は、繰り返し演算子と、選択演算子の「第一マッチ則(先に出現する選択肢が優先的にマッチする性質)」が相互作用し、これによって解析の停止性と精度を同時に保証することが難しくなるということである。本研究ではこの問題点に対し、閉包演算を明示的に含んだような型の表現を導入することによって解決する。

インターネットの普及により、WWWは非常に多くのユーザに利用され、情報社会のインフラストラクチャーとして生活にとってさえ不可欠な存在になっている。WWWのデータ記述言語として最も利用されているのがHTML(Hyper Text Markup Language)である。HTMLは言語仕様が簡潔であったため、WWW黎明期において非常な勢いで広がり、また初期の段階における需要をカバーするのには十分であった。しかし、おびただしい数のデータがHTMLにより記述されるに至り、HTMLの言語仕様の素朴さは、拡張性に乏しい物足りなさとして映るようになってしまった。

HTMLでは＜title＞Thesis＜/title＞のような＜＞で囲まれたタグを用いて、データを入れ子型に構造化しながら記述してゆく。HTMLの不自由な点の一つは、タグ名を自由に定義できないことである。また、住所録のようなデータを記述する場合には、構造化の順序を規定する文法を記述してから、データの中身を書けるようにできれば、データが文法に従って書かれているか自動的にチェックできる。しかしHTMLには文法を記述する機能が備わっていない。これらの要望を実現する形で最近WWWコンソーシアムの標準化委員会が提案したのがXML(eXtensible Markup Language)であり、技術的にはXML処理言語の設計が研究の焦点となっている。

本論文の第1章では、XML言語に関する簡潔な解説をした後、例題を用いながら非専門家にも研究成果がわかるように腐心している。

第2章では、XML処理言語の核となる機能を2つ、すなわち「正規表現型」と「正規表現パターンマッチ」を提案している。正規表現型は、スキーマ言語によく見られる「繰り返し(*)」や「選択(1)」などの正規表現の記法を型システムに採り入れる。さらに、「意味論」的に定義された部分型をサポートすることを試みている。そして、この部分型がもつ柔軟性が、XMLを用いたソフトウェアをスムーズに進化させるのに必要であることを論じている。正規表現パターンマッチは、従来の(関数型言語にあるような)パターンマッチ機構に、上記の繰り返しや選択の演算子を追加したものである。これら演算子を使うことによって、任意の長さを持つ部分木「列」をマッチすることができるようになるので、列中の任意の位置に一挙に飛んで、そこから欲しいデータを抽出するようなパターンが簡潔に記述できるという利点がある。本論文では、これら2つの機能を使った言語の例としてXDuce言語を設計し、その核言語を定式化し、型健全性を証明することで、言語の理論的基盤を与えている。本章のXDuceは巧妙に設計されており、計算不能な性質を生み出しかねない言語機能は注意深く避けた組み立てをしながらも、実用性を損なわない配慮が秀逸である。

第3章では、部分型の判定問題を計算量理論的に解析している。この判定問題は、正規ツリーオートマトンの包含判定問題に簡単に帰着できるが、この問題自体が指数時間完全という高い計算量をもつことが知られている。したがって理論的には、すべての場合に効率的なアルゴリズムを設計することは困難であることが示唆される。しかし、多くの現実例で効率的に動作するソフトウエアが切望されており、次章でこの問題の解決に取り組んでいる。

第4章では、実際の入力に対しては効率的に動作するアルゴリズムを開発し、意表を突く良い結果を出している。AikenとMurphyの集合制約の解消アルゴリズム考察し、それを拡張するアプローチを取っているものの、十分独創的であり、(1)完全性の証明、(2)XML処理で発生する典型例に対応した実装技法の提案、(3)予備実験がなされている。予備的実験では、現実例をいくつか試した結果、実用上申し分ない効率で動作することを確認している。XMLが広がるにつれて、ここで提案されたアルゴリズムが広く世の中で利用されてことが期待できる。

第5章では木構造を操作するための便利な言語機能を提示している。正規表現パターンマッチを型付きプログラミング言語に用いる際、パターンマッチに出現する変数の型を自動的に計算することにより、過度な型注釈をユーザに要求することを回避できる。そのために、パターンマッチを取り巻く文脈からパターンの変数へ、型情報を伝播するような型推論アルゴリズムを開発している。このアルゴリズムは、まず型とパターンをツリーオートマトンへ変換し、ツリーオートマトンの閉包演算(和・積・差)を使って型情報の伝播を行なっている。技術的に困難な点は、繰り返し演算子と、選択演算子の「第一マッチ則(先に出現する選択肢が優先的にマッチする性質)」が相互作用し、これによって解析の停止性と精度を同時に保証することが難しくなるということである。本論文では、閉包演算を明示的に含んだような型の表現を導入することにより、この問題点を解決している。技術的に困難な問題に解答を与えた点で評価できるだけでなく、このアルゴリズムも広く普及することが期待できる。

なお本論文はBenjamin Pierce,Jerome Vouillon氏との共同研究であるが、論文提出者が主体となって提案・分析・評価を行ったもので、論文提出者の寄与が十分であると判断する。

したがって、博士(理学)を授与できると認める。