(Comment) Pourrions-nous découvrir / analyser des problèmes NP en l'absence du modèle de calcul de Turing?

15

D'un point de vue purement abstrait de raisonnement mathématique / informatique, (comment) pourrait-on même découvrir ou raisonner sur des problèmes comme 3-SAT, Subset Sum, Travelling Salesman, etc.? Serions - nous encore en mesure de raisonner sur eux de quelque façon significative avec juste la fonction point de vue? Serait-ce même possible?

J'ai réfléchi à cette question uniquement à partir d'un point d'auto-enquête dans le cadre de l'apprentissage du modèle de calcul lambda de calcul. Je comprends que c'est "non intuitif" et c'est pourquoi Godel a privilégié le modèle Turing. Cependant, je voudrais juste savoir quelles sont les limites théoriques connues de cette fonctionnalité style de calcul et combien un obstacle serait - il pour l' analyse de la classe NP des problèmes?

Doctorat
la source
Ce n'est pas une question de recherche pour quelqu'un qui fait de la théorie du langage de programmation de manière professionnelle, mais je ne pense toujours pas que la question mérite tous les votes négatifs. Les downvoters pourraient-ils nous dire ce qui les dérange? Peut-être que la question peut être améliorée.
Andrej Bauer
2
@AndrejBauer: J'ai rétrogradé parce que (1) je pense que l'équivalence (polynomiale) entre les machines de Turing et le calcul lambda est assez bien connue, et (2) la publication a beaucoup de peluches qui masquent cela comme la question centrale. Cependant, votre réponse montre qu'il se passe plus de choses que je ne le pensais, donc je peux inverser mon vote.
Huck Bennett
J'accepte que le fluff appartient à Discovery Channel.
Andrej Bauer
2
@AndrejBauer, HuckBennet: Au départ, je décidais de publier ceci sur le portail informatique, mais je n'ai pas trouvé les balises pertinentes et je l'ai donc posté ici. J'ai enlevé les peluches pour aider à être direct avec ce que je veux savoir. J'ai laissé ma «raison» pour poser la question et l'ai donc étiquetée comme une question douce. Je suis vraiment intéressé à savoir comment on pourrait analyser les problèmes de NP uniquement d'un point de vue fonctionnel et s'il y a effectivement une valeur à le faire - avec l'espoir que je comprends quelque chose de plus profondément sur le calcul lambda
PhD
Je pense que le cœur de votre question est de savoir si la complexité pourrait être développée en utilisant le calcul lambda. La réponse est oui, et il y a une vieille question qui le demande sur le site iirc.
Kaveh

Réponses:

16

Vous voudrez peut-être examiner la sémantique des coûts pour les langages fonctionnels . Ce sont diverses mesures de complexité de calcul pour les langages fonctionnels qui ne pas passent par une sorte de machine de Turing, machine RAM, etc. Un bon endroit pour commencer la recherche est ce Lambda le poste ultime , qui a quelques bonnes références supplémentaires.

La section 7.4 des Fondements pratiques de Bob Harper pour les langages de programmation explique la sémantique des coûts.

L'article sur l'utilité relative des boules de feu par Accattoli et Coen montre que -calculus a au plus une explosion linéaire par rapport au modèle de machine RAM.λ

En résumé, sur cette autre planète, les choses seraient à peu près les mêmes en ce qui concerne le NP, mais il y aurait moins de débordements de tampon et il n'y aurait pas autant de déchets qui traînent.

Andrej Bauer
la source
Je suppose que les gens non typés -calculus inventeraient toujours un schéma (pur). Tant pis. λ
Andrej Bauer
C'est un bon lien sur le post LtU. Mais des liens vers des exemples concrets pour prouver cette classe de "NP" avec des problèmes comme 3Sat? Curiosités pour voir une "preuve" dans le calcul lambda
PhD
Damiano, vous pouvez poster vos commentaires comme une réponse appropriée qui démontre que l'on peut faire de la théorie liée au NP directement dans -calculus. λ
Andrej Bauer
@DamianoMazza - Je suis d'accord avec Andrej et je pense que votre commentaire devrait être une réponse
PhD
@Andrej: Terminé! J'ai supprimé mes commentaires précédents.
Damiano Mazza
14

À la demande d'Andrej et de PhD, je transforme mon commentaire en réponse, avec des excuses pour l'auto-publicité.

J'ai récemment écrit un article dans lequel je regarde comment prouver le théorème de Cook-Levin ( complétude P de SAT) en utilisant un langage fonctionnel (une variante du λ-calcul) au lieu des machines de Turing. Un résumé:NP

  • la notion clé est celle d'approximations affines, c'est-à-dire d'approximation de programmes arbitraires par des programmes affines (qui peuvent utiliser leurs entrées au plus une fois); l'intuition est que
    Circuits booléensMachines de Turing=affine λ-termesλ-termes
    si termes se rapprochent bien des calculs arbitraires, tout comme les circuits booléens;λ
  • le résultat est que, dans le monde λ -calculus, la preuve est beaucoup "de niveau supérieur", elle utilise la théorie de l'ordre, la continuité de Scott, etc. au lieu de pirater les circuits booléens; en particulier, le slogan "le calcul est local" (qui est donné par beaucoup comme le message sous-jacent au théorème de Cook-Levin) devient "le calcul est continu", comme prévu;λ
  • cependant, le N "naturel" problème -complete est pas CIRCUIT SAT mais HO CIRCUIT SAT, une sorte de « solvabilité » de X-termes linéaires ou, plus précisément,filets linéaires de preuve logique (qui sont commecircuits booléennes d'ordre supérieur) ;NP
  • bien sûr, on peut alors réduire HO CIRCUIT SAT en CIRCUIT SAT, prouvant ainsi le théorème de Cook-Levin habituel, et les détails sanglants de bas niveau sont tous déplacés pour construire une telle réduction.

NP - problème complet.

λλ -calculus que j'utilise dans mon article.


NP complétude sans machines de Turing?

λ calcul , les choses sont beaucoup moins évidentes: les modèles de coût du temps comme ceux mentionnés par Andrej et donnés dans le livre de Harper datent du milieu des années 90, les modèles de coût d'espace sont encore presque inexistants (je connais essentiellement un ouvrage publié en 2008 ).

λ termes et, 30 à 50 ans plus tard, les gens commencent à adapter leur travail à Turing Machines.

NPNPcoNPλ

λλ

NPλ, peu importe si vous savez que vos intuitions sont saines. Les machines de Turing ont donné une réponse immédiate et réalisable, et les gens n'ont pas (et ne ressentent toujours pas) le besoin d'aller plus loin.

Damiano Mazza
la source
2
Juste une clarification que beaucoup manquent: Steve a prouvé que NP était complet pour TAUT, la preuve pour SAT est implicite là-dedans. La notion de réduction de Karp n'existait pas à l'époque. Il est également important de noter que TAUT était la raison pour laquelle Steve s'est intéressé au sujet et est au cœur de la démonstration automatique des théorèmes, les gens seraient-ils aussi intéressés par la solvabilité des termes lambda linéaires? Le développement alternatif est possible, mais se produirait-il sans la connaissance préalable de l'exhaustivité de NP? Je trouve cela peu probable si l'on considère que le développement alternatif est plutôt récent. :)
Kaveh
1
Je me souviens avoir lu quelque part qu'une partie de la motivation de Levin pour développer l'exhaustivité NP était l'incapacité de résoudre le problème d'isomorphisme graphique et de taille de circuit minimum (MCSP), et l'espoir de montrer qu'ils étaient (ce que nous appellerions maintenant) NP-dur. Au moins, GI aurait toujours existé dans un monde de lambdas ...
Joshua Grochow
1
@Kaveh, merci pour votre commentaire, j'ai ajouté quelques paragraphes pour compléter la réponse.
Damiano Mazza
1
@Josh, TAUT et SAT aussi.
Kaveh