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

85

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ę?

Doktorat
źródło
6
Powiązany zestaw odpowiedzi wyjaśnia różnicę mocy między -calculus a TM: cstheory.stackexchange.com/questions/1117/…λ
Suresh Venkat
4
Być może interesująca jest także dyskusja na temat historycznych powodów przyjęcia maszyny Turinga jako podstawowego modelu obliczeń .
Martin Berger
5
W pewnym sensie jego wkład polegał na stworzeniu pola. Nie zapominaj, że Kościół najpierw wymyślił rachunek lambda, ale początkowo nie był postrzegany jako uniwersalny model obliczeń.
Dan Hulme
W moich podstawowych badaniach miałem Functional Programmingomówienie Haskell i trochę Lisp. Następcą tego było Principles of Programming Languagesużycie ML i wprowadzenie rachunku lambda. Jak pokazują niektóre odpowiedzi, tak naprawdę należy do rachunku lambda: w klasie o językach programowania, pisaniu itp.
Shaz
to pytanie jest podobne związek między TM i rachunku Lambda, a także omawia historyczny precedens rachunku Lambda
od

Odpowiedzi:

96

rachunek ma dwie kluczowe role.λ

  • 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 λλλλ-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 .λλ

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 βλλ

(λx.M.)N.βM.[N./x]
N.β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.λλM.N.M.N.

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

Martin Berger
źródło
8
To bardzo miła odpowiedź.
Suresh Venkat
9
Jeśli chodzi o „nierealizm” redukcji : Beniamino Accattoli i Ugo Dal Lago dowiodły ostatnio zaskakującego wyniku, stwierdzając, że liczba kroków β do normalnej postaci w dowolnej standardowej strategii redukcji (np. Skrajnie skrajnie lewostronnie) jest niezmienną miarą złożoności. Oznacza to, że nawet jeśli wdrożenie β -redukcja per se jest drogie, licząc liczbę redukcji nie jest nierealne miarą złożoności (na przykład, nie będzie miał wpływu na definicję klasy P ). βββP.
Damiano Mazza
5
@DamianoMazza Ponieważ jest to nowy wynik, nie mógł mieć wpływu na historię teorii A. Ponadto myślę, że ta rezolucja dotyczy tylko niektórych pojęć redukcji. Praca IIRC Aspertiego P = NP, aż do dzielenia się pokazuje, że P i NP rozpadają się, jeśli masz „optymalną” strategię redukcji w sensie J.-J. Nałożyć.
Martin Berger
6
@MartinBerger: tak, oczywiście. Mój komentarz miał na celu dodanie informacji o złożoności redukcji , a nie „poprawienie” twojego stwierdzenia o braku wpływu na Teorię A (którą powtórzyłem w mojej odpowiedzi). Nawiasem mówiąc, wyniki Accattoli i Dal Lago odnoszą się do zwykłej, najbardziej lewej, najbardziej zewnętrznej redukcji β ( por. S. 2, ok. 2, 11). Dlatego jest tak interesujący (i warty wspomnienia). Wynik Aspertiego dotyczy, jak mówisz, redukcji optymalnej dla Lévy'ego, która nie jest strategią redukcji β (w szczególności skrajne skrajne lewe skrajne nie są optymalne dla Lévy'ego). βββ
Damiano Mazza
27

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.λλ

  • 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.λμ

  • 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ń).λ

  • 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 .μλ

Bruno
źródło
20

λ

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

λλλ

λ

λ

Damiano Mazza
źródło
2
λλππ
5
Gdybym mógł się sklonować, zrobiłbym duplikat, aby przyjrzeć się P / NP przy użyciu BLL i możliwości realizacji. Relacje logiczne wydają się nie być „naturalnymi dowodami”, dyscyplina typu liniowego zapewnia, że ​​nie można relatywizować, a twierdzenia BLL o kompletności czasu działania wydają się pozwalać uniknąć martwienia się o to, czy istnieją klasy algorytmów, które zostały pominięte. Związek między liniowością a teorią reprezentacji sugeruje również powiązania z GCT. Przypuszczam, że właśnie dlatego jesteś kuszony i sfrustrowany. :)
Neel Krishnaswami
1
Hej @NeelKrishnaswami, czy mógłbyś wskazać mi materiały do ​​czytania, które dotyczą BLL (logika liniowa ograniczona) i naturalnych dowodów?
Martin Berger,
Re B vs. A: rachunek lambda polega tylko na lepszej strukturze tych samych obliczeń, ale nie może na przykład tworzyć lepszych algorytmów. Przez eliminację cięć i właściwość podformularza w wyniku, każdy program z typem pierwszego rzędu może być napisany bez funkcji pierwszej klasy. Ale eliminacja cięć odpowiada duplikowaniu kodu: dlatego ponownie okazuje się, że nie potrzebujesz funkcji wyższego rzędu, jeśli chcesz wykonać wystarczającą ilość wklejania kopii. (Defunkcjonalizacja Reynoldsa pozwala uniknąć nawet wklejania kopii, ale jest globalną transformacją, więc lepiej pozostawić to kompilatorowi).
Blaisorblade
Anegdotycznie rzecz biorąc, mój komentarz jest motywowany programowaniem z algorytmem - jest świetny, ale wydaje się, że jest abstrakcyjny w znacznie mniejszym stopniu, niż uważam za pożądany. Nie twierdzę, że to ogólne, ale twierdzę, że abstrakcja w kodzie często nie jest potrzebna / podkreślana podczas pisania algorytmów. (Zastanów się, ile implementacji Quicksort wstawia funkcję partycji - uważam to za niedopuszczalne).
Blaisorblade
13

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.

Hunan Rostomyan
źródło
6
Nie kupuję tego argumentu „dla samego siebie”. Matematyczny formalizm ma na celu wyjaśnienie naszego zrozumienia niektórych koncepcji. To, co zostanie wyjaśnione, może się rozwijać z czasem, ale jeśli formalizm nie pomoże nam lepiej myśleć o jakimś pomyśle, zwykle umrze. W tym sensie warto zrozumieć, jak rachunek lambda wyjaśnia pojęcie obliczeń w sposób, który nie jest uwzględniany przez bazy danych.
Sasho Nikolov
1
Myślę, że można badać rachunek lambda bez zastanawiania się nad redukcją i podstawieniem jako obliczeniem. Jeśli mam rację i jest to faktycznie możliwe, możemy zainteresować się rachunkiem lambda, nawet jeśli w ogóle nie jesteśmy zainteresowani obliczeniami. Ale dzięki za komentarz; Spróbuję odpowiednio edytować swoją odpowiedź, jak tylko będę miał szansę.
Hunan Rostomyan
@SashoNikolov - „w sposób, który nie jest objęty przez TM”. Z definicji jest to niemożliwe, ponieważ LC i TM są równoważne. Wszystko, co możesz wyrazić lub udowodnić za pomocą jednego, możesz to zrobić za pomocą drugiego (i odwrotnie). Czynią się więc zbędnymi (jak oboje robią z ogólną teorią rekurencyjną, jeszcze jednym formalizmem równoważnym TM). Czy to oznacza, że ​​powinniśmy wyrzucić wszystkie systemy równoważne TM oprócz samej TM? Nie powiedziałbym tego, ponieważ czasami rzeczy są łatwiejsze do wyrażenia w LC niż TM lub odwrotnie. To tylko inny sposób mówienia o obliczalności.
Gabriel L.
1
@GabrielL. Jeśli przeczytasz całe zdanie, powiedzą: „w jaki sposób rachunek lambda wyjaśnia pojęcie obliczeń w sposób, który nie jest uwzględniany przez TM”. Dwie matematyczne definicje, które są formalnie równoważne, mogą nadal wyjaśniać tę samą podstawową koncepcję na różne i uzupełniające się sposoby. Mój komentarz oznaczał, że rozsądnie jest zapytać, jaką jasność uzyskuje się, wyrażając obliczalność w kategoriach rachunku lambda, a nie w odniesieniu do baz TM. Nie chodzi tu wcale o formalną równoważność.
Sasho Nikolov
Rozumiem - udało się w jakiś sposób przeoczyć kluczowe słowo. Dziękuję za odpowiedź.
Gabriel L.
12

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.

Warbo
źródło
5

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!

vzn
źródło
1
addendum, rachunek Lambda również wydaje się być pod dużym wpływem Principia mathematica Whitehead / Russell, który również był główną inspiracją dla Godels thm . niektóre z tych badań zostały również zainspirowane 10-tym problemem Hilberta z przełomu wieków, który wymagał rozwiązania algorytmicznego, zanim „algorytm” został precyzyjnie (matematycznie) zdefiniowany, aw rzeczywistości to poszukiwanie w dużej mierze prowadzi do późniejszej dokładnej definicji technicznej.
dniu
btw / wyjaśnienie / iiuc to faktycznie systemy post kanoniczne były badane 1. pocztą i najwyraźniej prostszy problem korespondencji pocztowej jest szczególnym przypadkiem. także Kleene odegrał kluczową rolę w opracowaniu koncepcji kompletności Turinga (nie wymaganej pod tą nazwą), pomagając udowodnić, że wszystkie 3 główne systemy są wymienne / równoważne (TM, Lambda Calculus, post kanoniczny system).
dniu
zobacz także wikipedię Historia tezy Kościoła-Turinga, która śledzi wiele historycznych szczegółów / relacji
dniu
4
Trudno mi się nie obrazić w porównaniu z Cobolem.
Neil Toronto
-2

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.

użytkownik30412
źródło
Jaka była „aha” na kompilatorach ?
Dr
Twój ostatni akapit wydaje się całkowicie spekulacyjny i nigdy tak naprawdę nie wyjaśniasz, dlaczego jedno słowo „kompilatory” odpowiada na pytanie.
David Richerby,
@PhD: Zmniejszenie i podstawienie wersji beta nie są używane podczas uruchamiania programów, ale są używane w kompilatorach optymalizujących. To nie jest najważniejsze znaczenie rachunku lambda, ale jest to bardzo konkretne zastosowanie.
Blaisorblade,