Лямбда-исчисление

Разделы:

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

Содержание

1 Чистое '»`UNIQ—postMath-00000001-QINU`»‘-исчисление
2 Аппликация и абстракция
3 α-эквивалентность
4 β-редукция
5 η-преобразование
6 Каррирование (карринг)
7 Семантика бестипового '»`UNIQ—postMath-00000033-QINU`»‘-исчисления
8 Связь с рекурсивными функциями
9 В языках программирования
10 См. также
11 Примечания
12 Литература

Чистое λ{displaystyle lambda } $lambda$ -исчисление

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

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

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

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

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

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

Основная форма эквивалентности, определяемая в лямбда-термах, это альфа-эквивалентность. Например, λx.x{displaystyle lambda x.x}

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

β-редукция

Поскольку выражение λx.2⋅x+1{displaystyle lambda x.2cdot x+1}

$lambda x.2cdot x+1$ обозначает функцию, ставящую в соответствие каждому x{displaystyle x} $x$ значение 2⋅x+1{displaystyle 2cdot x+1} $2cdot x+1$ , то для вычисления выражения (λx.2⋅x+1) 3{displaystyle (lambda x.2cdot x+1) 3} $(lambda x.2cdot x+1) 3$ ,

в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм 2⋅x+1{displaystyle 2cdot x+1}

$2cdot x+1$ вместо переменной x{displaystyle x} $x$ . В результате получается 2⋅3+1=7{displaystyle 2cdot 3+1=7} $2cdot 3+1=7$ . Это соображение в общем виде записывается как(λx.t) a=t[x:=a],{displaystyle (lambda x.t) a=t[x:=a],} $(lambda x.t) a=t[x:=a],$

и носит название β-редукция. Выражение вида (λx.t) a{displaystyle (lambda x.t) a}

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

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

η{displaystyle eta }

-преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применёнными к любому аргументу, дают одинаковые результаты. η{displaystyle eta } $eta$ -преобразование переводит друг в друга формулы λx.f x{displaystyle lambda x.f x} $lambda x.f x$ и f{displaystyle f} $f$ (только если x{displaystyle x} $x$ не имеет свободных вхождений в f{displaystyle f} $f$ : иначе, свободная переменная x{displaystyle x} $x$ после преобразования станет связанной внешней абстракцией или наоборот).

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

Функция двух переменных x{displaystyle x}

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

Семантика бестипового λ{displaystyle lambda } $lambda$ -исчисления

Тот факт, что термы λ{displaystyle lambda }

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

Эту трудность в начале 1970-х годов преодолел Дана Скотт, построив понятие области D{displaystyle D}

$D$ (изначально на полных решётках [1], в дальнейшем обобщив до полного частично упорядоченного множества со специальной топологией) и урезав D→D{displaystyle Dto D} ${displaystyle Dto D}$ до непрерывных в этой топологии функций [2]. На основе этих построений была создана денотационная семантика [en] языков программирования, в частности, благодаря тому, что с помощью них можно придать точный смысл таким двум важным конструкциям языков программирования, как рекурсия и типы данных.

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

Основная статья: Комбинатор неподвижной точки

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

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

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

$r$ ), обязательно должен быть передан в тело функции.

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

f := g g

Это решает специфичную проблему вычисления факториала, но решение в общем виде также возможно. Получив лямбда-терм, представляющий тело рекурсивной функции или цикл, передав себя в качестве первого аргумента, комбинатор неподвижной точки возвратит необходимую рекурсивную функцию или цикл. Функции не нуждаются в явной передаче себя каждый раз.

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

Y = λg.(λx.g (x x)) (λx.g (x x))В лямбда-исчислении, Y g{displaystyle operatorname {Y g} }

{displaystyle operatorname {Y g} }

— неподвижная точка g{displaystyle operatorname {g} }

{displaystyle operatorname {g} }

; продемонстрируем это:

Y g

(λh.(λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g).Теперь, чтобы определить факториал, как рекурсивную функцию, мы можем просто написать g (Y g)⁡n{displaystyle operatorname {g (Y g)} n}

{displaystyle operatorname {g (Y g)} n}

, где n{displaystyle n}

n

— число, для которого вычисляется факториал. Пусть n=4{displaystyle n=4}

n=4

, получаем:

g (Y g) 4 (λfn.(1, if n = 0; and n·(f(n-1)), if n>0)) (Y g) 4 (λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0)) 4 1, if 4 = 0; and 4·(g(Y g) (4-1)), if 4>0 4·(g(Y g) 3) 4·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 3) 4·(1, if 3 = 0; and 3·(g(Y g) (3-1)), if 3>0) 4·(3·(g(Y g) 2)) 4·(3·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 2)) 4·(3·(1, if 2 = 0; and 2·(g(Y g) (2-1)), if 2>0)) 4·(3·(2·(g(Y g) 1))) 4·(3·(2·(λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 1))) 4·(3·(2·(1, if 1 = 0; and 1·((Y g) (1-1)), if 1>0))) 4·(3·(2·(1·((Y g) 0)))) 4·(3·(2·(1·((λn.(1, if n = 0; and n·((Y g) (n-1)), if n>0) 0)))) 4·(3·(2·(1·(1, if 0 = 0; and 0·((Y g) (0-1)), if 0>0)))) 4·(3·(2·(1·(1)))) 24

Каждое определение рекурсивной функции может быть представлено как неподвижная точка соответствующей функции, следовательно, используя Y{displaystyle operatorname {Y} }

${displaystyle operatorname {Y} }$ , каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.

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

В языках программирования под «λ{displaystyle lambda }

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

См. также

Примечания

↑ Scott D.S. The lattice of flow diagrams.— Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.— Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311—372.
↑ Scott D.S. Lattice-theoretic models for various type-free calculi. — In: Proc. 4th Int. Congress for Logic, Methodology, and the Philosophy of Science, Bucharest, 1972.

Литература

Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика: Пер. с англ. — М.: Мир, 1985. — 606 с.