A note on occur-check (extended report)
W{\l}odzimierz Drabent

TL;DR
This paper weakens the conditions under which the occur-check can be safely omitted in logic programming, broadening the applicability of occur-check elimination beyond previous methods.
Contribution
It introduces a relaxed notion of NSTO, showing that some run suffices for safe occur-check omission, and provides new sufficient conditions applicable to arbitrary selection rules.
Findings
More general conditions for safe occur-check omission.
Examples surpassing well-moded and nicely moded approaches.
A new sufficient condition based on NSTO for arbitrary rules.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
