¿Comprobación de axiomas como comprobación de tipos?

Question

Existe una conexión entre la teoría de tipos y la lógica, en la que los tipos son proposiciones, y la comprobación de tipos desempeña el papel de verificar si una prueba de una proposición es correcta (isomorfismo de Curry-Howard).

Pero puedo imaginar una conexión diferente: Parece que hay una similitud entre la comprobación de tipos y la comprobación de si una estructura matemática concreta satisface un conjunto de axiomas.

Podríamos decir que las proposiciones (axiomas) se formalizan como tipos (igual que en el isomorfismo CH), pero que ahora, una instancia de una proposición (es decir, una instancia de ese tipo) no es una prueba de la proposición, sino un modelo de la misma. La comprobación de tipos adopta entonces el papel de comprobar si una estructura matemática concreta es realmente un modelo de ese axioma.

¿Existe una formalización de "comprobar si una estructura es un modelo de una proposición" como comprobación de tipos? ¿Podría explicar tal formalización, o señalar una explicación de la misma?

Answer 1

La observación clave de la correspondencia Curry-Howard es que la estructura inductiva de los términos en la teoría de tipos refleja la estructura inductiva de las pruebas en la lógica.

Por ejemplo, dados dos términos $t_1$ y $t_2$ de tipos $A_1$ y $A_2$ puedo construir un término $(t_1,t_2)$ del tipo de producto $A_1\times A_2$ . Del mismo modo, dadas dos pruebas $p_1$ y $p_2$ de las proposiciones $Q_1$ y $Q_2$ Puedo unirlos para formar una prueba $(p_1,p_2)$ de la conjunción $Q_1\land Q_2$ .

Por otro lado, los modelos de una proposición (al menos en la semántica ordinaria para la lógica de primer orden / predicado) no tienen este mismo tipo de estructura inductiva. Los modelos dados $M_1$ y $M_2$ de frases $\varphi_1$ y $\varphi_2$ no hay una forma canónica de construir un modelo de la conjunción $\varphi_1\land \varphi_2$ . Así que no soy optimista en cuanto a que sea posible el tipo de ampliación de Curry-Howard que se busca.

Me parece que se podría cambiar la noción de "modelo" a algo suficientemente sintáctico para que esto funcione - pero eso probablemente implicaría hacer un "modelo" de $\varphi$ esencialmente una codificación de una prueba de $\varphi$ y, a continuación, basándose en la correspondencia habitual Curry-Howard.

Answer 2

Sí, aquí hay dos nociones de "encajar":

• Los términos (lo que aquí se llama instancias) "encajan" en los tipos o no, y eso se comprueba cuando se hace la comprobación de tipos
• Las estructuras (por ejemplo, las construcciones teóricas de conjuntos) "encajan en" las proposiciones o no, y eso se comprueba cuando se verifica si la estructura es un modelo.

Creo que no hay nada de malo en trazar una analogía de cómo las cosas "encajan" en otra aquí, ya que ambos procesos pueden considerarse bajo la apariencia de una tarea computacional. Aunque hay muchas estratificaciones implicadas.

• Por un lado, los lógicos matemáticos (y, por ejemplo, los teóricos de conjuntos) lo hacen todo formalmente con símbolos sobre el papel, pero, sin embargo, hacen una distinción conceptual entre sintaxis y semántica. Como resultado, tienes posiciones filosóficas como el platonismo matemático que considera las estructuras matemáticas como algo más alejado de la sintaxis y más cercano a algo "real". Algo que se realiza entre las semánticas posibles. Los teóricos del tipo de las ciencias de la computación (que también son lógicos, por supuesto, sólo que a veces están más cerca de otra escuela, digamos los teóricos de la prueba) trabajarán en gran parte puramente en el lado sintáctico (y la semántica se busca en configuraciones más generales que, por ejemplo, en los departamentos de los teóricos de conjuntos)
• En segundo lugar, como ya se ha mencionado, ambas "comprobaciones" son formas de cálculo y cabe señalar que lo que se pueda hacer aquí dependerá de la lógica subyacente. El Sistema tipo Hindley-Milner es el marco que motivó los lenguajes de programación ML y luego Haskell, y otorga una buena rutina de comprobación de tipos. Los marcos en los que es posible una buena comprobación hicieron recortes. Los esfuerzos modernos en el desarrollo de un lenguaje tipado dependiente se orientan hacia una comprobación constructiva/ intuicionista lógica que ahora incluyen formas fuertes de cuantificadores, mientras que los logicistas y los teóricos del modelo hacen en gran parte un estudio más profundo y por tanto menos variado (relativamente hablando) de las lógicas fuertes de primer orden o de orden superior establecidas desde hace tiempo. Las respuestas en esta lógica SE pregunta son una de las más interesantes de la plataforma. Como siempre ocurre con preguntas tan amplias sobre la lógica, ahora se podría bajar a muchos lugares de conejo. Podría dar un toque de atención a Teorema de restricción de Tarski para las lógicas fuertes. La decidibilidad también es una cuestión para los sistemas de tipos, si se elige cualquiera.
• Siguiendo con el tema de las restricciones, la comprobación de tipo de un término comprueba todo lo que puede, mientras que con las proposiciones, siempre hay muchos y diferentes aspectos de una estructura que se pueden validar. De nuevo, aquí, si haces recortes y tu sistema de tipos admite subtipos y demás, supongo que también puedes adoptar puntos de vista más gruesos sobre los términos.
• En esta última noción de "encajar", está el concepto de categoricidad y se puede intentar reflejar eso en los tipos de singularidad.
• Si ha acotado una de sus lógicas de interés y decide que quiere enfocar su pregunta desde una perspectiva de cálculo bruto y de "encaje", entonces el tema de reescritura abstracta y sistemas de reescritura que puede parecer incluso más formal que los subcampos de la lógica matemática, puede ser de su agrado.

Nota al margen 1: El proceso de verificación en este último caso ni siquiera tiene que limitarse a los axiomas, sino que podemos hacerlo para cualquier proposición.

Nota al margen 2: No soy fan de su redacción inicial "comprobar si una prueba de una proposición es correcta" . En cambio, yo diría "comprobar si una expresión es una prueba de una proposición" . Lo digo porque si se utiliza su lenguaje aquí, entonces concedemos a cada término la condición de ser una "prueba errónea" para casi todas las proposiciones. Sin embargo, eso es sólo una cuestión de nuestro lenguaje aquí.