Abstract

We show the completeness of the lazy conditional narrowing calculus (LCNC) with leftmost selection for the class of deterministic conditional rewrite systems (CTRSs). Deterministic CTRSs permit extra variables in the right-hand sides and conditions of their rewrite rules. From the completeness proof we obtain several insights to make the calculus more deterministic. Furthermore, and similar to the refinements developed for the unconditional case, we succeeded in removing all nondeterminism due to the choice of the inference rule of LCNC by imposing further syntactic conditions on the participating CTRSs and restricting the set of solutions for which completeness needs to be established.

BibTeX Entry

@inproceedings{MM-PPDP04,
 author    = "Mircea Marin and Aart Middeldorp",
 title     = "New Completeness Results for Lazy Conditional Narrowing",
 booktitle = "Proceedings of the 6th ACM SIGPLAN Conference on
              Principles and Practice of Declarative Programming",
 pages     = "120--131",
 year      = 2004,
 doi       = "10.1145/1013963.1013979"
}