Aplicações da geometria algébrica na teoria dos tipos / teoria das linguagens de programação

9

Ultimamente, me interessei por geometria algébrica e comecei a ler sobre ela. Ainda sei muito pouco sobre esse campo, mas quero saber se ele tem alguma conexão com meu campo principal, teoria de tipos e linguagens de programação.

Eu sei que a topologia algébrica tem muitas aplicações na teoria dos tipos (teoria dos tipos homotópicos e muito mais), mas e a geometria algébrica, além de que tanto a teoria dos tipos / teoria PL quanto a AG são bons motivadores da teoria das categorias?

xrq
fonte
11
Esta não é uma resposta para sua pergunta, mas a topologia algébrica também é aplicada na teoria da concorrência. Dê uma olhada na homotopia direcionada e há um artigo na Fossacs 2019 sobre isso também.
Henning Basold 16/05/19
Eu também estou interessado em programação de computadores e estudante de pesquisa em matemática. Meu supervisor é topologista. Mas quero fazer pesquisas em matemática relacionadas à ciência da computação, como álgebra linear. Preciso de ajuda para pesquisar meu tópico de tese para que eu possa fazer pesquisas em ciência da computação teórica, mas não sei por onde devo começar. Preciso de ajuda para o meu tópico de tese para que eu possa fazer pesquisas na minha área de interesse.
Syed Muhammad Asad
@SyedMuhammadAsad Também sou estudante, então não sou a pessoa a perguntar. Você deve consultar alguns especialistas neste campo. A topologia (particularmente algébrica) tem conexões profundas com a teoria de tipos, portanto você pode começar por aí.
xrq 21/05/19

Respostas:

10

Que eu saiba (que é definitivamente incompleto), tem havido relativamente pouco trabalho sobre isso, presumivelmente porque requer a assimilação de dois corpos de conhecimento relativamente intrincados. No entanto, pouco não significa inexistente. Thierry Coquand e seus colaboradores escreveram alguns artigos sobre as conexões entre álgebra comutativa e lógica construtiva.

  • Thierry Coquand, Henri Lombardi. Uma abordagem lógica para álgebra abstrata .

    Este artigo causou uma grande impressão em mim como estudante de graduação - a maneira livre e confiante de usar idéias da teoria da prova e da teoria dos modelos para fazer matemática não trivial e adequada é uma que eu admiro muito e à qual ainda aspiro.

  • Henri Lombardi e Claude Quitté têm um livro didático (disponível gratuitamente), Álgebra comutativa: métodos construtivos .

    Como o título sugere, trata-se de álgebra comutativa, e não de geometria algébrica, mas como a álgebra comutativa fornece grande parte da infraestrutura da geometria algébrica, isso ainda será interessante.

Há também uma série de teses de doutorado muito interessantes na área:

  • Tese de doutorado de Andres Mörtberg Formalizando refinamentos e álgebra construtiva na teoria dos tipos

    Depois de ter uma prova construtiva, você tem um algoritmo. Esta tese procura tornar esses algoritmos eficientes.

  • Tese de doutorado de Bassel Mannaa, Sheaf Semantics in Álgebra Construtiva e Teoria dos Tipos

    Nesta tese, ele prova construtivamente a correção do teorema de Newton-Puiseux, bem como a independência do princípio de Markov. Ele oferece um bom exemplo de como os métodos semânticos de feixe têm aplicações na geometria e na lógica.

  • Tese de doutorado de Ingo Blechschmidt, Usando a linguagem interna das toposes em geometria algébrica,

    Esta tese analisa refazer muitas das provas usuais da geometria algébrica na linguagem interna dos pequenos topos Zariski associados a um esquema, produzindo um tipo de "geometria algébrica sintética". (Ele também faz a "teoria do esquema sintético" usando os grandes topos de Zariski). Como seria de esperar, como os topos geralmente não são booleanos, as provas precisam ser feitas em um estilo intuicionista.

Também vale ressaltar a seguinte referência:

Neel Krishnaswami
fonte
6

Pode não ser exatamente o que você está procurando, mas uma aplicação da geometria algébrica em linguagens de programação é a análise de loops lineares:

Um loop linear é um programa muito simples da forma:

x=s

xF

xUMAx

s,xQdUMAQd×dF

UMA{UMAns:nN}UMA

Você pode dar uma olhada no artigo Sobre a complexidade do problema de órbita como um bom ponto de partida.

Shaull
fonte