等式付き書換え系の等式数を削減する変換  [in Japanese] Transformation of Equational Rewriting Systems for Removing some Equations  [in Japanese]

Search this Article

Author(s)

Abstract

与えられた等式集合を法として計算する等式付き書換え計質では,等式集合の語問題が決定不能であるため,一般には,与えられた項から1ステップで到達可能なすべての項を決定することができない.本稿では,与えられた等式付き書換え系を等価変換する手続きを与える.提案する手続きでは,等式の一部を規則化し,さらにそれらと重なる規則に対してそれらの等式を法として等価な左辺を持つ規則を追加する.元の等式集合から等式数を削減し,語問題が決定可能となる等式を残すことができれば,等式付き書換え系における1ステップの計算で到達可能なすべての項が決定可能となる.本変換は,等式付き書換え系の計算系列において各等式の適用順序が可換であるシステムを対象とする.また,本手法をプロセス計算の一つであるアンビェント計算に適用し,2つの単純な構造等価関係を規則化に成功した例を示す.

In equational rewriting, which is rewriting modulo equations, the set of all direct successors from a given term is in generally undecidable because the word problem for equations is undecidable. In this paper, we give an equivalent transformation of equational rewriting systems. The procedure converts some of the given equations to corresponding rewrite rules, and simultaneously adds rewrite rules whose left-hand sides are equivalent modulo equations with the left-hand sides of some of the given rules. Succeeded to reduce the number of equation so that the word problem for the remaining equation is decidable, the set of all direct successors of a given term becomes decidable. The procedure requires that input equations are commutative to the other equations. We also give a successful example of the procedure that is for ambient calculus.

Journal

  • IEICE technical report

    IEICE technical report 106(120), 7-12, 2006-06-15

    The Institute of Electronics, Information and Communication Engineers

References:  4

  • <no title>

    BAADER F.

    Term Rewriting and All That, 1998

    Cited by (1)

  • <no title>

    OHLEBUSCH E.

    Advanced Topics in Term Rewriting, 2001

    Cited by (1)

  • Mobile ambients

    CARDELLI L.

    Foundations of Software Science and Computation Structures : First International Conference, FOSSACS '98, 1998

    Cited by (1)

  • Dependency pairs for equational rewriting

    GIESL J.

    Proceedings of the 12th International Coference on Rewriting Techniques and Applications, 2001, 2001

    Cited by (1)

Cited by:  1

Codes

  • NII Article ID (NAID)
    110004750957
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    Journal Article
  • ISSN
    09135685
  • NDL Article ID
    7977513
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  CJPref  NDL  NII-ELS 
Page Top