SLD-resolution without occur-check, an example

TL;DR

This paper demonstrates that for certain logic programs, the occur-check in unification can be safely omitted without affecting correctness, simplifying Prolog execution.

Contribution

It proves occur-check can be skipped in specific cases and introduces an abstraction of unification without occur-check, expanding understanding of logic program execution.

Findings

The program is occur-check free for certain queries.

Prolog can execute some programs correctly without occur-check.

The paper introduces an abstraction of unification without occur-check.

Abstract

We prove that the occur-check is not needed for a certain definite clause logic program, independently from the selection rule. First we prove that the program is occur-check free. Then we consider a more general class of queries, under which the program is not occur-check free; however we show that it will be correctly executed under Prolog without occur-check. The main result of this report states that the occur-check may be skipped for the cases in which a single run of a standard nondeterministic unification algorithm does not fail due to the occur-check. The usual approaches are based on the notion of NSTO (not subject to occur-check), which considers all the runs. To formulate the result, it was necessary to introduce an abstraction of a "unification" algorithm without the occur-check.