2001 Fiscal Year Annual Research Report
宣言型プログラムを対象とする高階項書換え系の計算理論
| Project/Area Number |
12878047
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
鈴木 大郎 会津大学, コンピュータ理工学部, 助手 (90272179)
MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)
|
|---|
| Keywords | 宣言型プログラム / 計算モデル / ナローイング計算系 / 選択関数 / 球解完全性 / 高階遅延ナローイング |
|---|
| Research Abstract |
宣言型プログラミングの計算のモデルとしての高階項書換え系の諸性質の解明を行った.特に,高階の単一化に関わる機能や一階の項を操作する機構など,高階性に由来する強力な計算能力を活かした計算の理論の構築をはかり,宣言型プログラムのプログラム変換や自動導出研究の基礎の確立に貢献することを目指した.以下に得られた研究成果をまとめる.
1.高階書換え系における簡約の戦略について,一階の場合と同様な標準化定理が成立することを確認した.高階簡約の標準化定理はLeft-linear Fully-extendedであるパターン書換え系について成立する.
2.標準簡約の概念を組み込んだ高階の計算系HOLN(Higher-order Lazy Narrowing Calculi)を設計し,健全性・完全性の証明を得た.さらに,HOLNを関数・論理型言語の計算モデルとしたときに考えられるいくつかの最適化について考察した.最適化によっても,完全性が失われないことを示した.
3.HOLNは高階単一化,遅延ナローイングを組み込んだ計算系であり,本研究の成果をシステムとして実現するものである.さらにHOLNを実装し,関数・論理型言語のモデルとしての適切性について評価を行った.
条件付きナローイング計算系が,外変数のない合流性をもつ条件付き書換え系について,正規化可能解に関して完全であることを以前に示していたが,さらにゴールの中の等式選択の戦略として,最左戦略をとっても完全であることを新たに明らかにした.ここで得られた照明技法は上記2.において高階計算系HOLNの完全性を証明する上でも活用された.
|
Research Products
(4 results)
-
[Publications] Tetsuo Ida, Mircea Marin, Taro Suzuki: "Higher-order Lazy Narrowing Calculus : a Solver for Higher-order"Equations, Conference on Computer Aided Systems (EUROCAST 2001), Lecture Notes in Computer Science 2178, Las Palmas de Gran Canaria, Spain. 478-493 (2001)
-
[Publications] Mircea Marin, Taro Suzuki, Tetsuo Ida: "Refinements of Lazy Narrowing for Left-Linear Fully-Extended Pattern Rewrite Systems"Technical Report ISE-TR-01-180, Institute of Information Sciences and Electronics, University of Tsukuba. (2001)
-
[Publications] Taro Suzuki, Aart Middeldorp: "A Complete Selection Function for Lazy Conditional Narrowing"Proceedings of the 5th International Symposium on Functional and Logic Programming (FLOPS 2001), Lecture Notes in Computer Science 2024. 201-251 (2001)
-
[Publications] Mircea Marin, Tetsuo Ida, Taro Suzuki: "Cooperative Constraint Functional Logic Programming"Proceedings of the International Symposium on Principles of Software Evolution (ISPSE 2000), Kanazawa, IEEE Computer Society, pp. 214-220 (2001)
