Лямбда-исчисление. 
Функциональное программирование

В результате изучения материала главы 9 студент должен: знать

• • основные понятия лямбда-исчисления;
• • место и роль различных редукций в лямбда-исчислении;
• • роль Y-комбинатора в организации рекурсии;
• • методы представления констант и функций в чистом лямбда-исчислении; уметь
• • приводить выражения к нормальной и слабой заголовочной нормальной форме в системе редукций лямбда-исчисления;
• • отличать понятия чистого и расширенного лямбда-исчисления; владеть
• • навыками преобразования лямбда-выражений;
• • методами применения переименования переменных при приведении выражений к нормальной форме.

Представление выражений в лямбда-исчислении

Функциональные языки программирования появились в качестве средства для написания программ, не содержащих в явном виде понятий ячеек памяти для хранения значений (переменных) и последовательности вычислений как процесса изменения состояния памяти. Тем не менее основа для создания таких языков была предложена еще в середине 1930;х гг. Алонзо Черчем (Alonzo Church) и Стефаном Клини (Stephen Kleene). Мы рассмотрим теорию Черча, названную им лямбда-исчислением, в качестве теоретической основы и «минимального» функционального языка программирования. В конечном счете любую программу, написанную на языке Haskell или любом другом функциональном языке программирования, можно сравнительно несложными преобразованиями свести к формуле лямбда-исчисления.

Разумеется, ни Черч, ни Клини не создавали язык программирования. Тема, которой они интересовались, — формализация понятия вычислимой функции и создания универсального математического аппарата для определения и работы с вычислимыми функциями. В то время эта область математики активно развивалась в трудах уже упомянутых Черча и Клини, а также Алана Тьюринга (Alan Turing), Эмиля Поста (Emil Post) и других. Во многих работах предлагался следующий подход к формализации понятия функции: в качестве основы берется некоторый «минимальный» набор базовых функций и предлагаются способы построения из них более сложных функций с помощью тех или иных функционалов (функций высшего порядка). Таков, например, подход, использованный Куртом Фридрихом Гёделем (Kurt Friedrich Godel) при создании им теории рекурсивных функций. Напротив, в созданном им лямбда-исчислении Черч сумел построить такую систему, при которой базовых функций нет вовсе, а вместо способов построения сложных функций из простых используются правила преобразований, с помощью которых можно получать из одних функций другие, эквивалентные им. В результате Черчу удалось создать исчисление чистых функций, в котором все математические понятия, такие как числа, арифметика и др., сводятся к понятию функции.

Процесс преобразования формул в лямбда-исчислении Черча (редукции) напоминает процесс вычисления функции, происходящий при исполнении программ. Именно поэтому лямбда-исчисление и легло в основу определения языка Lisp в начале 1960;х гг., а затем оказалось в основе и других функциональных языков программирования.

Рассмотрим теорию Черча более подробно. Основным понятием в лямбда-исчислении является понятие выражения или формулы. Его можно определить рекурсивно. Прежде всего, зафиксируем набор идентификаторов, которые в дальнейшем будем называть переменными. Мы будем использовать в качестве имен латинские буквы x, y, f и др. В формулах переменные обычно обозначают аргументы функций, задаваемых лямбда-выражениями, однако сама по себе переменная является простейшим видом выражения. Два других вида выражений — это определение безымянной функции (лямбда-выражение) и применение функции.

Лямбда-выражение имеет вид (Хх.е), где х — имя переменной, а е — выражение. Семантически такое выражение обозначает функцию с аргументом х и телом е. Применение функции записывается в виде (el е2), где el и е2 — выражения (el — функция, а е2 — ее аргумент). Приведем несколько примеров:

• • Хх. х — простейшая функция, выдающая свой аргумент; скобки опущены, поскольку это не вызывает неоднозначности;
• • Xf. Хх. f х — функция с двумя аргументами, применяющая свой первый аргумент ко второму. Строго говоря, надо было бы расставить скобки, чтобы выражение приняло вид Xf. (Хх. (f х)), однако принято соглашение, по которому «операция» применения функции к аргументу имеет более высокий приоритет, чем «операция» образования лямбда-выражения. Функции при этом применяются в порядке слева направо, т. е. выражение f х у понимается как (f х) у — применение функции / к аргументу х и применение полученного результата к аргументу у. Образование же безымянной функции (операция «лямбда») наоборот применяется справа налево, так что выражение Хх. Ху. е понимается как Хх. (Ху. е);
• • (Хх.х х) (Хх.х х) — применение функции, заданной лямбдавыражением (Хх.х х), к аргументу, представляющему собой такое же лямбда-выражение. Внутри тела, задающего лямбда-выражение, аргумента: применяется к себе.

Мы будем рассматривать не классическое лямбда-исчисление, в котором кроме функций и их применений к другим функциям больше ничего нет, а некоторое его расширение. В нашем расширенном лямбда-исчислении помимо безымянных функций, заданных лямбда-выражениями, будут использоваться константы, смысл которых задан вне лямбда-исчисления. Это будут привычные нам по языкам программирования константы, представляющие целые числа, символы и логические значения, константа, представляющая пустой список NIL (этим идентификатором мы будем обозначать объект, который ранее в языке Haskell всегда обозначался нами парой квадратных скобок [ ]), а также константы, задающие примитивные функции. Примитивные функции нашей системы следует рассмотреть особо.

Многие примитивные функции уже хорошо нам знакомы по языку Haskell и многим другим языкам программирования. Это обычные арифметические операции сложения, умножения и др., операции сравнения величин «больше», «меньше», «равны» и др., операции над логическими значениями «И», «ИЛИ» и др. Мы будем пользоваться ими без какого-либо объяснения. Единственное отличие от стандартного использования этих и других операций от их применения в других языках программирования будет заключаться в том, что мы всегда будем использовать только префиксную запись операций, т. е. вместо привычного 3 + 5 будем записывать выражение +3 5. Конечно, все функции в нашем расширенном лямбдаисчислении будут карринговыми, т. е. выражение + 3 также имеет смысл и представляет собой применение функции + к константе 3, в результате которого получается функция увеличения целого аргумента на 3.

Следует заметить также и то, что если в классическом лямбда-исчислении применение любой функции к любому аргументу всегда осмысленно, поскольку любой «объект» — как аргумент, так и результат — всегда представляет собой лямбда-выражение — функцию одного аргумента, то в нашем расширенном лямбда-исчислении примитивные функции можно применять только к «правильным» аргументам. Так, бессмысленным будет выражение + TRUE 0, поскольку невозможно выполнить сложение логического значения TRUE с числом 0. Также бессмысленным будет выражение /3 0, поскольку результат деления числа 3 на число 0 не определен. Мы не будем рассматривать бессмысленные выражения.

Некоторые важные синтаксические конструкции функциональных языков программирования также будут представлены в нашем расширенном лямбда-исчислении в виде стандартных функций. Например, условные выражения if В then El else Е2 могут быть представлены применением стандартной функции IF с тремя аргументами В, Е1 и Е2. Кортежи будем представлять в виде применения стандартных функций кортежирования TUPLE-n, где п — произвольное натуральное число. Такая функция будет иметь п аргументов и выдавать в результате работы кортеж, содержащий эти аргументы. Обратная функция извлечения элемента кортежа по заданному номеру будет представлена стандартной функцией INDEX, аргументами которой будут номер элемента кортежа и сам этот кортеж. Например, если составить кортеж из чисел 2, 4 и 10, а затем извлечь из пего второй элемент, то мы должны в результате получить число 4. Соответствующая конструкция расширенного лямбда-исчисления будет выглядеть следующим образом:

INDEX 1 (TUPLE-3 2 4 10).

Обратите внимание, что элементы кортежа нумеруются с нуля, гак что второй элемент кортежа будет иметь номер 1.

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