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

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

 

Ламбда-исчисление было изобретено Алонсом Чёрчем около 1930 г. Чёрч первоначально строил l-исчисление как часть общей системы функций, которая должна стать основанием математики. Но из-за найденных парадоксов эта система оказалась противоречивой. Книга Чёрча [2] содержит непротиворечивую подтеорию его первоначальной системы, имеющую дело только с функциональной частью. Эта теория и есть l-исчисление.

Ламбда-исчисление - это безтиповая теория, рассматривающая функции как правила, а не как графики. В противоположность подходу (вводимому функции как множество пар, состоящих из аргумента и значения) более старое понятие определяет функцию как процесс перехода от аргумента к значению. С первой точки зрения x²-4 и (x+2)(x-2) - разные обозначения одной и той же функции; со второй точки зрения это разные функции.

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

Ламбда-исчисление представляет класс (частичных) функций (l-определимые функции), который в точности характеризует неформальное понятие эффективной вычислимости. Другими словами, l-исчисления, наряду с другими подходами формализует понятие алгоритма [7, с. 143-146].

Ламбда-исчисление стало объектом особенно пристального внимания в информатике после того, как выяснилось, что оно представляет собой удобную теоретическую модель современного функционального программирования [32].

Большинство функциональных языков программирования, например, Лисп, используют l-исчисление в качестве промежуточного кода, в который можно транслировать исходную программу. Функциональные языки "улучшают" нотацию l-исчисления в прагматическом смысле, но при этом, в какой-то мере, теряется элегантность и простота последнего.

Изучение и понимание многих сложных ситуаций в программировании, например, таких, как автоаппликативность (самоприменимость) или авторепликативность (самовоспроизводство), сильно облегчается, если уже имеется опыт работы в l-исчислении, где выделены в чистом виде основные идеи и трудности.

 

Ламбда-выражения и их вычисление

Что значит "функция 5x³+2"? Если кто-то хочет быть точным, он вводит по этому поводу функциональный символ, например f, и говорит: "функция f : Ñ à Ñ, определенная соотношением f(x) = 5x³+2". При этом очевидно, что переменную x можно здесь, не меняя смысла, заменить на другую переменную y. Ламбда-запись устраняет произвольность в выборе f в качестве функционального символа. Она предлагает вместо f выражение "lx. 5x³+2".

Кроме того, обычная запись f(x) может обозначать как имя функции f, так и вызов функции с аргументом x. Для более строгого подхода это необходимо различать. В ламбда-обозначениях вызов функции с аргументом x выглядит как (lx. 5x³+2)x.

Русский математик Шейфинкель заметил, что не обязательно вводить функции более чем одной переменной [3]. Действительно, для функции, скажем от двух переменных, f(x,y) мы можем рассмотреть функцию g_x с соотношением g_x (y) = f(x,y), а затем f' с соотношением f'(x) = g_x. Отсюда (f'(x))(y) = f(x,y). Позднее Карри [1] переоткрыл это свойство и поэтому сейчас сведение функций с несколькими переменными только к функциям одного переменного носит название карринг.

Ламбда-исчисление изучает функции и их аппликативное поведение (т. е. поведение относительно применения к аргументу). Поэтому применение (аппликация) функции к аргументу является исходной операцией l-исчисления. Функция f, примененная к аргументу a, обозначается через f a. Поэтому записи функции в виде lx . x^2+3 соответствует правило:

для любого a (lx . x^2 +3) (a) = a^2+3.

Выражение x + 2y можно считать как функцию от x (записывается lx.x+2y ) и как функцию от y (записывается ly. x +2y). Вызов (lx. x +2y )a приводит к значению a+2y, а вызов (ly. x +2y )a - к значению x+2a.

Запись ly.lx.E понимается как ly.(lx. E). Поэтому ((ly.lx. x+2y) a) b ® (lx. x+2a) b ® b+2a и ((lx.ly. x+2y) a) b ® (ly. a+2y) b ® a+2b.

Мы читаем символ l как “функция от” и точку (.) как “которая возвращает”.

Определение l-термов (l-выражений)

· Каждая переменная есть l-терм.

· Каждая константа есть l-терм.

· По любым l-термам M и N можно построить новый l-терм (MN) (обозначающий применение, или аппликацию, оператора M к аргументу N).

По любой переменной x и любому l-терму M можно построить новый l-терм (lx.M) (обозначающий функцию от x, определяемую l-термом M). Такая конструкция называется l-абстракция.

Набор констант произволен: целые числа, булевы константы, арифметические операции, булевы функции и т. п., причем для записи применения константы-оператора к операндам используется префиксная запись (так + 3 4 обозначает 3+4).

Символ x после l называется связанной переменной абстракции и соответствует понятию формального параметра в традиционной процедуре или функции. Выражение справа от точки называется телом абстракции, и, подобно коду традиционной процедуры или функции, оно описывает, что нужно сделать с параметром, поступившим на вход функции.

Переменная, расположенная не на месте связанной переменной, может ли быть связанной или свободной, что определяется с помощью следующих правил:

1. Переменная x оказывается свободной в выражении x.

2. Все x, имеющиеся в lx.M, являются связанными. Если кроме x в lx.M есть переменная y, то последняя будет свободной или связанной в зависимости от того, свободно она или связанна в M.

3. Переменная встречающаяся в термах M или N выражения (MN) будет связанной или свободной в общем терме в зависимости от того, свободна она или связанна в M или N. Свободные (связанные) переменные - это переменные, которые, по крайней мере, один раз появляются в терме в свободном (связанном) виде.

Мы отождествляем термы, отличающиеся только названием своих связанных переменных, например lx.x º ly.y.

Тело абстракции может быть любым допустимым l-выражением, и поэтому оно также может содержать другую абстракцию, например:

lx . ly . (x+y)*2

Это выражение читается как “функция от x, которая возвращает функцию от y, которая возвращает (x+y)*2”.

Используется соглашение: запись (...(((lx₁.lx₂....lx_n.E)a₁)a₂)...a_n) кратко пишется как (lx₁.lx₂. ... lx_n.E)a₁a₂ ...a_n.

Нам понадобится следующее определение подстановки. Для любых l-термов M, N и переменной x через [N/x]M обозначим результат подстановки N вместо каждого свободного вхождения x в M и замены всех ly в M таким образом, чтобы свободные переменные из N не стали связанными в [N/x]M. Более формально (мы употребляем запись M º N для обозначения того, что термы M и N совпадают):

а) [N/x]x º N;

b) [N/x]y º y, если переменная y не совпадает с x;

c) [N/x](PQ) º ([N/x]P [N/x]Q);

d) [N/x](lx.P) º lx.P;

e) [N/x](ly.P) º ly.[N/x]P, если y не имеет свободных вхождений в N и x имеет свободное вхождение в P;

f) [N/x](ly.P) º lz.[N/x]([z/y]P), если y имеет свободное вхождение в N и x имеет свободное вхождение в P и z - любая переменная, не имеющая свободных вхождений в N;

g) [N/x]t º t, если t является константой.

Следующие примеры пояснят суть определения. Пусть Mºly.yx.

Если N º vx, то [(vx)/x](ly.yx) º ly. [(vx)/x](yx) согласно (e)

º ly. y(vx) согласно (a).

Если N º yx, то [(yx)/x](ly.yx) º lz. [(yx)/x](zx) согласно (f)

º lz.z(yx) согласно (a).

Если бы пункт (f) в определении был опущен, то мы столкнулись бы со следующим нежелательным явлением. Хотя lv.x и ly.x обозначают одну и ту же функцию (константу, чье значение всегда есть x), после подстановки v вместо x они стали бы обозначать разные функции: [v/x](ly.x) º ly.v, [v/x](lv.x) º lv.v.

Мы рассмотрели, как l-нотация может быть использована для представления функциональных выражений и сейчас готовы к тому, чтобы определить правила вывода l-исчисления, которые описывают, как вычислять выражение, т. е. как получать конечное значение выражения из его первоначального вида.

Константы являются самоопределенными,т. е. их невозможно преобразовать в более простые выражения. Если константа, обозначающая функцию (оператор), применяется к соответствующему числу операндов, то такой подтерм называется d-редексом, процесс применения функции называется d-сворачиванием, и в результате появляется новое ламбда-выражение.

Применение константной функции записывается в виде встроенных соответствующих d-правил , например

+ 1 3 ®_d 4

Терм вида (lx.M)N называется b-редексом. (Он также обозначает применение оператора к входному значению.) Если b-редекс содержится в терме P и одно из его вхождений заменяется термом [N/x]M, то мы будем говорить, что происходит свертывание этого вхождение. Обозначение P®_b Q означает, что P b-сворачивается к Q. Конечная последовательность d- или b-свертываний называется редукцией. Если из контекста ясно, было ли d-свертывание или же b-свертывание, то один шаг редукции обозначается просто знаком ® без индекса.

Пример 6.1. Редукция выражений (используемые редексы подчеркнуты):

1) (lf.lx.f 3x) (ly.lx.* x y) 0

® (lx.(ly.lx .*xy)3x) 0 - выбрали один из двух возможных редексов

® (ly.lx.*xy)3 0

® (lx.*x3)0

® *03

® 0

2) (lf.lx.f3x) (ly.lx.*xy) 0

® (lx. (ly.lx.*xy)3 x) 0 - выбрали один из двух возможных редексов

® (lx.(lx.*x3)x )0 - снова делаем произвольный выбор

® (lx.*x3)0

® *03

® 0

Использование констант и d-правил является излишним. Все необходимые константы (числа, встроенные функции и т. п.) можно реализовать, используя в качестве атомарных термов только переменные (так называемое чистое l-исчисление).

Нормальные формы

Говорят, что l-выражение находится в нормальной форме, если к нему нельзя применить никакое правило редукции. Другими словами, l-выражение - в нормальной форме, если оно не содержит редексов. Нормальная форма, таким образом, соответствует понятию конца вычислений в традиционном программировании. Отсюда немедленно вытекает наивная схема вычислений:

while существует хотя бы один редекс

do преобразовывать один из редексов

end
(выражение теперь в нормальной форме).

Различные варианты сворачивания в процессе редукции могут приводить к принципиально различным последствиям.