1996 Fiscal Year Annual Research Report

高階関数・論理型プログラムの計算モデル

Research Project

Project/Area Number	08458059
Research Category	Grant-in-Aid for Scientific Research (B)
Research Institution	University of Tsukuba
Principal Investigator	井田哲雄筑波大学, 電子・情報工学系, 教授 (70100047)
Co-Investigator(Kenkyū-buntansha)	鈴木大郎筑波大学, 電子・情報工学系, 助手 (90272179) AART Middeld 筑波大学, 電子・情報工学系, 助教授 (30251044)
Keywords	ナロ-イング / 高階関数論理型言語 / 計算モデル / 条件付き項書換え系 / 安全性
Research Abstract	一階の関数論理型言語の計算モデルであるナロ-イング計算系を拡張し、より強力な表現力を備えた関数論理型言語を得ることを目指した、計算モデルに関する研究を行った。具体的には、本研究班でこれまでに開発を進めてきた遅延ナロ-イング計算系をベースに研究を展開し、計算系の実装、基礎理論のより深い展開、計算系の拡張を行った。研究の成果は次のとおりである。 (1)遅延ナロ-イング計算系を条件付き項書換え系を用いた計算系に拡張し、求解の完全性と強完全性をいくつかのクラスの条件付き項書換え系に対して示した。 (2)関数論理型言語の新たな宣言的意味論を構築し、既存の意味論との比較検討を行った。さらに、条件付き項書換え系を用いた場合へと、宣言的意味論を拡張した。 (3)ラムタ項を許す高階遅延ナロ-イング計算系を考案し、求解の安全性を示した。さらに、高階遅延ナロ-イング計算系に基づく、高階関数論理型プログラミングの様々な手法を明らかにした。 (4)並列ナロ-イング法を開発し、並列計算機に実装し、評価を行った。この結果、求解の安全性を保証し、かつ効率のよいアルゴリズムを見出した。 (5)Mathematicaを用いて、これまでに開発したナロ-イング計算系の試験的実装を行い、遅延ナロ-イング計算系の有効性を示した。特に、Mathematicaのもつ記号計算との融合が容易にできること明らかにした。 (6)遅延計算の新たな理論を展開し、遅延ナロ-イング計算系の理論的基礎を示した。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] ミデルド-ブアート: "Call by Need Computations と Root-Stable Form" Proc.of the 24th Annual ACM Symposium on POPL. 94-105 (1997)
[Publications] ミデルド-ブアート他: "Simple Termination of Rewrite Systems" Theoretical Computer Science. 175(1). 127-158 (1997)
[Publications] ミデルド-ブアート他: "Lazy Narrowing : Strong Completeness and Eager Variable Elimination" Theoretical Computer Science. 167. 95-130 (1996)
[Publications] 浜名誠他: "and Equivalence Between the Quotient Term Model and the Least Complete Herbrand Model for a Functional-Logic Language" The Journal of Functional and Logic Programming. 1997-1. 1-22 (1997)
[Publications] Mohamed Hamada他: "Stong Completeness of a Lazy Conditional Narrowing Calculus" Proc.of the 2nd Fuji International Workshop on FLP. 10-19 (1996)
[Publications] 鈴木大郎: "Standardization Theorem Revisite" Proc.of the 5th International Conf.on ALP. LNCS1139. 122-134 (1997)

1996 Fiscal Year Annual Research Report

高階関数・論理型プログラムの計算モデル

Principal Investigator

井田 哲雄 筑波大学, 電子・情報工学系, 教授 (70100047)

Research Products

[Publications] ミデルド-ブ アート: "Call by Need Computations と Root-Stable Form" Proc.of the 24th Annual ACM Symposium on POPL. 94-105 (1997)

[Publications] ミデルド-ブ アート他: "Simple Termination of Rewrite Systems" Theoretical Computer Science. 175(1). 127-158 (1997)

[Publications] ミデルド-ブ アート他: "Lazy Narrowing : Strong Completeness and Eager Variable Elimination" Theoretical Computer Science. 167. 95-130 (1996)

[Publications] 浜名誠 他: "and Equivalence Between the Quotient Term Model and the Least Complete Herbrand Model for a Functional-Logic Language" The Journal of Functional and Logic Programming. 1997-1. 1-22 (1997)

[Publications] Mohamed Hamada他: "Stong Completeness of a Lazy Conditional Narrowing Calculus" Proc.of the 2nd Fuji International Workshop on FLP. 10-19 (1996)

[Publications] 鈴木 大郎: "Standardization Theorem Revisite" Proc.of the 5th International Conf.on ALP. LNCS1139. 122-134 (1997)

井田哲雄筑波大学, 電子・情報工学系, 教授 (70100047)

[Publications] ミデルド-ブアート: "Call by Need Computations と Root-Stable Form" Proc.of the 24th Annual ACM Symposium on POPL. 94-105 (1997)

[Publications] ミデルド-ブアート他: "Simple Termination of Rewrite Systems" Theoretical Computer Science. 175(1). 127-158 (1997)

[Publications] ミデルド-ブアート他: "Lazy Narrowing : Strong Completeness and Eager Variable Elimination" Theoretical Computer Science. 167. 95-130 (1996)

[Publications] 浜名誠他: "and Equivalence Between the Quotient Term Model and the Least Complete Herbrand Model for a Functional-Logic Language" The Journal of Functional and Logic Programming. 1997-1. 1-22 (1997)

[Publications] 鈴木大郎: "Standardization Theorem Revisite" Proc.of the 5th International Conf.on ALP. LNCS1139. 122-134 (1997)