Comparación de las formulaciones existentes del álgebra universal y sus niveles de generalidad

Question

Soy un recién llegado al álgebra universal y acabo de leer este libro (muy bueno, en mi opinión) sobre el tema:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

En particular, los autores tratan el caso de las teorías de Lawvere finitarias de primer orden y ordenadas en 1 (equivalentemente: mónadas finitarias). Este es, según tengo entendido, el nivel de generalidad más común que aparece en la literatura para tratar el álgebra universal (categórica).

Además, los autores explican la relación entre el álgebra universal "a la antigua" -que aquí llamaremos teorías ecuacionales- y las teorías de Lawvere, así como la relación entre las teorías de Lawvere y las categorías de modelos de las teorías de Lawvere. El resultado rápido e informal es que hay un par de tales adjunciones: álgebra universal antigua, lawvere thies, modelos Dónde $\mathrm{EqTh}$ es la categoría de las teorías ecuacionales (es decir: firmas + ecuaciones), $\mathrm{AlgTh}$ es la categoría de las teorías de Lawvere, $\mathrm{AlgCat}$ es la categoría de las categorías algebraicas. Las categorías algebraicas se definen básicamente como categorías de modelos de teorías de Lawvere. La primera adjunción conecta presentaciones particulares de teorías con teorías de Lawvere. La segunda adjunción es una especie de dualidad Gabriel-Ulmer y vincula las teorías a sus modelos.

Mi pregunta es: ¿cuáles son las formas existentes de generalizar este cuadro? ¿Y existe un marco definitivo que englobe todas esas generalizaciones? Por ejemplo, me interesaría saber qué se puede hacer para obtener teorías de tipos como teorías algebraicas de algún tipo.

Algunos ejemplos de generalizaciones (en la presentación, en la teoría de Lawvere o en ambas): lógica de orden superior, teorías de Lawvere enriquecidas, esbozos, ordenaciones dependientes de la lógica de primer orden de Makkai (FOLDS), teorías infinitas. Seguro que hay muchas más.

EDITAR: Aquí hay un artículo sobre teorías algebraicas de orden superior

Answer 1

Hay muchas respuestas satisfactorias, pero no una sola. Me limitaré a soltar un montón de bibliografía relevante sin muchas explicaciones, y sin mucho contexto específico; quizá vuelva más tarde para hacer ajustes. Espero que sea mejor que nada.

• https://arxiv.org/abs/1904.08541
• https://arxiv.org/abs/1805.04346 (ésta es, en un sentido muy preciso, la correspondencia mónada-teoría más nítida que se puede obtener, por construcción; sin embargo, la noción de "teoría" es bastante general: ninguna suposición sobre $\cal A$ .)
• https://arxiv.org/abs/1112.3076 el resultado: si una teoría de Lawvere es una mónada finitaria, ¿cuál es una ley distributiva entre mónadas en términos de la identidad asociada en functores objeto /slash/ mónadas? Respuesta: un cierto tipo de sistema de factorización sobre la teoría/categoría asociada a la mónada compuesta.
• https://arxiv.org/abs/0907.2460 Ejemplo 4.17, y más abajo para la versión multiordenada.
• https://arxiv.org/abs/1511.02920 (en mi opinión, esto es lo más agudo que se puede llegar manteniendo al menos algunas de las características esenciales de lo que debe ser una "teoría algebraica").
• https://arxiv.org/abs/1307.2963 (en mi opinión, se trata de una brillante caracterización de las teorías de Lawvere como categorías enriquecidas a lo largo de $[{\sf Fin,Set}]$ ).
• https://arxiv.org/abs/1507.08710 véase la sección 5, y más adelante, donde los autores un criterio conceptual claro para cuando una teoría algebraica es el producto tensorial de dos dadas.

El punto de partida implícito de todos estos desarrollos diferentes merece al menos una palabra de explicación.

La idea es más o menos la siguiente: digamos que una "teoría Lawvere" es un functor de identidad sobre objeto ${\sf Fin}^o \to L$ donde $\sf Fin$ es la categoría de conjuntos y funciones finitos. Estos functores forman una categoría, la categoría $\sf Law$ de las teorías de Lawvere, de las que este artículo de Hyland y Power constituye un brillante estudio. https://www.sciencedirect.com/science/article/pii/S1571066107000874

Entonces existe una equivalencia de categorías entre

1. La categoría $\sf Law$ definido como arriba.
2. La categoría de promonadas en el objeto $\sf Fin$ considerado como un objeto de la bicategoría $\sf Prof$ de profunctores
3. La categoría de mónadas finitarias sobre $\sf Set$ (todos los conjuntos y funciones)
4. La categoría de " convolución monoidal cocontinua "mónadas en $[{\sf Fin,Set}]$ es decir, mónadas $T : [{\sf Fin,Set}] \to [{\sf Fin,Set}]$ que son functores preservadores del colímite y monoidales con respecto a la convolución de Day
5. La categoría de los "clones" (también llamados "operadas cartesianas"), es decir, los monoides con respecto a una cierta estructura monoidal sobre $[{\sf Fin,Set}]$ llamado "producto de sustitución".
6. La categoría de mónadas relativas en el ( inclinación )categoría monoidal $[{\sf Fin,Set}]$ .

Aquí nos encontramos en la misma situación de la famosa parábola del elefante y los ciegos: diversos enfoques han intentado generalizar, en diversa medida, cada una de estas diferentes perspectivas sobre la noción de teoría de Lawvere. Algunos de ellos funcionan mejor cuando se cambia la base de enriquecimiento; otros funcionan mejor cuando se intenta internalizar la noción de teoría algebraica (sorprendentemente, la primera noción de teoría algebraica interna se dio tomando 2 como definición primaria, en un brillante trabajo de Johnstone y Wraith https://link.springer.com/chapter/10.1007%2FBFb0061363 ), otros funcionan mejor cuando su escenario abstracto para la TC es doblemente categórico, otros son exquisitamente combinatorios.

Otra posible generalización es la siguiente (de la que no conozco ninguna referencia única y exhaustiva): $\sf Fin$ es la categoría libre con coproductos finitos sobre el punto, y dualmente ${\sf Fin}^o$ es la categoría libre con productos por encima del punto. por lo tanto, llame a ${\sf Fin} = P1$ y sustituir $\sf Fin$ , arriba, con otra categoría $D1$ la categoría libre con $D$ -sobre el punto, donde $D$ es sólo otra 2-mónada en $\sf Cat$ (por ejemplo, finalización bajo otras formas de colímites). ¿Qué partes de la correspondencia anterior se rompen?

¿Confluyen todos estos planteamientos en un marco verdaderamente global y unificado? No lo sé. Yo diría que algunos sí, pero...

Answer 2

Fosco da una buena visión general de la teoría general en su respuesta. Me gustaría señalar dos generalizaciones diferentes de la teoría algebraica que no están, que yo sepa, subsumidas en ninguna de ellas, pero que son relevantes para tu comentario:

Por ejemplo, me interesaría saber qué se puede hacer para obtener teorías de tipos como teorías algebraicas de algún tipo.

Las teorías de tipos simples pueden describirse como estructuras algebraicas con operadores de enlace multiordenados y estructura de ordenación algebraica. Un paso en esta dirección, desde la perspectiva de las teorías algebraicas, lo dan Fiore y Mahmoud en Teorías algebraicas de segundo orden . Consideran una generalización de la teoría algebraica en la que se consideran categorías con productos finitos y un objeto exponenciable. El objeto exponenciable permite la representación de operadores de segundo orden, como el $\lambda$ -del operador de abstracción de tipo simple $\lambda$ -Cálculo. Sólo consideran el entorno de ordenación simple, pero es bastante fácil extenderlo al entorno de ordenación múltiple. La equivalencia con una lógica ecuacional se encuentra en la obra de Fiore y Hur Lógica ecuacional de segundo orden .

Para los operadores de tipo (incluidos los operadores de tipo con vinculación, como los que se encuentran en los operadores polimórficos $\lambda$ -), Fiore y Hamana presentan un enfoque operádico/teórico de la hoja de cálculo. Teorías algebraicas polimórficas multiversales que también contiene la equivalencia con una lógica ecuacional.

Para las teorías de tipo subestructural, un punto de partida son los trabajos de Power y Tanaka, tales como Leyes pseudodistributivas y axiomática para la vinculación de variables que también se basa en el enfoque operádico/teórico de la hoja de cálculo.

La representación de otros tipos de teoría de tipos de este modo, como las teorías de tipos dependientes, es sobre todo una cuestión abierta. (Por "teoría de tipos" entiendo al menos alguna estructura con una noción de operador de enlace de variables).

Answer 3

Respuesta de @focso y Respuesta de @varkor dan respuestas excelentes que cubren la mayoría de los aspectos de su pregunta. Sólo añadiré algo más sobre la ampliación de estos marcos para cubrir las "teorías de tipos", es decir, para incluir tanto la dependencia de la ordenación como la vinculación de variables. Se trata de un tema bastante nuevo y abierto, pero ya se han sentado algunas bases.

La parte bien establecida se remonta a los años 80, a partir del trabajo de Cartmell. Este define categorías contextuales y, posteriormente, diversas variantes ligeras (categorías con atributos (CwA), categorías con familias (CwF) ) correspondientes a una denominada "teoría algebraica generalizada" o "teoría algebraica dependiente". Esto proporciona un buen tratamiento de los tipos dependientes, pero todavía no de la ligadura de variables. Las teorías de tipos específicos con ligaduras corresponden entonces a una estructura algebraica adicional sobre categorías contextuales (o CwA, CwF, etc.). Una buena introducción es el capítulo de Martin Hofmann Sintaxis y semántica de los tipos dependientes , doi:10.1007/978-1-4471-0963-1_2 , pdf sin pagar aquí .

Para las teorías de tipos individuales, esta correspondencia funciona satisfactoriamente (y ha sido desarrollada por muchos autores; no intentaré dar una bibliografía aquí); pero hasta hace muy poco, no se había generalizado a una noción general de "teoría de tipos". Entre las aproximaciones que se han hecho hasta ahora figuran:

• Isaev, Presentaciones algebraicas de teorías de tipo dependiente , arXiv:1602.08504 . Esto define directamente las teorías de tipos como ciertas extensiones esencialmente algebraicas de los CwA.

• Uemura, Un marco general para la semántica de la teoría de tipos , arXiv:1904.04097 . En mi opinión, éste es el enfoque más potente y mejor desarrollado hasta ahora. Da una definición abstracta categórica de las teorías de tipos como categorías de mapas representables (una generalización imaginativa y de gran alcance del reanálisis de Fiore/Awodey de los CwF), y un tratamiento sintáctico correspondiente (basado en el enfoque del "marco lógico"). Es mucho más general que cualquiera de los otros enfoques que menciono aquí, y está muy bien estructurado.

• Bauer-Lumsdaine-Haselwarter, Definición general de las teorías de tipos dependientes , arXiv:2009.05539 . Una definición sintáctica de las teorías de tipos generales, tomando en serio la vinculación de variables como primitiva, y escrita con un análisis categórico muy en mente (aunque no se da en el documento). Debería corresponder a una ligera variante de la definición algebraica de Isaev y a una subclase de la de Uemura.

Espero que en un futuro próximo se sigan desarrollando estos aspectos y las conexiones entre ellos, y que dentro de cinco años esta parte de su pregunta tenga mejor respuesta que ahora.