Usos de -categories no TCS

Eu não sou um cientista da computação teórico. Sou um teórico estável da homotopia usando -categories. Vi aplicações da teoria das categorias e da teoria topos à ciência da computação teórica, e fiquei imaginando se havia alguma maneira de usar -categories (e de preferência para mim, a teoria da homotopia estável) na ciência da computação. Acho que o HoTT deve ser um desses aplicativos, mas posso estar errado porque não sei quase nada sobre o HoTT. (Então, eu também não sei como o HoTT é usado no TCS.)∞$\infty$$\infty$

A aplicação de idéias teóricas mais elevadas da homotopia ao CS ainda é um campo muito incipiente! Meu entendimento é que não é tão antigo quanto um campo matemático.

Certamente o HoTT é o impulso central para tais idéias. Mesmo assim, houve poucas aplicações da teoria da categoria de "dimensão" maior que 2.

Uma boa "ciência da computação" é a Homotopical Patch Theory, de Anguili et al . Eles mostram que algumas operações e propriedades comuns inerentes aos gitsistemas de controle de versão podem ser melhor compreendidas usando a teoria dos tipos de homotopia.

Outra linha de pensamento não relacionada é um trabalho interessante sobre a relação entre a (2) teoria da homologia e a confluência dos sistemas de reescrita de termos (ou estruturas mais complexas, como álgebras superiores). Alguns exemplos são

Y. Guiraud Confluência da reescrita linear e homologia de álgebras .

Propriedade de Y. Lafont e A. Proute Church-Rosser e homologia de monóides .

Os cientistas teóricos da computação fazem muitas coisas, uma das quais é a modelagem matemática de várias coisas da ciência da computação. Por exemplo, gostamos de fornecer modelos matemáticos de linguagens de programação, para que as pessoas possam realmente provar coisas sobre programas (como provar que o programa faz o que deveria). Nesse sentido, é sempre bom ter um bom suprimento de técnicas matemáticas que nos proporcionem modelos para várias coisas que os cientistas da computação inventam.

De fato, os cientistas teóricos da computação tiveram que inventar alguns modelos matemáticos bastante avançados, porque queriam obter uma boa noção matemática do que os cientistas da computação estavam fazendo. Muitas vezes, a teoria dos conjuntos clássica não é bom o suficiente para os nossos propósitos, por exemplo, porque queremos um não-tivial categoria pequena completa ou um não-trivial conjunto satisfazendo .D ≅ D $D$$D \cong D^D$

Recentemente, foi descoberta uma conexão entre a teoria dos tipos (que é uma generalização comum das linguagens de programação, lógica e teoria dos conjuntos) e a teoria da homotopia. Ainda é muito cedo para dizer o que exatamente resultará disso, mas nosso entendimento da teoria dos tipos certamente foi avançado pelas idéias da teoria da homotopia. Por outro lado, está ficando claro que a teoria intensiva de tipos, seja o que for, é uma linguagem formal muito boa para descrever categorias . As pessoas suspeitam que deveria haver "teoria de tipos direcionada" que corresponderia a -categories, mas ninguém tem certeza ainda. Esta é uma área ativa de pesquisa.$(\infty,1)$$\infty$

A única conexão entre a teoria da homotopia estável e a teoria dos tipos que conheço é o trabalho de Matthijs Vákár na teoria dos tipos linear dependente . Aparentemente, um modelo é a teoria da homotopia estável, mas isso ainda não foi publicado, apenas sugerido no final do artigo vinculado.

Outro lugar onde você pode procurar aplicações da teoria da homotopia (estável ou não) na ciência da computação é a topologia computacional . Há homologia persistente foi recentemente encontrado muitos usos, e as pessoas estão certamente olhando para aplicações de homotopia teórica de tipo semelhante. A idéia básica é usar a topologia algébrica para estudar propriedades de grandes conjuntos de dados.

Sem dúvida, existem outras aplicações. Cody mencionou o uso da teoria da homotopia (disfarçada da teoria do tipo de homotopia) para estudar os sistemas de controle de revisão. Também existem aplicações da teoria da homotopia no estudo de cálculos paralelos e cuncorrentes, como " Topologia e simultaneidade algébrica ". Alguém mais qualificado pode ter a gentileza de fornecer melhores referências. De qualquer forma, você notará que todas essas aplicações (com a possível exceção da teoria dos tipos de homotopia) são bastante pouco sofisticadas do ponto de vista matemático - o que não significa que não valham nada!

isso tenta esboçar conexões mais gerais. parte deste programa pode ser considerada uma extensão muito recente e mais elaborada da antiga correspondência de Curry-Howard observada entre provas e programas. também existe uma conexão estreita com a prova automatizada de teoremas (também conhecida como assistentes de prova). muitas técnicas usadas nas provas de prova do teorema automatizado não estão em terreno matemático totalmente sólido e a teoria da homotopia acrescenta um aterramento mais firme.

Esta proposta de uma equipe considerável captura / pesquisa muitas das conexões atualmente conhecidas com CS: Homotopy Type Theory: Fundamentos Unificados de Matemática e Computação (Proposta MURI)

Licata dessa equipe está especialmente interessada em aplicações científicas da teoria da homotopia. algumas de suas palestras e uma de Voevodsky, fundador do destacado axioma da Univalência :

• Aplicações Matemáticas e Computacionais da Teoria dos Tipos de Homotopia. Colóquio na Universidade de Iowa. Novembro de 2013. [ slides ]

• Provas verificadas por computador na lógica da teoria da homotopia. Palestra convidada na Associação Norte-Americana de Lógica Simbólica. Maio de 2013. [ slides ]

• Programando e provando na teoria de tipos de homotopia. Colóquio em Wesleyan, Princeton e Cornell. Primavera de 2013. [ slides ]

• Ciência da Computação e Teoria da Homotopia , vídeo-aula de 10m de Voevodsky / IAS