Jak kombinator Y ilustruje „niespójność rachunku Lambda”?

44

Na stronie Wikipedii dla Fixed Point Combinators jest napisany dość tajemniczy tekst

Kombinator Y jest przykładem tego, co powoduje, że rachunek Lambda jest niespójny. Dlatego należy to traktować podejrzliwie. Można jednak bezpiecznie rozważyć kombinator Y, gdy jest on zdefiniowany tylko w logice matematycznej.

Czy wdałem się w jakąś powieść szpiegowską? Co na świecie rozumie się przez stwierdzenia, że -kalkulus jest „niespójny” i że należy go „podejrzewać” ?λ

Ben I.
źródło
3
FWIW, akapit ten znajduje się w artykule w Wikipedii od stycznia 2014 r., Kiedy to został wprowadzony do tego ogromnego przepisania prawie całego artykułu .
Ilmari Karonen

Odpowiedzi:

51

Jest inspirowany prawdziwymi wydarzeniami, ale sposób, w jaki zostało powiedziane, jest ledwo rozpoznawalny i „należy podejrzewać” to nonsens.

Spójność ma dokładne znaczenie logiczne: spójna teoria to taka, w której nie wszystkie dowody można udowodnić. W logice klasycznej, jest to równoznaczne z brakiem sprzeczności, czyli teoria jest sprzeczny wtedy i tylko wtedy, gdy znajduje się zdanietakie, że teoria dowodzi zarównoi jego negacja.AA¬A

Co to oznacza w odniesieniu do rachunku lambda? Nic. Rachunek lambda to system przepisywania, a nie logiczna teoria.

Możliwe jest przeglądanie rachunku lambda w odniesieniu do logiki. Traktuj zmienne jako reprezentujące hipotezę w dowodzie, abstrakcje lambda jako dowody w ramach pewnej hipotezy (reprezentowanej przez zmienną), a zastosowanie jako zestaw warunkowego dowodu i dowodu hipotezy. Następnie reguła beta odpowiada uproszczeniu dowodu poprzez zastosowanie modus ponens , podstawowej zasady logiki.

Działa to jednak tylko wtedy, gdy dowód warunkowy jest połączony z dowodem słusznej hipotezy. Jeśli masz dowód warunkowy, który zakłada, że a także masz dowód , nie możesz łączyć ich razem. Jeśli chcesz, aby ta interpretacja rachunku lambda działała, musisz dodać ograniczenie, że tylko dowody właściwej hipotezy zostaną zastosowane do dowodów warunkowych. Nazywa się to systemem typów , a ograniczeniem jest reguła pisania, która mówi, że gdy przekazujesz argument do funkcji, typ argumentu musi być zgodny z typem parametru funkcji.n=3n=2

Korespondencja Curry-Howard jest równoległy pomiędzy wpisywanych kamieni i systemów dowodu.

  • typy odpowiadają instrukcjom logicznym;
  • warunki odpowiadają dowodom;
  • typy zamieszkane (tj. takie, że istnieje termin tego typu) odpowiadają prawdziwym stwierdzeniom (tj. takim, że istnieje dowód na to stwierdzenie);
  • ocena programu (tj. reguły takie jak beta) odpowiadają przekształceniom dowodów (które lepiej przekształcić poprawne dowody w poprawne dowody).

Wpisany rachunek różniczkujący, który ma kombinator punktów stałych, taki jak pozwala na zbudowanie dowolnego rodzaju wyrażenia (spróbuj ocenić ), więc jeśli weźmiesz logiczną interpretację przez korespondencję Curry-Howarda, otrzymasz niespójną teorię. Zobacz Czy kombinator Y jest sprzeczny z korespondencją Curry-Howarda? po więcej szczegółów.YY(λx.x)

Nie ma to znaczenia dla rachunku czystego lambda, tzn. Dla rachunku lambda bez typów.

W wielu kalkulacjach maszynowych nie można zdefiniować kombinatora punktów stałych. Te kalkulacje maszynowe są użyteczne ze względu na ich logiczną interpretację, ale nie stanowią podstawy dla kompletnego języka programowania Turinga. W niektórych kalkulacjach maszynowych możliwe jest zdefiniowanie kombinatora punktów stałych. Te kalkulatory są przydatne jako podstawa dla języka programowania pełnego Turinga, ale nie w odniesieniu do ich logicznej interpretacji.

Podsumowując:

  • Rachunek lambda nie jest „niespójny”, ta koncepcja nie ma zastosowania.
  • Wpisywanych rachunek lambda, która przypisuje do każdego typu wyrażenia lambda jest niespójna. Niektóre kalkulacje lambda na maszynie są takie, inne sprawiają, że niektóre terminy są nietypowe i są spójne.
  • Typowane lambda nie są jedyną racją bytu dla rachunku lambda, a nawet niespójne kalkulacje lambda są bardzo przydatnymi narzędziami - po prostu nie do udowodnienia.
Gilles „SO- przestań być zły”
źródło
2
Wow, jest tu dla mnie dużo do rozpakowania. Dziękuję za szczegółowe wyjaśnienie. Zajmie mi trochę czasu, aby spróbować to wszystko.
Ben I.
4
Technicznie, oglądanie bez typu jak ONZ i wpisane, można zrobić korespondencji pomiędzy CH bez typu rachunku lambda i logiki. To tylko bardzo, bardzo nudna (i na pewno niespójna) logika. Pomocni asystenci, tacy jak NuPRL, trochę zabłocą wody. Język obiektowy NuPRL zawiera niepisany rachunek lambda i można łatwo zdefiniować kombinator Y. NuPRL dzieli rzeczy nieco inaczej, dlatego ma system dopracowywania typów, a nie system typów, a ćwiczenie nie polega na tworzeniu dobrze wpisywanych terminów, ale na tworzeniu pochodnych.
Derek Elkins
Czy to tylko ja, czy dziwne jest narzucanie paradygmatu „twierdzenia jako typy” na nietypowy rachunek lambda? Zawsze widziałem ludzi mówić o logice w rachunku bez typu lambda poprzez wprowadzenie konkretnych obiektów, aby być wartości logiczne truei false, a propozycje były rzeczy, które miały logiczną wartościową wyjście. (i były uważane jedynie propozycje na domenie rzeczy gdzie robi wyjście A wartość logiczną).
Trywialne (potwierdza każde stwierdzenie) i zawiera sprzeczności to dwie różne właściwości. Choć są one równoważne w logice klasycznej, w logice parakonsekwentnej system może być niespójny i nietrywialny.
Taemyr
1
„Niespójny”, dla logiki opartej na rachunku λ, oznacza „przypisuje każdy typ do jakiegoś terminu”, a nie „przypisuje typ do każdego terminu” (chociaż pierwszy z nich wynika z drugiego); istnieje wiele języków opartych na rachunku λ, które odpowiadają niespójnej logice, ale gdzie nie każdy termin rachunku λ jest typowalny.
Jonathan Cast
6

Chciałbym dodać jeden do tego, co powiedział @Giles.

Korespondencji Curry-Howard sprawia równolegle między -terms (bardziej konkretnie, te typy z -terms) i systemy dowodu.λλ

Na przykład ma typ (gdzie oznacza „funkcję od do ”), co odpowiada logicznej instrukcji . Funkcja ma typ , odpowiadający . Możemy przekonwertować dowolny typ rachunku lambda na logiczną tautologię poprzez, w pewnym sensie, „dopasowanie wzorca” funkcji.λx.λy.xa(ba)ababa(ba)λx.λy.xy(ab)(ab)(ab)(ab)

Problem pojawia się, gdy weźmiemy pod uwagę kombinator Y, zdefiniowany jako . Problem powstaje, ponieważ oczekujemy, że kombinator Y, jako kombinator „punktu stałego”, będzie miał typ (ponieważ przenosi funkcję z typu na ten sam typ i znajduje ustalone- punkt dla tej funkcji, która ma ten typ). Przekształcenie tego w wyrażenie logiczne daje . To jest sprzeczność:λf.(λx.f(xx))(λx.f(xx))(aa)a(aa)a

(aa)aaa(¬a¬a)(¬a)¬a¬a

Zaakceptowanie systemu typu prowadzi do niespójności systemu typu. Oznacza to, że możemy(aa)a

  • Nie zezwalaj na typy typu system A (daje to po prostu typ -calculus ) lub(aa)aλ
  • Żyj z systemem typów niespójnym jako system logicznej dedukcji.
Pisownia bezkontekstowa
źródło
1
CH odnosi typy do propozycji, programy do proofów, a nawet redukcje do przekształceń proofów. Nie chodzi tylko o typy. Następnie tylko typy zamieszkane odpowiadają tautologiom. jest (polimorficznym) typem rachunku lambda, nawet jeśli nie występują w nim żadne terminy. Zakładając, że masz na myśli typy takie jak , to akceptacja takich typów jest całkowicie w porządku, problemem jest to, czy ten typ ma mieszkańca, czy nie. I odwrotnie, możemy dodać prymitywne terminy do STLC, które spowodują, że odpowiednia logika będzie niespójna bez rozszerzania systemu typów. a,b.aba.(aa)a
Derek Elkins
@DerekElkins, jakie prymitywne terminy? Ponadto, jeśli dobrze rozumiem, to po prostu załóżmy, że (a -> a) -> a jest zawsze zamieszkałe, co powoduje niespójność? Więc nie ma już niespójności z językiem programowania, który wymaga potwierdzenia zakończenia? A może istnieje inne źródło niespójności w rachunku lambda bez typu lub Hindleya-Milnera?
Hibou57
1
@ Hibou57 Prymitywne terminy, tj. Stałe, jak fix. Możesz po prostu stwierdzić, że dla każdego typu istnieje stała . To już da ci niespójny system, jeśli chodzi o CH, ponieważ oznaczałoby, że każdy typ jest zamieszkany przez . Możesz dodatkowo dodać -rules, aby wykonać , a to zamieniłoby, powiedzmy, STLC z naturals w system Turinga kompletny, ale nie musisz dodawać tych reguł obliczeniowych, a system nadal byłoby niespójne. fixAAfix(λx.x)δfix
Derek Elkins