(Cómo) ¿Podríamos descubrir / analizar problemas de NP en ausencia del modelo de cómputo de Turing?

15

Desde un punto de vista puramente abstracto de razonamiento matemático / computacional, ¿cómo podría uno incluso descubrir o razonar sobre problemas como 3-SAT, Subset Sum, Travelling Salesman, etc.? Estaríamos incluso capaz de razonar sobre ellas de una manera significativa con sólo la funcionalidad punto de vista? ¿Sería posible?

He estado reflexionando sobre esta cuestión únicamente desde un punto de auto indagación como parte del aprendizaje del modelo de cálculo de cálculo lambda. Entiendo que es "no intuitivo" y por eso Godel favoreció el modelo de Turing. Sin embargo, solo deseo saber cuáles son las limitaciones teóricas conocidas de este estilo funcional de cómputo y cuánto obstáculo sería para analizar la clase de problemas NP.

Doctor
fuente
Esta no es una pregunta de nivel de investigación para alguien que hace teoría de lenguaje de programación profesionalmente, pero todavía no creo que la pregunta merezca todos los votos negativos. ¿Podrían los downvoters decirnos qué les molesta? Quizás la pregunta pueda mejorarse.
Andrej Bauer
2
@AndrejBauer: He votado en contra porque (1) creo que la equivalencia (polinómica) entre las máquinas de Turing y el cálculo lambda es bastante conocida, y (2) la publicación tiene mucha pelusa que oculta eso como la pregunta central. Sin embargo, su respuesta muestra que están sucediendo más cosas de las que pensaba, así que puedo revertir mi voto.
Huck Bennett
Estoy de acuerdo en que la pelusa pertenece al Discovery Channel.
Andrej Bauer el
2
@AndrejBauer, HuckBennet: Inicialmente decidí publicar esto en el portal de informática, pero no pude encontrar las etiquetas relevantes y, por lo tanto, lo publiqué aquí. Quité la pelusa para ayudar a ser directo con lo que quiero saber. He dejado mi "razón" para hacer la pregunta y, por lo tanto, la etiqueté como una pregunta suave. Estoy realmente interesado en saber cómo se pueden analizar los problemas de NP puramente desde una perspectiva funcional y si realmente hay algún valor en hacerlo, con la esperanza de que entiendo algo más profundamente sobre el cálculo lambda
PhD
Creo que el núcleo de su pregunta es si la complejidad podría desarrollarse utilizando el cálculo lambda. La respuesta es sí, y hay una vieja pregunta que pregunta eso en el sitio iirc.
Kaveh

Respuestas:

16

Es posible que desee ver la semántica de costos para lenguajes funcionales . Estas son varias medidas de complejidad computacional para lenguajes funcionales que no pasan por ningún tipo de máquina Turing, máquina RAM, etc. Un buen lugar para comenzar a buscar es esta publicación de Lambda the Ultimate , que tiene algunas buenas referencias adicionales.

La Sección 7.4 de los Fundamentos prácticos para lenguajes de programación de Bob Harper explica la semántica de costos.

El documento sobre la utilidad relativa de las bolas de fuego por Accattoli y Coen muestra que el cálculo tiene como máximo una explosión lineal con respecto al modelo de máquina RAM.λ

En resumen, en este otro planeta las cosas serían más o menos lo mismo con respecto a NP, pero habría menos desbordamientos de búfer y no habría tanta basura por ahí.

Andrej Bauer
fuente
Supongo que las personas sin cálculo cálculo aún inventarían el esquema (puro). Oh bien. λ
Andrej Bauer el
Ese es un buen enlace en la publicación de LtU. ¿Pero algún vínculo a ejemplos concretos de probar esta clase de "NP" con problemas como 3Sat? Curiosidades para ver una "prueba" en el cálculo lambda
PhD
Damiano, podrías publicar tus comentarios como una respuesta adecuada que demuestre que uno puede hacer teoría relacionada con NP directamente en cálculo . λ
Andrej Bauer, el
@DamianoMazza - Estoy de acuerdo con Andrej y creo que su comentario debería ser una respuesta
PhD
@Andrej: ¡Listo! Eliminé mis comentarios anteriores.
Damiano Mazza
14

A petición de Andrej y PhD, estoy convirtiendo mi comentario en una respuesta, con disculpas por la publicidad propia.

Recientemente escribí un artículo en el que miro cómo probar el teorema de Cook-Levin ( -completitud del SAT) usando un lenguaje funcional (una variante del cálculo λ) en lugar de las máquinas de Turing. Un resumen:nortePAG

  • la noción clave es la de aproximaciones afines, es decir, aproximación de programas arbitrarios por afines (que pueden usar sus entradas como máximo una vez); la intuición es que λ tan afines -términosλaproximan cálculos arbitrarios arbitrarios al igual que los circuitos booleanos;
    Circuitos booleanosMáquinas de Turing=afín λ-condicionesλ-condiciones
    λ
  • El resultado es que, en el mundo del cálculo , la prueba es mucho más "nivel superior", utiliza la teoría del orden, la continuidad de Scott, etc. en lugar de piratear circuitos booleanos; en particular, el eslogan "el cálculo es local" (que muchos dan como mensaje subyacente al teorema de Cook-Levin) se convierte en "el cálculo es continuo", como se esperaba;λ
  • sin embargo, el problema "natural" completo no es CIRCUIT SAT sino HO CIRCUIT SAT, una especie de "resolubilidad" de términos lineales λ o, más precisamente, redes lineales a prueba de lógica (que son como circuitos booleanos de orden superior) ;nortePAG
  • por supuesto, uno puede reducir HO CIRCUIT SAT a CIRCUIT SAT, lo que demuestra el teorema usual de Cook-Levin, y los detalles sangrientos de bajo nivel se mueven para construir tal reducción.

nortePAG

λλ


nortePAG

λ

λ

nortePAGnortePAGConortePAGλ

λλ

nortePAGλ, realmente no importa si sabes que tus intuiciones son sólidas. Las máquinas de Turing dieron una respuesta inmediata y viable, y la gente no sintió (y aún no siente) la necesidad de ir más allá.

Damiano Mazza
fuente
2
Solo una aclaración que muchos echan de menos: Steve demostró la integridad de NP para TAUT, la prueba de SAT está implícita allí. La noción de reducción de Karp no existía en ese momento. También es importante tener en cuenta que TAUT fue la razón por la cual Steve se interesó en el tema y es central para la demostración automática de teoremas, ¿estaría la gente tan interesada en la resolución de términos lambda lineales? El desarrollo alternativo es posible, pero ¿ocurriría sin el conocimiento previo de la integridad de NP? Me parece poco probable teniendo en cuenta que el desarrollo alternativo es bastante reciente. :)
Kaveh
1
Recuerdo haber leído en alguna parte que parte de la motivación de Levin para desarrollar la completitud de NP fue la incapacidad de resolver el isomorfismo gráfico y el problema de tamaño mínimo de circuito (MCSP), y la esperanza de demostrar que eran (lo que ahora llamaríamos) NP-hard. Al menos GI habría existido en un mundo de lambdas ...
Joshua Grochow
1
@Kaveh, gracias por tu comentario, agregué algunos párrafos para completar la respuesta.
Damiano Mazza
1
@ Josh, también lo haría TAUT y SAT.
Kaveh