Abstract

This paper is concerned with the lazy conditional narrowing calculus LCNC. In an earlier paper we proved that this calculus is complete with respect to normalizable solutions for the class of confluent but not necessarily terminating conditional rewrite systems without so-called extra variables in the conditional parts of the rewrite rules. Unfortunately, the proof does not provide any useful complete selection function, hence in implementations we need to backtrack over the choice of equations in goals in order to guarantee that all solutions are enumerated. This is in contrast to the unconditional case where completeness with respect to the leftmost selection function is known. In this paper we close the gap by proving the completeness of LCNC with respect to the leftmost selection strategy for the above-mentioned class of conditional rewrite systems.

BibTeX Entry

@inproceedings{SM-FLOPS01,
 author      = "Taro Suzuki and Aart Middeldorp",
 title       = "A Complete Selection Function for Lazy Conditional
                Narrowing",
 booktitle   = "Proceedings of the 5th International Symposium on
                Functional and Logic Programming",
 series      = "Lecture Notes in Computer Science",
 volume      = 2024,
 pages       = "201--215",
 year        = 2001,
 doi         = "10.1007/3-540-44716-4\_13"
}