On prolog and the occur check problem

Abstract

It is well-known that omission of the occur check in unification leads to unsound Prolog systems. Nevertheless, most Prolog systems omit the occur check because this makes unification much faster and unsoundness allegedly seldom manifests itself. We revisit the occur check problem and point to two aspects that have previously received no attention. Firstly, “unification without the occur check” is ambiguous, and in practice, Prolog systems vary markedly in their reaction to programs having occur check problems. Secondly, even very simple program transformations are unsafe for pure Prolog when the occur check is omitted. We conclude that the occur check problem is important, and in particular..