Лямбда-числення
З Вікіпедії, безкоштовно encyclopedia
Ля́мбда-чи́слення, або λ-чи́слення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій, а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак Парадокс Кліні-Россера[en] демонструє, що лямбда-числення не здатне уникнути теоретико-множинних парадоксів. Незважаючи на це, лямбда-числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування[1].
Лямбда-числення можна розглядати як ідеалізовану, мінімалістичну мову програмування, у цьому сенсі лямбда-числення подібне до машини Тюрінга, іншої мінімалістичної абстракції, здатної визначати будь-який алгоритм. Відмінність між ними полягає в тому, що лямбда-числення відповідає функціональній парадигмі визначення алгоритмів, а машина Тюрінга, натомість — імперативній. Тобто, машина Тюрінга має певний «стан» — перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда-числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних (сталість).
Ядро λ-числення ґрунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови[2].