1995 年度実績報告書

外変数のある条件付き書換えとナロ-イング

研究課題

研究課題/領域番号	07780220
研究機関	筑波大学
研究代表者	MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)
キーワード	条件付き項書換え系 / 外変数 / 条件付きナロ-イング / 階層合流性 / モジュラー性 / ナロ-イング計算系
研究概要	1.外変数のある条件付き項書換え系に対するナロ-イング昨年度、申請者らは、外変数をもつ条件付き項書換え系が階層合流性をもつための十分条件を提案した。階層合流性は、外変数をもつ条件付き項書換え系に対して、ナロ-イングの求解完全性を保証するために重要な性質である。この十分条件をみたす条件付き項書換え系について、外変数が書換え規則の条件部のみに現れるように制限を加えると、ナロ-イングが求解完全性をもつことを示した。本研究で得られたナロ-イングの求解完全性を保証する十分条件は、停止性をもたない条件付き項書換え系に対する既知の十分条件をすべて包含する。現在、書換え規則の右辺に外変数を含む場合でも、ナロ-イングの求解完全性が保証されるかどうか検討中である。 2.外変数のある条件付き項書換え系の階層合流性に対するモジュラー性ある性質がモジュラーであるとは、その性質をもつ2つの項書換え系を合わせてつくられる項書換え系について同じ性質が成り立ち、しかも、その性質をもつ項書換え系を2つの項書換え系に分割してもそれぞれ同じ性質が成り立つことをいう。モジュラー性は、規模の大きい書換え系の性質を、小さな書換え系へと分解して解析する場合、重要な性質である。申請者らは、書換え規則の条件部のみに外変数をもつ条件付き項書換え系に対して、階層合流性がモジュラーな性質であることを示した。1.の場合と同様に、書換え規則の右辺にも外変数を含む条件付き項書換え系について、階層合流性がモジュラーな性質であるかどうか検討する予定である。 3.遅延ナロ-イング計算系LNC 宣言型言語の計算モデルとしてLNC(Lazy Narrowing Calculus)とよばれるナロ-イング計算系を設計し、この計算系が等式の列の求解に対して強完全性をもつための十分条件を明らかにした。また、合流性をもつ項書換え系に対して、与えられた等式の列のうち、常に最左の等式を選択しても求解完全性が得られることを証明した。さらに、正交な項書換え系に限ることで、関数型言語で発展されてきたのと同等な遅延評価機構をナロ-イングに対しても導入できることを示した。

研究成果
(10件)

すべてその他

すべて文献書誌 (10件)

[文献書誌] ミデルドープアート: "Simple termination is difficult" Applicable Algebra in Engineering, Communication and Computing. 6. 115-128 (1995)
[文献書誌] 山田俊行: "条件付き項書換え系における階層合流性のモジュラ性" コンピュータソフトウエア. 12(5). 72-84 (1995)
[文献書誌] ミデルドープアート: "A Deterministic Lazy Narrowing Calculus" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 48-62 (1995)
[文献書誌] 中原鉱一: "A complete narrowing calculus for higher-order functional logic programming" Proc. of the 7et Int. Conf. on PLILP ′95, LNCS 982. 97-114 (1995)
[文献書誌] 奥居哲: "Lazy narrowing: Strong completeness and eager variable elimination" TAPSOFT CAAP, LNCS 915. 394-409 (1995)
[文献書誌] 鈴木大郎: "Level-confluence of conditional rewrite systems with extra variables in right-hand sides" Proc. of the 6th Int. Conf. on RTA ′95, LNCS 914. 1995. (179-193)
[文献書誌] 鈴木大郎: "Completeness of Narrowing for Orthogonal Conditional Rewrite Systems" Proc. of Fuji Int. Workshop on Functional and Logic Programming. 63-77 (1995)
[文献書誌] 井田哲雄: "Leftmost outside-in narrowing calculi" Journal of Functional Programming. (発表予定).
[文献書誌] ミデルドープアート: "Lazy narrowing: Strong completeness and eager variable elimination" Theoretical Computer Science. (発表予定).
[文献書誌] 大崎人士: "意味ラベリングによる分配消去法-項書換え系の停止性証明法-" コンピュータソフトウェア. (発表予定).

1995 年度 実績報告書

外変数のある条件付き書換えとナロ-イング

研究代表者

MIDDELDORP Aart 筑波大学, 電子・情報工学系, 助教授 (30251044)

研究成果

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

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

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

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

[文献書誌] 奥居哲: "Lazy narrowing: Strong completeness and eager variable elimination" TAPSOFT CAAP, LNCS 915. 394-409 (1995)

[文献書誌] 鈴木大郎: "Level-confluence of conditional rewrite systems with extra variables in right-hand sides" Proc. of the 6th Int. Conf. on RTA ′95, LNCS 914. 1995. (179-193)

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

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

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

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

1995 年度実績報告書