Соглашения об упрощении

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

В этой связи из соображения экономии пространства для вывода соотношений принимаются следующие соглашения, позволяющие значительно сократить запись и увеличить удобство прочтения и обработки ламбда- выражений.

1. Скобки для операции аппликации восстанавливаются по ассоциации влево, например:

xy = (xy), xyz = ((xy)z),...

2. Избыточные скобки могут опускаться, например:

(xy) = xy, ((xy)z) = xyz,...

3. Скобки для операции абстракции восстанавливаются по ассоциации вправо, например:

λxy.M = (λx.(λy.M)), λxyz.M = (λx.(λy.(λz.M))),...

Примеры формального описания исчисления ламбда-конверсий

Рассмотрим следующие шесть ламбда- термов, возможно, с цепочками вывода, согласно правилам построения алфавита:

	x	переменная
		константа
	λx.x	ламбда- абстракция переменного терма x к самому себе (определяет функцию тождества)
	λx.x + 1	добавляет* к аргументу x константу 1, т.е. определяет функцию инкремента (прибавления единицы)
	(λx.x + 1)2 = [2/x](x + 1) = 2+1 = 3	подстановка** согласно аксиоме (a) константы 2 вместо всех вхождений x в выражение x+1
	a $ b	недопустим из-за вхождения неопределенного символа "$"

*Заметим, что в алфавите ламбда-исчисления отсутствует функция сложения как таковая, так что возможны различные интрепретации символа "+" (будем считать его далее "встроенной" функцией сложения).

**Вычисление значения функции в число 3 возможно при корректной интерпретации символа "+".

Соответствие между ламбда-исчислением и функциональным языком

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

Приведем фрагменты SML-программ, соответствующих допустимым ламбда- термам из предыдущего списка:

	x	переменная, тип которой определяется в процессе трансляции на этапе контроля типизации в соответствии с выводом типов
		константа
	fn x => x	функция тождества
	fn x => x+1	функция инкремента
	(fn x => x+1) 2	вычисление значения функции, в результате выполнения получается целое число 3

Продолжим иллюстрацию соответствия между программами на языке SML и ламбда- выражениями.

В общем случае функция f языка программирования SML, имеющая формальный параметр x и тело b, задается следующим описанием:

fun f x = b;

Исследуем операцию аппликации функции к аргументу. Например, описание функции инкремента имеет вид:

fun f x = 1+x;

Для вычисления значения выражения необходимо произвести аппликацию функции к данному выражению; для аппликации функции f к целому числу 4 нужно записать:

f 4;

При вычислении значения функции аппликация производится к ближайшему аргументу. Так, запись

f 2 + 3;

означает порядок аппликации (f2)+3, а не f(2+3), т.е. находится в полном соответствии с соглашениями о скобках, принятыми в ламбда-исчислении.

Выводы по лекции 5

Рассмотрев формальное построение исчисления ламбда-конверсий (алфавит, аксиомы и правила вывода выражений) и сопоставив основные элементы (переменная, константа) и операции (аппликация, подстановка) этой теории с базовыми элементами (переменная, константа) и элементарными программами (объявление и аппликация функции) языка SML, можно сделать вывод о следующих несомненных преимуществах ламбда-исчисления как математической модели языка функционального программирования:

1. лаконичность (ограниченный необходимыми элементами алфавит, два способа построения выражений – аппликация и абстракция, небольшое количество аксиом и правил вывода);

2. интуитивная ясность (обозначения являются краткими и понятными);

3. иллюстративность (ламбда- термы легко интерпретируются не только с помощью алгебраической записи, но и посредством визуальной интерпретации в виде графов, причем редукция, т.е. упрощение вида графов, соответствует бета- редукции ламбда- термов);

4. полнота (в ламбда-исчислении можно представить произвольную, в частности, сколь угодно сложную, функцию);

5. естественная близость к языкам функционального программирования (SML, Scheme, Haskell, Miranda, Hope, Clean) была проиллюстрирована на примерах программ на языке SML.

Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [24, 32, 39, 43, 44, 47, 58, 76].

Дата добавления: 2014-01-07