Passeios casuais em torno de provas

Hoje, Ryan Williams publicou um artigo no arXiv (publicado anteriormente no SIGACT News) contendo uma versão menos técnica de sua recente técnica de limite inferior do ACC .

Minha pergunta não é sobre a técnica em si (é claro que merece imensos elogios), mas é sobre o estilo do artigo. No resumo, ele escreve:

A prova será descrita da perspectiva de alguém tentando descobri-la.

Impressionante! Na seção Background, ele adiciona:

Este artigo é uma discussão sobre como descobrir a prova - um passeio casual em torno dela. Nem todos os detalhes serão fornecidos, mas você verá de onde vieram todas as peças e como elas se encaixam. O caminho estará cheio de minhas próprias intuições tendenciosas sobre a teoria da complexidade - o que eu acho que deveria e não deveria ser verdade, e por quê. Grande parte dessa intuição pode estar errada; no entanto, posso dizer que me levou a uma direção produtiva em pelo menos uma ocasião.

Isso é incrível e é a primeira vez que eu o vejo. Sempre me perguntei por que os autores de artigos não escrevem como chegaram à prova, incluindo as abordagens fracassadas que tentaram antes de chegar à pista que levou à solução. Quando vi o artigo de Ryan no arXiv, fiquei muito motivado a lê-lo. Considero um artigo revolucionário deste ponto de vista. Na maioria das vezes, a única coisa que você pode fazer com um papel é verificar sua exatidão.

A questão é a seguinte:

• você conhece outros artigos no TCS em que um resultado inovador é apresentado em um "tour casual" em vez de uma série de lemas técnicos?

Estou falando de publicações em periódicos, não de posts em blogs ou relatórios técnicos.

Também o marquei como grande lista , com a esperança de que realmente seja.

Existe um artigo (2001) de estilo semelhante de Lov Grover, que descreve o caminho para o seu inovador algoritmo de busca quântica (1996).

Tim Gowers é um fã desse tipo de coisa. Veja especificamente sua exposição do método de aproximações de Razborov .

Em sua introdução, Gowers faz referência ao meu artigo expositivo sobre forçar , que é uma tentativa (não totalmente bem-sucedida) de fazer a mesma coisa para forçar. Forçar é normalmente pensado como uma técnica na lógica e na teoria dos conjuntos, mas ocasionalmente chega ao TCS. Ele aparece no estudo da aritmética limitada e da complexidade da prova proposicional (Krajíček e Takeuti são dois pesquisadores que buscaram essa conexão), e o conceito de um oráculo genérico está relacionado ao conceito de filtro genérico.

(Isso começou como um comentário e ficou muito longo).

Você pode apreciar o artigo de William Thurston On Proof and Progress in Mathematics .

Em algum sentido, a matemática tem uma linguagem comum: uma linguagem de símbolos, definições técnicas, cálculos e lógica. Essa linguagem transmite com eficiência alguns, mas não todos, modos de pensamento matemático. Os matemáticos aprendem a traduzir certas coisas quase inconscientemente de um modo mental para outro, para que algumas afirmações se tornem claras rapidamente. [...]

As pessoas familiarizadas com as maneiras de fazer as coisas em um subcampo reconhecem vários padrões de afirmações ou fórmulas como expressões idiomáticas ou circunlocução para certos conceitos ou imagens mentais. Mas para pessoas que ainda não estão familiarizadas com o que está acontecendo nos mesmos padrões não são muito esclarecedoras; eles são frequentemente até enganosos. O idioma não está vivo, exceto para quem o usa. [...]

Nós, matemáticos, precisamos nos esforçar muito mais na comunicação de idéias matemáticas. Para conseguir isso, precisamos prestar muito mais atenção na comunicação não apenas de nossas definições, teoremas e provas, mas também de nossas maneiras de pensar. Precisamos apreciar o valor de diferentes maneiras de pensar sobre a mesma estrutura matemática. Precisamos focar muito mais energia na compreensão e explicação da infraestrutura mental básica da matemática - com consequentemente menos energia nos resultados mais recentes. Isso implica o desenvolvimento de uma linguagem matemática eficaz com o objetivo radical de transmitir idéias a pessoas que ainda não as conhecem.

Em relação à questão original, existem artigos que não apresentam idéias no formato Definição-Teorema-Prova (DTP). Timothy Chow tem alguns trabalhos que se concentram na comunicação de idéias (embora não sejam os primeiros (ou segundos) trabalhos sobre o tópico / resultado).

1. Você poderia ter inventado seqüências espectrais , Timothy Chow, Avisos da AMS
2. Forçar para manequins , Timothy Chow

Uma razão possível para a prevalência do formato DTP é que todos nós estamos acostumados a isso de livros e papéis. Os revisores (e leitores) às vezes acham o estilo de escrita não-padrão perturbador. Um meio termo são papéis que gentilmente dividem o leitor em um resultado. Existem trabalhos que apresentam um caso especial ou um problema simples que ilustra a ideia geral.

1. A Estrutura Topológica da Computabilidade Assíncrona , Maurice Herlihy e Nir Shavit. O artigo tem muitas ilustrações e demonstra a idéia geral de um protocolo simples antes de aplicar o teorema principal para resolver alguns problemas em aberto.
2. $p$

Nenhuma discussão sobre uma apresentação fora do padrão de idéias notáveis ​​estaria completa sem mencionar o trabalho de Jean-Yves Girard . Único é provavelmente a melhor palavra para descrevê-lo (sem ser diplomático ou sarcástico). De, o papel Linear Logic .

A exegese filosófica das regras de Heyting deixa, de fato, muito pouco espaço para uma discussão mais aprofundada do cálculo intuicionista; mas alguém já tentou seriamente? De fato, a lógica linear, que é uma extensão clara e limpa da lógica usual, pode ser alcançada por meio de uma análise mais perspicaz da semântica das provas (não muito longe da abordagem da ciência da computação e, portanto, relegada para a próxima seção), ou por certas considerações mais ou menos imediatas sobre o cálculo sequencial. Essas considerações têm significado geométrico imediato, mas, para entendê-las, é preciso esquecer as intenções, lembrando, com um líder chinês, que não é a cor do gato que importa, mas o fato de capturar ratos.

Mais tarde:

Ainda há quem diga que, para produzir ciência da computação, é preciso essencialmente um ferro de soldar; essa opinião é compartilhada por lógicos que desprezam a ciência da computação e por engenheiros que desprezam os teóricos. No entanto, nos últimos anos, a necessidade de um estudo lógico da programação tornou-se cada vez mais clara e a ligação lógica-ciência da computação parece irreversível. [...]
Em certo sentido, a lógica desempenha o mesmo papel que a geometria da física: a estrutura geométrica impõe certos resultados de conservação, por exemplo, a fórmula de Stokes. As simetrias da lógica, presumivelmente, expressam uma profunda conservação da informação, em uma forma que ainda não foi corretamente conceituada.

Talvez os autores não incluam essas tentativas fracassadas e a história da pesquisa em seus artigos publicados por causa das restrições impostas pelos editores e membros do PC. Eu acho que é muito incomum um periódico (e provavelmente ainda mais incomum para uma conferência) aceitar um artigo em que a parte principal é dedicada a tentativas fracassadas. Mas na maioria dos casos, se você conversar com os autores ou especialistas da área, eles explicarão a história e as tentativas fracassadas (e muitos falam sobre isso em oficinas).

Eu já vi vários autores explicando, pelo menos, de onde vieram as idéias em seus artigos. Como exemplo, Girard explica em seu artigo que a idéia da lógica linear surgiu da tentativa de encontrar uma semântica denotacional para o OR intuicionista. Você pode encontrar esse tipo de informação também em monografias e biografias de pesquisadores famosos e volumes dedicados a eles ( a autobiografia de Halmos e a mais recente "Kreiseliana: About and Around Georg Kreisel " editada por Odifreddi vieram à mente, também existem volumes e artigos dedicado a alguns teóricos da complexidade). Esperançosamente, mais pessoas farão o que Ryan fez e explicarão sistematicamente o processo e contarão a história.

ps: você pode pensar nelas como tradição oral de pesquisa :) (um pouco semelhante à Torá Oral, que não podia ser escrita ).

Existe um artigo publicado por Laszlo Babai (1990) na forma de uma fábula sobre Arthur e Merlin descrevendo a dramática sequência de eventos que levaram a comunidade ao resultado do IP = PSPACE em 1989, o que era inacreditável apenas um ano antes.