条件付き項書換え系におけるナロ-イングおよび簡約の研究

点击翻译按钮获取中文摘要

1 遅延ナロ-イングナロ-イングは、合流性をもつ項書換え系で表現される等式理論を法とする等式の求解手続きとして重要である。正規化可能な解についてナロ-イングは完全であることは良く知られている。ナロ-イングの対象を複数の等式を含むゴールに拡張したとき、ゴール中の等式の選び方に関わらずナロ-イングが完全であるならば、ナロ-イングは強完全であるという。ナロ-イングを推論規則の集合である計算系により表現したものとして、Holldoblerにより提案された遅延ナロ-イング計算系がある。我々は、彼の主張に反して、この計算系が強完全性をもたないことを示した。我々はこの計算系の完全性を証明し、さらに、この計算系の強完全性と基本ナロ-イングの完全性との間に驚くべき関係が成り立つことを示した。我々は、変数除去問題(eager variable elimination problem)についても新たな結果を得た。推論規則のうち、変数除去規則を他の推論規則よりも先に用いることで、多くの冗長なナロ-イング導出列の生成が避けられることが知られている。我々は、正交な項書換え系について、変数除去問題の制限された完全性を証明した。我々が得た結果について述べた論文は、国際会議TAPSOFT/CAAP-95の論文集への採録が決定している。今後、我々はこの結果を条件付き項書換え系に拡張できるかどうか検討を加える予定である。2 条件付き書換え書換え規則に外変数の存在を許す条件付き項書換え系において、階層合流性は(条件付き)ナロ-イングの完全性を保証するために重要な概念である。我々は、書換え規則の右辺に外変数の存在を許す正交な書換え系について、停止性を仮定せずに、階層合流性を保証する構文的な条件を明らかにした。この条件を満たす条件付き項書換え系のクラスは、let式やwhere節のような局所定義を持つ関数・論理型プログラミング言語の計算モデルとみなすことができる。したがって、我々が得た結果は実用的にも重要な意義を持つ。我々が得た結果について述べた論文は、国際会議RTA-95の論文集への採録が決定している。現在、我々はここで明らかにした構文的な条件を満たす条件付き項書換え系についてのナロ-イングの完全性についての考察を行なっている。