Anti-unificació (ciències de la computació)

El anti-unificació és el procés de construir una generalisació comuna a dos expressions simbòliques donades. De la mateixa manera que en l'unificació, es distinguixen varis marcs de treball depenent de quines expressions (també cridades térmens) estan permeses i quines expressions es consideren iguals. Si les variables que representen funcions estan permeses en una expressió, el procés es diu "anti-unificació d'orde superior", de lo contrari li'l crida "anti-unificació de primer orde". Si es requerix que la generalisació tinga una instància lliteralment igual a cada expressió d'entrada, el procés es diu "anti-unificació sintàctica", de lo contrari "I-anti-unificació" o "teoria del mòdul de anti-unificació".

Un algoritme de anti-unificació deuria calcular per a les expressions donades un conjunt de generalisació complet i mínim, és dir, un conjunt que cobrixca totes les generalisacions i que no continga membres redundantes, respectivament. Depenent del marc de treball, un conjunt de generalisació complet i mínim pot tindre un, molts, possiblement infinits membres, o pot no existir en absolut; no pot estar buit, ya que existix una generalisació trivial en qualsevol cas. Per a la anti-unificació sintàctica de primer orde, Gordon Plotkin va proporcionar un algoritme que calcula un conjunt de generalisació singleton complet i mínim que conté la cridada "generalisació menys general" (least general generalization, LGG).

La anti-unificació no deu confondre's en la desunificación. Açò últim significa el procés de resoldre sistemes d'inecuaciones, és dir, trobar valors per a les variables de modo que se satisfacen totes les inecuaciones donades.

Esta tasca és prou diferent de trobar generalisacions.

Prerrequisitos

Formalment, un enfocament de antiunificación presupon:

• Un conjunt infinit V de variables. Per a la antiunificación d'orde superior, és convenient elegir V disjunto del conjunt de variables vinculades al terme lambda.

Un conjunt T de térmens tals que V ⊆ T. Per a la antiunificación de primer orde i d'orde superior, T sol ser el conjunt de térmens de primer orde (térmens construïts a partir de símbols de variables i funcions) i térmens lambda (térmens que contenen algunes variables d'orde superior), respectivament.

• Una relació d'equivalència $\equiv$ en $T$, indicant qué térmens es consideren iguals. Per a la antiunificación d'orde superior, generalment $t\equiv u$ Si $t$ i $u$ són alfa equivalents . Para I-anti-unificació de primer orde, l'operació $\equiv$ reflectix el coneiximent previ sobre certs símbols de funció; per eixemple, si $\oplus$ es considera conmutativo, $t\equiv u$ Si $u$ resulta de $t$ intercanviant els arguments de $\oplus$ en algunes (possiblement totes) ocurrències. Si no hi ha cap coneiximent de fondo (o previ), llavors solament els térmens lliteral o sintácticamente idèntics es consideren iguals.