stringtranslate.com

Álgebra de términos

En álgebra universal y lógica matemática , un término álgebra es una estructura algebraica generada libremente sobre una firma dada . [1] [2] Por ejemplo, en una firma que consiste en una sola operación binaria , el término álgebra sobre un conjunto X de variables es exactamente el magma libre generado por X. Otros sinónimos para la noción incluyen álgebra absolutamente libre y álgebra anárquica . [3]

Desde una perspectiva de teoría de categorías , un álgebra de términos es el objeto inicial para la categoría de todas las álgebras generadas por X de la misma firma , y ​​este objeto, único hasta el isomorfismo , se llama álgebra inicial ; genera por proyección homomórfica todas las álgebras en la categoría. [4] [5]

Una noción similar es la de universo Herbrand en lógica , usualmente utilizada bajo este nombre en programación lógica , [6] que se define (absolutamente libremente) a partir del conjunto de constantes y símbolos de función en un conjunto de cláusulas . Es decir, el universo Herbrand consiste en todos los términos básicos : términos que no tienen variables en ellos.

Una fórmula atómica o átomo se define comúnmente como un predicado aplicado a una tupla de términos; un átomo fundamental es entonces un predicado en el que solo aparecen términos fundamentales. La base de Herbrand es el conjunto de todos los átomos fundamentales que se pueden formar a partir de símbolos de predicado en el conjunto original de cláusulas y términos en su universo de Herbrand. [7] [8] Estos dos conceptos reciben su nombre de Jacques Herbrand .

Las álgebras de términos también juegan un papel en la semántica de los tipos de datos abstractos , donde una declaración de tipo de datos abstractos proporciona la firma de una estructura algebraica multiordenada y el álgebra de términos es un modelo concreto de la declaración abstracta.

Álgebra universal

Un tipo es un conjunto de símbolos de función, cada uno de los cuales tiene una aridad asociada (es decir, número de entradas). Para cualquier entero no negativo , denotemos los símbolos de función en de aridad . Una constante es un símbolo de función de aridad 0.

Sea un tipo y sea un conjunto no vacío de símbolos que representan los símbolos variables. (Para simplificar, supongamos que y son disjuntos). Entonces, el conjunto de términos del tipo sobre es el conjunto de todas las cadenas bien formadas que se pueden construir utilizando los símbolos variables de y las constantes y operaciones de . Formalmente, es el conjunto más pequeño tal que:

El término álgebra de tipos over es, en resumen, el álgebra de tipos que asigna cada expresión a su representación en cadena. Formalmente, se define de la siguiente manera: [9]

Un álgebra de términos se llama absolutamente libre porque para cualquier álgebra de tipo , y para cualquier función , se extiende a un homomorfismo único , que simplemente evalúa cada término a su valor correspondiente . Formalmente, para cada :

Ejemplo

Como ejemplo, un tipo inspirado en la aritmética de números enteros se puede definir mediante , , , y para cada .

El álgebra de tipo más conocida tiene como dominio los números naturales e interpreta , , , y de la forma habitual; nos referimos a ella como .

Para el conjunto de variables de ejemplo , vamos a investigar el álgebra de términos de tipo sobre .

En primer lugar, se considera el conjunto de términos del tipo over . Usamos el color rojo para marcar sus miembros, que de otra manera podrían ser difíciles de reconocer debido a su forma sintáctica poco común. Tenemos, por ejemplo:

En términos más generales, cada cadena en corresponde a una expresión matemática construida a partir de los símbolos admitidos y escrita en notación prefija polaca ; por ejemplo, el término corresponde a la expresión en notación infija habitual . No se necesitan paréntesis para evitar ambigüedades en la notación polaca; por ejemplo, la expresión infija corresponde al término .

Para dar algunos contraejemplos, tenemos por ejemplo:

Ahora que el conjunto de términos está establecido, consideramos el álgebra de términos de tipo sobre . Esta álgebra utiliza como dominio, en el que se deben definir la adición y la multiplicación. La función de adición toma dos términos y y devuelve el término ; de manera similar, la función de multiplicación asigna los términos dados y al término . Por ejemplo, evalúa al término . De manera informal, las operaciones y son ambas "perezosas" en el sentido de que solo registran qué cálculo se debe realizar, en lugar de hacerlo.

Como ejemplo de extensibilidad única de un homomorfismo, considere definido por y . De manera informal, define una asignación de valores a símbolos de variable y, una vez que esto se hace, cada término de puede evaluarse de manera única en . Por ejemplo,

De manera similar se obtiene .

Base de Herbrand

La firma σ de un lenguaje es un triple < O ,  F ,  P > que consiste en el alfabeto de constantes O , símbolos de función F y predicados P . La base de Herbrand [10] de una firma σ consiste en todos los átomos fundamentales de σ : de todas las fórmulas de la forma R ( t 1 , ...,  t n ), donde t 1 , ...,  t n son términos que no contienen variables (es decir, elementos del universo de Herbrand) y R es un símbolo de relación n -ario ( es decir, predicado ). En el caso de la lógica con igualdad, también contiene todas las ecuaciones de la forma t 1  =  t 2 , donde t 1 y t 2 no contienen variables.

Decidibilidad

Las álgebras de términos se pueden demostrar como decidibles mediante la eliminación de cuantificadores . La complejidad del problema de decisión es NO ELEMENTAL porque los constructores binarios son inyectivos y, por lo tanto, funciones de emparejamiento. [11]

Véase también

Referencias

  1. ^ Wilfrid Hodges (1997). Una teoría de modelos más breve . Cambridge University Press . pp. 14. ISBN. 0-521-58713-1.
  2. ^ Franz Baader ; Tobias Nipkow (1998). Reescritura de términos y todo eso. Cambridge University Press . p. 49. ISBN 0-521-77920-0.
  3. ^ Klaus Denecke; Shelly L. Wismath (2009). Álgebra universal y coalgebra. World Scientific . págs. 21-23. ISBN. 978-981-283-745-5.
  4. ^ TH Tse (2010). Un marco unificador para análisis estructurado y modelos de diseño: un enfoque que utiliza la semántica del álgebra inicial y la teoría de categorías . Cambridge University Press . pp. 46–47. doi :10.1017/CBO9780511569890. ISBN. 978-0-511-56989-0.
  5. ^ Jean-Yves Béziau (1999). "La estructura matemática de la sintaxis lógica". En Carnielli, Walter Alexandre; D'Ottaviano, Itala ML (eds.). Avances en lógica contemporánea y ciencia de la computación: Actas de la undécima conferencia brasileña sobre lógica matemática, 6-10 de mayo de 1996, Salvador, Bahía, Brasil . American Mathematical Society . pág. 9. ISBN. 978-0-8218-1364-5. Recuperado el 18 de abril de 2011 .
  6. ^ Dirk van Dalen (2004). Lógica y Estructura. Saltador . pag. 108.ISBN 978-3-540-20879-2.
  7. ^ M. Ben-Ari (2001). Lógica matemática para la informática. Springer . págs. 148-150. ISBN 978-1-85233-319-5.
  8. ^ Monroe Newborn (2001). Demostración automática de teoremas: teoría y práctica. Springer . p. 43. ISBN 978-0-387-95075-4.
  9. ^ Stanley Burris; HP Sankappanavar (1981). Un curso de álgebra universal. Springer. págs. 68-69, 71. ISBN 978-1-4613-8132-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
  10. ^ Rogelio Dávila. Descripción general de la programación por conjuntos de respuestas.
  11. ^ Jeanne Ferrante; Charles W. Rackoff (1979). La complejidad computacional de las teorías lógicas . Springer , Capítulo 8, Teorema 1.2.

Lectura adicional

Enlaces externos