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

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

Таким образом, для данного графа 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(Arl).

Пусть 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 (см. четвертую главу).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Последнее уравнение утверждает, что Т является терминальным объектом

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

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

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

((kxfMx)YxY =х ф(х).

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

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

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

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

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

как и утверждалось.

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

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

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

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

Категория

Базис

Тождества

Стрелки

IBB'

IB

(JbB)(g^B)=fg=>B

f. Ah В, g: BhC

MLc

JBB'

1я=и“=1я

E-W

IBB'

/: Th A, g:AhB=>C

R-W

IBB'

{T'gl-gf

f TH A,

Z-AhB

Т

IBB'

Cfr =/

f.ThC

Е

Т

/ТЬ А, g: Ah В з С

R

Т

н

«!

II

/Т(- А, g:Ah В

ЕМО

Е

=/^

f. А => ВУ- С, g:A-B

RM0

R

(7 *g')g=fg

f. Ah В, g? Тн А

S3

Е

>УГ =/

/• Ah В, g: C-D

54

Е

fg=f

f:A- В, g: Tl-C

J

R

/=Ол

f: Ah T

55

Е

7/ц _, = g/ 7"

f:(A^B)z>Ch H A z> B, g: ChD

С

J

gf® = g / У

f.Az>BhA,

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >