A Note on Occur-Check

TL;DR

This paper investigates conditions under which the occur-check in unification can be safely omitted, extending previous results and providing more general criteria than existing approaches based on program modes.

Contribution

It introduces weakened conditions for safely omitting the occur-check, broadening the applicability beyond well-moded and nicely moded programs.

Findings

Proposes less restrictive conditions for occur-check omission

Provides examples where the new approach applies but previous methods do not

Enhances understanding of safe unification in logic programming

Abstract

Most known results on avoiding the occur-check are based on the notion of "not subject to occur-check" (NSTO). It 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 this requirement is too strong. We show how to weaken it, and 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).