Экспоненциальные дедуктивные категории

Мы определяем экспоненциальную дедуктивную категорию, наделяя дедуктивную категорию А введенными правилами вывода и дополнительными тождествами:

Таким образом, для данного графа X мы можем сконструировать импликативные исчисления D (X) и свободную экспоненциальную категорию Fr (X), порожденную X.

Пусть Grph будет категорией графов, чьими объектами являются графы и каждая стрелка F: X -> Y есть пара отображений F:Obiects (X) —> Objects (Y) и F:Arrows (X) —> Arrows (Y), такая, что Х-*Х' влечет F{J): F{X) -> F (A^rl).

Пусть Exp будет категория экспоненциальных дедуктивных категорий, чьими объектами являются экспоненциальные дедуктивные категории, а стрелками — функторы сохраняющие экс поненциальную структуру, т. е.

Пусть U будет обычным «стирающим» функтором Exp->Grph. С каждым графом X мы можем ассоциировать морфизм графов Их-' X -> UF (X) следующим образом: Нх (Х)= X и, если f.X—>Y есть стрелка в X, то Hx (f) =/(классы эквивалентности/рассматриваются как доказательства в D (X)). Мы имеем следующее универсальное свойство:

Предложение 1. Для любой экспоненциальной дедуктивной категории, А и любого морфизма F: X —> U (A) графов существует единственная стрелка F': F (X) —> А в Ехр, такая, что U (F')Hx= F.

Доказательство. Конструкция F' требует от нас выполнения следующих условий:

Требуется проверить, что F' определен правильно, т. е. что для всех fg.Ah В в F‘ (X) f=g влечет F" (f) = F' (g). Последнее очевидно, поскольку никаких других, кроме требуемых нам, тождеств В Р (Х) не выполняется. ?

Подобное универсальное свойство в математике обычно расценивают как наличие сопряженности, т .е. что F есть функтор Grph—>Exp, левосопряженный к Uc сопряжением Нх: Id —> UF (см. четвертую главу).

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

Для данных объектов Ао и А категории А можно добавить индетерминант (= неопределенную стрелку) х: A₀h А различными способами. Одним из способов, например, было бы присоединение стрелки х: А₀1- А к лежащему в основании А графу и затем формирование категории, свободно порожденной новым графом. Согласно другому способу можно вначале сформировать дедуктивную систему Л[х], основанную на «допущении» х. Формулы А[х] являются объектами А, а доказательства Д[х] формируются из стрелок А и новой стрелки х: A₀h А путем соответствующего использования правил вывода.

Чтобы убедиться в том, что Л[х] является категорией и что включение А в А[х] будет функтором, следует проверить выполнение специальных тождеств между доказательствами. Если тождество доказательств обозначить как =_х, то можно рассматривать =_Л как наименьшее отношение эквивалентности в между доказательствами, такое, что:

для всех <�р (х): В- С, i|/(x)/(x): ОD, %(х)х'(х): DYЕ.

Заметим, что в виду закона рефлексивности = и =_х расширяют тождество в А. Стрелки в категории А[х] являются доказательствами при допущении х по модулю =, их можно рассматривать как полиномы по х.

В случае экспоненциальных дедуктивных категорий отношение эквивалентности = между доказательствами должно также выполнять следующие условия:

Предложение 2 (подстановка доказательств). Для данной экспоненциальной дедуктивной категории А, индетерминанта х:

A o')-А над А и стрелки a: AqYА, существует единственный функтор S_x^a: A[x] —> А, такой, что S/(x) — a и S_x^aHx= 1*.

Доказательство. Вначале докажем, что:

Для данной категории А, и индетерминанта х: Aoh А над А, функтора F: А—>В и любой стрелки Ъ: F (Ao)h F (A) в В имеется единственный функтор FА[х] -> В, такой, что F (x)= bn F’Нх= F.

Каждое доказательство ф (х) при допущении х может иметь следующую форму:

где к есть стрелка в А, т. е. постоянный полином. Решающим шагом является определение Р (ф (х)). Определим индуктивно:

Остается лишь показать, что F ' определен на полиномах, а не на доказательствах, то есть, что ф (х) =_х <�р'(х) влечет F '(ф (х)) = F.

'(ф'(х)). Если в последнем случае писать <�р (х) = (р'(х), то достаточно проверить, что = имеет все свойства подстановки и отвечает всем тождествам экспоненциальной категории. Например, чтобы проверить, что ф (х) ¹ = ф (х), мы вычисляем F '(ф (х) ⁵) = (F'(ф (х).

У ~(F'(фМГУ ит. д.

Теперь, чтобы получить доказательство нашего предложения, достаточно положить F= 1ая.

IBCWйТ-экспоненциальную дедуктивную категорию мы получаем теперь путем добавления следующих тождеств:

Последнее уравнение утверждает, что Т является терминальным объектом Для /вСИ'Л-экспоненциальных дедуктивных категорий можно теперь доказать следующую теорему, улучшающую теорему дедукции:

Теорема 1 (функциональная полнота). Для любого полинома ф (х):5н С по индетерминанту х: Тн А над IBCWKэкспоненциальной дедуктивной категорией мы можем получить единственную стрелку f: TV А => (В гзС), такую, что ((f)^sx)^s =.

Доказательство. Положим, как в доказательстве теоремы дедукции,/ = к_хе,4ф (х). Проверяем индукцией по длине доказательства ф (х), что.

((k_xfMx)YxY =_х ф (х).

Действительно, учитывая все виды доказательств в IBCWK- экспоненциальной категории (беря их из доказательства теоремы дедукции для /5СИ^/ЙТ-импликативного исчисления), получаем:

(где к: В- С, доказательство IBCWK-

исчисления),.

Следующим шагом является проверка того, что к_хеА ф (х) зависит от полинома ф (х), то есть, от класса эквивалентности доказательства ф (х) по модулю =. Будем писать ф (х) = ф (х) вместо.

^елф (х) = к_х€Л|/(х). Легко проверить, что = обладает всеми подстановочными свойствами и выполняет все условия, которые должно выполнять тождество в А[х]. Поскольку = было определено как наименьшее такое отношение эквивалентности, отсюда следует, что = содеожится в =. т. е. что имеет место как и утверждалось.

Проверим, например, что если 1л =э/= h в А, то 1л zd/= h (полагая /• 51- С). Действительно:

Наконец, чтобы доказать единственность f. Tt-А => (5 гэС) допустим что ((f)^sx)^s = (р (т). Тогда можно утверждать, что/ = k_xt/l

Действительно:

Можно получить теорему функциональной полноты для /ДОТЛ'-экспоненциальных дедуктивных категорий и по аналогии с комбинаторной полнотой для множества комбинаторов {B, C, W, K},. Достаточно адаптировать для нашего случая соответствующую версию алгоритма, позволяющего решить для любого комбинаторного терма, стратифицирован он или нет (см. [Curry 1969], [Hindley 1969]). Однако этот алгоритм несколько сложен, чтобы его можно было описать здесь чисто формальным образом.

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