Hay algunos lugares donde la teoría de la homotopía surge con frecuencia
Teoría del tipo:
Específicamente, la teoría de tipos de homotopía es una teoría aún en su infancia que básicamente trata de crear un sistema de tipos (sistema de verificación de pruebas) que modela más de cerca cómo los matemáticos escriben pruebas en topología algebraica. Para hacer esto, agrega el Axioma de Univalencia en las teorías de tipo tradicionales que básicamente establece que a partir de los isomorfismos de tipo puede probar la equivalencia de tipo (según lo definido por la teoría) y viceversa. Esto se parece mucho a lo que los matemáticos ya suponen que es cierto con frecuencia, pero no ha tenido sentido en el contexto de la informática hasta hace poco. En la teoría de tipos tradicional, solo asume que un teorema es verdadero si puede escribir un programa “total” que pruebe la interpretación de ese teorema (consulte la correspondencia de Curry-Howard).
- ¿Probar la conjetura de Goldbach ternario ayuda a probar la conjetura de Goldbach fuerte (binaria)?
- Informática teórica: ¿se puede crear una máquina que sea más poderosa que una máquina de turing?
- ¿Cuáles son algunos ejemplos de informática, matemáticas o algoritmos donde se aplica el problema de detención?
- Soy muy rápido en los cálculos matemáticos y me encantan las matemáticas. ¿En qué opciones de carrera puedo dar lo mejor?
- Dada una matriz binaria cuadrada donde puede voltear todos los elementos de una columna, ¿cómo puede encontrar el número máximo de puntos que puede obtener?
En la teoría de tipos, puede construir un predicado llamado identidad que es solo dos si dos tipos son idénticos. Cuando digo idéntico, quiero decir literalmente idéntico, no solo isomorfo. Por ejemplo, si tuvieras dos tipos en tu idioma, uno llamado Int y el otro llamado Integer , y ambos se comportaban exactamente de la misma manera en suma y resta, y ambos tenían la misma representación de máquina, serían isomorfos pero no idénticos. . Podría escribir un programa con bastante facilidad para convertir Int a Integer. Incluso podría hacer que el “predicado de identidad” sea una característica del lenguaje, de modo que si tuviera un programa para convertir números enteros en números enteros y viceversa, podría hacer que el lenguaje diga que son idénticos. Sin embargo, lo contrario no es tan fácil de entender. Si tuviera un predicado que demostrara ciegamente que dos tipos son idénticos, ¿cómo construiría automáticamente un programa para convertir entre estos tipos?
Asumiendo el Univalence Axiom te dice que puedes hacer esto, pero no te dice cómo hacerlo. Por el momento, parece haber un progreso significativo en este problema, específicamente en relación con la teoría de los tipos cúbicos, pero no sé si la historia está completamente completa. Dado esto, creo que la teoría del tipo de homotopía es más probable que proporcione avances futuros significativos para el campo de la teoría de la homotopía que el campo de la lógica computacional (fuera de sí mismo). Sigue siendo algo muy bueno.
- 15-819 Teoría del tipo de homotopía
- https://www.math.ias.edu/~amortb…
Geometría Computacional:
La teoría de la homotopía aparece con bastante frecuencia en la geometría computacional, donde se ha utilizado para todo, desde probar propiedades de triángulos bezier para simulaciones de fluidos (cosas en las que he trabajado personalmente), hasta toda la rama de la topología computacional.
- Topología computacional
