Se produce una comprobación

En informática , la comprobación de ocurrencias forma parte de los algoritmos de unificación sintáctica . Provoca que la unificación de una variable V y una estructura S falle si S contiene a V.

En la demostración de teoremas , la unificación sin la comprobación de ocurrencias puede conducir a una inferencia errónea . Por ejemplo, el objetivo de Prolog${\displaystyle X=f(X)}$ tendrá éxito, vinculando X a una estructura cíclica que no tiene contraparte en el universo de Herbrand . Como otro ejemplo, ^{[ 1 ]} sin verificación de ocurrencias, se puede encontrar una prueba de resolución para el no-teorema ^{[ 2 ].}${\displaystyle (\forall x\exists yp(x,y))\rightarrow (\exists y\forall xp(x,y))}$: la negación de esa fórmula tiene la forma normal conjuntiva${\displaystyle p(X,f(X))\land \lnot p(g(Y),Y)}$, con${\displaystyle f}$y${\displaystyle g}$que denotan la función de Skolem para el primer y segundo cuantificador existencial, respectivamente. Sin ocurre la comprobación, los literales${\displaystyle p(X,f(X))}$y${\displaystyle p(g(Y),Y)}$son unificables, produciendo la cláusula vacía refutatoria.

Las implementaciones de Prolog suelen omitir la comprobación de ocurrencias por razones de eficiencia, lo que puede conducir a estructuras de datos circulares y bucles. Al no realizar la comprobación de ocurrencias, la complejidad del peor caso de unificar un término ${\displaystyle t_{1}}$con término${\displaystyle t_{2}}$ se reduce en muchos casos de ${\displaystyle O({\text{tamaño}}(t_{1})+{\text{tamaño}}(t_{2}))}$ a ${\displaystyle O({\text{min}}({\text{tamaño}}(t_{1}),{\text{tamaño}}(t_{2})))}$; en el caso frecuente de unificación de términos variables, el tiempo de ejecución se reduce a ${\displaystyle O(1)}$. ^{[ nb 1 ]}

Las implementaciones, basadas en el Prolog II de Colmerauer, ^{[ 4 ] [ 5 ] [ 6 ] [ 7 ]} utilizan la unificación de árboles racionales para evitar bucles. Sin embargo, es difícil mantener la complejidad temporal lineal en presencia de términos cíclicos. Se pueden construir fácilmente ejemplos donde el algoritmo de Colmerauer se vuelve cuadrático ^{[ 8 ] .}

El trabajo de Jaffar de 1984 propuso un refinamiento basado en técnicas de unión-búsqueda, ^{[ 9 ]} reduciendo efectivamente la complejidad del peor caso a un tiempo casi lineal. Los sistemas modernos, incluidos SWI-Prolog, SICStus Prolog , Scryer Prolog y Ciao Prolog, parecen implementar variantes de este enfoque.

Consulte la imagen para ver un ejemplo de ejecución del algoritmo de unificación que se presenta en Unificación (informática)#Un algoritmo de unificación , que intenta resolver el objetivo.${\displaystyle cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))}$Sin embargo, sin la regla de verificación de ocurrencias (llamada "check" allí); aplicar la regla "eliminar" en su lugar conduce a un gráfico cíclico (es decir, un término infinito) en el último paso.

Las implementaciones de Prolog ISO tienen el predicado incorporado unify_with_occurs_check/2 para la unificación correcta, pero son libres de usar algoritmos incorrectos o incluso en bucle cuando se invoca la unificación de otra manera, siempre que el algoritmo funcione correctamente para todos los casos que "no están sujetos a la comprobación de ocurrencias" (NSTO). ^{[ 10 ]} El predicado incorporado acyclic_term/1 sirve para comprobar la finitud de los términos.

Las implementaciones que ofrecen una unificación sólida para todas las unificaciones son Qu-Prolog y Strawberry Prolog y (opcionalmente, mediante un indicador de tiempo de ejecución): XSB , SWI-Prolog , CxProlog , Tau Prolog , Trealla Prolog y Scryer Prolog . Una variedad ^{[ 11 ] [ 12 ]} de optimizaciones puede hacer factible la unificación sólida para casos comunes.

WP Weijland (1990). "Semántica para programas lógicos sin comprobación de ocurrencia" . Theoretical Computer Science . 71 : 155–174 . doi : 10.1016/0304-3975(90)90194-m .