Towards More Efficient Loop Checks

摘要

Loop checking is a mechanism for pruning infinite SLD derivations. Most loopchecks essentially compare the goals in a derivation: a derivation is pruned if sufficiently similar goals are detected. In theory a goal is usually compared with every previous goal in the derivation, but in practice such loop checks are too expensive. The alteration of such loop checks to obtain less expensive ones (notably such that the number of comparisons performed is linear in the number of goals generated) while retaining the soundness and completeness results of the original loop check is investigated. To this end, Van Gelder's tortoise and hare technique is modified and the number of comparisons performed by a loop check whose checkpoints are placed in accordance with the triangular numbers is studied in detail.