Aplicaciones de la geometría algebraica en la teoría de tipos / teoría del lenguaje de programación

Últimamente, me he interesado en la geometría algebraica y he comenzado a leer sobre ella. Todavía sé muy poco sobre este campo, pero quiero saber si tiene alguna conexión con mi campo principal, la teoría de tipos y los lenguajes de programación.

Sé que la topología algebraica tiene muchas aplicaciones en la teoría de tipos (teoría de tipos de homotopía y muchas más), pero ¿qué pasa con la geometría algebraica, además de que tanto la teoría de tipos / teoría PL como AG son buenos motivadores de la teoría de categorías?

Que yo sepa (que es definitivamente incompleto), ha habido relativamente poco trabajo en esto, presumiblemente porque requiere asimilar dos cuerpos de conocimiento relativamente intrincados. Sin embargo, poco no significa inexistente. Thierry Coquand y sus colaboradores han escrito bastantes artículos sobre las conexiones entre el álgebra conmutativa y la lógica constructiva.

• Thierry Coquand, Henri Lombardi. Un enfoque lógico para el álgebra abstracta. .

  Este documento me causó una gran impresión como estudiante de posgrado: la forma segura y libre en la que utilizó las ideas de la teoría de la prueba y la teoría del modelo para hacer matemáticas no triviales y apropiadas es algo que admiraba mucho y al que todavía aspiro.

• Henri Lombardi y Claude Quitté tienen un libro de texto (disponible gratuitamente), Álgebra conmutativa: métodos constructivos .

  Como sugiere el título, se trata de álgebra conmutativa en lugar de geometría algebraica, pero dado que el álgebra conmutativa proporciona gran parte de la infraestructura para la geometría algebraica, esto seguirá siendo de interés.

También hay una serie de tesis doctorales muy interesantes en el área:

• Tesis doctoral de Andres Mörtberg Formalización de refinamientos y álgebra constructiva en teoría de tipos

  Una vez que tiene una prueba constructiva, tiene un algoritmo. Esta tesis busca hacer que esos algoritmos sean eficientes.

• Tesis doctoral de Bassel Mannaa, semántica de gavilla en álgebra constructiva y teoría de tipos

  En esta tesis, demuestra la exactitud del teorema de Newton-Puiseux de manera constructiva, así como la independencia del principio de Markov. Ofrece un buen ejemplo de cómo los métodos semánticos sheaf tienen aplicaciones tanto en geometría como en lógica.

• Tesis doctoral de Ingo Blechschmidt, Usando el lenguaje interno de toposes en geometría algebraica,

  Esta tesis busca rehacer muchas de las pruebas habituales de geometría algebraica en el lenguaje interno de los pequeños topos de Zariski asociados con un esquema, produciendo una especie de "geometría algebraica sintética". (También hace "teoría del esquema sintético" usando los grandes topos de Zariski). Como era de esperar, dado que los topoi no son generalmente booleanos, las pruebas deben hacerse en un estilo intuitivo.

También vale la pena señalar la siguiente referencia:

• Saunders Mac Lane, Ieke Moerdijk. Gavillas en Geometría y Lógica Gavillas en Geometría y Lógica: Una primera introducción a la teoría de topos .

  Gran parte de la tecnología utilizada en este trabajo proviene de las conexiones entre la teoría de topos, la lógica y la geometría. Esta es la referencia estándar, aunque en su mayoría lo aprendí a través de los documentos de Steve Vickers.

Puede que esto no sea exactamente lo que está buscando, pero una aplicación de la geometría algebraica en lenguajes de programación es el análisis de bucles lineales:

Un bucle lineal es un programa muy simple de la forma:

$x=s$

$x\notin F$

$x\leftarrow Ax$

$s,x\in \mathbb Q^d$$A\in \mathbb Q^{d\times d}$$F$ es una condición de terminación, que puede ser un conjunto simplemente descrito (por ejemplo, un politopo o un conjunto semialgebraico).

$A$$\{A^ns: n\in \mathbb N\}$$A$

Puede echar un vistazo al documento Sobre la complejidad del problema de la órbita como un buen punto de partida.