| 研究課題/領域番号 |
08458059
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
|
|---|
| 研究分担者 |
鈴木 太郎 筑波大学, 電子・情報工学系, 助手 (90272179)
チャクラヴァーティ マニ 筑波大学, 電子・情報工学系, 講師 (30292535)
ミデルドーブ アート 筑波大学, 電子・情報工学系, 助教授 (30251044)
|
|---|
| キーワード | ナロ-イング / 高階関数論理型言語 / 計算モデル / 条件付き項書換え系 / 求解完全性 |
|---|
| 研究概要 |
高階の項を操作する機構を備えた関数論理型言語のための計算モデルとその宣言的意味論についての研究を行った。本研究班でこれまでに行ってきた遅延ナロ-イング計算系(LNG)をベースにし、高階の項を効率よく操作できるような計算系の拡張を行った。研究の成果は次の通りである。
1.高階項書換え系に対するナロ-イングを実現する高階ナロ-イング計算系HLNC(Higher-order Lazy Narrowing Calculus)を提案し、その求解完全性を示した。HLNCは一階の項書換え系に対するナロ-イングを実現していたLNCを高階に拡張したものである。HLNCは定数をもつラムダ計算を包含しており、ラムダ項を含む高階関数・論理型言語の基礎となる計算モデルを与えている。
2.関数型プログラミングに関係を導入することで、型付きラムダ計算に基づく並列関数論理型言語を設計した。この言語では、逐次的な処理は純粋な関数で表し、並列な振舞いは関係を用いて記述することで、並列プログラムを宣伝的に記述できる。得られた計算モデルに対して、線形論理との対応付けによる論理的な意味論と、それから導かれる並列処理の意味論を与えた。
3.ナロ-イングを条件付き項書換え系に対して拡張したときの、条件付きナロ-イングの求解完全性の検討を行い、新たな結果を得た。特に、外変数を書換え規則の右辺に持つ条件付き項書換え系に対するナロ-イングの求解完全性の十分条件の証明を行なった。この結果は、関数型言語におけるwhere節のような局所的定義をもつ関数論理型言語の計算モデルとして利用できる。
4.ナロ-イング計算系LNGを条件付きシステムLazy Conditional Narrowing Calculus(略してLCNC)へと拡張した。拡張は理論面では、強完全性と完全性をもつ条件付き項書換え系を明らかにした点、実用面ではLCNCd(deterministic LCNC)を設計し、Mathematica処理系上に実装した点である。
|
