[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #3 (Solved !)

Originator: Deepak Kapur
Date: April 1991

Summary: What is the complexity of deciding ground-reducibility?

A term t is ground reducible with respect to a rewrite system R if all its ground (variable-free) instances contain a redex. Ground reducibility is decidable for ordinary rewriting (and finite R) [Com88, KNZ87, Pla85], but nⁿⁿ is the best known upper bound in general, 2^{d n logn} and 2^{c n/ logn} are the best upper and lower bounds, respectively, for left-linear systems, where n is the size of the system R and c,d are constants [KNZ87]. Can these bounds be improved?

Remark

Ground-reducibility is EXPTIME-complete [CJ97, CJ03].

References

[CJ97]

Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. In Glynn Winskel, editor, Twelfth Symposium on Logic in Computer Science, pages 26–34, Warsaw, Poland, June 1997. IEEE.

[CJ03]

Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. Information and Computation, 187(1):123–153, 2003.

[Com88]

Hubert Comon. Unification et Disunification: Théorie et Applications. PhD thesis, Institut National Polytechnique de Grenoble, 1988. In French.

[KNZ87]

Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395–415, August 1987.

[Pla85]

David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2/3):182–215, May/June 1985.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]