Jakich funkcji nie może obliczyć System F?

W tym artykule na Wikipedii o kompletności Turinga stwierdza się, że:

Rachunek lambda bez typu jest zakończony przez Turinga, ale wiele typowych rachunków lambda, w tym System F, nie jest. Wartość typowanych systemów polega na ich zdolności do reprezentowania najbardziej typowych programów komputerowych przy wykrywaniu większej liczby błędów.

Jaki jest przykład całkowitej funkcji obliczeniowej, której system F nie oblicza ?

Ponadto, ponieważ Hindley-Milner to:

Ograniczenie systemu F.

z uwagi na fakt, że:

sprawdzanie typu jest nierozstrzygalne dla wariantu System F w stylu Curry, to znaczy takiego, w którym brakuje wyraźnych adnotacji dotyczących pisania.

Czy to oznacza, że ​​rachunek lambda leżący u podstaw systemów typu Hindley-Milner również nie jest kompletny?

Jeśli to prawda, skoro haskell jest wyraźnie zakończony i wiemy, że jego podstawą jest rachunek lambda i układ typu Hindley-Milner, jakie funkcje, które nie są obecne w rachunku lambda, zostały dodane, aby uzupełnić haskell?

System jest dość ekspresyjny. Jak wykazał Girard tutaj , funkcje typu (gdzie jest zdefiniowane jako ) są dokładnie definiowalnymi funkcjami ( ) w drugiej kolejności Heyting Arithmetic . Zauważ, że jest to to samo, co funkcje definiowane w arytmetyki Peano drugiego rzędu .$F$$\mathbb{N}\rightarrow\mathbb{N}$$\mathbb{N}$$\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$$\mathbb{N}\rightarrow\mathbb{N}$$\mathrm{HA}_2$

Prawdopodobnie będziesz chciał sprawdzić Dowody i typy jako bardziej czytelne odniesienia. Zauważ, że oznacza to, że wiele programów można napisać w systemie F, od funkcji Ackermann po interpretatory dla systemu Gödela . Podobnie jak w przypadku dowolnego języka programowania (z pewnymi łagodnymi warunkami) system nie może zaimplementować własnego interpretera , tj. Funkcji który przyjmuje jako dane wejściowe kod terminu z systemu i zwraca a (kod dla) normalną formę dla$T$$F$$\mathrm{eval}:\mathbb{N}\rightarrow\mathbb{N}$$t$$F$$t$. Dowód obejmuje wariant sztuczki diagonalizacyjnej stosowanej do nierozstrzygalności problemu zatrzymania. Andrej pięknie to tutaj wyjaśnia .

Aby odpowiedzieć na inne pytania: -calculus leżący u podstaw języków Hindley-Milner (HM) również nie jest kompletny. W rzeczywistości jest znacznie słabsza niż systemu , bliżej wyrazu do po prostu wpisany -calculus.$\lambda$$F$ $\lambda$

Haskell rzeczywiście jest kompletny. Najbardziej charakterystyczną cechą, która to umożliwia (choć istnieją inne), jest obecność nieograniczonej rekurencji : definicja dowolnego programu (funkcji) może odnosić się do samego programu. Jest to podobne do dodawania kombinatora , takiego jak ma to miejsce w definicji PCF, który jest po prostu typowany, ale zachowuje kompletność Turinga z kombinatorem$Y$$Y$

Należy pamiętać, że istnieją inne funkcje, które sprawiają, że Haskell Turing jest kompletny, ale zwykle nie uważa się ich za część podstawowego języka, np. Odniesienia do funkcji, nieograniczone typy danych itp.

Nieco mylące jest twierdzenie, że system pisania Haskella to „system typów Hinleya-Milnera”. Typy Haskella są znacznie potężniejsze, w tym, między innymi, typy lepiej dobrane. Rzeczywiście, system pisania jest tak potężny, że można osadzić kompletne języki programowania Turinga w systemie pisania, patrz tutaj . To nie jedyny powód siły Haskella, Cody wspomniał o kilku innych.