A Complete Selection Function for Lazy Conditional Narrowing
Taro Suzuki6
and Aart Middeldorp7 
| (6) |
Research Institute of Electrical Communication, Tohoku University, Sendai 980-8577, Japan |
| (7) |
Institute of Information Sciences and Electronics, University of Tsukuba, Tsukuba 305-8573, Japan |
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.
Acknowledgements Taro Suzuki is partially supported by the Grant-in-Aid for Encouragement of Young Scientist 11780204. Aart Middeldorp is partially
supported by the Grantin-Aids for Scientific Research B 12480066 and C(2) 11680338 of the Ministry of Education, Science,
Sports and Culture of Japan.
References secured to subscribers.