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

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.

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

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)

zmniejszy się do

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.$e$$e$$e'$$e'$

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

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$$\phi_T$$\phi_T$$T$

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

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 .$\mathbb{R}$$\mathbb{R}$

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.

$x^2$$x$$x^2$

$\lambda x.x^2$$x^2$

$f$$f(x) = x^2$$f$

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.

$\frac{d}{dx} x^2$$\frac{d}{dx}$$x^2$

$\theta : V \to 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

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

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 .

$\lambda$

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.

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