Quando (ou deveria) o CS teórico se importar com as provas intuicionistas?

Pelo que entendi (que é muito pouco, por favor, corrija-me onde erro!), A teoria das linguagens de programação geralmente se preocupa com provas "intuicionistas". Na minha própria interpretação, a abordagem exige que levemos a sério as consequências da computação na lógica e na provabilidade. Uma prova não pode existir a menos que exista um algoritmo construindo as conseqüências das hipóteses. Podemos rejeitar como axioma o princípio do meio excluído, por exemplo, porque ele exibe algum objeto, que é ou , não construtivamente.¬ $X$$\lnot X$

A filosofia acima pode levar-nos a preferir provas intuicionisticamente válidas sobre as que não são. No entanto, eu não vi nenhuma preocupação sobre o uso real da lógica intuicionista em trabalhos em outras áreas do CS teórico. Parecemos felizes em provar nossos resultados usando a lógica clássica. Por exemplo, alguém pode imaginar usar o princípio do meio excluído para provar que um algoritmo está correto. Em outras palavras, nos preocupamos e levamos a sério um universo limitado em termos computacionais em nossos resultados, mas não necessariamente em nossas provas desses resultados.

1. Os pesquisadores do CS teórico estão sempre preocupados em escrever provas intuicionisticamente válidas? Eu poderia facilmente imaginar um subcampo da ciência da computação teórica que busca entender quando os resultados do TCS, especialmente os algorítmicos, se mantêm na lógica intuicionista (ou, mais interessante, quando não o são). Mas ainda não encontrei nenhum.

2. Existe algum argumento filosófico que eles deveriam? Parece que se pode afirmar que os resultados da ciência da computação devem ser provados intuicionisticamente quando possível, e devemos saber quais resultados requerem, por exemplo, PEM. Alguém já tentou argumentar assim? Ou talvez exista um consenso de que essa questão não seja muito importante?

3. Como uma questão paralela, estou curioso para conhecer exemplos de casos em que isso realmente importa: Existem resultados importantes do TCS que se mantêm na lógica clássica, mas não na lógica intuicionista? Ou suspeito de não se sustentar na lógica intuicionista.

Desculpas pela suavidade da pergunta! Pode exigir reformulação ou reinterpretação após a audição dos especialistas.

Como eu disse nos comentários, a lógica intuicionista não é o ponto principal. O ponto mais importante é ter uma prova construtiva. Penso que a teoria do tipo de Martin-Löf é muito mais relevante para a teoria da linguagem de programação do que a lógica intuicionista e há especialistas que argumentaram que o trabalho de Martin-Löf é a principal razão do renascimento do interesse geral em matemática construtiva.

A interpretação computacional da construtividade é uma perspectiva possível, mas não é a única. Devemos ter cuidado aqui quando queremos comparar provas construtivas com provas clássicas. Embora ambos possam usar os mesmos símbolos, o que eles significam é diferente.

É sempre bom lembrar que as provas clássicas podem ser traduzidas para provas intuicionistas. Em outras palavras, em certo sentido, a lógica clássica é um subsistema da lógica intuicionista. Portanto, você pode realizar (digamos, usando funções computáveis) provas clássicas em um sentido. Por outro lado, podemos pensar na matemática construtiva como um sistema matemático no cenário clássico.

No final, formalismos, clássicos ou construtivos, são ferramentas para expressarmos declarações. Tomando um teorema clássico e tentando prová-lo construtivamente sem essa perspectiva, não faz muito sentido IMHO. Quando digo classicamente, quero dizer algo diferente do que digo A ∨ B construtivamente. Você pode argumentar qual "deveria" ser o verdadeiro significado de " ∨ ", mas acho que isso não é interessante se não estivermos discutindo o que queremos expressar em primeiro lugar. Queremos dizer (pelo menos) um deles e sabemos qual? Ou simplesmente queremos dizer que um deles é válido?$A \lor B$$A \lor B$$\lor$

Agora, com essa perspectiva, se queremos provar uma afirmação como e queremos relacionar isso a um mapeamento de x a algum y satisfatório φ ( x , y ), então a melhor maneira de Express pode ser o caminho construtivo. Por outro lado, se apenas nos importamos com a existência de y e não nos preocupamos em como encontrá-los, o modo clássico provavelmente faria mais sentido. Quando você prova a declaração de forma construtiva, também está criando implicitamente um algoritmo para encontrar y de $\forall x \ \exists y \ \varphi(x,y)$$x$$y$$\varphi(x,y)$$y$$y$$x$. Você pode fazer o mesmo explicitamente com uma fórmula mais complicada, como "o algoritmo possui a propriedade de todos os x , φ ( x , A ( x ) ) " onde A é um algoritmo explicitamente determinado. Se não está claro por que alguém pode preferir a maneira construtiva de expressar isso, pense nas linguagens de programação como uma analogia: você pode escrever um programa para o algoritmo MST da Kruskal na linguagem assembly x86, onde você precisa se preocupar com muitos problemas secundários ou você pode escrever um programa em Python.$A$$x$$\varphi(x,A(x))$$A$

Agora, por que não usamos a lógica intuicionista na prática? Existem várias razões. Por exemplo, a maioria de nós não é treinada com essa mentalidade. Também encontrar uma prova clássica de uma afirmação pode ser muito mais fácil do que encontrar uma prova construtiva dela. Ou podemos nos preocupar com detalhes de baixo nível que estão ocultos e não acessíveis em um cenário construtivo (veja também lógica linear ). Ou podemos simplesmente estar desinteressados ​​em obter o material extra que vem com uma prova construtiva. E, embora existam ferramentas para extrair programas de provas, essas ferramentas geralmente precisam de provas muito detalhadas e não foram amigáveis ​​o suficiente para o teórico geral. Em suma, muita dor para pouquíssimo benefício.

$\Pi^0_2$$PA$$PA$$PA$

Lembro que Douglas S. Bridges, na introdução de seu livro de teoria da computabilidade, argumentou que deveríamos provar nossos resultados de forma construtiva. Ele dá um exemplo que IIRC é essencialmente o seguinte:

Suponha que você trabalhe para uma grande empresa de software e que seu gerente solicite um programa para resolver um problema. Seria aceitável retornar com dois programas e informar ao seu gerente uma dessas duas soluções corretamente, mas não sei qual?

No final, devemos ter em mente que, embora usemos os mesmos símbolos para lógicas clássica e intuicionista, esses símbolos têm significados diferentes, e o que usar depende do que queremos expressar.

Para sua última pergunta, acho que o teorema de Robertson-Seymour seria um exemplo de um teorema que sabemos que é verdadeiro classicamente, mas não temos nenhuma prova construtiva dele. Veja também

• Existem provas de existência de algoritmos não construtivos?

Vale a pena pensar em POR QUE a lógica intuiscionista é a lógica natural da computação, pois muitas vezes as pessoas se perdem nos detalhes técnicos e não conseguem entender a essência do problema.

Muito simplesmente, a lógica clássica é uma lógica de informação perfeita: presume-se que todas as afirmações no sistema sejam conhecidas ou conhecíveis como inequivocamente verdadeiras ou falsas.

A lógica intuiscionista, por outro lado, tem espaço para afirmações com valores de verdade desconhecidos e incognoscíveis. Isso é essencial para o cálculo, pois, graças à indecidibilidade da rescisão no caso geral, nem sempre será certo qual será o valor de verdade de algumas declarações ou mesmo se um valor de verdade pode ou não ser atribuído a determinadas declarações. .

$\neg\neg P \implies P$

Na minha opinião, essas razões "semânticas" são uma motivação muito mais importante para o uso da lógica intuiscionista para a computação do que quaisquer outras razões técnicas que se possa reunir.

Funções hash criptográficas do mundo real, como MD5 e SHA, são sem chave. Como tal, torna bastante difícil aplicar técnicas de criptografia teórica para raciocinar sobre sua segurança. O motivo simples: para qualquer função hash sem chave, existe um programa / adversário muito pequeno que gera uma colisão sob essa função hash; ou seja, um programa que tenha essa colisão - que deve existir! - codificado.

O artigo de Phil Rogaway, Formalizando a ignorância humana: hash resistente a colisões sem as chaves lida com esse problema. Nele, ele mostra que alguns teoremas muito padronizados para funções de hash com chave (como o paradigma de construção de Merkle-Damgård e hash-então-sinal) podem ser adaptados e comprovados com declarações de teoremas "amigáveis ​​ao intuicionista" aplicáveis ​​a funções de hash não codificadas.

aqui está um bom capítulo sobre lógica intuicionista de um livro on-line abrangente, Logic for Computer Science , 300pp. [1] sec 9.5, p210, resumo da p220:

A lógica intuicionista surgiu do movimento construtivista da matemática que rejeitava as provas de existência não construtivas ou aquelas baseadas na lei do meio excluído. Recentemente, uma conexão entre matemática intuicionista e programação surgiu da observação de que proposições e tipos (no sentido de programação) são equivalentes. O desenvolvimento de algoritmos nesse sistema formal, que é baseado na dedução natural, consiste em escrever uma especificação em notação lógica e, em seguida, considerar isso como um tipo, provando que não é vazio. Como a lógica subjacente é construtiva, a prova, se for possível,

outra perspectiva próxima vem do TCSist Andrej Bauer escrevendo sobre "Matemática e computação; matemática para computadores" [2], que propõe basicamente que "a matemática intuicionista é boa para a física". a apresentação é principalmente em termos de física, mas para aqueles que consideram o CS fortemente associado à física, a ideologia geralmente é levada ao TCS.

Interpretação computacional. Essa é a interpretação da lógica intuicionista comumente apresentada na ciência da computação. Vemos todos os conjuntos como representados por estruturas de dados adequadas - um ponto de vista razoável para um cientista da computação. Então, uma afirmação é considerada verdadeira se existe um programa (evidência computacional) testemunhando sua verdade.

[1] Lógica para ciência da computação, Reeves e Clark

[2] Matemática intuicionista para a física Bauer