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
关键词
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 条
  • [31] On decidability of LTL model checking for process rewrite systems
    Bozzellil, Laura
    Kretinsky, Mojmir
    Rehak, Vojtech
    Strejcek, Jan
    FSTTCS 2006: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2006, 4337 : 248 - +
  • [32] On the normalization and unique normalization properties of term rewrite systems
    Godoy, Guillem
    Tison, Sophie
    AUTOMATED DEDUCTION - CADE-21, PROCEEDINGS, 2007, 4603 : 247 - +
  • [33] LSE narrowing for decreasing conditional term rewrite systems
    Bockmayr, A
    Werner, A
    CONDITIONAL AND TYPED REWRITING SYSTEMS, 1995, 968 : 51 - 70
  • [34] Uniqueness of Normal Forms for Shallow Term Rewrite Systems
    Radcliffe, Nicholas R.
    Moraes, Luis F. T.
    Verma, Rakesh M.
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2017, 18 (02)
  • [35] Inductively Sequential Term-Graph Rewrite Systems
    Echahed, Rachid
    GRAPH TRANSFORMATIONS, ICGT 2008, 2008, 5214 : 84 - 98
  • [36] Automated Amortised Resource Analysis for Term Rewrite Systems
    Moser, Georg
    Schneckenreither, Manuel
    FUNCTIONAL AND LOGIC PROGRAMMING, FLOPS 2018, 2018, 10818 : 214 - 229
  • [37] Autowrite: A Tool for Term Rewrite Systems and Tree Automata
    Durand, Irene
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 124 (02) : 29 - 49
  • [38] Confluence of shallow right-linear rewrite systems
    Godoy, G
    Tiwari, A
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2005, 3634 : 541 - 556
  • [40] Productivity of Non-Orthogonal Term Rewrite Systems
    Raffelsieper, Matthias
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (82): : 53 - 67