Aplicações sólidas da teoria das categorias no TCS?

Eu tenho aprendido alguns pedaços da teoria das categorias. Certamente é uma maneira diferente de ver as coisas. (Resumo muito rudimentar para quem ainda não a viu: a teoria das categorias fornece maneiras de expressar todos os tipos de comportamentos matemáticos apenas em termos de relações funcionais entre objetos. Por exemplo, coisas como o produto cartesiano de dois conjuntos são definidas completamente em termos de como outras funções se comportam com ele, não em termos de quais elementos são membros do conjunto.)

Tenho um entendimento vago de que a teoria das categorias é útil no lado das linguagens de programação / lógica (a "Teoria B") e estou imaginando quanto os algoritmos e a complexidade ("Teoria A") poderiam se beneficiar. Pode me ajudar a decolar, se eu conhecer algumas aplicações sólidas da teoria das categorias na Teoria B. (Eu já estou implicitamente assumindo que não há aplicações na Teoria A encontradas até agora, mas se você tiver algumas delas, isso é até melhor para mim!)

Por "aplicação sólida", quero dizer:

(1) A aplicação depende tão fortemente da teoria das categorias que é muito difícil de obter sem usar o maquinário.

(2) O aplicativo invoca pelo menos um teorema não trivial da teoria das categorias (por exemplo, o lema de Yoneda).

Pode ser que (1) implique (2), mas quero garantir que essas sejam aplicações "reais".

Enquanto eu tenho alguns antecedentes da "Teoria B", já faz um tempo, portanto, qualquer desconexão seria muito apreciada.

(Dependendo do tipo de resposta que recebo, posso transformar essa pergunta em wiki da comunidade mais tarde. Mas quero realmente boas aplicações com boas explicações, por isso parece uma pena não recompensar o (s) respondedor (es) com alguma coisa.)

Posso pensar em um exemplo em que a teoria das categorias foi diretamente "aplicada" para resolver um problema aberto em linguagens de programação: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann e Phil Scott, "Normalização por avaliação para cálculo lambda digitado com coprodutos" . De seu resumo: "Resolvemos o problema de decisão para o cálculo lambda simplesmente digitado com somas binárias fortes, equivalentemente o problema da palavra para categorias fechadas cartesianas livres com coprodutos binários. Nosso método é baseado na técnica semântica conhecida como 'normalização por avaliação' e envolve inverter a interpretação da sintaxe em um modelo de feixe adequado e extrair formas normais únicas apropriadas ".

Em geral, porém, acho que a teoria das categorias geralmente não é aplicada para provar teoremas profundos em linguagens de programação (das quais não existem tantas), mas oferece uma estrutura conceitual que é frequentemente útil (por exemplo, no exemplo acima, o idéia da semântica (pré) do feixe).

Um exemplo histórico importante é a sugestão de Eugenio Moggi de que a noção de mônada (que é básica e onipresente na teoria das categorias) poderia ser usada como parte de uma explicação semântica dos efeitos colaterais nas linguagens de programação (por exemplo, estado, não determinismo). Isso também inspirou alguma reflexão sobre a sintaxe das linguagens de programação, por exemplo, levando diretamente para a "classe de classe Monad" em Haskell (usada para encapsular efeitos).

Mais recentemente (na década passada), essa explicação dos efeitos em termos de mônadas foi revisada do ponto de vista da antiga conexão (estabelecida pelos teóricos das categorias, nos anos 60) entre mônadas e teorias algébricas: veja Martin Hyland e John Power. , "O entendimento teórico da categoria da álgebra universal: teorias de Lawvere e mônadas" . A idéia é que a visão monádica dos efeitos seja compatível com a visão algébrica (de certa forma mais atraente) dos efeitos, em que os efeitos (por exemplo, armazenamento) podem ser explicados em termos de operações (por exemplo, "pesquisa" e "atualização") e equações associadas (por exemplo, idempotência de atualização). Paul-André Melliès escreveu um artigo recente sobre essa conexão: "A condição de Segal encontra efeitos computacionais", que também se apóia fortemente em idéias provenientes da "teoria das categorias superiores" (por exemplo, a noção de "estrutura Yoneda" como uma maneira de organizar a semântica pré-posterior).

Outra classe de exemplos relacionados vem da lógica linear . Logo após sua introdução por Jean-Yves Girard nos anos 80 (com o objetivo de uma melhor compreensão da lógica construtiva), foram estabelecidas sólidas conexões com a teoria das categorias. Para alguma explicação sobre essa conexão, consulte John Baez e Mike Stay, "Física, Topologia, Lógica e Computação: Uma Pedra de Roseta" .

Por fim, essa resposta seria incompleta sem referência ao blog iluminador do sigfpe "Um bairro do infinito" . Em particular, você pode conferir "Uma ordenação parcial de alguma teoria de categoria aplicada a Haskell" .

Computação Quântica

Uma área muito interessante é a aplicação de várias categorias monoidais à computação quântica. Alguns podem argumentar que isso também é física, mas o trabalho é feito por pessoas nos departamentos de ciência da computação. Um artigo inicial nesta área é uma semântica categórica de protocolos quânticos de Samson Abramsky e Bob Coecke; muitos artigos recentes de Abramsky e Coecke e outros continuam trabalhando nesse sentido.

Neste corpo de trabalho, os protocolos quânticos são axiomatizados como (certos tipos de) categorias fechadas compactas. Essas categorias têm uma bela linguagem gráfica em termos de diagramas de seqüência de caracteres (e faixa de opções). As equações na categoria correspondem a certos movimentos das cordas, como endireitar uma corda emaranhada, mas não atada, que por sua vez corresponde a algo significativo na mecânica quântica, como um teletransporte quântico.

A abordagem categórica oferece uma visão lógica de alto nível sobre o que normalmente envolve cálculos de nível muito baixo.

Teoria de Sistemas

$F$$F$

Transformações de gráfico

$G_1,G_2$$P$$e_1:P\to G_1$$e_2:P\to G_2$$G_1$$G_2$$G_1$$G_2$$P$

$(L, K, R)$$L$$R$$K$$l:K\to L$$r:K\to R$$L\setminus K$$R\setminus K$$d$$K$$D$$d$$l$$G$$d$$k$

Linguagens de programação (via MathOverflow)

Existem muitas aplicações da teoria das categorias no design de linguagens de programação e na teoria das linguagens de programação. Respostas extensas podem ser encontradas no MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .

Bigraphs - Cálculo de processos

Finalmente, há os bigrafs de Milner , uma estrutura geral para descrever e raciocinar sobre sistemas de agentes interagindo. Pode ser visto como uma estrutura geral para raciocinar sobre álgebras de processos e suas teorias estruturais e comportamentais. A abordagem também se baseia em pushouts.

Eu já estou implicitamente assumindo que não existem aplicações na Teoria A encontradas até agora, mas se você tiver algumas delas, isso é ainda melhor para mim!

• Meu entendimento é que a teoria das espécies de Joyal é usada relativamente amplamente na combinatória enumerativa, como uma generalização das funções geradoras que, adicionalmente, mostram como permutar as coisas, além de quantas existem.

• Pippenger aplicou a dualidade de Stone para relacionar idiomas regulares e variedades de semigrupos. Jeandel introduziu autômatos topológicos para aplicar essas idéias para fornecer contas unificadas (e provas!) Para autômatos quânticos, probabilísticos e comuns.

• Roland Backhouse deu caracterizações abstratas de algoritmos gananciosos por meio de conexões de Galois com o semi-tropical.

Em uma veia muito mais especulativa, Noam mencionou modelos de feixe. Eles caracterizam abstratamente a técnica sintática das relações lógicas, que provavelmente é uma das técnicas mais poderosas da semântica. Nós os usamos principalmente para provar resultados de inexpressibilidade e consistência, mas isso deve ser interessante para os teóricos da complexidade, pois é um bom exemplo de uma técnica de prova prática não natural (no sentido de Razborov / Rudich). (No entanto, as relações lógicas geralmente são projetadas com muito cuidado para garantir que sejam relativizadas - como designers de linguagem, queremos garantir aos programadores que as chamadas de função são caixas pretas!

Edição: Vou continuar especulando, a pedido de Ryan. Pelo que entendi, uma prova natural é mais ou menos a mesma da tentativa de definir uma invariante indutiva da estrutura de um circuito, sujeita a várias condições sensíveis. Idéias semelhantes também são (sem surpresa) bastante comuns em linguagens de programação, quando você tenta definir invariantes mantidos indutivamente por um termo de cálculo lambda (por exemplo, para provar a segurança do tipo). 1

$A \to B$$A \to B$$A$

$A \to B$$A$$B$. Observe que não existe um invariante indutivo único - definimos toda uma família de invariantes por recursão sobre a estrutura da entrada e usamos outros meios para mostrar que todos os termos estão dentro desses invariantes. Em termos de prova, essa é uma técnica muito mais forte e é por isso que permite provar resultados de consistência.

A conexão com as roldanas decorre do fato de que muitas vezes precisamos raciocinar sobre termos abertos (ou seja, termos com variáveis ​​livres) e, portanto, precisamos distinguir entre ficar preso devido a erros e ficar preso devido à necessidade de reduzir uma variável. As polias surgem ao considerar as reduções do cálculo lambda como definindo os morfismos de uma categoria cujos termos são os objetos (ou seja, a ordem parcial induzida pela redução) e, em seguida, considerando os functores dessa categoria em conjuntos (ou seja, predicados). Jean Gallier escreveu alguns artigos interessantes sobre isso no início dos anos 2000, mas duvido que sejam legíveis, a menos que você já tenha assimilado uma boa quantidade de cálculo lambda.

Existem muitos exemplos, o primeiro que vem à mente é o uso da teoria de categorias por Alex Simpson para provar propriedades de linguagens de programação, veja, por exemplo, " Adequação computacional para tipos recursivos em modelos de teoria intuicionista de conjuntos ", Anais da lógica pura e aplicada 130: 207-275, 2004. Embora o título mencione a teoria dos conjuntos, a técnica é teórica por categoria. Veja a home page de Alex para mais exemplos.

Eu acho que você está fazendo duas perguntas sobre aplicabilidade, tipo A e tipo B separadamente.

Como você observa, existem muitas aplicações substantivas da teoria de categorias para tópicos do tipo B: semântica de linguagens de programação (mônadas, categorias fechadas cartesianas), lógica e provabilidade (topoi, variedades de lógica linear).

No entanto, parece haver poucas aplicações substantivas à teoria A (algoritmos ou complexidade).

Existem alguns usos em objetos elementares, como a descrição de categorias de autômatos ou objetos combinatórios (gráficos, sequências, permutações etc.). Mas estes parecem não explicar uma compreensão mais profunda da teoria ou dos algoritmos da linguagem.

Especulativamente, pode haver uma incompatibilidade entre as estratégias atuais da teoria da categoria e dos assuntos da teoria A:

• A estratégia central da teoria das categorias é lidar com a igualdade (quando as coisas são iguais e quando são diferentes e como elas se mapeiam).

• Para a teoria da complexidade, a estratégia principal é a redução e o estabelecimento de limites (alguém poderia pensar que uma redução é como uma flecha, mas não acho que nada além dessa semelhança superficial tenha sido estudado).

• Para algoritmos, não existe uma estratégia abrangente além do pensamento combinatório inteligente ad hoc. Para certos domínios, eu esperaria que houvesse uma exploração proveitosa (algoritmos para álgebras?), Mas ainda não a vi.

As aplicações "TCS-A" que me vêm à mente são as espécies combinatórias da Joyal (generalizações de séries de potência para functores, a fim de descrever objetos combinatórios como árvores, conjuntos, multisets etc.) e a formalização de "salto de jogo" criptográfico usando recursos relacionais, lógica probabilística de Hoare (Easycrypt, Certicrypt, trabalho de Andreas Lochbihler). Embora as categorias não apareçam diretamente nas últimas, elas foram fundamentais no desenvolvimento das lógicas subjacentes (por exemplo, mônadas).

PS: Desde que meu nome foi mencionado na primeira resposta: o uso de fibrações de grupóides para mostrar a impossibilidade de sobrevivência de um certo axioma na teoria dos tipos de Martin-Löf por Thomas Streicher e eu também pode ser considerado um uso "sólido" da teoria das categorias (embora em lógica ou "TCS-B").

O livro mais recente, Seven Sketches in Compositionality, lista várias aplicações da teoria das categorias em ciência da computação e engenharia. Notável o capítulo sobre bancos de dados em que os autores descrevem a consulta, combinação, migração e evolução de bancos de dados com base em um modelo categórico. Os autores levaram isso adiante e desenvolveram a Linguagem de consulta categórica (CQL) e um ambiente de desenvolvimento integrado (IDE) com base em seu modelo categórico de bancos de dados.