Rachunek lambda nie wydawał się abstrakcyjny. I nie widzę sensu


18

Podstawowe pytanie:

Co robi dla nas rachunek lambda , czego nie możemy zrobić z podstawowymi właściwościami funkcji i notacją ogólnie przyswojoną w algebrze gimnazjalnej?

Przede wszystkim, co oznacza streszczenie w kontekście rachunku lambda? Moje rozumienie słowa abstrakcja jest czymś oddzielonym od maszynerii, konceptualnym streszczeniem pojęcia.

Jednak funkcje lambda, usuwając nazwy funkcji, zapobiegają pewnemu poziomowi abstrakcji. Na przykład:

f(x) = x + 2
h(x, y) = x + 5 y

Ale nawet bez zdefiniowania mechanizmu tych funkcji możemy z łatwością porozmawiać o ich składzie. Na przykład:

1. h(x, y) . f(x) . f(x) . h(x, y) or 
2. h . f . f . h

Możemy dołączyć argumenty, jeśli chcemy, lub możemy całkowicie odreagować, aby dać przegląd tego, co się dzieje. I możemy szybko zredukować je do jednej funkcji. Spójrzmy na kompozycję 2. Potrafię mieć studenckie warstwy szczegółów, z którymi mogę pisać w zależności od mojego nacisku:

g = h . f . f . h
g(x, y) = h(x, y) . f(x) . f(x) . h(x, y)
g(x, y) = h . f . f . h = x + 10 y + 4

Wykonajmy powyższe za pomocą rachunku lambda lub przynajmniej zdefiniuj funkcje. Nie jestem pewien, czy to prawda, ale wierzę, że pierwsze i drugie wyrażenie zwiększają się o 2.

(λuv.u(u(uv)))(λwyx.y(wyx))x

I pomnożyć przez 5 lat.

(λz.y(5z))

Zamiast być abstrakcyjnym, wydaje się, że wchodzi to w samą maszynerię tego, co oznacza dodawanie, mnożenie itp. Abstrakcja, moim zdaniem, oznacza wyższy poziom niż niższy poziom.

Co więcej, staram się zrozumieć, dlaczego rachunek lambda jest w ogóle czymś. Jaka jest zaleta

(λuv.u(u(uv)))(λwyx.y(wyx))x

nad

h(x) = x + 5 y

lub notacja łączona

Hxy.x+5y

a nawet notację Haskella

h x y = x + 5 * y

Ponownie, co robi dla nas rachunek lambda, czego nie możemy zrobić z właściwościami funkcji typu f (x) i notacją, z którą wielu jest zaznajomionych.


9
To zabawne, że podajesz przykład z Haskell, ponieważ Haskell opiera się na rachunku lambda. Rachunek lambda nie dotyczy żadnego szczególnego zapisu. Jest to model obliczeniowy odpowiadający maszynom Turinga, w którym „wszystko jest funkcją”.
Yuval Filmus,

2
Tak, powiedziano mi, że opiera się na rachunku lambda. Pytanie, na które muszę jeszcze odpowiedzieć w sposób, który ma dla mnie sens, brzmi: dlaczego haskell opiera się na rachunku lambda w przeciwieństwie do sprawiedliwego. . . podstawowe atrybuty funkcji, których nauczyłem się w szkole podstawowej. To jest sedno tego całego pytania.
JDG,

6
Czy „od razu nie przychodzi mi do głowy” prawie definicja „abstrakcyjna”? :-)
David Richerby,

1
Nie powiedziałbym, że to uwłaczające. To traktowanie funkcji można zastosować za pomocą rachunku różniczkowego. Ale widzę, jak można by to interpretować jako „gimnazjum”. Dostosuję to.
JDG,

6
Wątpię, czy faktycznie masz formalną definicję „notacji funkcji algebry w szkole średniej”. Jeśli masz jakąś definicję takich funkcji, to prawdopodobnie jest to teoretyczna, która nie ma znaczenia obliczeniowego. Częścią rachunku różniczkowego lambda jest zrozumienie takiej notacji na własnych warunkach i, ośmielę się to powiedzieć, abstrahować od konkretnych aplikacji, takich jak funkcje wielomianowe lub rachunek różniczkowy.
Derek Elkins opuścił SE

Odpowiedzi:


24

Jest wiele powodów, dla których rachunek lambda jest tak ważny.

Bardzo ważnym powodem jest rachunek lambda, który pozwala nam mieć model obliczeń, w którym funkcje obliczeniowe są pierwszorzędnymi obywatelami.

Nie można wyrazić funkcji wyższego rzędu w języku algebry gimnazjalnej.

Weź jako przykład wyrażenie lambda

λf.λg.λx.f(g(x))

To proste wyrażenie pokazuje nam, że w rachunku lambda sam skład funkcji jest funkcją. W algebrze gimnazjalnej nie jest to łatwo wyrażone.

W rachunku lambda bardzo łatwo jest wyrazić, że funkcja zwróci funkcję jako wynik.

Oto mały przykład. Wyrażenie (gdzie tutaj zakładam zastosowany rachunek lambda z dodatkowymi i stałymi liczbami całkowitymi)

(λf.λg.λx.f((g(x)))(λx.x+2)

zmniejszy się do

λg.λx.g(x)+2

Zauważ też, że w rachunku lambda funkcje są wyrażeniami, a nie definicjami postaci . To uwalnia nas od konieczności nazywania funkcji i rozróżniania składniowej kategorii wyrażeń od składniowej kategorii definicji.f(x)=e

Ponadto, gdy staje się niemożliwe (lub po prostu utrudnione notacyjnie) wyrażanie funkcji wyższego rzędu, będą również problemy z przypisywaniem typów do wyrażeń.

Kompozycja funkcji ma typ polimorficzny

α.β.γ.(βγ)((αβ)γ)

w systemie typu Hindley-Milner.

Bardzo mocną stroną sprzedaży rachunku lambda jest precyzyjne pojęcie wypisanego rachunku lambda . Różne systemy typów dla funkcjonalnych języków programowania, takie jak Haskell i rodzina ML, oparte są na systemach typów dla obliczeń lambda, a te systemy typów dają silne gwarancje w postaci twierdzeń matematycznych:

Jeśli program jest dobrze napisany, a e zmniejsza się do resztkowego e , wówczas e również będzie dobrze napisany.eeee

A jeśli jest dobrze wpisane, następnie e nie będzie wykazywać pewne błędy.ee

Dowody jak programy korespondencja jest szczególnie godne uwagi. Izomorfizm Curry'ego-Howarda (patrz np. Https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf ) pokazuje, że istnieje bardzo dokładna zgodność między prostym typem rachunku lambda a intuicyjną logiką zdań: do każdego typu odpowiada logiczny wzór cp T . Dowód ϕ T odpowiada terminowi lambda dla typu T , a redukcja beta tego terminu odpowiada przeprowadzeniu eliminacji cięcia w dowodzie.TϕTϕTT

Wzywam tych, którzy uważają, że algebra gimnazjalna jest dobrą alternatywą dla rachunku lambda, aby opracowali opis algebry gimnastycznej wyższego rzędu o typie polimorficznym wraz z odpowiednim pojęciem izomorfizmu Curry'ego-Howarda. Jeśli potrafisz nawet opracować interaktywnego asystenta dowodu opartego na algebrze gimnazjalnej, który pozwoliłby nam udowodnić wiele twierdzeń sformalizowanych za pomocą asystentów dowodowych opartych na rachunku lambda, takich jak Coq i Isabelle, byłoby to jeszcze lepsze. Wtedy zacznę używać algebry gimnazjalnej i jestem pewien, że wielu innych ze mną.


To świetne wytłumaczenie. Dobrze jest usłyszeć, że funkcje wyższego rzędu (takie jak kompozycja) i pisanie są lepiej reprezentowane w rachunku lambda, co jest zachęcające, a nawet więcej, że ułatwia to sprawdzanie poprawności i sprawdzalny kod. Nie widzę konsekwencji wielu z tego, co wspomniałeś, i dlaczego tradycyjna notacja jest nieodpowiednia (np. O tym, że nie potrzebujesz osobnej składni definicji f (x) = e), jednak pomocne jest, aby wymienić niektóre z tych przyczyn i pokazuje, jakie obszary są poprawiane przez rachunek lambda.
JDG,

Można oczywiście wprowadzić lokalne definicje formy ale można je już wyrazić w składni rachunku lambda jako ( λ x . e ) e . Rachunek lambda pozwala nam wyrażać funkcje bez konieczności ich nazywania, tak jak można (w algebrze gimnazjalnej!) Mówić o liczbie 4 bez konieczności nazywania ich jakąś zmienną. letx=eine(λx.e)e4
Hans Hüttel,

5

Kiedy funkcje są po raz pierwszy opisywane młodym, są one zasadniczo identyfikowane za pomocą wykresów (wykresów) lub być może za pomocą wzorów; w taki sposób historycznie rozumiano funkcje przed pojawieniem się formalistycznych trendów w matematyce. W dzisiejszych czasach funkcje, jak uczy się w pierwszym roku rachunku, są funkcjami rzeczywistymi, czyli funkcje od do R .RR

Funkcje w rachunku lambda są znacznie bardziej ogólne. Dokładna definicja zależy od tego, czy rachunek lambda jest wpisany, czy nie. W czystym niepisanym rachunku lambda wszystko jest funkcją. Jest to o wiele bardziej ogólne niż rzeczywiste funkcje rachunku różniczkowego.

Nawet języki proceduralne czasami używają pomysłów z rachunku lambda. Funkcja sortowania w C przyjmuje jako parametr funkcję porównania , której używa do porównywania elementów. Rachunek lambda idzie znacznie dalej - funkcje nie tylko akceptują funkcje jako dane wejściowe, ale mogą je również generować.

Rachunek lambda to model obliczeniowy równoważny mocy maszynom Turinga. Jest to system sam w sobie kompletny. Czysty rachunek lambda nie ma „5” ani „+” jako prymitywnych terminów - można je zdefiniować wewnątrz rachunku, podobnie jak „5” i „+” nie są prymitywami teorii mnogości. (Praktyczne języki programowania implementują liczby naturalne naturalnie ze względu na wydajność.)

Podejrzewam, że jednym z powodów, dla których nie jesteś pod wrażeniem rachunku lambda, jest to, że jego pomysły tak bardzo przeniknęły dyskurs programistyczny, że nie wygląda już nowatorsko.


„Podejrzewam, że jednym z powodów, dla których nie jesteś pod wrażeniem rachunku lambda” Therin zadaje pytanie: co robi dla nas rachunek lambda? Innymi słowy, kiedy nie używamy rachunku lambda, co się dzieje. Kiedy korzystamy z rachunku lambda, co zyskujemy? Jeśli rachunek lambda był po raz pierwszy, że ludzie pomyśleli, co jeśli funkcje mogłyby same tworzyć funkcje, to czy to robi wrażenie? Wśród moich początkowych programów w języku Python znalazłem tekst zawierający funkcje, które później przeanalizowałem, podobnie jak przekazanie zadania podejmowania decyzji innej osobie. Czy to oczywiste?
JDG,

to było zanim dowiedziałem się wiele o niczym. Pomyślałem, że kod jest irytujący w ciągłym pisaniu, a programowanie powinno pomóc mi w automatycznym generowaniu funkcjonalności, w tym samych funkcji.
JDG,

2
Python obsługuje programowanie funkcjonalne. Pierwsze języki programowania nie. Gdybyś programował w FORTRAN, nie stworzyłbyś programów z tekstem zawierającym funkcje, które później oceniałeś. Nawet tego nie zauważając, wykorzystałeś możliwości oferowane przez pomysły z rachunku lambda.
Yuval Filmus,

2
Eval pochodzi z LISP , na który duży wpływ miał rachunek lambda. Coś takiego nie jest możliwe w FORTRAN, C, COBOL i wielu innych językach programowania.
Yuval Filmus,

Tak, python obsługuje funkcjonalne programowanie --- ale nie jestem pewien, czy jego zdolność eval () została zainspirowana przez λCalc --- nie λCalc myśli: chcę wygenerować kod, który będę mógł później wyewaluować. To tak, jakby powiedzieć, że λCalc musi pomyśleć: „Powiem Mirandzie, żeby dokonała najlepszego osądu, jak prowadzić swój dział” - innymi słowy uzyskanie funkcji do generowania własnych funkcji. Nie potrzebujesz λCalc, aby myśleć o delegowaniu zadań wysokiego poziomu. Jeśli chcesz porozmawiać o czerpaniu inspiracji z λCalc, bardziej odpowiednie jest odniesienie do funkcji lambda, zrozumienia itp.
JDG

4

x2xx2

λx.x2x2

ff(x)=x2f

Zastosowanie wyrażeń lambda w językach programowania ma podobną zaletę; możesz napisać, co robi funkcja tam, gdzie jest potrzebna, zamiast definiować zupełnie nową funkcję w innym miejscu w programie.

ddxx2ddxx2


θ:VV

θ(v)(f)=f(v)

Wiele osób uważa, że ​​notacja podwójnej oceny jest myląca i / lub niepokojąca, a także rekurencyjne stosowanie punktowej definicji funkcji. Wersja abstrakcyjna lambda

θ=λv.λf.f(v)

nie ma tego problemu.


Wreszcie istnieje twierdzenie o abstrakcyjnych bzdurach, że „prosty typ rachunku lambda” jest w zasadzie tym samym, co „kartezjańska kategoria zamknięta” - więc jeśli kiedykolwiek zechcesz wykonać obliczenia w kartezjańskiej kategorii zamkniętej, prawdopodobnie dobrym pomysłem jest użycie wystarczy napisać rachunek lambda, aby to zrobić.


Wracam do tego pytania i uważam, że ta odpowiedź jest świetna. Dziękuję Ci. Odpowiedzi tutaj ogólnie są naprawdę interesujące.
JDG

4

Powiem z góry, że nie jestem ekspertem w tym temacie, ale spędziłem trochę czasu na studiowaniu go, a jedną z najbardziej fascynujących rzeczy w jakimkolwiek temacie jest historia. Dla mnie zrozumienie historii za pomocą rachunku lambda pomaga wyjaśnić, dlaczego jest to przydatne.

Krótkie podsumowanie jest takie, że na początku XX wieku po tym, jak teoria zbiorów zaczęła się rozwijać, a matematyka została ponownie wyobrażona na podstawie zbiorów, niektórzy matematycy zauważyli, że chociaż definicja teorii zbiorów pozwala twierdzić, że istnieje pewna struktura, nie mówią ci, w jaki sposób skonstruować i obliczyć. Więc definicje set-teoretyczny są nonconstructive . Matematycy zaczęli się zastanawiać, czy istnieje sposób na opracowanie konstruktywnych definicji, które wykraczałyby poza udowodnienie, że coś istnieje, a zamiast tego udowodnić, jak jest .

Z Wikipedii :

W matematyce dowód konstruktywny to metoda dowodu, która demonstruje istnienie obiektu matematycznego poprzez utworzenie lub dostarczenie metody tworzenia obiektu. Jest to sprzeczne z dowodem niekonstruktywnym (znanym również jako dowód istnienia lub twierdzenie o istnieniu czystym), który dowodzi istnienia określonego rodzaju obiektu bez podania przykładu.

Następnie wykazano, że rachunek lambda i maszyna Turinga mogą reprezentować dowolną funkcję obliczalną, a zatem są równoważne.

Teoretycznie każdą funkcję lub pojęcie matematyczne można zakodować w postaci rachunku lambda i obliczyć. Oznacza to, że rachunek lambda może być całkowicie oddzielną podstawą dla matematyki, choć oczywiście wyjątkowo żmudną.

Rachunek lambda nie jest „użyteczny” w tym sensie, że nie zamierzasz pisać przy jego użyciu kodu, ale stanowi on podstawę dla semantyki denotacyjnej, która jest używana do opisywania programów i ich dynamicznych efektów. Jest to wykorzystywane w dyskusjach na temat poprawności programu i znaczenia semantycznego. Oczywiście miało to również duży wpływ na rozwój funkcjonalnych języków programowania, które całą koncepcję wykonania czerpią z rachunku lambda.

Mam nadzieję, że to pomaga.

Edytuj, aby dodać: Właśnie wskazano mi ten artykuł pokazujący związek między topologią, rachunkiem lambda i fizyką. Przeglądając go krótko natknąłem się na to fantastyczne stwierdzenie:

Chociaż maszynę Turinga można postrzegać jako wyidealizowany, uproszczony model sprzętu komputerowego , rachunek lambda przypomina raczej prosty model oprogramowania . ... Poetycko mówiąc, rachunek lambda opisuje wszechświat, w którym wszystko jest programem, a wszystko jest danymi: programy są danymi .

Chodzi o to, że rachunek lambda jest wyidealizowanym modelem obliczeń oprogramowania i jako taki nie jest związany z konkretną implementacją w żadnym języku programowania. Modeluje czyste obliczenia .


Więcej na temat historii: Krótka historia rachunku λ w Encyklopedii Filozoficznej Stanforda. Mają więcej wpisów niż można przetworzyć w ciągu całego życia.
David Tonhofer,


3

Rachunek Lambda nie został zaprojektowany jako język programowania. Rzeczywiście, został stworzony w latach 30. XX wieku, na dziesiątki lat zanim mieliśmy nawet programowalne komputery. Został raczej stworzony jako formalny model do studiowania obliczeń. Jeśli jesteś rozczarowany, jak łatwo wyraża kod lub funkcje matematyczne, to dlatego, że nie po to jest.


1
„dziesięciolecia, zanim mieliśmy nawet programowalne komputery” - źle. Komputer programowalny istniał wcześniej (jeśli nie uniwersalny), a pierwsze komputery uniwersalne zostały zbudowane w latach 30. XX wieku.
Raphael

-2

Rachunek lambda istnieje, dzięki czemu można tworzyć anonimowe (aka lambda) funkcje. Jeśli nie zrezygnujesz z nazw funkcji, przestrzeń nazw może być zaśmiecona i można zabraknąć dostępnych nazw funkcji. Jest to szczególnie ważne w przypadku tak zwanych „funkcji wyższego rzędu”, które zwracają funkcje (lub wskaźniki funkcji) z oczywistych powodów.

Zasadniczo funkcje lambda są równoważne zmiennym o zasięgu lokalnym. Programowanie funkcjonalne bez funkcji lambda jest analogiczne do programowania proceduralnego bez żadnych zmiennych lokalnych, tj. Strasznego pomysłu.

„dlaczego rachunek lambda jest w ogóle rzeczą” matematycy uwielbiają nadmiarowość. rachunek lambda jest rzadko używany w matematyce, ponieważ jak odkryłeś, notacja nie jest zbyt przydatna.

„Jeśli potrafisz nawet opracować interaktywnego asystenta dowodu opartego na algebrze gimnazjalnej, który pozwoliłby nam udowodnić wiele twierdzeń sformalizowanych za pomocą asystentów dowodowych opartych na rachunku lambda, takich jak Coq i Isabelle, byłoby jeszcze lepiej. potem zacznijcie korzystać z algebry gimnazjalnej, i jestem pewien, że wielu innych by ze mną. ” Czy słyszałeś o metamacie? Nie bierze w tym udziału żaden rachunek lambda, może udowodnić wiele twierdzeń coq / izabelle


Oprócz niektórych opinii, co oferuje ta odpowiedź?
Raphael

@Raphael Misinformation. Większość tej odpowiedzi nie ma nawet sensu. Nie brakuje nazwisk. „Funkcje Lambda” nie są równoważne zmiennym o zasięgu lokalnym; to nawet nie ma sensu. Zakładam, że ma to dotyczyć let, ale chociaż letmożna je zakodować za pomocą anonimowych funkcji, najwyraźniej nie można tego zrobić inaczej. Programowanie funkcjonalne nie wymaga „funkcji lambda”, np. FP lub Sisal Backusa .
Derek Elkins opuścił SE

głównie chciałem opublikować komentarz do odpowiedzi hana, ale nie miałem dość karmy. więc postanowiłem zamienić komentarz w pełnoprawną odpowiedź
sn
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.