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

Что значит "функция 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-исчисление).