1995 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number	06680300
Research Institution	University of Tsukuba
Principal Investigator	井田哲雄筑波大学, 電子・情報工学系, 教授 (70100047)
Co-Investigator(Kenkyū-buntansha)	鈴木大郎筑波大学, 電子・情報工学系, 助手 (90272179) MIDDELDORP A 筑波大学, 電子・情報工学系, 助教授 (30251044)
Keywords	条件付き書換え系 / 宣言型プログラミング / 関数・論理型言語 / ナロ-イング / 階層合流性 / モジュラー性 / プログラム意味論
Research Abstract	本研究では、宣言型プログラミング言語の操作的意味を与える計算モデルとして条件付き項書換え系の性質を調べ、宣言型プログラミング言語の実用化の手がかりを得ようと試みた。我々が掲げた課題とその成果を以下に示す。 1.条件付き項書換え系を宣言型プログラミング言語にするための様々な条件の検討。特に求解法の一つであるナロ-イング計算系の求解の完全性を与える有効な十分条件の探索条件付き項書換え系を宣言型プログラミング言語として用いるために、OINC(Outside-In Narrowing Calculus)とLNC(Lazy Narrowing Calculus)という二つのナロ-イング計算系を設計した。これらは関数型言語において発展されてきた遅延評価の概念を関数論理型言語へと拡張するために設計された。また、これらの計算系が項書換え系に対して完全性をもつことを証明した。また、我々が昨年度提案した書換え規則の右辺に外変数の存在を許す条件付き項書換え系が階層合流性をもつための構文的な十分条件に関する結果に基づき、外変数を持つ正交な条件付き項書換え系に対してナロ-イングが完全性をもつための新たな十分条件を示した。さらに我々は、条件付きナロ-イングと宣言型プログラミング言語のモデルとの関係についても考察を行った。厳格等式のみを条件部にもつ正交な条件付き項書換え系に対して、条件付きナロ-イングは関数論理型言語の意味を与える代表的な2つのモデルに関して健全かつ完全になることを示した。 2.条件付き項書換え系の諸性質を利用したメタプログラミングのありかたの検討外変数をもつ条件付き項書換え系の階層合流性のモジュラー性について研究し、この性質がモジュラー性をもつことを示した。

Research Products
(16 results)

All Other

All Publications (16 results)

[Publications] 浜名誠: "作用型項書換え系に基づく関数論理型言語の設計と実装" 情報処理学会論文誌. 36(8). 1897-1905 (1995)
[Publications] ミデルドープアート: "Simple termination is difficult" Applicable Algebra in Engineering,Communication and Computing. 6. 115-128 (1995)
[Publications] 中川康二: "遅延ナロ-イング抽象機械" 電子情報通信学会論文誌. J78-D-1(5). 467-477 (1995)
[Publications] 佐々木重雄: "制約解消系を備えた関数・論理型言語の処理系とその実装" 情報処理学会論文誌. 36(9). 2152-2160 (1995)
[Publications] 山田俊行: "条件付き項書換え系における階層合流性のモジュラ性" コンピュータソフトウエア. 12(5). 72-84 (1995)
[Publications] 浜名誠: "Eqiuvalence Between the Quotient Term Model and Least Complete Herbrand Model for a Functional-Logic Language" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 155-170 (1995)
[Publications] 鈴木太郎: "Completeness of Narrowing for Orthogonal Conditional Rewrite Systems" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 63-77 (1995)
[Publications] 井田哲雄: "Leftmost outside-in narrowing calculi" Journal of Functional Programming. (発表予定).
[Publications] ミデルドープアート: "Lazy narrowing:Strong completeness and eager variable elimination" Theoretical Computer Science. (発表予定).
[Publications] 大崎人士: "意味ラベリングによる分配消去法-項書換え系の停止性証明法-" コンピュータソフトウェア. (発表予定).
[Publications] ミデルドープアート: "A Deterministic Lazy Narrowing Calculus" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 48-62 (1995)
[Publications] 中原鉱一: "A complete narrowing calculus for higher-order functional logic programming" Proc. of the 7the Int. Conf. on PLILP'95, LNCS 982. 97-114 (1995)
[Publications] 中川康二: "Compiling Programs of an Applicatived Narrowing Calculus" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 78-91 (1995)
[Publications] 奥居哲: "Lazy narrowing:Strong completeness and eager vadriable elimination" TAPSOFT CAAP. 394-409 (1995)
[Publications] 佐々木重雄: "An Efficient Calculus for Constraint Functional-Logic Programming Languages" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 171-185 (1995)
[Publications] 鈴木大郎: "Level-confluence of conditional rewrite systems with extra Variables in reight-hand sides" Proc. of the 6th Int. Conf. on RTA'95. 179-193 (1995)

1995 Fiscal Year Annual Research Report

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

Principal Investigator

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

Research Products

[Publications] 浜名誠: "作用型項書換え系に基づく関数論理型言語の設計と実装" 情報処理学会論文誌. 36(8). 1897-1905 (1995)

[Publications] ミデルドープアート: "Simple termination is difficult" Applicable Algebra in Engineering,Communication and Computing. 6. 115-128 (1995)

[Publications] 中川康二: "遅延ナロ-イング抽象機械" 電子情報通信学会論文誌. J78-D-1(5). 467-477 (1995)

[Publications] 佐々木重雄: "制約解消系を備えた関数・論理型言語の処理系とその実装" 情報処理学会論文誌. 36(9). 2152-2160 (1995)

[Publications] 山田俊行: "条件付き項書換え系における階層合流性のモジュラ性" コンピュータソフトウエア. 12(5). 72-84 (1995)

[Publications] 浜名誠: "Eqiuvalence Between the Quotient Term Model and Least Complete Herbrand Model for a Functional-Logic Language" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 155-170 (1995)

[Publications] 鈴木太郎: "Completeness of Narrowing for Orthogonal Conditional Rewrite Systems" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 63-77 (1995)

[Publications] 井田哲雄: "Leftmost outside-in narrowing calculi" Journal of Functional Programming. (発表予定).

[Publications] ミデルドープアート: "Lazy narrowing:Strong completeness and eager variable elimination" Theoretical Computer Science. (発表予定).

[Publications] 大崎人士: "意味ラベリングによる分配消去法-項書換え系の停止性証明法-" コンピュータソフトウェア. (発表予定).

[Publications] ミデルドープアート: "A Deterministic Lazy Narrowing Calculus" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 48-62 (1995)

[Publications] 中原鉱一: "A complete narrowing calculus for higher-order functional logic programming" Proc. of the 7the Int. Conf. on PLILP'95, LNCS 982. 97-114 (1995)

[Publications] 中川康二: "Compiling Programs of an Applicatived Narrowing Calculus" Proc. of Fuji Int.Workshop on Functional and Logic Programming. 78-91 (1995)

[Publications] 奥居哲: "Lazy narrowing:Strong completeness and eager vadriable elimination" TAPSOFT CAAP. 394-409 (1995)

[Publications] 佐々木重雄: "An Efficient Calculus for Constraint Functional-Logic Programming Languages" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 171-185 (1995)

[Publications] 鈴木大郎: "Level-confluence of conditional rewrite systems with extra Variables in reight-hand sides" Proc. of the 6th Int. Conf. on RTA'95. 179-193 (1995)

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