Jakich funkcji nie może obliczyć System F?

28

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?

Mike HR
źródło
Przykładem funkcji, która sprawia, że ​​Haskell jest kompletny, jest natywny interfejs kodu.
Trismegistos,
@cody dzięki za komentarz. Nie znam systemu T. Czy mam rację zakładając, że jest to system T wymieniony tutaj ? Jak porównuje system T i kontrastuje z systemem F?
Mike HR
UWAGA, w system T vs. system FGoogle'a znalazłem coś, co odpowiada na moje ostatnie pytanie, które zostało tutaj sformułowane w następujący sposób: Jak Haskell dodał Turinga do systemu F
Mike HR
1
Myślę, że @Trismegistos podnosi interesującą kwestię filozoficzną: czym dokładnie jest Haskell, gdzie są jego granice?
Martin Berger,

Odpowiedzi:

45

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 .FNNNX. X(XX)XNNHA2

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ę dlaTFeval:NNtFt. 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.λF λ

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 kombinatoremYY

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.

cody
źródło
1
Wow, to jest niesamowita odpowiedź i doskonale odpowiada na wszystko. Dziękuję Ci!
Mike HR
„Jak w każdym języku programowania…” To nie jest całkiem poprawne. Według mnie, istnieje kilka autoportretów dla wszystkich języków, które wykluczają nieterminowe programy jako źle napisane. Zobacz ten artykuł
jmite
@jmite, jak stwierdzono, moje roszczenie jest poprawne. Ten artykuł jest wspomniany w powiązanej dyskusji, a Andrej ma kilka uwag na swoim blogu: math.andrej.com/2016/01/04/…
cody
11

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.

Martin Berger
źródło
Dzięki. moją główną ekspozycją na Hindley-Milnera było haskell, więc chyba mogłem założyć, że typy wyższego rodzaju były jego częścią. Czy Hindley-Milner odnosi się po prostu do wnioskowania o typie (więc najprawdopodobniej algorytmu W)? czy to coś więcej? Rozumiem, że jest to matematyczne podłoże w rachunku lambda, staram się tylko zrozumieć, gdzie są logiczne granice między potężnym systemem typu haskell i jaka byłaby minimalna implementacja „systemu typu Hindley-Milner”.
Mike HR
Uwaga: Jeśli ktoś jest zainteresowany mocą systemu typu haskell, poleciłbym film Edwarda Kmetta na temat hask , który zagłębia się (głęboko) w teorię kategorii za pomocą systemu typu haskell.
Mike HR
1
@ MikeH-R Zazwyczaj mamy na myśli, że Hindley – Milner jest systemem do pisania lub, bardziej precyzyjnie, typem -calculus, podczas gdy algorytm jest algorytmem wnioskowania typu dla systemu Hindley – Milner. Niezwykłe w systemie Hindley-Milnera jest to, że łączy on polimorfizm parametryczny z możliwością wnioskowania o najbardziej ogólnym typie dowolnego programu bez adnotacji typu. Artykuł w Wikipedii jest wart przeczytania. λW
Martin Berger