Комбинаторная логика как формальная система

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

Представлено формальное введение в типизированный вариант комбинаторной логики, первоначально предложенный X. Карри. Изложение формальной теории производится в традиционной для математики последовательности: алфавит, аксиомы и правила вывода. Обсуждается понятие базисного набора комбинаторов: будут рассмотрены несколько вариантов базисов, включая минимально возможный.

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

Задать синтаксис языка возможно, перечислив описание его конструкций, например, с помощью форм Бэкуса — Наура, или БНФ. БНФ созданы в 1960;х гг. Дж. Бэкусом (John Backus) и развиты П. Науром (Peter Naur) как метаязык для формализации синтаксиса языка программирования ALGOL 60. Впоследствии БНФ получили широкое распространение и в настоящее время являются основной нотацией для формализации синтаксиса языков программирования (мы будем пользоваться БНФ для формализации синтаксиса языка программирования F#). В данной нотации символ «:=» интерпретируется словами «может иметь вид», а символ «|» — словом «или». Определяемое и определяющие понятия записываются в угловых скобках, первое — слева, а последние — справа от значка «:=».

Формализуем синтаксис выражений комбинаторной логики (или комбинаторов). БНФ-описание комбинатора имеет вид.

:= К | S | ().

БНФ-описание терма комбинаторной логики, возможно, содержащего переменные, имеет вид.

:=.

К | S |.

|.

().

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

• (1)1 а=а;
• (К)К ab=a;
• (S)S abc=ac (bc);
• (B) В abc=a (bc);
• © С abc=acb;
• (W)W ху=хуу.

Соотношение (I), как уже отмечалось, характеризует комбинатор тождества.

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

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

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

Соотношения © и (W) определяют соответственно пермутацию (перестановку) и дублирование аргументов.

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

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

В ходе исследований было выяснено, что редукция (преобразование для сокращения записи) комбинаторных термов возможна в соответствии с правилами вывода, аналогичными аксиомам (К) и (S).

Проиллюстрируем моделирование механизма редукции следующим примером.

Рассмотрим комбинаторный терм вида S К Кх.

Пользуясь аксиомами (К) и (S), а также правилами вывода, произведем редукцию терма:

S К К х = (по правилу S).

К х (К х) = (по правилу К) х.

В результате получаем, что S К К х=х, откуда, с учетом аксиом и правила (I), I=SKK.

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

Необходимость продолжения рассуждений приводит нас к понятию базиса.

Множество (минимальной мощности) комбинаторов, через элементы которого выразим произвольный комбинатор, называется минимальным базисом.

Можно доказать, что:

• 1) базис термов для комбинаторной логики действительно существует (причем существует бесконечное множество возможных базисов);
• 2) для любого базиса справедливо, что он обеспечивает представление произвольного комбинаторного терма (в силу свойства полноты, которым обладает система комбинаторной логики);
• 3) минимальный базис состоит всего из двух «инструкций"-комбинаторов, например {K, S}.

Приведем еще несколько примеров базисов:

{I.K.S};

{I, B, C, S};

{B, W, K}.

Разложение термов в базисе {K, S} для ранее рассмотренных комбинаторов имеет вид.

B=S (KS)K;

W=SS (K (SKK));

C=S (BBS)(KK).

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

Оказывается, что комбинаторная логика обладает возможностью не только моделировать процесс реализации программного обеспечения на языке функционального программирования, но и прозрачно формализовать процедуру приписывания типов объектам этого языка.

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

В случае комбинаторной логики будем считать, что тип, а приписан комбинатору X тогда и только тогда, когда это утверждение получено из следующих аксиом:

• (FI) |- #(1)=(а, а),
• (FK) |- #(К)=(а, (b, a))=(a, b, a),
• (FS) |- #(S)=((a, (b, c)), ((а, Ь)(а, с)))

и правила вывода.

(F) если |- #(Х)=(а, Ь) и |- #(U)=a, то |- #(XU)=b.

Заметим, что процедура контроля соответствия типов транслятора языка программирования реализована сходным образом, причем в ней существенно используется механизм сопоставления с образцом. В языке программирования F#, кроме того, применяется механизм получения логического вывода о типе выражения исходя из контекста его использования. Этот механизм, известный также как выводимость типов (type inference), адекватно моделируется в терминах комбинаторной логики.

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

let I х=х;

let К х у=х;

let S х у z=x z (у z);

Реализация функций достаточно прозрачна и не требует пояснений. Заметим лишь, что функция I реализует комбинатор тождества I, функция К — комбинатор-канцелятор К, а функция S — комбинатор-коннектор S.

Заметим в заключение, что произвольный терм комбинаторной логики выразим через приведенные базисные комбинаторы.

Контрольные вопросы Вопрос 1.

Вариант 1: в чем состоит основное назначение комбинаторной логики?

• а) формализация функциональной программы (+);
• б) формализация программной среды Microsoft .NET;
• в) формализация выводимости типов.

Вариант 2: что является преимуществом комбинаторной логики перед классической логикой?

• а) возможность оптимизации программного кода (+);
• б) возможность формализации процесса программирования (+);
• в) наглядность.

Вариант 3: что из перечисленного является этапом развития комбинаторной логики?

• а) логика первого порядка;
• б) теория простых функций (+);
• в) теория вычислений.

Вопрос 2.

Вариант 1: для реализации какого из перечисленных языков программирования использовалась категориальная комбинаторная логика?

• а) CaML (+);
• б) SML;
• в) Mosml.

Вариант 2: что понимается под комбинатором?

• а) лямбда-терм без переменных;
• б) лямбда-терм без связанных переменных;
• в) лямбда-терм без свободных переменных (+).

Вариант У. каковы основные операции формальной системы комбинаторной логики?

• а) аппликация (+);
• б) абстракция;
• в) аппликация и абстракция.

Вопрос 3.

Вариант 1: каковы основные компоненты формальной теории комбинаторной логики?

• а) алфавит, аксиомы, теоремы;
• б) алфавит, аксиомы, правила вывода (+);
• в) алфавит, теоремы, правила вывода.

Вариант 2 что отличает аксиомы комбинаторной логики от прочих утверждений?

• а) лаконичность формулировок;
• б) фундаментальность;
• в) отсутствие необходимости доказательства истинности (+).

Вариант 3: каким образом осуществляется построение комбинаторов?

• а) посредством рекурсии;
• б) дедукции;
• в) индукции (+).