El álgebra libre de términos sintácticos construidos a partir de una firma dada y un conjunto de variables: los elementos son árboles de términos formales y las operaciones son los símbolos de formación de términos; satisface la propiedad universal del objeto libre en la categoría de álgebras de esa firma.

Principio

Generación sintáctica y sustitución: los términos se forman inductivamente a partir de variables y símbolos de función, y la sustitución/evaluación define el homomorfismo único del álgebra de términos hacia cualquier álgebra que interprete la firma.

Demostración

Para la firma con un símbolo binario * y variables {x,y}, el término *(x,*(y,x)) es un elemento del álgebra de términos; dada cualquier álgebra A que interprete *, toda asignación de x,y en A induce un homomorfismo único que evalúa el término a un elemento de A.

Aplicación incorrecta

Confundir el álgebra de términos con el álgebra de todas las funciones sobre un conjunto de variables o con un cociente del álgebra de términos por ecuaciones no triviales; el álgebra de términos en bruto codifica la sintaxis pura, no identificaciones semánticas salvo que se forme un cociente.

Consecuencia

Los álgebra de términos proporcionan modelos iniciales, sustentan algoritmos de unificación y emparejamiento, y suministran representantes sintácticos para álgebras libres y para presentar cocientes que implementan teorías ecuacionales.

Inversión

Un cociente del álgebra de términos por la menor congruencia generada por un conjunto de ecuaciones produce el álgebra libre en la teoría ecuacional correspondiente; el cociente colapsa distinciones sintácticas en igualdades semánticas.

Límite

Los álgebra de términos puros no imponen identidades más allá de la igualdad sintáctica; cualquier axioma impuesto produce cocientes — así el álgebra de términos no pertenece a las variedades definidas por identidades no triviales hasta que se toma el cociente.

Tensión semántica

Entre sintaxis y semántica: el álgebra de términos es puramente sintáctica y refleja los árboles de derivación, mientras que las álgebras semánticas interpretan símbolos y pueden identificar términos distintos; la reconciliación se obtiene mediante cocientes por teorías ecuacionales.

Síntesis

El álgebra de términos es el universo sintáctico de términos para una firma que, mediante su propiedad universal de mapeo, genera tanto las álgebras libres como sirve de fuente para cocientes que presentan teorías ecuacionales y Horn; es el puente de la sintaxis a la semántica algebraica.