Anti-unificación (ciencias de la computación)

El anti-unificación es el proceso de construir una generalización común a dos expresiones simbólicas dadas. Al igual que en la unificación, se distinguen varios marcos de trabajo dependiendo de qué expresiones (también llamadas términos) están permitidas y qué expresiones se consideran iguales. Si las variables que representan funciones están permitidas en una expresión, el proceso se llama "anti-unificación de orden superior", de lo contrario se lo llama "anti-unificación de primer orden". Si se requiere que la generalización tenga una instancia literalmente igual a cada expresión de entrada, el proceso se llama "anti-unificación sintáctica", de lo contrario "E-anti-unificación" o "teoría del módulo de anti-unificación".

Un algoritmo de anti-unificación debería calcular para las expresiones dadas un conjunto de generalización completo y mínimo, es decir, un conjunto que cubra todas las generalizaciones y que no contenga miembros redundantes, respectivamente. Dependiendo del marco de trabajo, un conjunto de generalización completo y mínimo puede tener uno, muchos, posiblemente infinitos miembros, o puede no existir en absoluto; no puede estar vacío, ya que existe una generalización trivial en cualquier caso. Para la anti-unificación sintáctica de primer orden, Gordon Plotkin​​ proporcionó un algoritmo que calcula un conjunto de generalización singleton completo y mínimo que contiene la llamada "generalización menos general" (least general generalization, LGG).

La anti-unificación no debe confundirse con la desunificación. Esto último significa el proceso de resolver sistemas de inecuaciones, es decir, encontrar valores para las variables de modo que se satisfagan todas las inecuaciones dadas.

Esta tarea es bastante diferente de encontrar generalizaciones.​

Prerrequisitos

Formalmente, un enfoque de antiunificación presupone:

• Un conjunto infinito V de variables. Para la antiunificación de orden superior, es conveniente elegir V disjunto del conjunto de variables vinculadas al término lambda.
• Un conjunto T de términos tales que V ⊆ T. Para la antiunificación de primer orden y de orden superior, T suele ser el conjunto de términos de primer orden (términos construidos a partir de símbolos de variables y funciones) y términos lambda (términos que contienen algunas variables de orden superior), respectivamente.
• Una relación de equivalencia $\equiv$ en $T$, indicando qué términos se consideran iguales. Para la antiunificación de orden superior, generalmente $t\equiv u$ Si $t$ y $u$ son alfa equivalentes . Para E-anti-unificación de primer orden, la operación $\equiv$ refleja el conocimiento previo sobre ciertos símbolos de función; por ejemplo, si $\oplus$ se considera conmutativo, $t\equiv u$ Si $u$ resulta de $t$ intercambiando los argumentos de $\oplus$ en algunas (posiblemente todas) ocurrencias. Si no hay ningún conocimiento de fondo (o previo), entonces solo los términos literal o sintácticamente idénticos se consideran iguales.

Referencias

• Datos: Q17003866