Jakie są granice całkowitego programowania funkcjonalnego?

Jakie są ograniczenia całkowitego programowania funkcjonalnego? Nie jest to kompletna metoda Turinga, ale nadal obsługuje dużą część możliwych programów. Czy istnieją ważne konstrukcje, które można napisać w języku kompletnym Turinga, ale nie w języku funkcjonalnym?

I czy słuszne jest stwierdzenie, że programy napisane w całkowicie funkcjonalnych językach mogą być całkowicie analizowane statycznie, podczas gdy analiza statyczna w językach kompletnych Turinga jest ograniczona przez takie rzeczy jak problem z zatrzymaniem? Nie mam na myśli tego, że we wszystkich językach funkcjonalnych wszystko można ustalić statycznie, ponieważ niektóre rzeczy są znane tylko w czasie wykonywania, ale mam na myśli, że teoretycznie programy napisane w idealnym funkcjonalnym języku programowania można analizować, tak aby wszystko, co Teoretycznie można określić statycznie Można ustalić statycznie. Czy też nadal istnieją nierozstrzygalne problemy dziedziczone w językach funkcjonalnych, które powodują, że analiza statyczna jest niekompletna? Niektóre problemy zawsze będą nierozstrzygalne, bez względu na to, w jakim języku są napisane, ale interesują mnie takie problemy, które są dziedziczone w tym języku,

computability pl.programming-languages functional-programming Matthijs Steen
źródło

Odpowiedzi:

To zależy od całkowitego języka funkcjonalnego .

Ta odpowiedź brzmi jak knock-out, ale nie można powiedzieć nic bardziej szczegółowego. W końcu rozważ każdy ważny program rozstrzygający, który Cię interesuje. Napisz program w swoim ulubionym języku kompletnym Turinga, aby go rozwiązać. Ponieważ problem jest rozstrzygalny, twój program zatrzyma się na wszystkich danych wejściowych.

(Prawdopodobnie problem, który nie podlega rozstrzygnięciu, może mieć interesujące programy, ale nie takie, z których ludzie mogą korzystać, ponieważ nigdy nie będą w stanie czekać wystarczająco długo, aby poznać odpowiedź).

Teraz zdefiniuj nowy język, tak aby miał tylko jeden poprawny program wejściowy: program, który właśnie napisałeś, z taką samą semantyką jak wcześniej. Jest to z pewnością całkowite, ponieważ wszystkie wejścia do wszystkich programów w nim zapisanych (których jest tylko jeden) zawsze kończą się.

Ta tania sztuczka jest naprawdę przydatna: na przykład język Coq jest językiem funkcjonalnym, w którym żaden program nie sprawdza typów, chyba że istnieje dowód, że się kończy. (Gdybyś zrzekł się tego wymogu, byłby to kompletny Turing, więc jedyną przeszkodą jest znalezienie dowodu wypowiedzenia).

Nie jestem pewien, co rozumiesz przez „wszystko, co teoretycznie można ustalić statycznie, można ustalić statycznie”; brzmi to tautologicznie prawda. Niemniej jednak całkowite języki z natury nie są łatwe do analizy; wiesz, że nic nie jest rozbieżne, co jest użytecznym faktem, ale związek między danymi wejściowymi i wyjściowymi jest nadal złożony. (W szczególności istnieje wciąż nieskończenie wiele możliwych danych wejściowych, więc nie można wyczerpująco wypróbować ich wszystkich, nawet teoretycznie.)

Paul Stansifer
źródło

Dziękuję za odpowiedź. Zatem bycie totalnym nieco pomaga, ale pozostaje to bardzo trudnym problemem. Miałem na myśli to, że „wszystko, co teoretycznie można ustalić statycznie, można ustalić statycznie” było to, że byłoby niezwykle trudne lub nie do przeanalizowania wszystkich związków między wkładem i wyjściem, gdybyś miał wystarczająco dużo zasobów, aby to zrobić . Czy są to podstawowe przyczyny, dla których jest to ograniczone? Podobnie jak teoria Rice'a, dowodzi, że tak jest w przypadku funkcji częściowych. Czy też źle rozumiem twierdzenie Rice'a?

Matthijs Steen,

Myślę, że może to zależeć od tego, co rozumiesz przez „związek”. W szczególności, jeśli masz na myśli „wejście A idzie do wyjścia B”, można to w prosty sposób określić w całym języku funkcjonalnym; po prostu uruchom program. Ale prawdopodobnie interesują Cię analizy, które mówią coś o nieskończonej klasie danych wejściowych.

Paul Stansifer

(ups; naciśnij Enter przypadkowo) ... ale to otwiera kolejną głupią sztuczkę, ponieważ mogę zadać niezdecydowane pytania dotyczące funkcji tożsamości, jeśli chcę: „Dla niektórych Xjest (identity X)to maszyna Turinga, która się zatrzymuje?” Jasne, że nie wydaje się być o identity , ale w jaki sposób można zdefiniować „o”?

Paul Stansifer

Tak, chcę wiedzieć, czy zachowuje się dla wszystkich możliwych wartości wejściowych niektórych definicji, a nie dla poszczególnych danych wejściowych. Więc jeśli dobrze cię rozumiem, masz na myśli, że zawsze będą jakieś nierozstrzygalne pytania, bez względu na to, jakiego rodzaju języka programowania użyjesz? Chociaż niektóre z tych nierozstrzygalnych pytań można obejść, zapobiegając przede wszystkim pojawieniu się problemu, na przykład całkowitym językom funkcjonalnym problemu zatrzymania? Bo czy twoje pytanie dotyczące funkcji tożsamości nie byłoby rozstrzygalne w pełnym języku funkcjonalnym?

Matthijs Steen,

Tak; zmodyfikowana wersja problemu, w której „maszyna Turinga” jest zastąpiona przez „psuje się po wygaśnięciu gwarancji, maszyna Turinga” jest łatwa do rozwiązania. Z tego powodu kłopotliwe jest to, że problem zatrzymania jest przykładem nierozstrzygalnego problemu, gdy badanie programów jest pełne nierozstrzygalności.

Paul Stansifer,

Jakie są ograniczenia całkowitego programowania funkcjonalnego? Nie jest to kompletna metoda Turinga, ale nadal obsługuje dużą część możliwych programów. Czy istnieją ważne konstrukcje, które można napisać w języku kompletnym Turinga, ale nie w języku funkcjonalnym?

$L$ $L$ $L$

$L$ $L$ $L$ $L$ jest spójny. Właśnie to wyklucza twierdzenie Goedela, zakładając, że umiesz wykonywać arytmetykę. Wiemy zatem, że nie możemy pisać autoportretów we wszystkich językach funkcjonalnych.
Wadą tego jest jednak to, że ograniczenia mocy ekspresyjnej wszystkich języków są zasadniczo ograniczeniami mocy ekspresyjnej samej matematyki . Na przykład funkcje definiowane w Coq (asystent dowodu) to te, które można udowodnić, że można je obliczyć za pomocą ZFC, z niezliczoną liczbą niedostępnych kardynałów. Tak więc w Coq można zdefiniować dowolną funkcję, którą można by w pełni zadowolić pracującego matematyka.
Drugą stroną jest to, że matematyka jest trudna! Dlatego nie ma łatwego sensu, w którym wszystkie języki są „w pełni analizowalne” - nawet jeśli wiesz, że funkcja się kończy, być może nadal będziesz musiał wykonać wiele pracy twórczej, aby udowodnić, że ma właściwość, którą chcesz. Na przykład sam fakt, że funkcja od list do list jest sumą, nie prowadzi cię daleko do udowodnienia, że jest to funkcja sortująca ...

Neel Krishnaswami
źródło

Dziękuję za odpowiedź. Przeczytałem post o tym problemie na blogu Lambda the Ultimate , ale niektóre osoby w komentarzach twierdzą, że chociaż nie jest możliwe, aby jego własny ewaluator był regularnym, wyraźnie konstruowalnym terminem, możliwe byłoby stworzenie działającego self-self ewaluator z pewnymi sztuczkami. Zastanawiam się więc, czy są problemy, których nie da się rozwiązać (lub w przybliżeniu) w funkcjonalnym języku z pewnymi sztuczkami objazdów?

Matthijs Steen,

Powiedziałbym, że samoocena nie stanowi problemu, ponieważ różni się w zależności od języka. Problem „oceniaj program w języku X” jest tym samym problemem, niezależnie od tego, czy próbujesz go rozwiązać w języku X czy Y. W szczególności, jeśli język X jest językiem funkcjonalnym całkowicie, problem można rozwiązać w jakimś języku funkcjonalnym , używając tej samej głupiej sztuczki, której użyłem wcześniej.

Paul Stansifer

Neel, wydaje się, że powinno być znacznie łatwiej udowodnić, że cały język nie jest w stanie obsłużyć własnego tłumacza. Czy ja ciebie nie rozumiem? Przez prostą diagonalizację każdy język z funkcją bez stałych punktów nie może obsługiwać własnego interpretera (niezależnie od tego, czy obsługuje arytmetykę, czy nie). Argument został opracowany przez Conora McBride tutaj: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html

Tom Ellis

@TomEllis: Mój argument jest zasadniczo taki sam jak argument Conora. W rzeczywistości jego post już dokonuje tej obserwacji (z charakterystycznym dowcipem Conora), kiedy nazywa ją „argumentem Epimenides / Cantor / Russell / Quine / Godel / Turing”.

Neel Krishnaswami,