简介
编辑在计算机科学中,发生检查是句法统一算法的一部分。如果S包含V,它将导致一个变量V和一个结构S的统一失败。
在定理证明中的应用
编辑在定理证明中,没有发生检查的统一会导致不健全的推理。例如,Prolog的目标X=f(X){displaystyleX=f(X)}就会成功,将X绑定到一个循环上。作为另一个例子,在没有发生检查的情况下,一个解析证明会将X绑定到Herbrand宇宙中没有对应的循环结构上。
没有发生检查,就可以为非定理找到一个解析证明有理树统一Prolog的实现通常出于效率的考虑而省略了发生检查,这可能会导致循环数据结构和循环。由于不执行发生检查,统一一个术语的最坏情况下的复杂度为现代的实现,基于Colmerauer的PrologII。
使用有理树统一来避免循环。然而,在存在循环项的情况下,很难保持复杂性时间的线性。可以很容易地构建Colmerauer算法变得二次的例子,但也存在完善的建议。
统一(计算机科学)#中给出的统一算法的运行实例见图片,试图解决目标的统一算法然而,没有发生检查规则(在那里被命名为检查);应用消除规则反而导致最后一步的循环图(即一个无限的项)。
健全的统一
编辑ISOProlog实现有内置的谓词unify_with_occurs_check/2用于健全的统一,但是当统一被调用时,可以自由地使用不健全的甚至是循环的算法,只要该算法对所有不受发生检查(NSTO)的情况正确工作。
内置的acyclic_term/1用于检查术语的有限性。为所有统一提供健全统一的实现是Qu-Prolog和StrawberryProlog以及(可选择通过运行时标志)。XSB、SWI-Prolog、TauProlog和ScryerProlog。各种各样的优化可以使声音统一在普通情况下变得可行。
内容由匿名用户提供,本内容不代表vibaike.com立场,内容投诉举报请联系vibaike.com客服。如若转载,请注明出处:https://vibaike.com/170988/