Como devo pensar em redes de prova?

Em sua resposta a essa pergunta , Stephane Gimenez me indicou um algoritmo de normalização em tempo polinomial para provas em lógica linear. A prova no artigo de Girard usa redes de prova, que são um aspecto da lógica linear de que eu realmente não sei muito.

Agora, eu tentei ler artigos sobre redes de prova antes (como as anotações de Pierre-Louis Curien sobre elas), mas eu realmente não as entendi. Então, minha pergunta é: como devo pensar sobre eles? Por "como pensar sobre eles", quero dizer tanto a intuição informal por trás deles (por exemplo, como eles se comportam computacionalmente ou como estão relacionados a sequências), e também quais teoremas sobre eles devo provar para eu realmente obtê-los.

Ao responder a essa pergunta, você pode assumir: (1) conheço bem a teoria da prova da lógica linear (incluindo coisas como a prova da eliminação de cortes e também de forma focalizada); (2) sua semântica categórica em termos de espaços de coerência ou via convolução do dia, e (3) os rudimentos muito básicos da construção do Gd.

As redes de prova são interessantes essencialmente por três razões:

1) IDENTIDADE DE PROVAS. Eles fornecem uma resposta para o problema "quando duas provas são iguais"? No cálculo sequencial, você pode ter muitas provas diferentes da mesma proposição, que diferem apenas porque o cálculo sequencial força uma ordem entre as regras de dedução, mesmo quando isso não é necessário. Obviamente, pode-se adicionar uma relação de equivalência nas provas de cálculo sequenciais, mas é preciso mostrar que a eliminação de corte se comporta adequadamente nas classes de equivalência, e também é necessário recorrer ao módulo de reescrita, que é muito mais técnico do que a reescrita simples. As redes de prova resolvem o problema de lidar com classes de equivalência, fornecendo uma sintaxe em que cada classe de equivalência é recolhida em um único objeto. De qualquer forma, essa situação é um pouco idealista, pois, por muitas razões, as redes de prova geralmente são estendidas com alguma forma de equivalência.

2) NENHUMA ETAPA COMUNTATIVA DE ELIMINAÇÃO. A eliminação de cortes em redes de prova tem um sabor bem diferente do que nos cálculos sequenciais porque as etapas comutativas de eliminação de cortes desaparecem. O motivo é que, nas redes de prova, as regras de dedução são conectadas apenas por sua relação causal. Os casos comutativos são gerados pelo fato de que uma regra pode ser oculta por outra regra causalmente não relacionada. Isso não pode acontecer em redes de prova, onde regras causalmente não relacionadas estão distantes. Como a maioria dos casos de eliminação de cortes é comutativa, obtém-se uma impressionante simplificação da eliminação de cortes. Isso tem sido particularmente útil para estudar cálculos lambda com substituições explícitas (porque exponenciais = substituições explícitas). Novamente, essa situação é idealizada, pois algumas apresentações de redes de prova exigem etapas comutativas. Contudo,

3) CRITÉRIOS DE CORRECÇÃO. As redes de prova podem ser definidas pela tradução de provas de cálculo sequenciais, mas geralmente um sistema de redes de prova não é aceito como tal, a menos que seja fornecido com um critério de correção, isto é, um conjunto de princípios teóricos para gráficos que caracterizam o conjunto de gráficos obtidos pela tradução de uma prova. prova de cálculo sequencial. A razão para exigir um critério de correção é que a linguagem gráfica livre gerada pelo conjunto de construtores de redes de prova (chamados links) contém "muitos gráficos", no sentido de que alguns gráficos não correspondem a nenhuma prova. A relevância da abordagem dos critérios de correção é geralmente completamente incompreendida. É importante porque fornece definições não indutivas do que é uma prova, fornecendo perspectivas surpreendentemente diferentes sobre a natureza das deduções. O fato de a caracterização não ser indutiva é geralmente criticado, enquanto é exatamente o que é interessante. Obviamente, não é facilmente passível de formalização, mas, novamente, esse é seu ponto forte: as redes de prova fornecem insights que não estão disponíveis na perspectiva indutiva usual de provas e termos. Um teorema fundamental para redes de prova é o teorema da seqüencialização, que diz que qualquer gráfico que satisfaça o critério de correção pode ser decomposto indutivamente como prova de cálculo sequencial (traduzindo de volta para o gráfico correto).

Permitam-me concluir que não é preciso dizer que as redes de prova são uma versão clássica e linear da dedução natural. O ponto é que eles resolvem (ou tentam resolver) o problema da identidade das provas e que a dedução natural resolve com êxito o mesmo problema para uma lógica intuicionista mínima. Mas redes de prova também podem ser feitas para sistemas intuicionistas e para sistemas não lineares. Na verdade, eles funcionam melhor para sistemas intuicionistas do que para sistemas clássicos.

Vamos chamar uma lógica "simétrica", onde uma ( "não A") suposição significa o mesmo que provando e uma prova de significa o mesmo que um pressuposto de . A lógica clássica e a lógica linear são simétricas nesse sentido. A lógica intuicionista não é.A - $-A$$A$$-A$$A$

Girard notou que a dedução natural é assimétrica exatamente dessa maneira. É por isso que combina com a lógica intuicionista. As redes de prova representam uma tentativa de Girard de inventar uma forma simétrica de dedução natural.

A melhor introdução a essas idéias está nas "provas e tipos" de Girard. Se você trabalha com o sistema de dedução natural e cálculo sequencial para o fragmentar a lógica intuicionista, e lê atentamente as seções 5.3 e 5.4 que estabelecem um homomorfismo do cálculo sequencial à dedução natural, você aprecia o que é dedução natural. tudo sobre. Então o Apêndice de Lafont introduz redes de prova no mesmo espírito. É mais ou menos simples estender o homomorfismo das seções 5.3-4 para um entre cálculo de seqüência lógica linear e redes de prova de lógica linear (pelo menos para o fragmento multiplicativo).$\land\to$

Uma coisa que talvez seja desnecessariamente confusa sobre o tratamento de Girard é que ele dispensa sequências de dois lados e usa sequências de um lado no interesse da economia. Para o cálculo sequencial, isso funciona mais ou menos bem. Mas, quando a mesma economia é aplicada à dedução natural, as coisas parecem estranhas. Uma rede de prova é, portanto, uma "prova de dedução natural" de uma disjunção de fórmulas, sem nenhuma premissa . A dedução do tipo é transformada em uma rede de prova do tipo . Se isso o confunde, você pode escrever um cálculo seqüencial de dois lados e uma forma de suposição-conclusão de redes de prova. Isso pode esclarecer as coisas.⊢ y ⊥ , $\Gamma \vdash A$$\vdash \Gamma^\perp, A$

Algo que perdi na minha resposta original: Redes de prova são uma maneira de escrever provas, e sabemos que provas são programas. Portanto, redes de prova também são uma maneira de escrever programas.

A notação funcional tradicional para escrever programas é assimétrica, assim como a dedução natural. Assim, as redes de prova apontam para uma maneira de escrever programas de forma simétrica . É assim que o cálculo do processo entra em cena.

Outra maneira de representar a simetria é através da programação lógica, que explorei em dois artigos: uma base tipificada para programas de lógica direcional e aspectos de ordem superior da programação lógica

Eu me concentro em como as redes de prova estão relacionadas ao cálculo sequencial, deixando coisas mais dinâmicas.

Redes de prova abstraem provas de cálculo sequenciais: uma rede de provas representa um conjunto de provas de cálculo sequenciais. As redes de prova esquecem diferenças sem importância entre as provas de cálculo sequenciais (como qual fórmula é decomposta abaixo da qual). O teorema importante aqui é "sequencialização", que converte uma rede de provas em uma prova de cálculo sequencial.

Isso está relacionado principalmente à parte "como eles se comportam computacionalmente" da sua pergunta. Uma maneira de entender bem as redes de prova da perspectiva computacional é olhando para interpretações um pouco mais concretas (por exemplo, processo algébrico).

Você pode estar interessado no seguinte:

• O artigo de Abramsky (a seção CLL sobre Expressões de Prova): Interpretações Computacionais da Lógica Linear . Este artigo também apresenta alguns resultados próximos aos correspondentes para redes de prova, portanto, isso pode ajudar no segundo aspecto da sua pergunta.

• O artigo de Honda e Laurent, que mostra como um tipo específico de Redes de prova, chamado Redes de prova polarizada, corresponde aos processos de cálculo Pi, e mencionado acima por Martin Berger: Uma correspondência exata entre um cálculo pi digitado e a prova polarizada redes

• (aqui anuncio descaradamente meu próprio trabalho) O rascunho: Redes de prova em forma algébrica de processo

Existem também alguns trabalhos relacionados a redes de prova e cálculo lambda, que também fornecem intuições substanciais. Por exemplo, o seguinte por Delia Kesner e Stéphane Lengrand:

• Operadores de recursos para cálculo λ

Você também pode se interessar por esse tipo de trabalho (muito orientado para aspectos teóricos), que se baseia em estruturas de prova para provar em detalhes a propriedade Normalização forte da LL, de Michele Pagani e Lorenzo Tortora de Falco.

• Propriedade de normalização forte para lógica linear de segunda ordem (este artigo contém um bom mapa de teoremas importantes).

Em geral, quais teoremas devem ser estudados? Bem, eu dificilmente sou uma autoridade, mas você pode querer olhar para "Sequencialização" (relacionando redes de prova e provas sequenciais; veja o artigo original do TCS sobre LL) e a forte prova de normalização (bastante envolvida, como esperado, mas muito importante). Os teoremas de PN estão relacionados a ele [ou, usados ​​para provar isso]).

Se você está familiarizado com o foco, também pode estar interessado neste artigo de Andreoli:

• Redes de focagem e de prova na lógica linear e não comutativa

Espero que isto ajude. Novamente, essas referências são realmente não exaustivas.

melhor, Dimitris

Recentemente, houve um trabalho interessante para tornar mais estreita a relação entre a rede de prova e os cálculos focados, usando variantes "multi-focadas", nas quais você pode ter vários furos esquerdos simultâneos, e estudando provas "com foco máximo". Se você escolher o cálculo corretamente, as provas com foco máximo podem corresponder às redes de prova MLL ou, na lógica clássica, às provas de expansão ( O Isomorfismo Entre Provas de Expansão e Provas Sequenciais Multifocadas, Kaustuv Chaudhuri, Stefan Hetzl e Dale Miller, 2013)

Você pode verificar meu artigo " Uma pesquisa de redes e matrizes de prova para lógicas subestruturais ".

Abstrato:

Este artigo é uma pesquisa de dois tipos de esquemas de prova "compactados", o \ emph {método de matriz} e \ emph {redes de prova}, aplicados a uma variedade de lógicas que variam ao longo da hierarquia subestrutural, desde a clássica até a sistema Lambek não-associativo. É fornecido um novo tratamento de redes de prova para o último. As descrições de redes e matrizes de prova são fornecidas em uma notação uniforme com base em seqüências, para que as propriedades dos esquemas para as várias lógicas possam ser facilmente comparadas.