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

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ć” ?$\lambda$

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.$A$$A$$\neg 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=3$$n=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.$Y$$Y (\lambda 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.

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.$\lambda$$\lambda$

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.$\lambda x.\lambda y.x$$a \to (b \to a)$$a \to b$$a$$b$$a \implies (b \implies a)$$\lambda x.\lambda y.xy$$(a \to b) \to (a \to b)$$(a \implies b) \implies (a \implies b)$

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ść:$\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$(a \to a) \to a$$(a \implies a) \implies a$

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

• Nie zezwalaj na typy typu system A (daje to po prostu typ -calculus ) lub$(a \to a) \to a$$\lambda$
• Żyj z systemem typów niespójnym jako system logicznej dedukcji.