关于出现检查的注记

大多数关于避免出现检查（occur-check）的已知结果都基于“不受出现检查约束”（NSTO）这一概念。它意味着合一（unification）仅在这种原子对上执行：对于它们，在非确定性合一算法的任何运行中出现检查都不会成功。这里我们表明该要求过强。我们展示如何弱化它，并给出一些相关的充分条件，在这些条件下可以安全地省略出现检查。我们展示了若干例子，对所提方法比基于良模式（well-moded）和良模式（nicely moded）程序的方法给出更一般的结果（这包括后者方法不适用的情况）。