Anti-unificación

Generalización lógica para expresiones simbólicas

La antiunificación es el proceso de construcción de una generalización común a dos expresiones simbólicas dadas. Al igual que en la unificación , se distinguen varios marcos de trabajo en función de qué expresiones (también llamadas términos) se permiten y qué expresiones se consideran iguales. Si se permiten variables que representan funciones en una expresión, el proceso se denomina "antiunificación de orden superior"; en caso contrario, "antiunificació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 denomina "antiunificación sintáctica"; en caso contrario, "antiunificación E" o "teoría de antiunificación módulo".

Un algoritmo de antiunificación debería calcular para expresiones dadas un conjunto de generalización completo y mínimo, es decir, un conjunto que cubra todas las generalizaciones y no contenga miembros redundantes, respectivamente. Dependiendo del marco, un conjunto de generalización completo y mínimo puede tener uno, un número finito o posiblemente un número infinito de miembros, o puede no existir en absoluto; ^{[nota 1]} no puede estar vacío, ya que en cualquier caso existe una generalización trivial. Para la antiunificación sintáctica de primer orden, Gordon Plotkin ^{[1] [2]} proporcionó un algoritmo que calcula un conjunto de generalización singleton completo y mínimo que contiene la denominada "generalización menos general" (lgg).

La antiunificación no debe confundirse con la desunificación . Esta última hace referencia al proceso de resolver sistemas de inecuaciones , es decir, de encontrar valores para las variables de modo que se satisfagan todas las inecuaciones dadas. ^{[nota 2]} Esta tarea es bastante diferente de la de encontrar generalizaciones.

Prerrequisitos

Formalmente, un enfoque antiunificación presupone

• Un conjunto infinito V de variables . Para una antiunificación de orden superior, es conveniente elegir V disjunto del conjunto de variables ligadas 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.
• Relación de equivalencia en , que indica qué términos se consideran iguales. Para la antiunificación de orden superior, normalmente si y son alfa equivalentes . Para la E-antiunificación de primer orden, refleja el conocimiento previo sobre ciertos símbolos de función; por ejemplo, si se considera conmutativo, si resulta de al intercambiar los argumentos de en algunas ocurrencias (posiblemente todas). ^{[nota 3]} Si no hay ningún conocimiento previo, entonces solo los términos idénticos literal o sintácticamente se consideran iguales. ${\displaystyle \equiv }$ ${\displaystyle T}$ ${\displaystyle t\equiv u}$ ${\displaystyle t}$ ${\displaystyle u}$ ${\displaystyle \equiv }$ ${\displaystyle \oplus }$ ${\displaystyle t\equiv u}$ ${\displaystyle u}$ ${\displaystyle t}$ ${\displaystyle \oplus }$

Término de primer orden

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

• Cada símbolo 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 , se puede construir un término mayor . ${\displaystyle f(t_{1},\ldots ,t_{n})}$

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 por la primera, segunda y tercera regla de construcción de términos, respectivamente. El último término generalmente se escribe como x +1, utilizando la notación infija y el símbolo de operador más común + para mayor comodidad.

Término de orden superior

Sustitución

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

Generalización, especialización

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

Si es identidad literal (sintáctica) de 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 solo en sus nombres de variable, no en su estructura sintáctica; tales términos se llaman variantes o renombramientos entre sí. Por ejemplo, es una variante de , ya que y . Sin embargo, no es una variante de , ya que ninguna sustitución puede transformar el último término en el primero, aunque logre la dirección inversa. El último término es, por lo tanto, propiamente más especial que el primero. ${\displaystyle \equiv }$ ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$ ${\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})}$ ${\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})}$ ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ ${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$ ${\displaystyle \{x_{1}\mapsto x_{2},z_{1}\mapsto x_{2},y_{1}\mapsto x_{2}\}}$

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

Problema de antiunificación, conjunto de generalizaciones

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

Antiunificación sintáctica de primer orden

El marco de la antiunificación sintáctica de primer orden se basa en ser el conjunto de términos de primer orden (sobre un conjunto dado de variables, de constantes y de símbolos de funciones -arias) y en ser igualdad sintáctica . En este marco, cada problema de antiunificación tiene un conjunto de soluciones único , completo y obviamente mínimo . Su miembro se llama generalización general mínima (lgm) del problema, tiene una instancia sintácticamente igual a y otra sintácticamente igual a . Cualquier generalización común de y subsume . La lgm es única hasta variantes: si y son conjuntos de soluciones completos y mínimos del mismo problema de antiunificación sintáctica, entonces y para algunos términos y , que son renombramientos entre sí. ${\displaystyle T}$ ${\displaystyle V}$ ${\displaystyle C}$ ${\displaystyle F_{n}}$ ${\displaystyle n}$ ${\displaystyle \equiv }$ ${\displaystyle \langle t_{1},t_{2}\rangle }$ ${\displaystyle \{t\}}$ ${\displaystyle t}$ ${\displaystyle t_{1}}$ ${\displaystyle t_{2}}$ ${\displaystyle t_{1}}$ ${\displaystyle t_{2}}$ ${\displaystyle t}$ ${\displaystyle S_{1}}$ ${\displaystyle S_{2}}$ ${\displaystyle S_{1}=\{s_{1}\}}$ ${\displaystyle S_{2}=\{s_{2}\}}$ ${\displaystyle s_{1}}$ ${\displaystyle s_{2}}$

Plotkin ^{[1] [2]} ha dado un algoritmo para calcular el lgg de dos términos dados. Presupone una aplicación inyectiva , es decir, una aplicación que asigna a cada par de términos una variable propia , de modo que no haya dos pares que compartan la misma variable. ^{[nota 4]} El algoritmo consta de dos reglas: ${\displaystyle \phi :T\times T\longrightarrow V}$ ${\displaystyle s,t}$ ${\displaystyle \phi (s,t)}$

Por ejemplo, esta generalización menos general refleja la propiedad común de ambas entradas de ser números cuadrados. ${\displaystyle (0*0)\sqcup (4*4)\rightsquigarrow (0\sqcup 4)*(0\sqcup 4)\rightsquigarrow \phi (0,4)*\phi (0,4)\rightsquigarrow x*x}$

Plotkin utilizó su algoritmo para calcular la " generalización mínima relativa (rlgg) " de dos conjuntos de cláusulas en lógica de primer orden, que fue la base del enfoque Golem para la programación lógica inductiva .

Teoría del módulo antiunificación de primer orden

• Jacobsen, Erik (junio de 1991), Unificación y antiunificación (PDF) , Informe técnico
• Østvold, Bjarte M. (abril de 2004), Una reconstrucción funcional de la antiunificación (PDF) , Nota NR, vol. DART/04/04, Centro Noruego de Computación
• Boytcheva, Svetla; Markov, Zdravko (2002). "Un algoritmo para inducir la mínima generalización bajo implicación relativa". Proc. FLAIRS-02 . AAAI. págs. 322–326.
• Kutsia, Temur; Levy, Jordi; Villaret, Mateu (2014). "Anti-unificación para términos no clasificados y coberturas" (PDF) . Journal of Automated Reasoning . 52 (2): 155–190. doi : 10.1007/s10817-013-9285-6 .Software.

Teorías ecuacionales

• Una operación asociativa y conmutativa: Pottier, Loic (febrero de 1989), Algorithms des complete et generalization en logic du premier ordre (These de doctorat); Pottier, Loic (1989), Generalización de términos en teoría ecuación – 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 ordenados: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "Un algoritmo de generalización ecuacional modular ordenado por orden". Información y Computación . 235 : 98–136. doi : 10.1016/j.ic.2014.01.006 . hdl : 2142/25871 .
• Teorías puramente idempotentes: Cerna, David; Kutsia, Temur (2020). "Antiunificación idempotente". ACM Transactions on Computational Logic . 21 (2): 1–32. doi :10.1145/3359060. hdl :10.1145/3359060. S2CID  207861304.

Antiunificación ordenada de primer orden

• Tipos taxonómicos: Frisch, Alan M.; Page, David (1990). "Generalización con información taxonómica". AAAI : 755–761.; Frisch, Alan M.; Page Jr., C. David (1991). "Generalización de átomos en lógica de restricciones". Proc. Conf. 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. págs. 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". Proc. 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 antiunificació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 antiunificación para expresar generalizaciones refinadas (PDF) , Informe de investigación, vol. TM-94-04, DFKI
• Teorías A, C, AC, ACU con ordenamientos ordenados: ver arriba

Antiunificación nominal

• 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.

Aplicaciones

• Análisis del programa:
  • Bulychev, Peter; Minea, Marius (2008). "Detección de código duplicado mediante antiunificación". Actas del Coloquio de primavera/verano para jóvenes investigadores sobre ingeniería de software (2).;
  • Bulychev, Peter E.; Kostylev, Egor V.; Zakharov, Vladimir A. (2009). "Algoritmos antiunificación y sus aplicaciones en el análisis de programas". En Amir Pnueli e Irina Virbitskaite y Andrei Voronkov (ed.). Perspectivas de la informática de sistemas (PSI) – 7.ª conferencia internacional en memoria de Andrei Ershov . LNCS. Vol. 5947. Springer. págs. 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 antiunificación de clases regulares , Informe técnico, vol. 94-21, TU Berlin
• Extracción de información:
  • Thomas, Bernd (1999). "Aprendizaje basado en antiunificación de envoltorios T para 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ág. 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 (diciembre de 1978). Un enfoque deductivo para la síntesis de programas (PDF) (Nota técnica). SRI International . Archivado desde el 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 (2018). "Anti-Unificación y procesamiento del lenguaje natural". Quinto taller sobre lenguaje natural y ciencias de la computación, NLCS'18 . Preimpresiones de EasyChair. Informe EasyChair n.º 203. doi : 10.29007/fkrh . S2CID  49322739.

Antiunificación de orden superior

• Cálculo de construcciones:
  • Pfenning, Frank (julio de 1991). "Unificación y antiunificación en el cálculo de construcciones" (PDF) . Proc. 6th LICS . Springer. págs. 74–85.
• Cálculo lambda de tipos simples (entrada: términos en la forma eta-larga beta-normal. Salida: patrones de orden superior):
  • Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (junio de 2013). Una variante de la antiunificación de orden superior. Proc. RTA 2013. Vol. 21 de LIPIcs. Schloss Dagstuhl, 113-127. Software.
• Cálculo lambda de tipos simples (Entrada: Términos en la forma eta-long beta-normal. Salida: Varios fragmentos del cálculo lambda de tipos simples, incluidos patrones):
  • Cerna, David; Kutsia, Temur (junio de 2019). "Un marco genérico para generalizaciones de orden superior" (PDF) . 4ta Conferencia Internacional sobre Estructuras Formales para Computación y Deducción, FSCD, 24 al 30 de junio de 2019, Dortmund, Alemania . Schloss Dagstuhl - Leibniz-Zentrum für Informatik. págs. 74–85.
• Sustituciones restringidas de orden superior:
  • Wagner, Ulrich (abril de 2002), Antiunificación de orden superior restringida combinatoriamente , TU Berlin; Schmidt, Martin (septiembre de 2010), Antiunificación restringida de orden superior para proyección de teoría impulsada por heurística (PDF) , PICS-Report, vol. 31–2010, Univ. Osnabrück, Alemania, ISSN  1610-5389

Notas

1. Siempre existen conjuntos de generalización completos, pero puede darse el caso de que cada conjunto de generalización completo no sea mínimo.
2. Comon se refirió en 1986 a la resolución de inecuaciones como "antiunificación", lo que hoy en día se ha vuelto bastante inusual. Comon, Hubert (1986). "Completitud suficiente, sistemas de reescritura de términos y 'antiunificación'". Proc. 8ª Conferencia Internacional sobre Deducción Automatizada . LNCS. Vol. 230. Springer. págs. 128–140.
3. Por ejemplo ${\displaystyle a\oplus (b\oplus f(x))\equiv a\oplus (f(x)\oplus b)\equiv (b\oplus f(x))\oplus a\equiv (f(x)\oplus b)\oplus a}$
4. Desde un punto de vista teórico, tal mapeo existe, ya que tanto como son conjuntos infinitos contables ; para fines prácticos, se pueden construir según sea necesario, recordando los mapeos asignados en una tabla hash . ${\displaystyle V}$ ${\displaystyle T\times T}$ ${\displaystyle \phi }$ ${\displaystyle \langle s,t,\phi (s,t)\rangle }$

Referencias

1. Plotkin, Gordon D. (1970). Meltzer, B.; Michie, D. (eds.). "Una nota sobre generalización inductiva". Inteligencia artificial . 5 : 153–163.
2. Plotkin, Gordon D. (1971). Meltzer, B.; Michie, D. (eds.). "Una nota adicional sobre la generalización inductiva". Inteligencia artificial . 6 : 101–124.
3. CC Chang; H. Jerome Keisler (1977). A. Heyting; HJ Keisler; A. Mostowski; A. Robinson; P. Suppes (eds.). Teoría de modelos . Estudios de lógica y fundamentos de las matemáticas. Vol. 73. Holanda Septentrional.; aquí: Sec.1.3