Abstract

In this paper we study decidable approximations to call by need computations to normal and root-stable forms in term rewriting. We obtain uniform decidability proofs by making use of elementary tree automata techniques. Surprisingly, by avoiding complicated concepts like index and sequentiality we are able to cover much larger classes of term rewriting systems.

BibTeX Entry

@inproceedings{DM-CADE97,
 author    = "Ir\`ene Durand and Aart Middeldorp",
 title     = "Decidable Call by Need Computations in Term Rewriting
              (Extended Abstract)",
 booktitle = "Proceedings of the 14th International Conference on Automated
              Deduction",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 1249,
 pages     = "4--18",
 year      = 1997,
 doi       = "10.1007/3-540-63104-6\_2"
}