DECIDABILITY OF THE CONFLUENCE OF FINITE GROUND TERM REWRITE SYSTEMS AND OF OTHER RELATED TERM REWRITE SYSTEMS

被引：53
|
作者：
DAUCHET, M
HEUILLARD, T
LESCANNE, P
TISON, S
机构：
[1] UNIV PARIS 11,RECH INFORMAT LAB,F-91405 ORSAY,FRANCE
[2] LORIA,F-54506 VANDOEUVRE NANCY,FRANCE
[3] CTR RECH INFORMAT NANCY,CNRS,UA 262,F-54506 VANDOEUVRE NANCY,FRANCE
来源：
INFORMATION AND COMPUTATION | 1990年 / 88卷 / 02期
关键词：
D O I：
10.1016/0890-5401(90)90015-A
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The aim of this paper is to propose an algorithm to decide the confluence of finite ground term rewrite systems. Actually a more general class of possibly infinite ground term rewrite systems is studied. It is well known that the confluence is not decidable for general term rewrite systems, but this paper proves it is for ground term rewrite systems following a conjecture made by Huet and Oppen in their survey. The result is also applied to the confluence of left-linear and right-ground term rewrite systems. We also sketch an algorithm for checking this property. This algorithm is based on tree automata and tree transducers. Here, we regard them as rewrite systems and specialists in automata theory would translate that easily in their language. © 1990.
引用
收藏
页码：187 / 201
页数：15
相关论文
共 50 条
  • [21] Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
    Goeller, Stefan
    Lin, Anthony Widjaja
    CONCUR 2011: CONCURRENCY THEORY, 2011, 6901 : 543 - +
  • [22] Higher-order rewrite systems and their confluence
    Mayr, R
    Nipkow, T
    THEORETICAL COMPUTER SCIENCE, 1998, 192 (01) : 3 - 29
  • [23] Confluence Criteria for Logically Constrained Rewrite Systems
    Schoepf, Jonas
    Middeldorp, Aart
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 474 - 490
  • [24] CONFLUENCE OF INDIRECTION REDUCTIONS IN GRAPH REWRITE SYSTEMS
    VANDENBROEK, PM
    INFORMATION PROCESSING LETTERS, 1988, 29 (03) : 143 - 148
  • [25] Confluence of terminating conditional rewrite systems revisited
    Gramlich, B
    Wirth, CP
    REWRITING TECHNIQUES AND APPLICATIONS, 1996, 1103 : 245 - 259
  • [26] Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
    Goeller, Stefan
    Lin, Anthony Widjaja
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (04)
  • [27] Confluence of Logically Constrained Rewrite Systems Revisited
    Schoepf, Jonas
    Mitterwallnel, Fabian
    Middeldorp, Aart
    AUTOMATED REASONING, IJCAR 2024, PT II, 2024, 14740 : 298 - 316
  • [28] Deterministic bottom-up tree transducers and ground term rewrite systems
    Sandor Vagvoelgyi
    THEORETICAL COMPUTER SCIENCE, 2009, 410 (21-23) : 2250 - 2278
  • [29] On decidability of LTL model checking for process rewrite systems
    Bozzelli, Laura
    Kretinsky, Mojmir
    Rehak, Vojtech
    Strejcek, Jan
    ACTA INFORMATICA, 2009, 46 (01) : 1 - 28
  • [30] On decidability of LTL model checking for process rewrite systems
    Laura Bozzelli
    Mojmír Křetínský
    Vojtěch Řehák
    Jan Strejček
    Acta Informatica, 2009, 46 : 1 - 28
12345