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

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

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