Klasyfikacja typowych / nietypowych rodzajów Lambda Calculi

Czy ktoś może krótko wyjaśnić (jeśli to możliwe!) Lub odesłać mnie do referencji, podsumowującej różnice między niepisanym rachunkiem lambda i bardziej popularnym typem rachunku lambda?

Szczególnie szukam stwierdzeń o ich mocy ekspresyjnej, równoważności z systemami logicznymi / arytmetycznymi lub metodami obliczeniowymi oraz, w stosownych przypadkach, analogii do języków programowania.

Chociaż z pewnością zamierzam czytać, coś w rodzaju tabeli odniesienia przedstawiającej rachunek różniczkowy i ich ekwiwalenty / różnice / miejsce w hierarchii byłoby OGROMNYM odniesieniem do pomocy w ich uporządkowaniu.

Nie mówię, że poniżej jest poprawne, po prostu próbuję naszkicować niektóre wrażenia, które muszę zobaczyć, czy służą one przynajmniej jako punkt wyjścia (lub coś do poprawienia!)

Rachunek lambda bez typu - równ. do logiki pierwszego rzędu - nie można wykonać X

Wystarczy wpisać rachunek lambda - eq to ... logika, związana z Lisp?

„Polimorficzna” lambda calc - itp.

Rachunek konstrukcji - logika intucjonistyczna?

Logika kombinacyjna - porównywalna do ??? typowany rachunek lambda, związany z językami APL / J

Jeśli wiąże się to z kostką lambda i jej trzema osiami, tym lepiej.

Chociaż znam podstawy rachunku lambda i programowania przy użyciu języków funkcjonalnych, nigdy nie owijałem głowy ani nie nawiązałem żadnych istotnych powiązań z układami typów i różnymi smakami rachunku lambda (a może pi?).

Kiedy próbuję to zbadać, nie mogę pomóc, ale jestem odsunięty na bok, otwierając wiele kart przeglądarki i rozgałęziając się w tak wielu kierunkach, że nigdy nie docieram do żadnej z nich z głębokością!

Nie jestem pewien, czy to, o co proszę, jest rozsądne, ale mam nadzieję, że przynajmniej namalowałem wystarczająco dużo obrazu, aby zasugerować lekturę, która może wyjaśnić, czego szukam?

Twój stół jest trochę zagubiony; tutaj jest lepszy.

• Rachunek lambda bez typu - bez logicznej interpretacji, jak zauważa Andrej
• Prosty typ rachunku lambda - intuicyjna logika zdań
• Polimorficzny rachunek lambda - czysta logika drugiego rzędu (tj. Bez kwantyfikatorów pierwszego rzędu)
• Typy zależne - uogólnienie logiki pierwszego rzędu
• Rachunek konstrukcji - uogólnienie logiki wyższego rzędu

Zależność typów jest bardziej ogólna niż kwantyfikacja pierwszego rzędu, ponieważ zamienia proofy w obiekty, które można kwantyfikować. Rachunki lambda odpowiadające zwykłym intuicyjnym FOL istnieją, ale nie są wystarczająco szeroko stosowane, aby mieć specjalną nazwę - ludzie zwykle przechodzą bezpośrednio na typy zależne.

Możesz także powiązać składniową postać rachunku różniczkowego z systemami logicznymi.

• Rachunkowość kombinatoryczna (np. Kombinatory SKI) - systemy w stylu Hilberta
• Forma normalna - rachunek sekwencyjny
• Rachunek lambda typowy - odliczenie naturalne

Czysty, bez typu rachunek jest Turinga kompletny, tj. Częściowa mapa teoretyczna liczby jest obliczalna, jeśli tylko wtedy, gdy jest możliwa do zdefiniowania w nietypowym λ- rachunku. Moc obliczeniowa wpisanego λ- rachunku jest znacznie mniejsza. Na przykład, jeśli dodamy typ liczb naturalnych do wpisanego λ- rachunku, wraz z 0 , następcą i prymitywną rekurencją, otrzymamy coś, co jest powszechnie znane jako T Gödela . Oblicza tylko pierwotne funkcje rekurencyjne (i wszystkie są całkowite).$\lambda$$\lambda$$\lambda$nat$\lambda$$0$$T$

Bez typu -calculus nie posiada wystarczającą wykładnię do korespondencji Curry-Howard, natomiast wpisany λ -calculus odpowiada dokładnie intuicjonistycznej rachunku zdań.$\lambda$$\lambda$

Modele wpisanego rachunku są dokładnie kategoriami zamkniętymi kartezjańsko. Modele nieoznaczonego λ- rachunku są mniej dobrze wychowane. Chociaż można o nich mówić, z pewnością nie są one tak szeroko badane jak kategorie zamknięte kartezjańsko.$\lambda$$\lambda$

$\lambda$$\lambda$$\lambda$Ulambda : U -> (U -> U)gamma : (U -> U) -> U$\lambda$$\mathbb{U}$$\lambda$$\mathcal{C}$$\mathbb{U}$$\mathbb{U}$$[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$$\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$

Bibliografia:

• Dana S. Scott: „ Lambda Calculus: Some Models, Some Philosophy ”, Studies in Logic and the Foundations of Mathematics, tom 101, 1980, strony 223-265, The Kleene Symposium

• Hendrik Pieter Barendregt: „ Rachunek lambda: jego składnia i semantyka ”, Elsevier, 1984.

Dość obszerną dyskusję na ten temat można znaleźć w tej książce: Lectures on the Curry-Howard Isomorphism . Jest to oparte na swobodnie dostępnej starszej wersji: Wykłady na temat izomorfizmu Curry-Howarda .