Jaki jest wkład rachunku lambda w dziedzinę teorii obliczeń?

Właśnie czytam rachunek lambda, żeby go „poznać”. Widzę to jako alternatywną formę obliczeń w przeciwieństwie do maszyny Turinga. Jest to interesujący sposób robienia rzeczy z funkcjami / redukcjami (z grubsza mówiąc). Niektóre pytania wciąż mnie dręczą:

• Jaki jest sens rachunku lambda? Po co przechodzić przez te wszystkie funkcje / ograniczenia? Co jest celem?
• W rezultacie zastanawiam się: co dokładnie zrobił rachunek lambda, aby rozwinąć teorię CS? Jakie były jej wkłady, które pozwoliłyby mi na chwilę „aha” zrozumienia potrzeby jego istnienia?
• Dlaczego rachunek lambda nie jest ujęty w tekstach dotyczących teorii automatów? Wspólną drogą jest przejście przez różne automaty, gramatyki, maszyny Turinga i klasy złożoności. Rachunek Lambda jest zawarty jedynie w sylabusie dla kursów w stylu SICP (być może nie?). Ale rzadko widziałem, aby była to część podstawy CS. Czy to oznacza, że ​​nie jest to aż tak cenne? Może nie, a może coś mi brakuje?

Zdaję sobie sprawę, że funkcjonalne języki programowania są oparte na rachunku lambda, ale nie uważam tego za ważny wkład, ponieważ został on utworzony na długo przed pojawieniem się języków programowania. Tak więc, po co sens poznania / zrozumienia rachunku lambda, jego zastosowania / wkładu w teorię?

rachunek ma dwie kluczowe role.$\lambda$

• Jest to prosta matematyczna podstawa sekwencyjnego, funkcjonalnego zachowania obliczeniowego wyższego rzędu.

• Jest to przedstawienie dowodów w konstruktywnej logice.

Jest to również znane jako korespondencja Curry-Howard . Wspólnie, podwójne postrzeganie rachunek różniczkowy jako dowód i jako (sekwencyjny, funkcjonalny, język programowania wyższego rzędu), wzmocniony algebraicznym odczuciem λ- rachunku (który nie jest wspólny dla maszyn Turinga), doprowadziło do masowego transferu technologii między logiką, podstawami matematyki i programowaniem. Ten transfer jest nadal w toku, na przykład w teorii typów homotopii . W szczególności rozwój języków programowania w ogóle, aw szczególności dyscyplin pisania, jest nie do pomyślenia bez $\lambda$$\lambda$$\lambda$-rachunek różniczkowy. Większość języków programowania jest w pewnym stopniu zadłużona wobec Lisp i ML (np . Wymyślono usuwanie śmieci dla Lisp), które są bezpośrednimi potomkami kalkulatora . Drugim obszarem pracy, na który duży wpływ ma λ- rachunek, są interaktywni asystenci dowodu .$\lambda$$\lambda$

Czy trzeba znać rachunek, aby być kompetentnym programistą, a nawet teoretykiem informatyki? Nie. Jeśli nie interesują Cię typy, języki weryfikacji i programowania z funkcjami wyższego rzędu, to prawdopodobnie jest to model obliczeniowy, który nie jest dla ciebie szczególnie przydatny. W szczególności, jeśli interesuje Cię teoria złożoności, to λ- rachunek prawdopodobnie nie jest modelem idealnym, ponieważ podstawowy krok redukcji ( λ x . M ) N → β M [ N / x ] jest potężny: może tworzyć dowolną liczbę kopii na N , więc → $\lambda$$\lambda$

$$(\lambda x.M) N \rightarrow_{\beta} M[N/x]$$ $N$$\rightarrow_{\beta}$jest nierealistycznym podstawowym pojęciem w rozliczaniu mikroskopijnych kosztów obliczeń. Myślę, że to jest główny powód, dla którego Teoria A nie jest tak zakochana w rachunku. Odwrotnie, maszyny Turinga nie są zbyt inspirujące dla rozwoju języka programowania, ponieważ nie istnieją żadne naturalne pojęcia składu maszynowego, natomiast z X -calculus, jeśli M i N są programy, a następnie tak jest M N . Ten algebraiczny pogląd na obliczenia odnosi się naturalnie do języków programowania używanych w praktyce, a rozwój języka można rozumieć jako poszukiwanie i badanie nowych operatorów kompozycji programów.$\lambda$$\lambda$$M$$N$$MN$

Encyklopedyczny przegląd historii -rachunku znajduje się w Historii rachunku Lambda i logice kombinatorycznej autorstwa Cardone i Hindleya .$\lambda$

Myślę, że rachunek przyczynił się na wiele sposobów do tego pola i nadal się do niego przyczynia. Oto trzy przykłady, które nie są wyczerpujące. Ponieważ nie jestem specjalistą od λ- rachunku, z pewnością brakuje mi kilku ważnych punktów.$\lambda$$\lambda$

• Po pierwsze, myślę, że posiadanie różnych modeli obliczeń, które okazują się reprezentować dokładnie ten sam zestaw funkcji, było początkiem tezy Church-Turinga , a calculus odegrał ważną rolę, obok maszyn Turinga i funkcji μ- rekurencyjnych.$\lambda$$\mu$

• Po drugie, jeśli chodzi o funkcjonalny język programowania, nie rozumiem jako nieważnego wkładu : Zasadniczo wszystkie nasze modele obliczeń zostały wymyślone na długo przed tym, zanim coś się wydarzyło w informatyce! Tak więc rachunek przyniósł inne spojrzenie na obliczenia, w pewnym sensie ortogonalne dla maszyn Turinga, które jest bardzo owocne w dziedzinie języków programowania (która jest częścią dziedziny teorii obliczeń).$\lambda$

• Wreszcie, jako bardziej konkretny przykład, myślę o niejawnej złożoności obliczeniowej, która ma na celu scharakteryzowanie klas złożoności za pomocą dedykowanych języków. Pierwsze wyniki, takie jak Twierdzenie Bellantoniego-Cooka, podano w kategoriach -funkcji rekurencyjnych, ale nowsze wyniki wykorzystują słownictwo i techniki λ- kalkulatora. Zobacz krótkie wprowadzenie do niejawnej złożoności obliczeniowej, aby uzyskać więcej wskazówek i wskazówek na temat warsztatów DICE .$\mu$$\lambda$

$\lambda$

Co dokładnie zrobił rachunek lambda, aby rozwinąć teorię CS?

$\lambda$$\lambda$$\lambda$

$\lambda$

$\lambda$

Do twoich pytań można podchodzić z wielu stron. Chciałbym odłożyć na bok aspekty historyczne i filozoficzne i odnieść się do waszego głównego pytania, które moim zdaniem jest następujące:

Jaki jest sens rachunku lambda? Po co przechodzić przez te wszystkie funkcje / ograniczenia?

Jaki jest sens algebry boolowskiej, algebry relacyjnej, logiki pierwszego rzędu, teorii typów lub innego formalizmu / teorii matematycznej? Odpowiedź brzmi, że nie mają wrodzoną cel do nich, nawet jeśli ich projektanci stworzyli je w jakimś celu lub innego. Leibniz, wznosząc fundamenty algebry Boolean, miał na myśli pewien projekt filozoficzny ; Boole studiował to z własnych powodów. Praca de Morgana nad relacyjną algebrą była również motywowana różnymi jego projektami; Peirce i Frege mieli własne motywy do stworzenia nowoczesnej logiki.

Chodzi o to: bez względu na powód, jaki Kościół miał przy tworzeniu rachunku lambda, punkt rachunku lambda różni się w zależności od praktykującego.

• Dla kogoś jest to wygodny zapis do mówienia o obliczeniach; alternatywa dla maszyn Turinga i tak dalej.

• Innym jest solidna matematyka, na której można zbudować bardziej wyrafinowany język programowania (np. McCarthy, Stanley).

• Dla trzeciej osoby jest to rygorystyczne narzędzie do nadawania semantyki języków naturalnych i programowania (np. Montague, Fitch, Kratzer).

Myślę, że rachunek Lambda jest językiem formalnym, który warto uczyć się dla niego samego. Możesz dowiedzieć się, że w niepisanym rachunku lambda mamy te małe bestie zwane „kombinatorami Y”, i jak pomagają nam definiować funkcje rekurencyjne i czynią dowód nierozstrzygalności tak eleganckim i prostym. Możesz dowiedzieć się niesamowitego faktu, że istnieje ścisła zgodność między prostym typem rachunku lambda a rodzajem intuicyjnej logiki . Jest wiele innych interesujących tematów do zbadania (np. Jak powinniśmy podać semantykę rachunku lambda? W jaki sposób możemy przekształcić rachunek lambda w system dedukcyjny, taki jak FOL?)

---

Zapoznaj się z wstępem Hindleya i Seldina do Kombinatorów i rachunku λ – Rachunku . Barendregt's The Lambda Calculus to biblia, więc jeśli jesteś uzależniony od Hindleya i Seldina, istnieje wiele tematów zarówno semantycznych, jak i syntaktycznych.

Turing twierdził, że matematykę można sprowadzić do kombinacji symboli czytania / pisania wybranych z zestawu skończonego i przełączania się między skończoną liczbą „stanów” mentalnych. Potwierdził to w swoich maszynach Turinga, w których symbole są zapisywane w komórkach na taśmie, a automat śledzi stan.

Jednak maszyny Turinga nie są konstruktywnym dowodem tej redukcji. Argumentował, że jakakolwiek „skuteczna procedura” może być wdrożona przez jakąś maszynę Turinga, i pokazał, że Uniwersalna maszyna Turinga może zaimplementować wszystkie inne maszyny, ale tak naprawdę nie podał zestawu symboli, stanów i zasad aktualizacji, które implementują matematykę w sposób, w jaki się kłócił. Innymi słowy, nie zaproponował „standardowej maszyny Turinga” ze standardowym zestawem symboli, których możemy użyć do spisania naszej matematyki.

Z drugiej strony właśnie jest rachunek Lambda. Kościół szczególnie starał się ujednolicić zapisy używane do spisania naszej matematyki. Po wykazaniu, że LC i TM są równoważne, moglibyśmy użyć LC jako naszej „standardowej maszyny Turinga” i wszyscy mogliby czytać nasze programy (cóż, teoretycznie;)).

Teraz moglibyśmy zapytać, dlaczego traktować LC jako prymitywny, a nie dialekt TM? Odpowiedź jest taka, że ​​semantyka LC jest denotacyjna : terminy LC mają „wewnętrzne” znaczenie. Istnieją liczby kościelne, są funkcje dodawania, mnożenia, rekurencji itp. To sprawia, że ​​LC jest bardzo dobrze dopasowane do tego, jak (formalna) matematyka jest praktykowana, dlatego wiele (funkcjonalnych) algorytmów jest nadal prezentowanych bezpośrednio w LC.

Z drugiej strony, semantyka programów Tm operacyjny : sens jest definiowana jako zachowanie maszyny. W tym sensie nie możemy wyciąć fragmentu taśmy i powiedzieć „to jest dodatek”, ponieważ jest on zależny od kontekstu. Zachowanie się maszyny, gdy uderza ona w tę sekcję taśmy, zależy od stanu maszyny, długości / przesunięć / itp. argumentów, ile taśmy zostanie zużyte na wynik, czy jakakolwiek poprzednia operacja spowodowała uszkodzenie tej części taśmy itp. Jest to przerażający sposób pracy („Nikt nie chce programować maszyny Turinga”), dlatego tak wiele (imperatywnych) algorytmów jest przedstawianych jako pseudokod.

inne odpowiedzi są dobre, oto jeden dodatkowy punkt widzenia / powód do rozważenia, że ​​zazębiają się one z innymi, ale mogą być jeszcze bardziej ostateczne, niemniej jednak trudniej jest o tym pamiętać, ponieważ stare pochodzenie jest nieco zatracone w piaskach czasu:

historyczny precedens!

Rachunek lambda został wprowadzony co najmniej już w 1932 r. W następującym numerze referencyjnym:

• A. Church, „Zbiór postulatów dla podstaw logiki”, Annals of Mathematics, Series 2, 33: 346–366 (1932).

Turing Maszyna została wprowadzona w ~ 1936 roku , więc rachunek lambda poprzedza pojawienie TM przez kilka lat!

• Turing, AM (1936). „O liczbach obliczalnych z aplikacją do problemu Entscheidungs”. Postępowanie London Mathematical Society. 2 (1937) 42: 230–265. doi: 10.1112 / plms / s2-42.1.230

innymi słowy podstawową odpowiedzią jest to, że Lambda Calculus jest pod wieloma względami ostatecznym starszym systemem TCS. wciąż działa tak samo, jak Cobol, mimo że nie ma aż tak wielu zmian w języku! wydaje się być najwcześniej wprowadzonym systemem obliczeniowym Turinga, a nawet wyprzedza podstawową ideę kompletności Turinga. dopiero później retrospektywna analiza wykazała, że ​​rachunek Lambda, maszyny Turinga i problem korespondencyjny były równoważne i wprowadzono koncepcję równoważności Turinga i tezy Kościoła-Turinga .

Rachunek lambda jest po prostu sposobem na badanie obliczeń z pov -logicznego pov bardziej pod względem reprezentowania go jako twierdzeń matematycznych i pochodnych formuł logicznych itp. pokazuje także głęboki związek między obliczeniami a rekurencją oraz dalsze ścisłe powiązanie z indukcją matematyczną .

jest to dość niezwykły fakt, ponieważ sugeruje, że pod wieloma względami (przynajmniej teoretyczne ) początki obliczeń były zasadniczo w logice / matematyce , teza została rozwinięta / rozwinięta szczegółowo przez Davisa w jego książce Engines of Logic / Mathematicians i początkach komputer . (oczywiście pochodzenie i fundamentalna rola algebry boolowskiej dodatkowo wzmacniają te konceptualne ramy historyczne).

stąd, dramatycznie, można nawet powiedzieć, że rachunek Lambda jest trochę jak pedagogiczna wehikuł czasu do odkrywania początków informatyki!

Właśnie natrafiłem na ten post i pomimo tego, że mój post był raczej późny dzień (rok!), Pomyślałem, że być może moja wartość „grosza” może się przydać.

Podczas studiowania tego przedmiotu na uniwersytecie miałem podobne zdanie na ten temat; więc zadałem wykładowcy pytanie „dlaczego”, a odpowiedź brzmiała: „kompilatory”. Gdy tylko o tym wspomniała, siła stojąca za redukcją i umiejętność oceny, jak najlepiej nią manipulować, nagle stały się głównym celem tego, dlaczego była i nadal jest potencjalnie użytecznym narzędziem.

Cóż, że tak można powiedzieć, to była moja chwila „aha”.

Moim zdaniem często uważamy, że języki wysokiego poziomu, wzorce, automaty, złożoność algorytmów itp. Są użyteczne, ponieważ możemy odnieść je do „zadania” pod ręką; podczas gdy rachunek lamdba wydaje się zbyt abstrakcyjny. Jednak wciąż są tacy, którzy pracują z językami na niskim poziomie - i wyobrażam sobie rachunek lambda, rachunek obiektowy i inne powiązane formalizacje, które pomogły im zrozumieć i być może opracować nowe teorie i technologie, z których może skorzystać przeciętny programista. Rzeczywiście, prawdopodobnie nie jest to moduł podstawowy z tego powodu, ale (z powodów, o których wspomniałem) będzie kilku dziwnych - poza naukowcami - którzy mogą uznać to za integralną część ich wybranej ścieżki kariery w informatyce.