Главная
Новости
Строительство
Ремонт
Дизайн и интерьер



















Яндекс.Метрика

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

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

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

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

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

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

  • Аппликация (лат. applicatio — прикладывание, присоединение) означает применение или вызов функции по отношению к заданному значению. Её обычно обозначают f   a {displaystyle f a} , где f {displaystyle f} — функция, а a {displaystyle a} — аргумент. Это соответствует общепринятой в математике записи f ( a ) {displaystyle f(a)} , которая тоже иногда используется, однако для λ-исчисления важно то, что f {displaystyle f} трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация f {displaystyle f} к a {displaystyle a} может рассматриваться двояко: как результат применения f {displaystyle f} к a {displaystyle a} , или же как процесс вычисления f   a {displaystyle f a} . Последняя интерпретация аппликации связана с понятием β-редукции.
  • Абстракция или λ-абстракция (лат. abstractio — отвлечение, отделение) в свою очередь строит функции по заданным выражениям. Именно, если t ≡ t [ x ] {displaystyle tequiv t[x]} — выражение, свободно содержащее x {displaystyle x} , тогда запись   λ x . t [ x ] {displaystyle lambda x.t[x]} означает: λ функция от аргумента x {displaystyle x} , которая имеет вид t [ x ] {displaystyle t[x]} , обозначает функцию x ↦ t [ x ] {displaystyle xmapsto t[x]} . Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы x {displaystyle x} свободно входило в t {displaystyle t} , не очень существенно — достаточно предположить, что λ x . t ≡ t {displaystyle lambda x.tequiv t} , если это не так.

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

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

β-редукция

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

( λ x .2 ⋅ x + 1 )   3 {displaystyle (lambda x.2cdot x+1) 3} ,

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

( λ x . t )   a = t [ x := a ] , {displaystyle (lambda x.t) a=t[x:=a],}

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

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

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

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

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

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

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

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

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

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

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

В лямбда-исчислении функция не может непосредственно ссылаться на себя. Тем не менее, функции может быть передан параметр, связанный с ней. Как правило, этот аргумент стоит на первом месте. Связав его с функцией, мы получаем новую, уже рекурсивную функцию. Для этого аргумент, ссылающийся на себя (здесь обозначен как r {displaystyle 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} } — неподвижная точка 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} , где n {displaystyle n} — число, для которого вычисляется факториал. Пусть n = 4 {displaystyle 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} } , каждое рекурсивное определение может быть выражено как лямбда-выражение. В частности, мы можем определить вычитание, умножение, сравнение натуральных чисел рекурсивно.

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

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