Rachunek lambda

Ten artykuł od 2021-03 zawiera treści, przy których brakuje odnośników do źródeł.

Należy dodać przypisy do treści niemających odnośników do źródeł. Dodanie listy źródeł bibliograficznych jest problematyczne, ponieważ nie wiadomo, które treści one uźródławiają.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

Rachunek lambda – system formalny używany do badania zagadnień związanych z podstawami matematyki jak rekurencja, definiowalność funkcji, obliczalność, podstawy matematyki np. definicja liczb naturalnych, wartości logicznych itd. Rachunek lambda został wprowadzony przez Alonzo Churcha w 1930 roku. Jest uniwersalną reprezentacją obliczeń i równoznaczny maszynie Turinga, tzn. dowolne wyrażenie w rachunku lambda można przedstawić jako program na maszynie Turinga i odwrotnie. Został użyty do udowodnienia hipotezy, nazwanej później hipotezą Churcha-Turinga.

Rachunek lambda jest przydatny do badania algorytmów. Wszystkie algorytmy, które dadzą się zapisać w rachunku lambda, dadzą się zaimplementować na maszynie Turinga i odwrotnie.

Istnieje wiele rodzajów rachunku lambda, z czego najprostszym jest rachunek lambda bez typów, stanowiący pierwotną inspirację dla powstania programowania funkcyjnego (Lisp). Rachunek lambda z typami jest podstawą dzisiejszych systemów typów w językach programowania.