Pregunta:
El Instituto de Estudios Avanzados ha tenido un programa especial de un año dedicado al Programa de Fundamentos Univalentes .
Al final de este han producido un libro y un repositorio de código .
Al final de esto, vemos una entrada de blog en Scientific American que afirma:
…podría proporcionar una base nueva y autónoma para todas las matemáticas.
Ahora bien, esta es una afirmación audaz. Por el contrario, puedo ver afirmaciones más humildes, como una prueba simple en Agda de que la suma de dos probabilidades es siempre un par .
Mi pregunta es: ¿Qué investigación novedosa produjeron estos muchachos al final del año? Todo lo que indica el artículo es que escribieron algún código en Agda. ¿Es solo que tenemos una nueva visión de la teoría de tipos de Martin-Löf con algunas aplicaciones?
suposiciones
- Entiendo las ideas más amplias de la teoría de tipos de Martin-Löf en relación con el isomorfismo entre Tipos y Pruebas.
Respuesta:
El libro es en sí mismo representativo del producto de investigación del programa. El código que escribieron en realidad está mayormente en Coq, que yo sepa, y ciertamente el desarrollo que acompaña al libro fue escrito en Coq.
La teoría de tipos homotópicos en sí misma constituye esencialmente Martin-Löf, junto con el axioma de univalencia , que esencialmente establece que los tipos equivalentes son iguales. La noción de equivalencia proviene de una visión que establece una conexión entre una teoría de homotopía sintética y la teoría de tipos de Martin-Löf, de ahí el nombre. Este axioma da paso a una poderosa teoría de tipos que el libro muestra que es capaz de razonar sobre una gran cantidad de importantes matemáticas fundamentales existentes.
De hecho, la parte 2 del libro comprende desarrollos de una versión más tradicional, motivada topológicamente, de la teoría de la homotopía, la teoría de conjuntos, la teoría de categorías y una bonita presentación constructiva de los números reales. Todavía no he explorado mucho el código de Coq, pero entiendo que todas estas presentaciones están acompañadas por la fuente de Coq correspondiente. Dado que podemos formular todos estos fundamentos importantes completamente dentro de la teoría del tipo de homotopía, la hipótesis de que podría ser un fundamento importante para las matemáticas en el futuro tiene sentido. La idea es que los matemáticos puedan extender estos desarrollos seminales hacia más resultados en campos como el álgebra, la topología y el análisis.
Dado que la teoría de tipos de homotopía se refiere a poder hacer matemáticas en Coq a través de la correspondencia de Curry-Howard, puede pensar que la teoría de tipos de homotopía corresponde a una instancia más poderosa de Curry-Howard. La contribución más emocionante de este trabajo es realmente que les da a los matemáticos un lenguaje para hablar sobre las matemáticas en términos de teoría de tipos, y la idea es que esto debería permitir, por un lado, que más matemáticas vayan acompañadas de demostraciones mecanizadas en probadores como Coq, como así como pruebas de computadora que se corresponden más estrechamente con sus equivalentes en inglés simple. Cualquiera que haya usado Coq le dirá que las pruebas que produce a menudo no se parecen mucho a las pruebas equivalentes en inglés simple.