Rachunek lambda poza programowaniem funkcjonalnym?

21

Jestem studentem uniwersytetu i obecnie studiujemy rachunek Lambda Calculus. Nadal jednak trudno mi zrozumieć, dlaczego jest to dla mnie przydatne. Zdaję sobie sprawę, że jeśli wykonujesz mnóstwo programowania funkcjonalnego, może to być przydatne, ale uważam, że tak naprawdę nie jest ono potrzebne do nauki programowania funkcjonalnego, co myślisz?

Po drugie, czy Lambda Calculus ma jakieś zastosowanie w dziedzinie informatyki, ale poza funkcjonalnymi językami programowania?

lambda-calculus functional-programming Jakub
źródło

15

Rachunek lambda ma podstawowe znaczenie w logice, teorii kategorii, teorii typów, weryfikacji formalnej, ... Zasadniczo, ma to związek z semantyką języka programowania i logiką formalną. Jest to tak fundamentalny formalizm, że ludzie pracujący w tych dziedzinach nawet nie kwestionują jego korzyści.

Myślę, że jest to niezwykle przydatne do zrozumienia programowania funkcjonalnego, ponieważ daje istotę programowania funkcjonalnego. Funkcje, zastosowanie, podstawienie. Na tej podstawie możesz budować swoje umiejętności rozumowania programów funkcjonalnych i ich transformacji. Funkcje wyższego rzędu to pestka.

Pewnie, że możesz nauczyć się programowania funkcjonalnego bez rachunku lambda, ale nigdy tak naprawdę nie zrozumiałbyś programowania funkcjonalnego bez niego.

Dave Clarke
źródło

Bardzo dziękuję za odpowiedź, Dave. Myślę, że weryfikacja formalna jest najlepszym z dotychczasowych powodów, dlaczego rachunek lambda jest dla mnie przydatny do nauki, a co ciekawe, w przyszłym semestrze przeprowadzę kurs weryfikacji formalnej. Czy użyłbyś również rachunku lambda do formalnej weryfikacji oprogramowania napisanego w dowolnym języku, np. Imperatywnym lub obiektowym?

Jacob

1

Nie możesz używać rachunku lambda bezpośrednio podczas weryfikacji formalnej, ale pojawi się on w podstawach weryfikacji formalnej. Pisanie specyfikacji często obejmuje pisanie w funkcjonalnym języku, nawet w przypadku kodu imperatywnego / OO.

Dave Clarke

Ok, to ciekawe, dziękuję, teraz mam trochę więcej powodów, żeby się tego uczyć. Czy wiesz, czy rachunek lambda służy do projektowania języków niefunkcjonalnych (na niższych poziomach)?

Jacob

1

ALGOL. Scala Ostatecznie na twoje pytanie trudno odpowiedzieć. Rachunek lambda stał się częścią powszechnej wiedzy dla (większości) projektantów języków i dlatego wpływa na projektowanie języka, nawet jeśli nie jest jawnie używany. Rozważ bloki w Smalltalk lub Ruby, anonimowe klasy w Javie. Są to zamknięcia, które są ściśle powiązane z funkcjami wyższego rzędu w rachunku lambda.

Dave Clarke

Ok, wielkie dzięki Dave, to bardzo doceniane.

Jacob

17

Pytasz o aplikację poza informatyką i logiką. Można to łatwo znaleźć, na przykład w topologii algebraicznej wygodnie jest mieć zamkniętą kategorię przestrzeni kartezjańskich, patrz wygodna kategoria przestrzeni topologicznych na nLab. Formalnym językiem odpowiadającym kartezjańskim kategoriom zamkniętym jest właśnie rachunek. Pozwól, że zilustruję bardzo prostym przykładem, jak to się przydaje. $\lambda$

Najpierw załóżmy, że ktoś pyta cię, czy funkcja zdefiniowana przez jest różniczkowalna. W rzeczywistości nie musisz tego potwierdzać, po prostu zauważasz, że jest to skład funkcji różniczkowalnych, a zatem różniczkowalnych. Innymi słowy, wyciągnąłeś łatwy wniosek na podstawie formy definicji. $f : \mathbb{R} \to \mathbb{R}$ $f(x) = x^2 e^x + \log (1 + x^2)$

Teraz prawdziwy przykład. Załóżmy, że ktoś pyta cię, czy funkcja zdefiniowana przez $f : \mathbb{R} \to \mathbb{R}$

fa (x) = (λ fa : do (R) . \int_{- x}^{x} fa (1 + t^{2)}) re t) (λ y : R . max (x, grzech (y + 3)))

$f(x) = \left(\lambda f : \mathcal{C}(\mathbb{R}) . \int_{-x}^{x} f(1 + t^2) dt\right)(\lambda y : \mathbb{R} . \max(x, \sin(y + 3))$ jest ciągły. Ponownie możemy natychmiast odpowiedzieć „tak”, ponieważ funkcja jest definiowana za pomocą

rachunku i rozpoczynając od ciągłych map

,

itp.

λ

$\lambda$

max

$\max$

\int

$\int$

\sin

$\sin$

Różne rozszerzenia kalkulatora umożliwiają robienie tego samego w innych obszarach. Na przykład, ponieważ gładki topos jest kartezjańską kategorią zamkniętą, każda mapa, która jest zdefiniowana za pomocą rachunku, zaczynając od pochodnych i struktury pierścieniowej reali (i możesz wrzucić funkcję wykładniczą, jeśli chcesz) jest automatycznie gładka . (W rzeczywistości głównym celem gładkiego toposu jest istnienie nilpotentnych nieskończoności, które pozwalają w znaczący sposób powiedzieć rzeczy takie jak „rozcinamy dysk na nieskończenie cienkie trójkąty równoramienne”.) $\lambda$ $\lambda$

Andrej Bauer
źródło

1

Dziękuję za wypracowaną odpowiedź. Właściwie próbowałem znaleźć zastosowanie rachunku lambda w informatyce, ale poza programowaniem funkcjonalnym, przepraszam, jeśli nie było to jasne. Zmieniłem pytanie, aby jaśniej to stwierdzić.

Jakub

Ach, szkoda, napisałbym na ten temat szczegółową odpowiedź.

Andrej Bauer,

Przepraszam za to. Dodaj komentarze, jeśli chcesz dodać dodatkowe informacje :)

Jacob

2

λ

$\lambda$

7

$\lambda$ $\lambda$

$\lambda$

Martin Berger
źródło

5

$\lambda$

Peter Wone
źródło

2

Nie wiedząc o tym więcej, słyszę, że językoznawcy używają rachunku lambda.

http://www.sfu.ca/~jeffpell/Ling406/LambdaAbstractionOH.pdf , https://files.nyu.edu/cb125/public/Lambda/

Lukas Rytz
źródło

11

Czy możesz podsumować, co kryje się za linkami? Mają tendencję do pękania. Dzięki temu Twoja odpowiedź będzie bardziej samodzielna.

Juho,

Rachunek lambda poza programowaniem funkcjonalnym?

Odpowiedzi: