Лямбда-исчисление
Материал из Поле цифровой дидактики
| Описание | Ля́мбда-исчисле́ние (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости. |
|---|---|
| Область знаний | Математика |
| Авторы | Чёрч |
| Поясняющее видео | |
| Близкие понятия | Функциональное программирование |
| Среды и средства для освоения понятия |
В основу λ-исчисления положены две фундаментальные операции:
- Аппликация (прикладывание, присоединение) означает применение функции к заданному значению аргумента (т.е. вызов функции). Её обычно обозначают [math]\displaystyle{ f\ a }[/math], где [math]\displaystyle{ f }[/math] — функция, а [math]\displaystyle{ a }[/math] — аргумент. Это соответствует общепринятой в математике записи [math]\displaystyle{ f(a) }[/math], которая тоже иногда используется, однако для λ-исчисления важно то, что [math]\displaystyle{ f }[/math] трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация [math]\displaystyle{ f }[/math] [math]\displaystyle{ a }[/math] может рассматриваться двояко: как результат применения [math]\displaystyle{ f }[/math] к [math]\displaystyle{ a }[/math], или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием β-редукции.
- Абстракция или λ-абстракция — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если [math]\displaystyle{ t\equiv t[x] }[/math] — выражение, содержащее [math]\displaystyle{ x }[/math], тогда запись [math]\displaystyle{ (\lambda x.t[x]) }[/math] означает: λ функция от аргумента [math]\displaystyle{ x }[/math], которая имеет вид [math]\displaystyle{ t[x] }[/math], и обозначает функцию [math]\displaystyle{ x\mapsto t[x] }[/math]. Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы [math]\displaystyle{ x }[/math] свободно входило в [math]\displaystyle{ t }[/math], не обязательно — в этом случае [math]\displaystyle{ \ \lambda x.t }[/math] обозначает функцию [math]\displaystyle{ x\mapsto t }[/math], т.е. такую, которая игнорирует свой аргумент.
- Пример на Python
lambda x: x * 2
