Ля́мбда-исчисле́ние ( λ-исчисление ) — формальная система , разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости .

Чистое λ-исчисление

Чистое λ-исчисление , термы которого, называемые также объектами («обами»), или λ -термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличие каких-либо констант не предполагается.

Аппликация и абстракция

В основу λ-исчисления положены две фундаментальные операции:

• Аппликация ( лат. applicatio — прикладывание, присоединение) означает применение функции к заданному значению аргумента (то есть вызов функции). Её обычно обозначают ${\displaystyle f\ a}$ , где ${\displaystyle f}$ — функция, а ${\displaystyle a}$ — аргумент. Это соответствует общепринятой в математике записи ${\displaystyle f(a)}$ , которая тоже иногда используется, однако для λ-исчисления важно то, что ${\displaystyle f}$ трактуется как алгоритм , вычисляющий результат по заданному входному значению. В этом смысле аппликация ${\displaystyle f}$ ${\displaystyle a}$ может рассматриваться двояко: как результат применения ${\displaystyle f}$ к ${\displaystyle a}$ , или же как процесс вычисления этого результата. Последняя интерпретация аппликации связана с понятием β-редукции .

• Абстракция или λ-абстракция ( лат. abstractio — отвлечение, отделение), в свою очередь, строит функции по заданным выражениям. Именно, если ${\displaystyle t\equiv t[x]}$ — выражение, содержащее ${\displaystyle x}$ , тогда запись ${\displaystyle (\lambda x.t[x])}$ означает: λ функция от аргумента ${\displaystyle x}$ , которая имеет вид ${\displaystyle t[x]}$ , и обозначает функцию ${\displaystyle x\mapsto t[x]}$ . Здесь скобки не обязательны и использованы для ясности, так как точка является частью нотации и отделяет имя связанной переменной от тела функции. Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы ${\displaystyle x}$ свободно входило в ${\displaystyle t}$ , не обязательно — в этом случае ${\displaystyle \ \lambda x.t}$ обозначает функцию ${\displaystyle x\mapsto t}$ , то есть такую, которая игнорирует свой аргумент.

α-эквивалентность

Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, ${\displaystyle \lambda x.x}$ и ${\displaystyle \lambda y.y}$ это альфа-эквивалентные лямбда-термы которые оба представляют одну и ту же функцию — а именно, функцию тождества ${\displaystyle x\mapsto x}$ . Термы ${\displaystyle x}$ и ${\displaystyle y}$ не являются альфа-эквивалентными, так как являются свободными переменными.

Вообще говоря, ${\displaystyle \alpha }$ -преобразование это переименование связанных переменных, не меняющее «смысла» терма. Структурно, два λ-терма ${\displaystyle \alpha }$ -эквивалентны если это один и тот же терм, либо если какие-либо их составляющие термы соответстветственно ${\displaystyle \alpha }$ -эквивалентны.

Для абстракций, терм ${\displaystyle \lambda y.t[y]}$ ${\displaystyle \alpha }$ -эквивалентен ${\displaystyle \lambda x.t[x]}$ , если ${\displaystyle t[y]}$ это ${\displaystyle t[x]}$ в котором все свободные появления ${\displaystyle x}$ заменены на ${\displaystyle y}$ , при условии, что 1.) ${\displaystyle y}$ не входит свободно в ${\displaystyle t[x]}$ , и 2.) ${\displaystyle x}$ не входит свободно ни в одну абстракцию ${\displaystyle \lambda y}$ внутри ${\displaystyle t[x]}$ (если такие есть).

Требование, чтобы ${\displaystyle y}$ не была свободной переменной в ${\displaystyle t[x]}$ — существенно, так как иначе она окажется «захваченной» абстракцией ${\displaystyle \lambda y}$ после ${\displaystyle \alpha }$ -преобразования, и из свободной переменной в ${\displaystyle \lambda x.t[x]}$ превратится в связанную переменную в ${\displaystyle \lambda y.t[y]}$ .

Второе требование необходимо чтобы предотвратить случаи подобные тому, когда, например, ${\displaystyle \lambda y.x}$ является частью ${\displaystyle t[x]}$ . Тогда необходимо произвести ${\displaystyle \alpha }$ -преобразование такой абстракции, например, в данном случае, в ${\displaystyle \lambda z.x}$ .

β-редукция

Применение некой фунции к некоему аргументу выражается в ${\displaystyle \lambda }$ -исчислении как аппликация ${\displaystyle \lambda }$ -терма, выражающего эту функцию, и ${\displaystyle \lambda }$ -терма аргумента. Например, применение функции ${\displaystyle f(x)=2x+1}$ к числу 3 выражается аппликацией

${\displaystyle (\lambda x.2\cdot x+1)\ 3,}$

в которой на первом месте находится соответствующая абстракция . Поскольку эта функция ставит в соответствие каждому ${\displaystyle x}$ значение ${\displaystyle 2x+1}$ , для вычисления результата необходимо заменить каждое свободное появление переменной ${\displaystyle x}$ в терме ${\displaystyle 2\cdot x+1}$ на терм 3.

В результате получается ${\displaystyle 2\cdot 3+1=7}$ . Это соображение в общем виде записывается как

${\displaystyle (\lambda x.t)\ a=t[x:=a]}$

и носит название β-редукция . Выражение вида ${\displaystyle (\lambda x.t)\ a}$ , то есть применение абстракции к некоему терму, называется редексом (redex). Несмотря на то, что β-редукция по сути является единственной «существенной» аксиомой λ-исчисления, она приводит к весьма содержательной и сложной теории. Вместе с ней λ-исчисление обладает свойством полноты по Тьюрингу и, следовательно, представляет собой простейший язык программирования .

η-преобразование

${\displaystyle \eta }$ -преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты.

${\displaystyle \eta }$ -преобразование переводит друг в друга формулы ${\displaystyle \lambda x.f\ x}$ и ${\displaystyle f}$ , но только если ${\displaystyle x}$ не появляется свободно в ${\displaystyle f}$ . Иначе, свободная переменная ${\displaystyle x}$ в ${\displaystyle f}$ после преобразования стала бы связанной внешней абстракцией ${\displaystyle \lambda x}$ , и наоборот; и тогда применение этих двух выражений сводилось бы ${\displaystyle \beta }$ -редукцией к разным результатам.

Перевод ${\displaystyle \lambda x.f\ x}$ в ${\displaystyle f}$ называют ${\displaystyle \eta }$ -редукцией, а перевод ${\displaystyle f}$ в ${\displaystyle \lambda x.f\ x}$ — ${\displaystyle \eta }$ -экспансией.

Каррирование (карринг)

Функция двух переменных ${\displaystyle x}$ и ${\displaystyle y}$ ${\displaystyle f(x,y)=x+y}$ может быть рассмотрена как функция одной переменной ${\displaystyle x}$ , возвращающая функцию одной переменной ${\displaystyle y}$ , то есть как выражение ${\displaystyle \ \lambda x.\lambda y.x+y}$ . Такой приём работает точно так же для функций любой арности . Это показывает, что функции многих переменных могут быть выражены в λ-исчислении и являются « синтаксическим сахаром ». Описанный процесс превращения функций многих переменных в функцию одной переменной называется карринг (также: каррирование ), в честь американского математика Хаскелла Карри , хотя первым его предложил Моисей Шейнфинкель ( 1924 ).

Соответственно, аппликация n -арных функций это на самом деле аппликация вложенных унарных функций, одна за другой. Например, для бинарных функций:

 (λxy. ...x...y...) a b = (λx.λy. ...x...y...) a b = (λx.(λy. ...x...y...)) a b = (((λx.(λy. ...x...y...)) a) b) = (λy. ...a...y...) b = ...a...b... 

Семантика бестипового λ-исчисления

Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе), приводит к сложностям построения адекватной семантики λ-исчисления. Чтобы придать λ-исчислению какой-либо смысл, необходимо получить множество ${\displaystyle D}$ , в которое вкладывалось бы его пространство функций ${\displaystyle D\to D}$ . В общем случае такого ${\displaystyle D}$ не существует по соображениям ограничений на мощности этих двух множеств, ${\displaystyle D}$ и функций из ${\displaystyle D}$ в ${\displaystyle D}$ : второе имеет бо́льшую мощность, чем первое.

Эту трудность в начале 1970-х годов преодолел Дана Скотт , построив понятие ${\displaystyle D}$ (изначально на , в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией ) и урезав ${\displaystyle D\to D}$ до непрерывных в этой топологии функций . На основе этих построений была создана языков программирования , в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных .

Связь с рекурсивными функциями

Рекурсия — это определение функции через саму себя; на первый взгляд, лямбда-исчисление не позволяет этого, но это впечатление обманчиво. Например, рассмотрим рекурсивную функцию ${\displaystyle f}$ , вычисляющую факториал :

f(n) = 1, if n = 0; else n × f(n - 1).

Эта функция не может быть выражена λ-термом (λn.(1, if n = 0; else n × (f (n-1)))) , так как в нём f является свободной переменной. Функция ${\displaystyle f}$ ссылается на саму себя посредством ссылки на своё имя, но в лямбда-исчислении у λ-термов имен нет.

Тем не менее, λ-термы могут быть переданы как аргумент, в том числе и самим себе. Терм-функция может получить сам себя как аргумент, который окажется связанным с его параметром. Как правило, этот параметр стоит на первом месте. Когда он связан с самой функцией, получается новый λ-терм, выражающий уже саму рекурсивную функцию. Для этого параметр, ссылающийся на себя (здесь обозначен как ${\displaystyle h}$ ), обязательно должен быть передан явным образом как аргумент при рекурсивном вызове (как ${\displaystyle h\ h}$ ):

U := λh. h h

F := U (λh. λn. (1, if n = 0; else n × ((h h) (n-1))))

где ${\displaystyle U}$ — это комбинатор само-аппликации, ${\displaystyle Uh=h\ h}$ .

Этот приём позволяет решить каждую конкретную проблему, как вычисление факториала здесь, создавая рекурсивную функцию через изменение λ-терма, для его явной передачи самому себе как добавочного аргумента. Но решение в общем виде также возможно. Несколькими несложными преобразованиями получается (подразумевая каррирование):

 U (λh. λn. (1, if n = 0; else n × (h h (n-1)))) U (λh. (λr. λn. (1, if n = 0; else n × (r (n-1)))) (h h)) (λg. U (λh. g (h h))) (λr. λn. (1, if n = 0; else n × (r (n-1)))) 

Это эквивалентное выражение состоит из аппликации двух независимых λ-термов, где второй — это просто лямбда-выражение рекурсивной функции без изменений, но с абстрагированным рекурсивным вызовом ${\displaystyle (\lambda r)}$ . А первый это некий комбинатор, называемый ${\displaystyle Y}$ :

G := (λr. λn. (1, if n = 0; else n × (r (n-1)))) Y := λg. U (λh. g (h h)) = λg. (λh. g (h h)) (λh. g (h h)) 

Этот комбинатор создает рекурсивную функцию из аргумента, являющегося закрытым (то есть в котором нет свободных переменных) λ-термом исходного выражения функции (то есть без удвоения параметра). Таким образом,

Y g = (λh. g (h h)) (λh. g (h h)) = g ((λh. g (h h)) (λh. g (h h))) = g (Y g) 

то есть ${\displaystyle \operatorname {Y} }$ — это комбинатор неподвижной точки: он вычисляет неподвижную точку своего аргумента. Для закрытого λ-терма с соответствующей арностью, его неподвижная точка выражает рекурсивную функцию, так как ${\displaystyle Y\ g\ n=g\ (Y\ g)\ n}$ , то есть аргумент который здесь создаётся для вызова внутри ${\displaystyle g}$ — это та же самая функция ${\displaystyle Y\ g\ }$ .

F = Y (λr. λn. (1, if n = 0; else n × (r (n-1)))) = Y G = G (Y G) = (λr. λn. (1, if n = 0; else n × (r (n-1)))) (Y G) = (λn. (1, if n = 0; else n × (Y G (n-1)))) = (λn. (1, if n = 0; else n × (F (n-1)))) = G F 

Итак, ${\displaystyle G}$ — это закрытый функционал, то есть λ-терм, вызывающий свой аргумент в качестве функции; его неподвижная точка — это функция (здесь, ${\displaystyle F}$ ), которая передаётся ему в качестве аргумента; а вызов той же самой функции и есть рекурсивный вызов.

Существует несколько определений комбинаторов неподвижной точки. Вышеуказанное — самое простое:

Y := λg. (λh. g (h h)) (λh. g (h h))

Используя стандартные комбинаторы ${\displaystyle B}$ и ${\displaystyle C}$ ,

Y g = U (λh. g (U h)) = U (λh. B g U h) = U (B g U) = U (C B U g) = B U (C B U) g 

В самом деле:

U (B g U) = B g U (B g U) = g (U (B g U)) = g (Y g) 

Итак, чтобы определить факториал как рекурсивную функцию, мы можем просто написать ${\displaystyle \operatorname {Y} G\ n}$ , где ${\displaystyle n}$ — число, для которого вычисляется факториал. Пусть ${\displaystyle n=4}$ , получаем:

Y G 4 Y (λrn.(1, if n = 0; else n×(r (n-1)))) 4 (λrn.(1, if n = 0; else n×(r (n-1)))) (Y G) 4 (λn.(1, if n = 0; else n×(Y G (n-1)))) 4 1, if 4 = 0; else 4×(Y G (4-1)) 4×(Y G 3) 4×(G (Y G) 3) 4×((λrn.(1, if n = 0; else n×(r (n-1)))) (Y G) 3) 4×(1, if 3 = 0; else 3×(Y G (3-1))) 4×(3×(G (Y G) 2)) 4×(3×(1, if 2 = 0; else 2×(Y G (2-1)))) 4×(3×(2×(G (Y G) 1))) 4×(3×(2×(1, if 1 = 0; else 1×(Y G (1-1))))) 4×(3×(2×(1×(G (Y G) 0)))) 4×(3×(2×(1×(1, if 0 = 0; else 0×(Y G (0-1)))))) 4×(3×(2×(1×(1)))) 24 

Итак, каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующего закрытого функционала описывающего «один вычислительный шаг» рекурсивной функции. Следовательно, используя ${\displaystyle \operatorname {Y} }$ , каждое рекурсивное определение может быть выражено как лямбда-выражение (λ-терм). В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно, и выразить их как λ-термы.

В языках программирования

В языках программирования под «λ-исчислением» зачастую понимается механизм « анонимных функций » — callback -функций, которые можно определить прямо в том месте, где они используются, и которые имеют доступ ко всем переменным видимым в месте их вызова в текущей функции ( замыкание ).

См. также

• Типизированное λ-исчисление
• Комбинаторная логика
• Функциональное программирование
• Теорема Чёрча — Россера

Примечания

Литература

• Барендрегт, Хенк . Ламбда-исчисление. Его синтаксис и семантика. — М. : Мир , 1985. — 606 с. — 4800 экз.