(Como) Poderíamos descobrir / analisar problemas de NP na ausência do modelo de computação de Turing?

15

De um ponto de vista puramente abstrato do raciocínio matemático / computacional, (como) alguém poderia descobrir ou raciocinar sobre problemas como 3-SAT, Subset Sum, Traveling Salesman etc.? Será que vamos ser mesmo capaz de raciocinar sobre eles de qualquer maneira significativa com apenas o funcional ponto de vista? Seria possível?

Estive refletindo sobre essa questão puramente a partir de um ponto de auto-indagação como parte do aprendizado do modelo de cálculo do cálculo lambda. Entendo que é "não intuitivo" e é por isso que Godel favoreceu o modelo de Turing. No entanto, gostaria apenas de saber quais são as limitações teóricas conhecidas desse estilo funcional de computação e quanto seria um obstáculo para analisar a classe de problemas NP?

Doutorado
fonte
Essa não é uma pergunta em nível de pesquisa para alguém que pratica a teoria da linguagem de programação profissionalmente, mas ainda não acho que a pergunta mereça todos os votos negativos. Poderiam os abatidos dizer-nos o que os incomoda? Talvez a questão possa ser melhorada.
21416 Andrej Bauer
2
@AndrejBauer: Eu diminuí a votação porque (1) acho que a equivalência (polinomial) entre as máquinas de Turing e o cálculo lambda é bastante conhecida, e (2) o post tem um monte de penugem que mascara isso como a questão principal. No entanto, sua resposta mostra que há mais coisas acontecendo do que eu pensava, portanto, posso reverter meu voto.
Huck Bennett
Concordo que o cotão pertence ao Discovery Channel.
Andrej Bauer
2
@AndrejBauer, HuckBennet: Inicialmente, decidi postar isso no portal de ciência da computação, mas não consegui encontrar as tags relevantes e, portanto, as publiquei aqui. Tirei o cotão para ajudar a ser direto com o que quero saber. Deixei minha "razão" para fazer a pergunta e, portanto, a marquei como uma pergunta suave. Estou genuinamente interessado em saber como é possível analisar problemas de NP puramente de uma perspectiva funcional e se há realmente algum valor em fazer isso - com a esperança de que eu entenda algo mais profundamente sobre o cálculo lambda
PhD
Penso que o cerne da sua pergunta é se a complexidade poderia ser desenvolvida usando o cálculo lambda. A resposta é sim, e há uma pergunta antiga no site iirc.
Kaveh #

Respostas:

16

Você pode querer procurar semântica de custos para linguagens funcionais . Essas são várias medidas de complexidade computacional para linguagens funcionais que não passam por nenhum tipo de máquina de Turing, RAM, etc. Um bom lugar para começar a procurar é este post do Lambda the Ultimate , que tem boas referências adicionais.

A Seção 7.4 dos Fundamentos práticos de Bob Harper para linguagens de programação explica a semântica dos custos.

O artigo Sobre a utilidade relativa de bolas de fogo de Accattoli e Coen mostra que o cálculo tem uma explosão linear no máximo em relação ao modelo de máquina RAM.λ

Em resumo, neste outro planeta as coisas seriam praticamente as mesmas com relação ao NP, mas haveria menos transbordamentos de buffer e não haveria tanto lixo por aí.

Andrej Bauer
fonte
Suponho que as pessoas não- tipadas do cálcio ainda inventariam o esquema (puro). Ah bem. λ
Andrej Bauer 28/11
Esse é um bom link no post do LtU. Mas existem links para exemplos concretos de provar essa classe de "NP" com problemas como o 3Sat? Curios para ver uma "prova" no cálculo lambda
PhD
Damiano, você pode postar seus comentários como uma resposta adequada, demonstrando que é possível fazer a teoria relacionada à PN diretamente no cálcio. λ
Andrej Bauer
@DamianoMazza - Concordo com Andrej e acredita que seu comentário deve ser uma resposta
PhD
@Andrej: Feito! Eu removi meus comentários anteriores.
Damiano Mazza
14

A pedido de Andrej e PhD, estou transformando meu comentário em uma resposta, com desculpas por autopublicidade.

Recentemente, escrevi um artigo no qual analiso como provar o teorema de Cook-Levin ( NP completidade do SAT) usando uma linguagem funcional (uma variante do λ-cálculo) em vez de máquinas de Turing. Um resumo:

  • a noção principal é a de aproximações afins, isto é, aproximar programas arbitrários por afins (que podem usar suas entradas no máximo uma vez); a intuição é que os tão afimλ
    Boolean circuitsTuring machines=affine λ-termsλ-terms
    λ -Termos computações arbitrárias aproximados arbitrário bem como circuitos booleanos;
  • o resultado é que, no λ mundo dos cálculos , a prova é muito "de nível superior", usa teoria das ordens, continuidade de Scott etc. em vez de invadir circuitos booleanos; em particular, o slogan "computação é local" (que é dada por muitos como a mensagem subjacente ao teorema de Cook-Levin) se torna "computação é contínua", como esperado;
  • no entanto, o "natural" NP não é problema -completo CIRCUITO sab mas HO CIRCUITO sab, uma espécie de "solvabilidade" de X-termos lineares ou, mais precisamente, as redes à prova lógica lineares (que são como de ordem superior circuitos booleanos) ;
  • é claro, pode-se reduzir HO CIRCUIT SAT para CIRCUIT SAT, provando o teorema comum de Cook-Levin e os detalhes sangrentos e de baixo nível são todos movidos para a construção dessa redução.

Portanto, a única coisa que mudaria "deste lado do planeta" é, talvez, que consideraríamos um problema relacionado ao cálculo λ, em vez de um problema relacionado ao circuito booleano, ser o "primordial" NP - problema completo.

Uma observação lateral: a prova acima mencionada pode ser reformulada em uma variante do cálcio do Accattoli com substituições explícitas lineares mencionadas na resposta de Andrej, que talvez seja mais padrão do que o λ- cálcio que uso no meu trabalho.λλ


Edição posterior: minha resposta foi um pouco mais do que recortar e colar do meu comentário e percebo que algo mais deve ser dito sobre o cerne da pergunta que, como eu a entendo, é: seria possível desenvolver a teoria de NP -completeness sem máquinas de Turing?

Concordo com o comentário de Kaveh: a resposta é sim , mas talvez apenas retrospectivamente. Ou seja, quando se trata de complexidade (contando tempo e espaço), as máquinas de Turing são imbatíveis na simplicidade, o modelo de custo é evidente por tempo e quase evidente por espaço. No cálculo- , as coisas são muito menos evidentes: modelos de custo de tempo como os mencionados por Andrej e dados no livro de Harper são de meados dos anos 90, modelos de custo de espaço ainda quase inexistentes (conheço essencialmente um trabalho publicado Em 2008λ ).

Portanto, é claro que podemos fazer tudo usando a perspectiva puramente funcional, mas é difícil imaginar um universo alternativo no qual Hartmanis e Stearns definam classes de complexidade usando λ e, 30 a 50 anos depois, as pessoas começam a adaptar seu trabalho a Turing máquinas

NPNPcoNPλ

λλ

NPλ, realmente não importa se você sabe que suas intuições são sólidas. As máquinas de Turing deram uma resposta imediata e viável, e as pessoas não sentiram (e ainda não sentem) a necessidade de ir mais longe.

Damiano Mazza
fonte
2
Apenas um esclarecimento que muitos erram: Steve provou que a NP é completa para TAUT, a prova para SAT está implícita lá. A noção de redução de Karp não existia na época. Também é importante observar que TAUT foi a razão pela qual Steve se interessou pelo tópico e é central para a prova automática de teoremas. As pessoas estariam tão interessadas na resolubilidade de termos lineares lambda? O desenvolvimento alternativo é possível, mas aconteceria sem o conhecimento prévio da completude do NP? Acho isso improvável, considerando que o desenvolvimento alternativo é bastante recente. :)
Kaveh
1
Lembro-me de ler em algum lugar que parte da motivação de Levin para desenvolver a completude do NP era a incapacidade de resolver o isomorfismo dos grafos e o problema do tamanho mínimo do circuito (MCSP), e a esperança de mostrar que eles eram (o que chamaríamos agora) de NP-hard. Pelo menos GI seria ainda tem existido em um mundo de lambdas ...
Joshua Grochow
1
@ Kaveh, obrigado pelo seu comentário, adicionei alguns parágrafos para completar a resposta.
Damiano Mazza
1
@ Josh, então TAUT e SAT.
Kaveh