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

共 10 条

[1]

DAUCHET M, 1987, 2ND P S LOG COMP SCI, P353

[2] VARIATIONS ON THE COMMON SUBEXPRESSION PROBLEM [J].

DOWNEY, PJ ;

SETHI, R ;

TARJAN, RE .

JOURNAL OF THE ACM, 1980, 27 (04) :758-771

[3]

Gallier J., 1988, 9th International Conference on Automated Deduction Proceedings, P182, DOI 10.1007/BFb0012832

[4]

Gecseg F., 1984, TREE AUTOMATA

[5]

HUET G, 1978, 283 TECH REP

[6]

HUET G, 1980, FORMAL LANGUAGE THEO, P349

[7] FAST DECISION PROCEDURES BASED ON CONGRUENCE CLOSURE [J].

NELSON, G ;

OPPEN, DC .

JOURNAL OF THE ACM, 1980, 27 (02) :356-364

[8] THE CHURCH-ROSSER PROPERTY FOR GROUND TERM-REWRITING SYSTEMS IS DECIDABLE [J].

OYAMAGUCHI, M .

THEORETICAL COMPUTER SCIENCE, 1987, 49 (01) :43-79

[9]

OYAMAGUCHI M, 1987, CHURCH ROSSER PROPER

[10]

SNYDER W, 1989, LECTURE NOTES COMP S

← 1 →