Antiunificación

Dado un conjunto${\displaystyle V}$de símbolos variables, un conjunto${\displaystyle C}$de símbolos y conjuntos constantes${\displaystyle F_{n}}$de${\displaystyle n}$símbolos de función -aria, también llamados símbolos de operador, para cada número natural${\displaystyle n\geq 1}$, el conjunto de términos (de primer orden no ordenados)${\displaystyle T}$se define recursivamente como el conjunto más pequeño con las siguientes propiedades: ^{[ 3 ]}

• cada símbolo de variable es un término: V ⊆ T ,
• cada símbolo constante es un término: C ⊆ T ,
• de cada n términos t ₁ ,..., t _n , y cada símbolo de función n -aria f ∈ F _n , un término mayor${\displaystyle f(t_{1},\ldots ,t_{n})}$se puede construir.

Por ejemplo, si x  ∈ V es un símbolo de variable, 1  ∈ C es un símbolo de constante y add  ∈ F ₂ es un símbolo de función binaria , entonces x  ∈ T , 1  ∈ T , y (por lo tanto) add( x ,1)  ∈ T según la primera, segunda y tercera regla de construcción de términos, respectivamente. El último término se suele escribir como x +1, utilizando la notación infija y el símbolo de operador más común + para mayor comodidad.

Una sustitución es una asignación ${\displaystyle \sigma :V\longrightarrow T}$de variables a términos; la notación${\displaystyle \{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}}$se refiere a una asignación de sustitución para cada variable${\displaystyle x_{i}}$al término${\displaystyle t_{i}}$, para${\displaystyle i=1,\ldots ,k}$y cada otra variable consigo misma. Aplicando esa sustitución a un término t se escribe en notación posfija como${\displaystyle t\{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}}$; significa reemplazar (simultáneamente) cada aparición de cada variable${\displaystyle x_{i}}$en el término t por${\displaystyle t_{i}}$El resultado t σ de aplicar una sustitución σ a un término t se llama instancia de ese término t . Como ejemplo de primer orden, aplicando la sustitución${\displaystyle \{x\mapsto h(a,y),z\mapsto b\}}$al término

Si un término${\displaystyle t}$tiene una instancia equivalente a un término${\displaystyle u}$, es decir, si${\displaystyle t\sigma \equiv u}$por alguna sustitución${\displaystyle \sigma }$, entonces${\displaystyle t}$se llama más general que${\displaystyle u}$, y${\displaystyle u}$se denomina más especial que, o subsumido por,${\displaystyle t}$. Por ejemplo,${\displaystyle x\oplus a}$es más general que${\displaystyle a\oplus b}$si${\displaystyle \oplus }$es conmutativa , puesto que entonces${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$.

Si${\displaystyle \equiv }$es la identidad literal (sintáctica) de los términos, un término puede ser a la vez más general y más especial que otro solo si ambos términos difieren únicamente en sus nombres de variables, no en su estructura sintáctica; tales términos se denominan variantes o renombramientos entre sí. Por ejemplo,${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$es una variante de${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$, desde${\displaystyle f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})}$y${\displaystyle f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1})}$. Sin embargo,${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$no es una variante de${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$, puesto que ninguna sustitución puede transformar el último término en el primero, aunque${\displaystyle \{x_{1}\mapsto x_{2},z_{1}\mapsto x_{2},y_{1}\mapsto x_{2}\}}$logra la dirección inversa. Por lo tanto, este último término es propiamente más especial que el primero.

Una sustitución${\displaystyle \sigma }$es más especial que, o está subsumido por, una sustitución${\displaystyle \tau }$si${\displaystyle x\sigma }$es más especial que${\displaystyle x\tau }$para cada variable${\displaystyle x}$. Por ejemplo,${\displaystyle \{x\mapsto f(u),y\mapsto f(f(u))\}}$es más especial que${\displaystyle \{x\mapsto z,y\mapsto f(z)\}}$, desde${\displaystyle f(u)}$y${\displaystyle f(f(u))}$es más especial que${\displaystyle z}$y${\displaystyle f(z)}$, respectivamente.

Un problema de anti-unificación es un par${\displaystyle \langle t_{1},t_{2}\rangle }$de términos. Un término${\displaystyle t}$es una generalización común , o antiunificador , de${\displaystyle t_{1}}$y${\displaystyle t_{2}}$si${\displaystyle t\sigma _{1}\equiv t_{1}}$y${\displaystyle t\sigma _{2}\equiv t_{2}}$para algunas sustituciones${\displaystyle \sigma _{1},\sigma _{2}}$. Para un problema de anti-unificación dado, un conjunto${\displaystyle S}$de antiunificadores se llama completo si cada generalización engloba algún término${\displaystyle t\in S}$; el conjunto${\displaystyle S}$Se denomina mínimo si ninguno de sus miembros engloba a otro.

• Una operación asociativa y conmutativa: Pottier, Loïc (febrero de 1989), Algorithmes de complétion et généralisation en logique du premier ordre (Thèse de doctorat); Pottier, Loïc (1989), Généralisation de termes en théorie équationelle – Cas associatif-commutatif , Informe INRIA, vol. 1056, INRIA 
• Teorías conmutativas: Baader, Franz (1991). "Unificación, unificación débil, límite superior, límite inferior y problemas de generalización" . Actas de la 4.ª Conferencia sobre Técnicas y Aplicaciones de Reescritura (RTA) . LNCS. Vol. 488. Springer. págs. 86–91 . doi : 10.1007/3-540-53904-2_88 .  
• Monoides libres: Biere, A. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF) , Univ. Karlsruhe, Alemania
• Clases regulares de congruencia: Heinz, Birgit (diciembre de 1995), Anti-Unifikation módulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung , GMD Berichte, vol. 261, TU Berlín, ISBN  978-3-486-23873-0; Burghardt, Jochen (2005). "E-Generalización mediante gramáticas". Inteligencia Artificial . 165 (1): 1– 35. arXiv : 1403.8118 . doi : 10.1016/j.artint.2005.01.008 . S2CID 5328240 . 
• Teorías A, C, AC y ACU con ordenamientos: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "Un algoritmo de generalización ecuacional modular ordenado" . Information and Computation . 235 : 98–136 . doi : 10.1016/j.ic.2014.01.006 . hdl : 2142/25871 .
• Teorías puramente idempotentes: Cerna, David; Kutsia, Temur (2020). "Anti-Unificación idempotente" . ACM Transactions on Computational Logic . 21 (2): 1– 32. doi : 10.1145/3359060 . hdl : 10.1145/3359060 . S2CID 207861304 . 

• Clasificación taxonómica: Frisch, Alan M.; Page, David (1990). "Generalización con información taxonómica". AAAI : 755–761 .; Frisch, Alan M.; Page Jr., C. David (1991). "Generalizando átomos en lógica de restricciones" . Actas de la Conferencia sobre Representación del Conocimiento .; Frisch, AM; Page, CD (1995). "Construyendo teorías en instanciación". En Mellish, CS (ed.). Proc. 14th IJCAI . Morgan Kaufmann. pp. 1210– 1216. CiteSeerX 10.1.1.32.1610 .  
• Términos característicos: Plaza, E. (1995). "Casos como términos: Un enfoque de términos característicos para la representación estructurada de casos". Actas de la 1.ª Conferencia Internacional sobre Razonamiento Basado en Casos (ICCBR) . LNCS. Vol. 1010. Springer. págs. 265–276 . ISSN 0302-9743 .   
• Idestam-Almquist, Peter (junio de 1993). "Generalización bajo implicación por anti-unificación recursiva" . Actas de la 10.ª Conferencia sobre Aprendizaje Automático . Morgan Kaufmann. págs. 151–158 . 
• Fischer, Cornelia (mayo de 1994), PAntUDE – Un algoritmo anti-unificación para expresar generalizaciones refinadas (PDF) , Informe de investigación, vol.  TM-94-04, DFKI
• Teorías A, C, AC y ACU con clasificaciones ordenadas: véase más arriba.

• Baumgartner, Alejandro; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (junio de 2013). Antiunificación nominal . Proc. ACR 2015. vol. 36 de LIPIcs. Castillo Dagstuhl, 57-73. Software.

• Análisis del programa:
  • Bulychev, Peter; Minea, Marius (2008). "Detección de código duplicado mediante anti-unificación" . Actas del Coloquio de Jóvenes Investigadores de Primavera/Verano sobre Ingeniería de Software (2).;
  • Bulychev, Peter E.; Kostylev, Egor V.; Zakharov, Vladimir A. (2009). «Algoritmos anti-unificación y sus aplicaciones en el análisis de programas» . En Amir Pnueli, Irina Virbitskaite y Andrei Voronkov (eds.). Perspectivas de la informática de sistemas (PSI) – 7.ª Conferencia Internacional en Memoria de Andrei Ershov . LNCS. Vol.  5947. Springer. pp. 413–423 . doi : 10.1007/978-3-642-11486-1_35 . ISBN  978-3-642-11485-4.
• Factorización de código:
  • Cottrell, Rylan (septiembre de 2008), Semiautomatización de la reutilización de código fuente a pequeña escala mediante correspondencia estructural (PDF) , Univ. Calgary
• Prueba de inducción:
  • Heinz, Birgit (1994), Descubrimiento de lemas mediante la antiunificación de tipos regulares , Informe técnico, vol. 94–21 , TU Berlín 
• Extracción de información:
  • Thomas, Bernd (1999). "Aprendizaje basado en anti-unificación de T-Wrappers para la extracción de información" (PDF) . Informe técnico de la AAAI . WS-99-11: 15–20 .
• Razonamiento basado en casos:
  • Armengol; Plaza, Enric (2005). "Uso de descripciones simbólicas para explicar la similitud en {CBR}" . En Beatriz López y Joaquim Meléndez y Petia Radeva y Jordi Vitrià (ed.). Investigación y Desarrollo de Inteligencia Artificial, Proc. 8vo Int. Conf. de la ACIA, CCIA . Prensa IOS. págs. 239-246 . 
• Síntesis de programas: La idea de generalizar términos con respecto a una teoría ecuacional se remonta a Manna y Waldinger (1978, 1980), quienes deseaban aplicarla en la síntesis de programas . En la sección "Generalización", sugieren (en la página  119 del artículo de 1980) generalizar reverse ( l ) y reverse ( tail ( l ))<>[ head ( l )] para obtener reverse(l')<>m' . Esta generalización solo es posible si se considera la ecuación de fondo u <>[]= u .
  • Zohar Manna ; Richard Waldinger (dic. 1978). Un enfoque deductivo para la síntesis de programas (PDF) (Nota técnica). SRI International . Archivado del original (PDF) el 27 de febrero de 2017. Consultado el 29 de septiembre de 2017 .— preimpresión del artículo de 1980
  • Zohar Manna y Richard Waldinger (enero de 1980). "Un enfoque deductivo para la síntesis de programas". ACM Transactions on Programming Languages ​​and Systems . 2 : 90–121 . doi : 10.1145/357084.357090 . S2CID 14770735 . 
• Procesamiento del lenguaje natural:
  • Amiridze, Nino; Kutsia, Temur (mayo de 2018). Anti-Unificación y procesamiento del lenguaje natural (EasyChair Preprints). Vol.  203. doi : 10.29007/fkrh . S2CID 49322739 .