A note on occur-check (extended report)

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.