条件付き書換え系の宣言型プログラミングへの応用

1994 年度 実績報告書

• 研究課題/領域番号: 06680300
• 研究機関: 筑波大学
• 研究代表者: 井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)
• 研究分担者: MIDDELDORP A 筑波大学, 電子・情報工学系, 講師 (30251044)
• キーワード: 宣言型言語 / 関数 論理型言語 / ナロ-イング / 条件付項書換え系

研究概要

(1)宣言型プログラミングの計算モデルとして、Outside-Inナロ-イングとよばれる計算の機構を提示し、Outside-Inナロ-イングを実現する計算系を設計した。Outside-Inナロ-イングは、これまで関数型言語において発展されてきた遅延評価の概念を関数論理型言語へと拡張したものである。さらに、Outside-Inナロ-イングの等式の求解手続きとしての完全性を証明した。
(2)Outside-Inナロ-イング戦略を実現する計算系の設計方法について考察し、最適な推論規則の組み合せに関する知見を得た。これをさらに進めて、この計算系を効率よく実行する。遅延ナロ-イング抽象機械を設計した。
(3)設計した遅延ナロ-イング抽象機械の上で実行される関数論理型言語処理系を実装し、計算系の効率や、実装上の問題点を解明した。
(4)階層合流性や、階層停止性をもつ様々な条件付き項書換え系について、Basicナロ-イングの完全性を証明した。
(5)条件付き項書換え系の完全性を示す上で重要な概念である階層合流性について検討を加え、階層合流性がモジュラーな性質を持つことを証明した。
(6)書換え規則の右辺に外変数を許す条件付き正交書換え系について、停止性を仮定せずに階層合流性を保証する構文的な条件を明らかにした。これにより、let式やwhere節のような局所定義をもつ関数論理型言語の計算モデルの理論的取り扱いが可能となった。

研究成果

• [文献書誌] 山田俊行, Aart Middeldorp,井田哲雄: "条件付き項書換え系における階層合流性のモジュラ性" コンピュータソフトウェア. (印刷中). (1995)
• [文献書誌] Tetsuo Ida,Satoshi Okui: "Conditional Outside-In Narrowing" IEICE Transactions on Informaition and Systems. E77-D. 631-641 (1994)
• [文献書誌] 中川康二,中原鉱一,鈴木大郎,井田哲雄: "遅延ナロ-イング抽象機械" 電子情報通信学会論文誌. (印刷中). (1995)
• [文献書誌] S.Okui,A.Middeldorp,and T.Ida: "Lazy Narrowing:Strong Completeness and Eager Variable Elimination" Proceedings of the 20th Colloquium on Trees in Algebra and Programming,Lecture Notes in Computer Science. (印刷中). (1995)
• [文献書誌] T.Suzuki,A.Middeldorp,and T.Ida: "Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides" Proceedings of the 6th International Conferece on Rewriting Techniques and Applications,Lecture Notes in Computer Science. (印刷中). (1995)
• [文献書誌] A.Middeldorp and E.Hamoen: "Completeness Results for Basic Narrowing" Applicable Algebra in Engineering,Communication and Computing. 5. 213-253 (1994)