Лямбда-исчисление (Файлы для подготовки к экзамену)

11

Элементарное введение в -исчисление

Введение.

-Исчисление представляет собой формальную систему, базирующуюся на предложенной А. Черчем идее -нотации функций. При определении функций с помощью выражений, определяющих их значения, аргументы традиционно записывались в той же нотации, которая использовалась и для вызова значения определяемой функции для фактических значений ее аргументов, т.е. либо в скобочной функциональной нотации, либо в бесскобочной нотации, обычно, префиксной. Примеры таких традиционных определений: . В качестве альтернативы А. Черч предложил нотацию, в которой в левой части определения указывается только имя определяемой функции, а список ее аргументов перенесен в правую часть определения. Для приведенных выше примеров это выглядит так: . -нотация позволяет также отказаться от рассмотрения функций арности : предполагается, что такая функция имеет единственный аргумент, а ее значением, в свою очередь, является функция аргументов: , причем при единственном аргументе отпадает необходимость и в использовании разделяющей точки (если символы переменных представляют собой неделимые языковые конструкции). -Нотация функций естественным образом решает вопрос о подстановке определений функции вместо вызовов для вычисления ее значений с конкретными значениями параметров, позволяя рассматривать операцию применения функции к аргументу (аппликацию) как обычную связку. Нетрудно заметить, что -операция функциональной абстракции в конструкции имеет явные черты оператора, связывающего операторную переменную в выражении , описывающем значение конструируемой функции. Как будет видно из дальнейшего, язык, построенный с применением единственной бинарной связки (аппликации) и единственного -оператора (при наличии потенциально бесконечного множества различных переменных), может играть роль универсальной формальной модели вычислимости, обладая при этом новыми интересными особенностями, не присущими традиционным моделям – теории частично-рекурсивных функций и различным математическим уточнениям понятия алгоритма. Базирующаяся на -исчислении теория комбинаторов выглядит еще более «фундаментальной», сохраняя черты универсальности при большей синтаксической простоте.

1. - Термы.

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

Для построения натуральных чисел используются два конструктора: и , а для построения термов - три конструктора: , и .

Далее будет использоваться обычное для описания -исчисления представление:

Для некоторых доказательств мы будем пользоваться понятием -контекста (сорт объектов ); для построения контекстов дополнительно вводится нульарный конструктор . Порождаемый им элементарный контекст будем представлять «дыркой» - символом . Для простоты при построении других контекстов будем использовать те же конструкторы и , что и для построения термов, причем с сохранением представления: , , . Если - контекст, а - терм, то будет обозначать терм, полученный заменой в единственного символа  на терм . Если и - контексты, то обозначает контекст, полученный заменой в контексте единственного символа  на контекст .

Вхождением терма в терм называется пара , такая, что . Различные вхождения одного и того же терма в один и тот же терм отличаются вторыми компонентами соответствующих пар, т.е. контекстами вхождений.

На множестве термов определена функция : называется множеством свободных переменных терма и определяется индуктивно по конструкции терма :

Иными словами, свободной переменной терма называется терм-переменная (или, просто, переменная), имеющая в него хотя бы одно свободное вхождение, т. е.

.

Введем операцию подстановки: .

назовем результатом подстановки терма в терм вместо свободных вхождений переменной и определим его индуктивно по конструкции терма :

Случай , пока остается не определенным.

1. Редукция и конверсия -термов.

Определим преобразование термов (известное и в других формальных системах с переменными и операторами) и назовем его -правилом, или правилом замены операторной (связанной) переменной:

Так как , то и, обратно, . В связи с этим, это правило называют правилом -конверсии термов. Далее термы рассматриваются с точностью до -конверсии или, иными словами, с точностью до обозначения связанных переменных. С учетом этого замечания можно доопределить и операцию подстановки. В ранее не определенном случае всегда можно найти переменную , такую, что , и сделав замену переменной на , можно внести операцию подстановки под знак -оператора:

.

Основу -исчисления составляет так называемое правило -редукции термов, формализующее связь аппликации и -оператора. Если вспомнить, что неформальной основой -исчисления является -нотация функций, то легко заметить, что значение функции для аргумента, являющегося значением выражения , есть значение выражения, полученного подстановкой в выражение вместо переменной , точнее, вместо ее свободных вхождений в выражение . Так, например, значение функции для аргумента – денотата константы 3, есть денотат константы , то есть число десять. Формально эта взаимосвязь представлена в -исчислении в форме бинарного отношения так называемой -редукции термов, определяемого как некоторое замыкание базового отношения между термами:

.

Терм слева называется -редексом, а справа - -контрактом. Отношение -редукции определяется как наименьшее отношение, удовлетворяющее следующим требованиям:

1. .

2. .

3. .

4. , где - произвольный -контекст.

Еще раз заметим, что термы рассматриваются с точностью до -конверсии.

Последовательность термов , , называется процессом редукции терма к терму , если

1. ,

2. ,

3. для всех существуют -редекс , соответствующий ему -контракт и контекст , такие, что и .

Определение 1. Терм находится в нормальной форме, если он не содержит -редексов. Иными словами, терм находится в нормальной форме, если не существуют такие и контекст , что .

Очевидно, что соответствующий предикат , проверяющий, находится терм – аргумент в нормальной форме или нет, рекурсивен (разрешим). В следующем разделе можно найти его описание.

Определение 2. Терм имеет нормальную форму, если существует такой терм в нормальной форме, что .

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

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

Теорема 1 (о стандартной редукции).

Если терм имеет нормальную форму, то она достигается в результате стандартной редукции.

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

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