O que é o análogo Curry-Howard para lógicas lineares?

Conforme definido pela Wikipedia,

(A correspondência de Curry-Howard) é uma generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberta pela primeira vez pelo matemático americano Haskell Curry e pelo lógico William Alvin Howard.

Relacionado a ele, está o cubo λ, que é uma representação gráfica dos possíveis eixos de refinamento, de tipos simples ao cálculo de construções, que tem uma interpretação lógica:

Até onde eu sei, a correspondência de Curry-Howard é uma conexão entre a teoria dos tipos e a lógica clássica. Minha pergunta é: existe alguma correspondência analógica entre sistemas de tipos e lógicas lineares ?

Você pode impor requisitos semelhantes em seu sistema de tipos, o que significa exigir que os objetos nunca sejam destruídos nem duplicados. Para um exemplo de aplicação prática, consulte Tipos lineares podem mudar o mundo! por Philip Wadler, que especifica regras de digitação para isso. Também mostra como um sistema de tipos pode combinar tipos lineares e não lineares.

Para uma aplicação prática disso, dê uma olhada no std::unique_ptrC ++. Aqui, a linearidade garante que a desalocação sempre ocorra exatamente uma vez.

Em uma linguagem funcional, a linearidade também oferece a possibilidade de atualizações destrutivas (que parecem puras para o programador). No entanto, na prática, parece que as mônadas são uma abordagem mais comum para resolver esse problema.

Atualização : notei que, na tabela de Trinitarianismo Computacional do NLab, a ausência de contração em uma lógica (isto é, ser incapaz de duplicar uma suposição) corresponde ao Teorema da Não-Clonagem da mecânica quântica. Eu (infelizmente) não entendo as implicações disso, mas achei que você poderia achar interessante.

A lógica linear corresponde a um sistema de tipos para um cálculo de processo (uma variante do π-cálculo interno ), em que:

• provas correspondem a processos ;
• as proposições correspondem aos tipos de sessão (protocolos de comunicação).

Esta é uma área de pesquisa bastante ativa. Enquanto as pessoas esperavam uma correspondência entre a lógica linear e algum modelo de simultaneidade desde o início da lógica linear por Girard [1987] , encontrar algo que seja satisfatório tanto da perspectiva da modelagem lógica quanto da simultaneidade tem sido um tanto esquivo.

Aqui está um resumo dos principais desenvolvimentos até agora.

• Abramsky [1994] e Bellin e Scott [1994] propuseram a primeira correspondência "Provas como processos", em que proposições lineares são tipos de canais lineares em um cálculo de processo. Por exemplo, a proposição$A \otimes B$ é interpretado como o tipo de canal "send $A$ e $B$"; é usado para digitar um processo que usa um canal para emitir uma mensagem incluindo algo do tipo $A$ e $B$(um par, se desejar), respectivamente, e o canal não deve mais ser usado. A idéia principal é que a regra de corte da lógica linear possa ser usada para digitar a execução paralela de dois processos que se comunicam através de um canal privado. A verificação de dualidade realizada pela regra de corte na lógica linear corresponde à verificação de que os dois processos usam o canal privado compartilhado de maneiras compatíveis.
• A idéia de dualidade também inspirou várias disciplinas de digitação para cálculos de processos, principalmente tipos lineares e tipos de sessão, mas o vínculo direto com a lógica linear foi perdido. Os tipos de sessão, em particular, por Honda [1993] , descrevem os protocolos de comunicação e sua aplicabilidade tornou-se evidente logo: a idéia gerou uma área de pesquisa.
• Sete anos depois, depois que a Honda desenvolveu tipos de sessões, Caires e Pfenning [2010] descobriram que proposições na lógica linear intuicionista podem ser interpretadas como tipos de sessões. Por exemplo, a proposição$A \otimes B$ é interpretado como o protocolo "send $A$ e depois proceda como $B$". Essa descoberta rejuvenesceu a linha de pesquisa" Provas como processos ": existem muitos artigos publicados sobre esse assunto na última década. Graças aos fundamentos lógicos, podemos importar idéias da lógica para estender a disciplina de digitação dos tipos de sessão .
• Wadler [2014] reformulou a correspondência com tipos de sessão para lógica linear clássica e formalizou a primeira conexão entre uma apresentação padrão de tipos de sessão para uma linguagem funcional e lógica linear.
• Há uma "questão" compartilhada por todos os trabalhos citados acima: enquanto o lado lógico linear é o esperado, o lado do cálculo do processo não é, tanto sintática quanto semanticamente. Por exemplo, uma discrepância notável é que a composição paralela ($P|Q$) não é um construtor de termo independente, porque não possui uma regra correspondente para raciocinar sobre ele diretamente na lógica linear. Esse problema foi resolvido em [Kokke et al., 2019] (exoneração de responsabilidade: sou um dos autores), reformulando de forma conservadora as regras para$\otimes$, corte e misture. Isso dá origem a novas transformações de prova, que acabam correspondendo à semântica observacional esperada do cálculo π.

Se você está procurando alguns documentos para começar, eu começaria a partir de [Wadler, 2014] e depois de [Kokke et al., 2019] (para ver o sistema mais recente).