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

Посмотреть архив целиком

12



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


Введение.

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


  1. - Термы.

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

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

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

Название конструкции

Конструкция объекта

Представление

Номер переменной

Представление числа в десятичной системе счисления

Терм - переменная

Терм - аппликация

Функциональный терм


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