(Jak) Czy możemy odkryć / przeanalizować problemy NP przy braku modelu obliczeniowego Turinga?

Z czysto abstrakcyjnego punktu widzenia rozumowania matematycznego / obliczeniowego (jak) można nawet odkryć lub wyjaśnić problemy takie jak 3-SAT, suma częściowa, podróżny sprzedawca itp.,? Czy bylibyśmy w stanie w jakikolwiek sensowny sposób uzasadnić je tylko z funkcjonalnego punktu widzenia? Czy to w ogóle możliwe?

Zastanawiam się nad tym pytaniem wyłącznie z punktu widzenia samego siebie w ramach uczenia się modelu obliczeniowego rachunku lambda. Rozumiem, że jest to „nieintuicyjne” i dlatego Godel faworyzował model Turinga. Chciałbym jednak wiedzieć, jakie są znane teoretyczne ograniczenia tego funkcjonalnego stylu obliczeń i na ile stanowiłoby to przeszkodę w analizie problemów klasy NP?

— Doktorat
źródło

To nie jest pytanie na poziomie badawczym dla kogoś, kto profesjonalnie programuje teorię języka, ale nadal nie sądzę, że qustion zasługuje na wszystkie opinie. Czy downvoters mogą nam powiedzieć, co im przeszkadza? Być może pytanie można poprawić.

— Andrej Bauer,

@AndrejBauer: Przegłosowałem, ponieważ (1) myślę, że (wielomianowa) równoważność maszyn Turinga z rachunkiem lambda jest dość dobrze znana, i (2) post ma dużo puchu, co maskuje to jako podstawowe pytanie. Twoja odpowiedź pokazuje jednak, że dzieje się więcej, niż myślałem, więc mogę cofnąć głosowanie.

— Huck Bennett

Zgadzam się, że puch należy do Discovery Channel.

— Andrej Bauer

@AndrejBauer, HuckBennet: Początkowo postanowiłem opublikować to na portalu informatycznym, ale nie mogłem znaleźć odpowiednich tagów i dlatego opublikowałem je tutaj. Usunąłem puch, aby pomóc w bezpośrednim zrozumieniu tego, co chcę wiedzieć. Zostawiłem swój „powód” zadawania pytania i dlatego oznaczyłem je jako pytanie miękkie. Naprawdę interesuje mnie wiedza, w jaki sposób można analizować problemy NP wyłącznie z perspektywy funkcjonalnej i czy rzeczywiście jest w tym jakaś wartość - z nadzieją, że rozumiem coś głębiej o rachunku lambda

— dr

Myślę, że sednem twojego pytania jest to, czy złożoność mogłaby zostać rozwinięta za pomocą rachunku lambda. Odpowiedź brzmi „tak”, a na stronie znajduje się stare pytanie.

— Kaveh

Odpowiedzi:

Możesz spojrzeć na semantykę kosztów dla języków funkcjonalnych . Są to różne miary złożoności obliczeniowej dla języków funkcjonalnych, które nie przechodzą przez żadną maszynę Turinga, maszynę RAM itp. Dobrym miejscem do rozpoczęcia wyszukiwania jest ten post Lambda Ultimate , który ma kilka dobrych referencji.

Sekcja 7.4 praktycznych podstaw języka programowania Boba Harpera wyjaśnia semantykę kosztów.

Artykuł na temat względnej przydatności kul ognistych Accattoli i Coena pokazuje, że rachunek ma co najwyżej liniowy wybuch w stosunku do modelu maszyny RAM. $\lambda$

Podsumowując, na tej innej planecie sytuacja byłaby prawie taka sama w odniesieniu do NP, ale byłoby mniej przepełnień bufora i nie byłoby tak dużo śmieci wokół.

— Andrej Bauer
źródło

Przypuszczam, że ludzie bez rodzaju

rachunek wciąż wymyśliliby (czysty) schemat. No cóż.

λ

$\lambda$

— Andrej Bauer

To ładny link do postu LtU. Ale jakieś linki do konkretnych przykładów dowodzenia, że ta klasa „NP” ma problemy takie jak 3Sat? Ciekawostki, aby zobaczyć „dowód” w rachunku lambda

— doktorat

Damiano, możesz zamieścić swoje komentarze jako prawidłową odpowiedź, która pokazuje, że teorię związaną z NP można wykonać bezpośrednio w

rachunku.

λ

$\lambda$

— Andrej Bauer,

@DamianoMazza - Zgadzam się z Andrejem i uważam, że twój komentarz powinien być odpowiedzią

— dr

@Andrej: Gotowe! Usunąłem moje poprzednie komentarze.

— Damiano Mazza,

Na prośbę dr Andreja i doktora zmieniam swój komentarz w odpowiedź, przepraszając za autoreklamę.

Niedawno napisałem papieru , w którym patrzę na jak udowodnić twierdzenie Stoły Levin ( -completeness z SAT) za pomocą języka funkcjonalnych (wariant X-rachunku) zamiast maszyn Turinga. Podsumowanie: $\mathsf{NP}$

kluczowym pojęciem jest przybliżenie afiniczne, tzn. przybliżenie dowolnych programów przez programy afiniczne (które mogą wykorzystać swoje dane wejściowe najwyżej); intuicja jest taka, że $\frac{Obwody boolowskie}{Maszyny Turinga} = \frac{afiniczny λ -warunki}{λ -warunki}$ $\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$ $\lambda$
$\lambda$
$\mathsf{NP}$
oczywiście można wówczas zredukować HO CIRCUIT SAT do CIRCUIT SAT, dowodząc w ten sposób zwykłego twierdzenia Cooka-Levina, a krwawe szczegóły na niskim poziomie są przenoszone na budowę takiej redukcji.

$\mathsf{NP}$

$\lambda$ $\lambda$

$\mathsf{NP}$

$\lambda$

$\mathsf{NP}$ $\mathsf{NP}$ $\mathsf{coNP}$ $\lambda$

$\lambda$ $\lambda$

$\mathsf{NP}$ $\lambda$ , nie ma znaczenia, czy wiesz, że twoje intuicje są prawidłowe. Maszyny Turinga dały natychmiastową, wykonalną odpowiedź, a ludzie nie (i nadal nie) czuli potrzeby pójścia dalej.

— Damiano Mazza
źródło

Tylko wyjaśnienie, za którym wielu tęskni: Steve udowodnił kompletność NP dla TAUT, dowód na SAT jest tam ukryty. Pojęcie redukcji karpu nie istniało wówczas. Należy również zauważyć, że TAUT był powodem, dla którego Steve zainteresował się tym tematem i ma kluczowe znaczenie dla automatycznego dowodzenia twierdzeń, czy ludzie byliby równie zainteresowani rozwiązywalnością liniowych warunków lambda? Alternatywny rozwój jest możliwy, ale czy nastąpiłby bez wiedzy o kompletności NP? Uważam to za mało prawdopodobne, biorąc pod uwagę, że alternatywny rozwój jest dość nowy. :)

— Kaveh

Pamiętam, że gdzieś czytałem, że częścią motywacji Levina do opracowania kompletności NP była niezdolność do rozwiązania problemu izomorfizmu grafów i problemu minimalnej wielkości obwodu (MCSP), a także nadzieja na wykazanie, że były to (jak to nazwalibyśmy) NP-trudne. Przynajmniej GI nadal istniałby w świecie lambdów ...

— Joshua Grochow

@Kaveh, dziękuję za komentarz, dodałem kilka akapitów, aby uzupełnić odpowiedź.

— Damiano Mazza

@Josh, też TAUT i SAT.

— Kaveh