A note on occur-check (extended report)
Abstract
We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the occur-check never succeeds in any run of a nondeterministic unification algorithm. Here we show that "any run" can be weakened to "some run". We present some related sufficient conditions under which the occur-check may be safely omitted. We show examples for which the proposed approach provides more general results than the approaches based on well-moded and nicely moded programs (this includes cases to which the latter approaches are inapplicable). We additionally present a sufficient condition based on NSTO, working for arbitrary selection rules.
Cite
@article{arxiv.2204.05379,
title = {A note on occur-check (extended report)},
author = {Włodzimierz Drabent},
journal= {arXiv preprint arXiv:2204.05379},
year = {2025}
}
Comments
21 pages. Extended version of arXiv:2109.07914 in "Proceedings 37th ICLP (Technical Communications)". This version: corrections, extensions, simplifications