La 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 dependiendo de qué expresiones (también llamadas términos) están permitidas y qué expresiones se consideran iguales. Si se permiten variables que representan funciones en una expresión, el proceso se denomina "anti-unificación de orden superior", de lo contrario "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 anti-unificación".
Un algoritmo anti-unificación debería calcular para expresiones dadas un conjunto de generalización mínimo y completo, es decir, un conjunto que cubra todas las generalizaciones y que no contenga miembros redundantes, respectivamente. Dependiendo del marco, un conjunto de generalización mínimo y completo puede tener uno, un número finito o posiblemente un número infinito de miembros, o puede que no exista en absoluto; [nota 1] 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 [1] [2] proporcionó un algoritmo que calcula un conjunto completo y mínimo de generalización singleton que contiene la llamada "generalización mínima general" (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. [nota 2] Esta tarea es bastante diferente a encontrar generalizaciones.
Prerrequisitos
Formalmente, un enfoque anti-unificación presupone
- Un conjunto infinito V de variables . Para anti-unificación de orden superior, es conveniente elegir V disjoint del conjunto de variables enlazadas de término lambda .
- Un conjunto T de términos tales que V ⊆ T . Para anti-unificació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 función y variable) y términos lambda (términos que contienen algunas variables de orden superior), respectivamente.
- Una relación de equivalencia en , indicando qué términos se consideran iguales. Para anti-unificación de orden superior, generalmente Si y son equivalentes alfa . Para E-anti-unificación de primer orden,refleja el conocimiento previo sobre ciertos símbolos de función; por ejemplo, si se considera conmutativo, Si resultados de intercambiando los argumentos de en algunas (posiblemente todas) ocurrencias. [nota 3] Si no hay ningún conocimiento previo, entonces sólo literal o sintácticamente, los términos idénticos se consideran iguales.
Término de primer orden
Dado un conjunto de símbolos variables, un conjunto de símbolos y conjuntos constantes de -símbolos de función de orden, también llamados símbolos de operador, para cada número natural , el conjunto de términos (de primer orden sin clasificar) se define de forma recursiva como el conjunto más pequeño con las siguientes propiedades: [3]
- cada símbolo de variable es un término: V ⊆ T ,
- todo símbolo constante es un término: C ⊆ T ,
- de cada n términos t 1 ,…, t n , y cada símbolo de función n -aria f ∈ F n , un término mayor se puede construir.
Por ejemplo, si x ∈ V es un símbolo de variable, 1 ∈ C es un símbolo constante, y suma ∈ F 2 es un símbolo de función binaria, entonces x ∈ T , 1 ∈ T , y (por lo tanto) suma ( x , 1) ∈ T por la regla de construcción del primer, segundo y tercer término, respectivamente. El último término generalmente se escribe como x +1, usando notación Infix y el símbolo de operador más común + por conveniencia.
Término de orden superior
Sustitución
Una sustitución es un mapeode variables a términos; la notación se refiere a un mapeo de sustitución de cada variable al término , por y cualquier otra variable a sí misma. La aplicación de esa sustitución a un término t se escribe en notación postfija como; significa (simultáneamente) reemplazar cada ocurrencia de cada variableen el término t por. El resultado tσ de aplicar una sustitución σ a un término t se denomina instancia de ese término t . Como ejemplo de primer orden, aplicando la sustitución al término
f ( X , a , g ( z ), y ) rendimientos f ( h ( a , y ) , a , g ( B ), y ) .
Generalización, especialización
Si un término tiene una instancia equivalente a un término , es decir, si por alguna sustitución , luego se llama más general que, y se llama más especial que, o subsumido por,. Por ejemplo, es más general que Si es conmutativa , desde entonces.
Si es una identidad literal (sintáctica) de términos, un término puede ser 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; estos términos se denominan variantes o renombramientos entre sí. Por ejemplo, es una variante de , desde y . Sin emabargo,no es una variante de, ya que ninguna sustitución puede transformar el último término en el primero, aunque logra la dirección inversa. El último término es, por tanto, propiamente más especial que el anterior.
Una sustitución es más especial que, o subsumido por, una sustitución Si es mas especial que para cada variable . Por ejemplo, es mas especial que , desde y es mas especial que y , respectivamente.
Problema de anti-unificación, conjunto de generalización
Un problema anti-unificación es un parde términos. Un términoes una generalización común , o anti-unificadora , de y Si y para algunas sustituciones . Para un problema de anti-unificación dado, un conjuntode anti-unificadores se llama completo si cada generalización subsume algún término; el conjuntose llama mínimo si ninguno de sus miembros subsume a otro.
Anti-unificación sintáctica de primer orden
El marco de la anti-unificación sintáctica de primer orden se basa en siendo el conjunto de términos de primer orden (sobre un conjunto dado de variables, de constantes y de -símbolos de función de reenvío) y en siendo igualdad sintáctica . En este marco, cada problema anti-unificacióntiene un conjunto de soluciones singleton completo y, obviamente, mínimo. Su miembrose llama la generalización mínima (lgg) del problema, tiene una instancia sintácticamente igual a y otro sintácticamente igual a . Cualquier generalización común de y subsume . El LGG es único hasta variantes: si y son conjuntos de soluciones completos y mínimos del mismo problema sintáctico anti-unificación, entonces y por algunos términos y , que son renombramientos el uno del otro.
Plotkin [1] [2] ha proporcionado un algoritmo para calcular el lgg de dos términos dados. Presupone un mapeo inyectivo , es decir, un mapeo 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:
si la regla anterior no aplica
Por ejemplo, ; esta generalización mínima refleja la propiedad común de ambas entradas de ser números cuadrados.
Plotkin usó su algoritmo para calcular la " generalización mínima relativa (rlgg) " de dos conjuntos de cláusulas en lógica de primer orden, que era la base del enfoque de Golem para la programación lógica inductiva .
Teoría del módulo anti-unificación de primer orden
- Jacobsen, Erik (junio de 1991), Unificación y anti-unificación (PDF) , Informe técnico
- Østvold, Bjarte M. (abril de 2004), A Functional Reconstruction of Anti-Unification (PDF) , NR Note, DART / 04/04, Norwegian Computing Center
- Boytcheva, Svetla; Markov, Zdravko (2002). "Un algoritmo para inducir la menor generalización bajo implicación relativa" (PDF) . Cite journal requiere
|journal=
( ayuda ) - Kutsia, Temur; Levy, Jordi; Villaret, Mateu (2014). "Anti-unificación para términos y coberturas no clasificados" (PDF) . Revista de razonamiento automatizado . 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; Pottier, Loic (1989), Generalization de termes en theorie ecuación, Cas associatif-commutatif , Informe INRIA, 1056 , INRIA
- Teorías conmutativas: Baader, Franz (1991). "Problemas de unificación, unificación débil, límite superior, límite inferior y generalización". Proc. 4ta Conf. sobre técnicas y aplicaciones de reescritura (RTA) . LNCS. 488 . Saltador. págs. 86–91.
- Monoides libres: Biere, A. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF) , Univ. Karlsruhe, alemania
- Clases de congruencia regulares: Heinz, Birgit (diciembre de 1995), Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung , GMD Berichte, 261 , TU Berlin, ISBN 978-3-486-23873-0; Burghardt, Jochen (2005). "E-Generalización utilizando gramáticas". Inteligencia artificial . 165 (1): 1–35. arXiv : 1403.8118 . doi : 10.1016 / j.artint.2005.01.008 .
- Teorías A, C, AC, ACU con clases ordenadas: Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José (2014). "Un algoritmo de generalización de ecuaciones ordenadas por orden modular" (PDF) . Información y Computación . 235 : 98-136. doi : 10.1016 / j.ic.2014.01.006 . hdl : 2142/25871 .
- Teorías puramente ideológicas: Cerna, David; Kutsia, Temur (2019). "Anti-Unificación Idempotente" . Transacciones ACM en lógica computacional . 21 (2). hdl : 10.1145 / 3359060 .
Anti-unificación ordenada de primer orden
- Clases taxonómicas: 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 restricción" . Proc. Conf. sobre Representación del Conocimiento .; Frisch, AM; Page, CD (1995). "Construyendo teorías en instanciación". En Mellish, CS (ed.). Proc. 14º IJCAI . Morgan Kaufmann. págs. 1210–1216.
- Términos de la característica: Plaza, E. (1995). "Casos como términos: un enfoque de término característico para la representación estructurada de casos". Proc. I Congreso Internacional de Razonamiento Basado en Casos (ICCBR) . LNCS. 1010 . Saltador. págs. 265-276. ISSN 0302-9743 .
- Idestam-Almquist, Peter (junio de 1993). "Generalización bajo implicación por anti-unificación recursiva" . Proc. 10ª Conf. 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 , Informe de investigación, TM-94-04, DFKI
- Teorías A, C, AC, ACU con clases ordenadas: ver arriba
Anti-unificación nominal
- Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (junio de 2013). Anti-Unificación nominal . Proc. RTA 2015. Vol. 36 de LIPIcs. Schloss Dagstuhl, 57-73. Software.
Aplicaciones
- Análisis del programa: Bulychev, Peter; Minea, Marius (2008). "Detección de código duplicado mediante Anti-Unificación" . Cite journal requiere
|journal=
( ayuda ); Bulychev, Peter E .; Kostylev, Egor V .; Zakharov, Vladimir A. (2009). "Algoritmos anti-unificación y sus aplicaciones en el análisis de programas". Cite journal requiere|journal=
( ayuda ) - Factorización de código: Cottrell, Rylan (septiembre de 2008), Reutilización de código fuente a pequeña escala semiautomatizada mediante correspondencia estructural (PDF) , Univ. Calgary
- Demostración por inducción: Heinz, Birgit (1994), Lemma Discovery by Anti-Unification of Regular Sorts , Technical Report, 94-21, TU Berlín
- Extracción de información: Thomas, Bernd (1999). "Aprendizaje basado en anti-unificación de T-Wrappers para extracción de información" (PDF) . Informe técnico AAAI . WS-99-11: 15-20.
- Razonamiento basado en casos: Armengol, Eva; Plaza, Enric (2005). "Uso de descripciones simbólicas para explicar la similitud en CBR" (PDF) . Cite journal requiere
|journal=
( ayuda ) - 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. 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 de la síntesis del programa (PDF) (Nota técnica). SRI Internacional . - preimpresión del artículo de 1980
- Zohar Manna y Richard Waldinger (enero de 1980). "Un enfoque deductivo de la síntesis del programa". Transacciones ACM sobre lenguajes y sistemas de programación . 2 : 90-121. doi : 10.1145 / 357084.357090 .
Anti-unificación de orden superior
- Cálculo de construcciones: Pfenning, Frank (julio de 1991). "Unificación y anti-unificación en el cálculo de las construcciones" (PDF) . Proc. 6º LICS . Saltador. págs. 74–85.
- Cálculo lambda de tipo simple (Entrada: términos en la forma beta-normal eta-long. Salida: patrones de orden superior): Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (junio de 2013). Una variante de anti-unificación de orden superior . Proc. RTA 2013. Vol. 21 de LIPIcs. Schloss Dagstuhl, 113-127. Software.
- Cálculo lambda de tipo simple (entrada: términos en la forma beta-normal eta-long. Salida: varios fragmentos del cálculo lambda de tipo simple, 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), Anti-unificación de orden superior restringido combinatoriamente , TU Berlín; Schmidt, Martin (septiembre de 2010), Anti-unificación de orden superior restringido para la proyección de la teoría impulsada por heurística (PDF) , Informe PICS, 31-2010, Univ. Osnabrück, Alemania, ISSN 1610-5389
Notas
- ^ Siempre existen conjuntos completos de generalización, pero puede darse el caso de que cada conjunto completo de generalizaciones no sea mínimo.
- ↑ Comon se refirió en 1986 a la resolución de desigualdades como "anti-unificación", lo que hoy en día se ha vuelto bastante inusual. Comon, Hubert (1986). "Completitud suficiente, sistemas de reescritura de términos y 'anti-unificación ' ". Proc. VIII Congreso Internacional de Deducción Automatizada . LNCS. 230 . Saltador. págs. 128–140.
- ^ Por ejemplo
- ^ Desde un punto de vista teórico, tal mapeo existe, ya que tanto y son conjuntos infinitos contables ; para fines prácticos, se puede construir según sea necesario, recordando las asignaciones asignadas en una tabla hash .
Referencias
- ^ a b Plotkin, Gordon D. (1970). Meltzer, B .; Michie, D. (eds.). "Una nota sobre la generalización inductiva". Inteligencia de máquina . 5 : 153-163.
- ^ a b Plotkin, Gordon D. (1971). Meltzer, B .; Michie, D. (eds.). "Una nota adicional sobre la generalización inductiva". Inteligencia de máquina . 6 : 101-124.
- ^ 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. 73 . Holanda Septentrional.; aquí: Sección 1.3