Top> NUEセミナー> NUEセミナー(2001年)

NUEセミナー(2001年)

東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています． テーマはプログラム理論や定理自動証明を中心に， 情報科学の理論的なさまざまな話題をとりあげています． 興味をおもちの方はどなたでもフラリと気楽におたちより下さい．

第７回NUEセミナー

日時 2001年11月30日
講演者 佐伯 豊 (東北大学)
題目 拡張可能なプログラミング言語のための安全な拡張方式にむけて
要旨 近年，並列・分散処理や，適応可能なソフトウェアなど，複雑なソフ トウェアを構築する際に有効な，動的な適応性や発展的なソフトウェア開発を サポートする開発環境への要求が高まっている．しかし従来の固定された記述 体系(言語)では，このような新たな要求を満たすモデルを直接表現することが できないため，メンテナンスや機能拡張の際に問題が生じる可能性が高い．そ のような問題点を解決するための方法として，プログラミング言語をアプリケー ションプログラムの問題領域に応じて拡張するアプローチが有効であることが 知られている．拡張部品の設計および配布と，その利用者との分離が必ずしも 実現されているとは言えない．本研究ではコンパイラのコード生成の過程の定 義を部品化(言語モジュール)し，各部品単位での抽象度の高い機能拡張を実現 することを目的とする．また，言語部品の利用者が衝突のおこらないような部 品の選択をおこなう，あるいは拡張記述の間の衝突の可能性を検出し，修正を 容易にするための枠組みについて考察する．

第６回NUEセミナー

日時 2001年9月21日
講演者 酒井正彦 (名古屋大学)
題目 PT関数の逆関数を定義するTRSの生成
要旨 パターン照合の機能を持ち、右辺に入れ子の関数呼び出しを持たない pure treeless 関数定義から、指定された関数の逆関数の定義を持つCTRSを生 成するアルゴリズムを提案する。さらに、PT関数定義の右辺が線形のとき、本 アルゴリズムにより生成されたCTRSはTRSに変換できることを示す。

第５回NUEセミナー

日時 2001年6月14日
講演者 細谷晴夫 (筑波大学)
題目 XMLのための正規表現型
要旨 XMLは木構造データのための単純でかつ柔軟性のある汎用データ形式で ある。またXMLは、そのサブセットをスキーマを用いて定義することができ、 それを個別のアプリケーションのデータ交換形式として用いることができる。 近年XMLが次世代Webアプリケーションへ急速に採用されてきているに従い、 XML を用いたソフトウェア開発に助けとなるようなよりよいプログラミング言 語機能のサポートが求められている。特に、強い要望のある機能は、(1) 出力 データが、与えられたスキーマに必ず従うことを保証する静的プログラム解析、 (2) 木構造を操作するために便利な言語機能である。
本研究では、XML処理言語の核となる機能を２つ、すなわち「正規表現型」と 「正規表現パターンマッチ」を提案する。正規表現型は、スキーマ言語によく 見られる「繰り返し (*)」や「選択 (|)」などの正規表現の記法を型システム に採り入れる。さらに、「意味論」的に定義された部分型をサポートする。本 研究では、この部分型がもつ柔軟性が、XMLを用いたソフトウェアをスムーズ に進化させるのに必要であることを論じる。正規表現パターンマッチは、従来 の (関数型言語にあるような) パターンマッチ機構に、上記の繰り返しや選択 の演算子を追加したものである。これら演算子を使うことによって、任意の長 さを持つ部分木「列」をマッチすることができるようになるので、列の中の任 意の位置に一挙に飛んで、そこから欲しいデータを抽出するようなパターンが 簡潔に記述できる。本研究ではさらに、これら２つの機能を使った言語の例と してXDuce言語を設計し、その核言語を定式化し、型健全性を証明する。
さらに本研究では、上記の機能を実現する上で発生するアルゴリズム上の問題 にも取り組む。部分型の判定問題は、正規ツリーオートマトンの包含判定問題 に簡単に帰着できるが、この問題自体が指数時間完全という高い計算量をもつ ことが分かっている。この問題点に対し本研究では実際の入力に対しては効率 的に動作するアルゴリズムを開発する。まず出発点としてAiken とMurphy の 集合制約の解消アルゴリズムを用いる。本研究での追加点は(1) 完全性の証明、 (2) XML処理で発生する典型例に対応した実装技法、(3) 予備実験である。予 備的実験では、ある程度現実的な例をいくつか試した結果、実用的な効率で動 作することを確認した。
正規表現パターンマッチを型付きプログラミング言語に用いる際、パターンマッ チに出現する変数の型を自動的に計算し、過度な型注釈をユーザに要求しない ようにすると言うことが重要である。そのために本研究では、パターンマッチ を取り巻く文脈からパターンの変数へ、型情報を伝播するような型推論アルゴ リズムを開発する。このアルゴリズムは、まず型とパターンをツリーオートマ トンへ変換し、ツリーオートマトンの閉包演算 (和・積・差) を使って型情報 の伝播を行なう。技術的に困難な点は、繰り返し演算子と、選択演算子の「第 一マッチ則 (先に出現する選択肢が優先的にマッチする性質) 」が相互作用し、 これによって解析の停止性と精度を同時に保証することが難しくなるというこ とである。本研究ではこの問題点に対し、閉包演算を明示的に含んだような型 の表現を導入することによって解決する。
[外山研究室] [電気通信研究所] [東北大学]
ご意見お問い合わせは webmaster まで．