Применения логических исчислений к изучению естественных преобразований в категориях тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Соловьев, Сергей Владимирович
- Специальность ВАК РФ01.01.06
- Количество страниц 157
Оглавление диссертации кандидат физико-математических наук Соловьев, Сергей Владимирович
ВВЕДЕНИЕ
I. Одаой из важных тем общей теории категорий является изучение естественных преобразований б категориях, снабженных дополнительнойктурой, состоящей из выделенных объектов, выделенных функторов (чаще всего в этой роли фигурировали функторы типа тензорного произведения, внутреннего 1гопг -функтора, прямой суммы или прямого произведения) и выделенных естественных преобразований (типа естественного изоморфизма коммутативности тензорного произведения, естественного изоморфизма сопряженности тензорного произведения и внутреннего К^-функтора, или естественных проекций прямого произведения), при условии, что все эти данные подчиняются определенным соотношениям (скажем, ОС - \ , где С обозначает естественный изоморфизм коммутативности тензорного произведения)
В диссертации к проблемам этой тематики применяется ряд методов и конструкций, "подсказанных" математической логикой (теорией доказательств, теорией формальных систем) и на этой основе решен ряд конкретных задач, касающихся естественных преобразований суперпозиций выделенных функторов в категориях с дополнительной структурой.
История воцроса восходит к началу 60-х годов (см. [I] ). Естественные преобразования в категориях с дополнительной структурой активно изучались с того времени С.Маклейном, С. Эйленбергом, И.Ламбе-ком и рядом других математиков (см., например, [2] , [3] , [5] , [8] , [18] , [29] , [30] ).
Рассматривались в основном задачи, связанные с естественными преобразованиями, которые могут быть представлены некоторыми термами, построенными из символов выделенных естественных, преобразований при помощи символов выделенных функторов и символа композиции (тавив естественные преобразования мы будем называть, в духе работ С.Маклейна [2] , [25] каноническими естественными преобразованиями; их точное определение для рассматриваемых в этой работе типов категорий дается ниже, в
§ 2), в частности задачи о корегентнооти канонических естественных цреобразований (верно ли, что все диаграммы в том иди ином классе диаграмм канонических естественных цреобразований комздутативны).
Полученные результаты находили применение в различных областях математики: ври построении бесконечнократннх пространств петель в алгебраической топологии (см. [2] , [4] , [5] ); при построении "длинных точных последовательностей" в гомологической алгебре [6]; при определении операций Стинрода в абелевых категориях [7] и т.д. Н.П.Титов нашел неожиданные применения результатов о когерентности к вопросам описания работы систем ЭВМ [8 ] •
2. В ряде случаев для решения задач упомянутых типов с успехом применялась теория исчислений. Связующим звеном между теорией категорий и теорией исчислений служит тот факт, что с классом категорий, имеющих заданную дополнительную структуру, может быть связано (вообще говоря, многими способами) некоторое исчисление секвенциального типа, которое оказывается свободной категорией того же класса при следующем "распределении ролей": формулы играют роль объектов; роль морсоизмов из А в В отводится класоам эквивалентных друг другу выводов секвенции А-В (или их кодов) при некотором отношении эквивалентности =■ , оцределяемом на основании соотношений, выполнение которых требуется в рассматриваемом классе категорий (в частности, класс эквивалентности аксиомы А^А играет роль единичного морфизма); роль композиции играет правило сечэния ——^—^ ; роль функторов играют пропозициональные связки (на объектах) и правила введения соответствующей связки на морфизмах); роль естественных преобразований играют схемы аксиом или иногда (например, для изоморфизмов сопряженности) правила вывода.
Впервые, по-видимому, начал применять исчисления для изучения канонических естественных преобразований И.Ламбек (см. [9] - [И]), обнаруживший не только связь мевду исчислениями и категориями, имевшую описанный выше характер, но и то, что исчислениям, рассматриваемым в связи со шогими интересными классами категорий, можно придать формулировку, допускающую применение хорошо известных методов теории доказательств, например, устранение сечения. Ряд дальнейшие результатов можно найти в статьях [з] , [12] - [16] и в книге [17] • В [17] описываются исчисления, отвечающие большинству представленных в литературе вариантов дополнительной структуры в категориях. (В основном эти исчисления оказались близки к различным фрагментам интуиционистского исчисления высказываний).
3. Однако предоставляемые теорией исчислений возможности использовались не в полном объеме. Привлекаемая в этих работах техника теории исчислений сводилась в основном к различным вариантам теорем об устранимости сечения (в исчислениях генценовокого) типа и о нормализуемости выводов (в исчислениях натурального типа, чему соответствовала возможность обойтись без композиций (за исключением некоторых специальных случаев) в термах, представлящих канонические естественные преобразования.
В данной диссертации рассматривается и решается ряд новых задач теории категорий (и некоторые ранее известные); при этом используются некоторые методы теории исчислений, которые раньше в этой связи не применялись. Среди новых задач теории категорий рассматривается* например, задача описания всех (а не только канонических) естественных преобразований всевозможных суперпозиций виделенных функторов над данной категорией. В тех случаях, когда удается решить ее (скажем, для категории конечнопорозденных проективных модулей над кашутативным кольцом 1 с I и суперпозиций &х и кот; ) теория исчислений помогает свести общий случай к сравнительно несложным алгебраическим теоремам. Из ранее не применявшихся в такш направлении методов теории исчислений отметим преобразования выводов, включающие (в отличие от процедуры устранения сечения) преобразование конечной секвенции (особую роль будут играть операции, обладающие некоторыми свойствами обратимости); анализ "зацеплений" вхождений переменных в секвенцию; метод оценок (придания истинных значений пропозициональным переменным).
Рассматриваются три класса категорий о дополнительной структурой. Это, прежде всего, класс так называемых симметрических моно-дцальных замкнутых (далее - СМЗ-) категорий, и два подкласса класса СМЗ-категорий (дополнительная структура категорий, принадлежащих этим подклаосам, получается в результате обогащения структуры ШЗ-категорий в двух различных направлениях: класс компактных замкнутых (далее - КЗ-) категорий, и класс декартово замкнутых (далее - ДЗ-) категорий. Охарактеризуем коротко эти классы (определения даются в
§ I).
В СМЗ-категориях выделенными функторами являются коммутативное и ассоциативное с точностью до естественных изоморфизмов "тензорное произведение" и сопряженный к нему справа внутренний кот -функтор. Мы будем обозначать эти функторы через Лиз соответственно (существует значительное сходство мезвду свойствами этих функторов и свойствами конъюнкции и импликации в логике; ср. [II] , [13]
Г?] ). Имеется выделенный объект, обозначаемый обычно через Т , который является (с точностью до естественного изоморфизма) "тензорной единицей". Выделенными являются также некоторые естественные изоморфизмы, обеспечивающие выполнение перечисленных условий на I, Л и о . Эти естественные изоморфизмы должны удовлетворять определенным соотношениям.
В КЗ-категориях треюуется, кроме того, чтобы для любых объектов X , Y объекты , а также и были естественно изоморфны (к выделенным в СМЗ-категориях естественным изоморфизмам добавляются соответствующие естественные изоморфизмы, на которые накладываются некоторые дополнительные соотношения).
В ДЗ-категориях вместо этого требуется, чтобы функтор Л был произведением в обычном категорнсм смысле олова, а объект 1 - правым нулем (терминальным объектом). К структуре ШЗ-категории добавляются соответствующие данные, на которые накладываются определенные соотношения (выражащие терминальность 1 и т.п.).
Типичным примеров ШЗ-категории может служить категория модулей над коммутативным кольцом 1 о I, с функторами и 1готг в качестве А и "з соответственно [30} (эта категория будет обозначаться далее через МОД-I); примером КЗ-категории - подкатегория конечнопоровденных проективных модулей категории МОД-I со структурой СМЗ-категории, индуцированной структурой MOft-I, и двумя дополнительными (стандартными для таких модулей) естественными изоморфизмами указанного выше вида [29] (эта категория будет обозначаться через ШОД-1). Функторы X и (vom. вместе со стандартная! естественными цреобразованиями определяют структуру ДЗ-категории на категории множеств и отображений (эта категория будет обозначаться через Se-i* ). ДЗ-категориями являются также топосы. В
§ 15 будет указан еще ряд примеров СМЗ-, КЗ- и ДЗ-категорий.
Исчисление, на котором вводится структура ДЗ-категории, цредс-тавляет собой (л, э; -фрагмент интуиционистского исчисления высказываний с константой "истина". Для СМЗ-категорий подобную роль играет исчисление, получаемое из этого фрагмента некоторым ослаблением структурных правил. Исчисление для КЗ-категорий не является логический в том смысле, что в нем выводимы не только тавтологии; оно, по-видимому, ранее не рассматривалось. Исчисление для КЗ-категорий содержит исчисление для СМЗ-категорий.
4. Опишем коротко структуру диссертации и распределение содержания по
главам.
Диссертация состоит из Введения и 4-х глав. Гл.1 носит вводный, в основном обзорный характер. В гл.2 рассматриваются некоторые операции над каноническими морфизмами и над естественными преобразованиями, связанные с операциями над выводами в соответствующих исчислениях. В гл.З рассматриваются связи между свойствами "зацеплений" вхождений переменных в секвенцию и ее выводимостью. В гл.4 при помощи теорем глав 2 и 3 изучаются свойства цроизвольных естественных преобразований суперпозиций функторов А и о в СМЗ-и КЗ-категориях
§§ 11-13) и канонических морфизмов в ДЗ-категори-ях
§ 14).
§ 15 гл.4 содержит примеры применений теорем, полученных в
§§ 11-14«
Отметим, каков характер связи этой работы с конструктивным направлением в математике.
Аппаратное ядро" работы, как по языку, так и по способам понимания и доказательства утверждений лежит в рамках конструктивного направления в математике. Здесь имеется в виду все, что касается языка исчислений, описаний выводов и методов оперирования с ними. Однако в результатах, относящихся к характеризации естественных цреобразований, речь обычно идет об объектах, определяемых и рассматриваемых в теоре тико-множе ственной математике, и упомянутая конструктивная часть работы применяется в таких ситуациях в соответствии с традициями классической математики, В то же время "аппаратное ядро" представляет собой самостоятельную часть работы о некоторыми строго конструктивными применениями.
В главах 2-
§§ 7, 8 главы 2,-
глава 3 и
§ 14 главы 4 полностью лежат в рамках конструктивного направления в математике. В
§§ 5,6 главы 2 конструктивными являются все те утверждения, в формулировках которых не упоминаются интерпретации в категориях естественных преобразований (над какой-либо категорией).
§§11-13 главы 4 по используемым понятиям и методам доказательств утверждений относятся к теоретико-множественной математике
§ 15 носит обзорный характер)
5. Перечислим основные результаты работы и некоторые их следствия. Получено описание всех естественных преобразований (в этом принципиальное отличие от [29] , где рассматриваются только канонические естественные преобразования) произвольных суперпозиций функторов Лиз над произвольной КЗ-категорией К » при условии, что объект X является образуицим в К . А именно, кавдое естественное преобразование может быть получено из некоторых канонических естественных цреобразований и некоторого эндоморфизма объекта 1 при помощи функтора Л и композиции (теорема 12.1; эта теорема имеет место, в частности, в категории ЕМОД-1).
Из полученного описания следует критерий коммутативности произвольной диаграммы естественных цреобразований суперпозиций функторов Л и "Э над К : диаграмма коммутативна, если и только если она коммутативна, когда все аргументы суперпозиций, входящих в диаграмму, равны Г (теорема 12.2). Из него следует также коммутативность всех диаграмм канонических естественных преобразований над К (теорема 12.3).
О помощью этого описания получается также (при выполнении некоторых, сравнительно "широких", дополнительных условий) необходимое и достаточное условие продолжаемости ненулевого естественного преобразования над КЗ-категорией К до естественного преобразования над объемлющей ШЗ-категорией , "структурно согласованной" с категорией К . Это условие состоит в существовании канонического естественного преобразования (тех же функторов) над Ь , или, что эквивалентно, в выводимости некоторой секвенции (теорема 13,3). (Отметим, что в работе широко иопользуетоя понятие обобщенного естественного преобразования [24] (ср. [25] , р.214), и что теоремы, перечисленные выше, в действительности формулируются и доказываются для обобщенных естественных преобразований).
Помимо перечисленных, к основным результатам диссертации относится теорема когерентности для канонических морфизмов в ДЗ-катего-риях (теорема 14.1). (Под каноническими морфизмами здесь понимаются морфизмн в свободной ДЗ-категории; их определение дается в
§ 2). Эта теорема была одновременно и независимо доказана автором и А. Бабаевым существенно различными методами (см. введение к [20] ).
Некоторые теоремы, доказанные в работе, являются "внутренними" теоремами теории логических исчислений, например, теорема 8.2, в которой говорится, по существу, о сохранении эквивалентности выводов в исчислении высказываний при понижении "глубины" секвенции; теорема 10.1, в которой устанавливается связь выводимости секвенции со структурой ее графа зацеплений; теорема когерентности для канонических морфизмов в ДЗ-категориях, которая может рассматриваться как теорема о существовании не более чем одного нормального вывода секвенции, содержащей не более двух вхоэдений каждой переменной в (л -фрагменте интуиционистского исчисления высказываний (ср. [13] ). в. Несколько слов о нумерации и обозначениях. В диссертации используется сквозная нумерация параграфов. Номер теоремы, леммы и т.п. состоит из номера параграфа и порядкового номера ее в этом параграфе, причем теоремы, леммы и т.п. нумеруются независимо. Параграфы разбиты на пункты, и при ссылке на тот или иной пункт указывается сначала номер параграфа, а затем номер пункта в этом параграфе.
Символ с] будет обозначать конец доказательства. Символ будет использоваться как сокращение для "тогда и только тогда, когда .". Символ "¡7 будет использоваться для переноса формальных выражений со строки на строку. Символ = будет обозначать графическое равенство синтаксических выражений. Остальные обозначения вводятся по ходу дела.
- II
Глава I. ОБЗОР НЕОБХОДИМЫХ ОБЩЕНИЙ ИЗ ТЕОРИИ КАТЕГОРИЙ и теории исчис.
Терминология теории категорий, иопользуемая в диссертации, в основном согласована с [25] t [26] ; терминология теории исчислений - о [27] , [28]
Коснемся одного формального момента, связанного с определением категории. Мы, следуя С.Маклейну [25], будем считать, что всякая категория гЧ включает, помимо класса объектов 0UK) и класса морфизмов Mnt {<) 9 также функции oiom. и cocí , ставящие в соответствие каждому морфизму F его область определения и область значений;" функцию 1 , ставящую в соответствие каждому объекту У единичный морфизм , и частичную функцию • , задащую композицию морфизмов. В тех случаях, когда требуется явно указать область определения и область значений, морфизмами будут называться также тройки вида , где RMfficKí^tWtF^-ccoUF) ср. [26] ).
§ I. Некоторые типы категорий о дополнительной структурой
I. Симметрической моновдальной замкнутей категорией (СМЗ-кате-горией) называется всякий упорядоченный набор вида А; Э, р} , У , Jí jJt'1) где 14 - категория,
ГвОкК) ,л:К*К-К
- бифгнкторн, OUK)xOUK)xOb(K)-* Могс Ю, ^: 0U K)->Mtn( К), ж'3цесь обозначает категорию множеств и отображений.
-l rrr естественные изоморфизмы ( сГ , jf - обратные к <1 , ß
Ju естественные изоморфизмы; из дальнейшего будет следовать, что у - обратный к самому себе) с компонентами вида: т:(ХлУ)л2 — Хл(Ул1)
Ь'.ХАГ -X и-ХлУ-УлХ -TüxV2. : когл (ХлУД ) ivowi (X, Y=> Ъ ) здесь X .У Л eOtik) ) 'и коммутативны оледущие диаграммы
XAVmZMH CXaV)A(IAU) ■Ь-ХлШЫЛ) да 4iu (.ХдСУл2))дЦ-*-*ХлШ)лЫ)
СХлУм! ^XA(VAI) ХлУХулу v д* да Ч л дл .п. луЗдесь и далее аргументы естественных преобразований, включенных в дополнительны!} структуру К » а также некоторых естественных -преобразований,явным образом определяемых через эти естественные преобразования, пшцутся в виде нижних индексов. В некоторых случаях (когда недостающие индексы легко восстанавливаются, исходя из требования осмысленности рассматриваемых выражений) все или часть индексов не будут указываться явно (например, ос ( "(ХАу ) следует -читать как ХХУ£ХаУ)( ; , поскольку с- (ХлУДлУ), см. также диаграммы Д1 - Д4).
УлХ)лг
Это - так называемые условия когерентности Келли-Маклейна ( [18] , ср. также [17] гл.З и 8).
2. Выпишем явно условия, которым подчиняются все данные, входящие в состав СМЗ-категории (они пригодятся вскоре при описании отношения эквивалентности для соответствующего исчисления) Выписываемые ниже условия не будут независимыми; мы стремимся выписать все варианты, которые могут в дальнейшем понадобиться.
А1. Для любого морфизма Р'Х^У, Р-^ • Р- Р
А2. Для любых морфизмов р : ~Ъ Ц , & : У^ Ъ, Н: Х-» У
Р-&)'Н = Г(Сг-И)
Эти два условия выражают свойство единицы и ассоциативность композиции в К • в связи с ассоциативностью мы часто будем записывать кратные композиции без скобок. Следующие четыре условия выражают функторность I? и л
АЗ. Для любых морфизмов Р^: Х^ХЬ £:Х^Х
А4. = -|хэу
А5. Для любых морфизмов Р,: Х^Х,, Д.'У^ Сг
А6. ^л/
Для любых ХуУуЯ 6- ОЬ(К)
А7. о^хуг ' ^ У'УН ~ ^лдсулг) ' ' = ^(хлу)лг > аз ^-р* = хац
Для любых морфизмов F: ХаУ ¿ Q : X
А9. зихуг(Л"х'уг (Q)) = Q , UXY3f С F;) = р.
Следующие тождества выражают коммутативность Д1 - Д4.
АЮ. ^XYtZüUí'^rXAVÍZtí = ^ ' ¿VIVA*} U.'( d*Y¿ Л ^ )
AH. (\ж л ) • ¿луг = px-v ;
AI2. • У// - ^хлу (это условие можно записать как /•у=/1 , т.е. ^ = у1 , здесь • обозначает композицию естественных преобразований, a i - тождественное естественное преобразование функтора л );
AI3. о£угх
Следующие условия выражают естественность oi) еС\ ^ Для любых морфизмов F: X ~*Х ; &: У У/ Н ' Л ~~> '
AI4. (Fa(GaH))'¿xy2 = e¿xV/?,-Л Рл&^дН J ; Ais. F- рх - ¡v • Г Fa iT); б Fa ^ ) *р"х = • F¡
AI6. (FaG)Yxv ^У*
GaF).
Следующие условия выражают естественность jü и Jü~' (в них НX Л Y Z , СЛ X^Y'^ - произвольные морфизмы, F, G, Н - те же, что и выше).
AI7. 3lXYÍ, ( Н • И • ( FA & )) = (& = Н )• (Jl„Vz Í Н')> Г. Используя функтор K^ovuu , это соотношение можно записать как AI7'. )«лих/у/г *
Ais. H-cx-^Í&VíFAG-).
Аналогично, с использованием Uovuu AI8 переписывается как
AI8'. • клил, ( F, & => Н ) ^Uuí FAG-,H)'XXV¿
Символ ^=7 здесь и ниже читается "введем в качестве обозначения".
Пусть ^ отброшенные нижние индексыцри 01 и Л4 легко восстановить). Отображения <í:X,Yi-*íiy hê^Y^êxy суть единица и коеди-ница сопряжения Jû (в терминологии [25] ). Следующие тождества следуют из А9 и AI7, AI8.
AI9. ( i 3 ¿хг )'<W)X = i
А20. ЁусУлЮ'^^^у ) И XAV •
Следующие два условия выражают естественность <Г по первому и £ по второму аргументу (в обычном смысле). Они следуют из AI7, AI8. Для любых морфизмов RX-X , G:Y-r :
A2I. Ну ^FaÍOKv = ¿>y-F ; A22. fixV'ff^GMxH G'fxy • Естественности <Г по второму и £ по первому аргументам (в обычном смысле слова) не будет, однако имеет место естественность в обобщенном смысле из [24] , а именно, выполняются ( F ,G- те же, что и в A2I,: А22) : А23. Ну -3 (ix aG))-¿xy "(fi^W)'^ i A24. Sx/y • ( 1X/3Y aF) = fCF
Понятие обобщенного естественного преобразования описывается подробнее в
§ 4.
Отметим, что Л и Л4 выражаются через £ и <Г , а именно, для любых
JûyzC F)-Hx^F).cTxv v = ev¡l-(GлЬ)
В дальнейшем, там, где это не ведет к недоразумениям, мы обычно будем обозначать категорию с дополнительной структурой (т.е.набор) так же, как собственно категорию, входящую в состав этого набора.
3. Компактной замкнутой категорией (КЗ-категорией) будет называться всякий упорядоченный набор вида где К - ШЗ-категория, £ : естественные изоморфизмы о компонентами вида
Потребуем, чтобы при этом также выполнялись следующие условия. Пусть ©xv Тогда справедливы:
А25. 6xy 'i>xy ~ ^хэу 9 £xv "бху = '
А26, = ? = ^х •
В том, чтобы выписывать условия, выражающие естественность £ и ^ нет необходимости. Из AI-A24 следует естественность отобра
• Теперь А25 и А26 влекут то, что $ и ^ - естественные изоморфизмы.
Компактные замкнутые категории рассматриваются в [29] . Там приводится несколько отличное по форме определение. Наши условия кажутся более слабыми (тривиально доказывается, что всякая КЗ-категория в смысле [29] является КЗ-категорией в нашем смысле), но в действительности эквивалентны условиям из [29]
4. Наконец, декартовой замкнутой категорией (ДЗ-категорией) называется всякий упорядоченный набор вида
К;0,< >) гдеК- ШЗ-категория, < >: 0U ЮЛЮ *(%(!<)-* Möt( Sek ) естественный изоморфизм и
- естественное преобразование с компонентами соответственно вида
Чтобы записать условия, которым должны подчиняться эти данные, введем обозначения!: ^ху ми О,) 'Ум •
А27. 0Х = р для любого р: X I (те^минальность I ; это условие влечет также естественность 0 ).
Для любых морфиамов Г: X ~*У, С.'Х-* 2 , Н:Уд Ъ т. е^Ш-Р ; А29. <е.н,а.н> = н в этих условиях отброшены очевидные нижние индексы). Как показывают А28 и А29, д (на объектах) и < > (на морфизмах) определяют произведение в категории К , причем отображения У1-» йху и а служат его естественными проекциями (естественность следует из определения I и ч, ). Этих условий уже достаточно, чтобы рассматриваемая структура была структурой ДЗ-катего-рии ( [30] , р.551): из них следует естественность ( > и то, что это изоморфизм, а также согласованность со структурой СМЗ-катего-рии. Под согласованностью здесь понимается выполнение тождеств:
АЗО. «с ^Ч^МУ^гУ^^А^^^хт У
А31. Длялюбых -1М) здесь и в следующих условиях отброшенные нижние индексы легко восстанавливаются) . 0гшетим еще следующие условия, являющиеся следствием условий на Л , от-' , г , <Г и А27-А29. Для любых морфиз
НОВ Р.-ХдУ-г :
А32. £У2 Р)-еху А*у> - Г ;
АЗЗ. =
5. Некоторые общие замечания» а) Каждая КЗ- или ДЗ-категория содержит в качестве поднабора некоторую СМЗ-категорию. Допуская некоторую вольность речи, мы будем говорить, что каэдая КЗ- или ДЗ-категория является одновременно СМЗ-категорией (можно считать, что применяется обычный "забывающий" функтор). б) Пусть символ 2 обозначает любое из выражений: СМЗ,КЗ,ДЗ. Существенную роль в дальнейшем играет понятие Гектора.
Пусть К и К' - некоторые £ -категории. Функтор Т^К-^К' назы-ваетоя ¿функтор™, ео® дай любы, XX, Ъ < ОКЮ ШЫ,
Т(ХлУ)=ТО0л'Т(У) ,Т(Х=У)-ТГХ)='Т(У) (и аналогично для морфизмов), п Коотмтт ж аналогично для р ^ а также для £ и ^ (если ¿Е есть КЗ) либо для 0 (если И есть ДЗ), далее, если для любого морфизма
СП (К;
Т(ЗГХУг( Г)) = ^тсхтуота/^^ • аналогично для (и для ^ > в том случае, когда £ есть ДЗ). Штрихами здеоь помечены данные к'. • в) Пусть
К жК-Екатегории. К называется ¿'-подкатегорией \С , если (без учета дополнительной структуры) К , и функтор включения является Z-функтором. г) Любая СМЗ-категория К содержит СМЗ-подкатегорию , структура которой допускает расширение до структуры КЗ-категории. (В качестве К0 можно взять подкатегорию, содержащую в точности те объекты К » для которых бХу и из п. 1.3 являются изо-иор&гашш [29] ). д) Важную роль будут играть 2, -категории, в которых выделенный объект является образупцим, т.е. для любых морфизмов
Т-'Х+У и &: X У имеем, если для всех морфизмов И : I имеет место РН = С'Н » то |--£г
§ 2. Естественные исчисления для некоторых типов категорий с дополнительной структурой
Естественность исчислений донимается здесь в том смысле, что их структура "буквально" копирует структуру соответствуадих категорий«
Естественные исчисления дня СМЗ-, КЗ- и ДЗ-категорий будут обозначаться через ЕИСМЗ> , , соответственно. СимволЕ будет обозначать любое из выражений СМЗ, КЗ, ДЗ.
I. Формулы еие строятся обычным образом при помощи двуместных связок А и з и скобок из переменных . и константы
I . (точнее, переменные и Г суть формулы, если А и В суть формулы, то (А А В) и (А^В) - формулы; внешние скобки на практике обычно не пишутся). Символы , Ь , с , Л , е (с ивдекса-ми или без) будут использоваться для обозначаения произвольных переменных; А ,В .С .й . Е (с индексами или без) для обозначения произвольных формул.
Выводимые объекты Ж Е будут называться £-каноническими морфизмами или, коротко, 2-морфизмами. Допуская некоторую избыточность (см. замечание 2.2 ниже), мы определим ¿чуюрфизш как тройки вида £: А -> В где А и В - некоторые фориуяы и где £ - некоторый терм, построенный цри помощи А , з , • (символа композиции) и скобок из символа 1 и символов естественный преобразований, входящих в структуру Е-категории, снабженных некоторыми формулами в качестве нижних, индексов. Типом морфизма А В будет называться секвенция А В . Символы £, ^ (с индексами или без) будут использоваться далее для обозначения термов, входящих в состав
2 -морфизмы определяются индуктивно при помощи следующих схем аксиом и правил вывода.
Рассмотрим следующие три группы схем аксиом.
1) 1.11Д:А-*А ; 1.
1.3 <Ф Ал(ВЛС) -^(ЛлВмС; 1.4 ■■ ЛлГ ->• А ; 1.5 р;':А-»Аа1 ; 1.6 №■ АлВ^ВлА ;
2) 2.
§ав:(А2.2 ^д:(А=>М-А;
3) 0Д:А—I
Схемами аксиом Ейсмз являются схемы группы (I), схемами Ей« схемы групп (I) и (2), а схемами ЕИДЗ - схемы групп (I) и (3). Следующие пять правил являются правилами всех трех исчислений: А -> В а:В . /:АлВ->С
15 -*а ' 2) ^ф.-А-в-С '
• ,, /•• А^В 9: С-В
5) д:С-»В
Правило I) называется также правилом композиции или сечения. В Ейдз имеется также следующее правило:
2. ЗАМЕЧАНИЕ 2.1. Непосредственно из определения видно, что исчисления ЕИ къ иЕИдз являются расширениями исчисления Шсиъ т.е. все СМЗ-морфизмы являются также КЗ- и ДЗ-морфизмами.
ЗАМЕЧАНИЕ 2.2. Включая тип в задание 2 -морфизма, мы следуем [ 17] (объекты, соответствующие 2 -морфизмам, называются там Ь^МиЬ ъиушлтЛь ). В таком задании имеется определенная избыточность (оправдываемая выигрышем в наглядности). Если морфизм, то по / однозначно восстанавливаются (при помощи рекурсии) вывод этого /] -морфизма (таким образом, £ является кодом вывода) и его тип - секвенция . Это очевидно для аксиом, а далее легко доказывается индукцией по процессу порождения морфизма
§• АВ . Поскольку тип восстанавливается по ^ также будет называться орфизмом , а развернутая запись -¿•А-В будет применяться только там, где есть необходимость, Кроне того, иногда будет говориться, что I есть ^-иорфгаи типа
Будем говорить, что секвенция А В выводима в , если существует /-, аморфизм т типа
ЗАМЕЧАНИЕ 2.3. Если истолковывать 2.«. э • • • как пропозициональные пероиенные, Г - как константу "истина", А и "э -как конъюнкцию и импликацию, то выводимость секвенции вида в ЕИдз равносильна ее выводимости в интуиционистском исчислении высказываний; исчислению ЕИСЮ отвечает в этом смысле некоторое более слабое исчисление (см.
§ 3). Что касается Ейкз , то оно вообще не является логическим в том смысле, что не'все выводимые в нем секвенции являются тавтологиями (например, не является тавтологиями А ^В 9 Л (А =1 ) и (А^Г)3! -»А • ). Это, однако, не мещает теоретико-категорным приложениям ЕИ , так как для теории категорий основной интерес представляют КЗ-морфизмы.
Во многих случаях нет необходимости указывать явно все нижние индексы в 2~морфизмах, поскольку недостающие индексы легко /восстанавливаются, исходя из требования, чтобы все рассматриваемые выражения были И-морфизмами.
Введем по аналогии с обозначениями в случае 2-категорий, обозначения (это может также рассматриваться как иллюстрация к вышесказанному): ^ Рл<'1*&04) аб ^ (V НалОв) в Здесь были отброшены очевидные нижние индексы при ЛГ и Л"1 «
3; Определим отношение эквивалентности = на 2 -морфизмах (если
§ = ^ для некоторых И-морфизмов | и } , то мы будем говорить также, что £ и ^ ¿^-эквивалентны).
Отношение = будет, грубо говоря, наименьшей конгруэнцией, цревращаадей в Х-категорию. Точнее, = определяется индуктивно при помощи описываемых ниже аксиом и правил.
Пусть А э 1-Аэ 33 получаются из А1-АЗЗ (см.
§ I) заменой = на =| , символов X , У , 2 , Ц на А , В , С , Й , символов $ & »Н -на £ , £ , ^ , при этом "морфизмы" следует всюду заменить на " Е -морфизмы". Аксиомы для . А э 0 . f 1 £
А э X - А э 24 . Этими аксиомами исчерпываются аксиомы для =н
Аксиомами Ц являются также А э 25 и Аэ 26.
Аксиомами = - также А э 27 - А э 33 (вместо А э 25 ж Аэ 26).
Правила для
0.1 * * 3 а 1 ^ 0.
З1 ^ к.
Эти правила (вместе с А э 0) обеспечивают, что = - отношение эквивалентности. Следуицие правила I) - 6) выражают "устойчивость" = относительно правил вывода с соответствующими номерами.
Предполагается, что X-морфизмы в рассматриваемых правилах таковы, что выражения, стоящие слева и справа от = в заключениях этих правил, являются 2 ^орфизмаш. Не указываемые явно нижние индексы X , Х-1 и > определяются типами соответствующих Гчлорф^ов.
П /.1 8< • 2Ч :
ТГГТ^ТТТГ з) jLZ.ii—— ; 4) £19»
5) ^ Л 1$«.
Этими правилами исчерпываются правила для ^ и
§ . Для =? добавляется правило
6) /тЕ^
Заметим, что если } ^ у , то типа / и совпадают. Это непосредственно проверяется для авсиом, и далее доказывается стандартной индукцией по обоснованию щ
Пусть [/обозначает класс эквивалентности / по | Предыдущее свойство позволяет писать такая запись будет применяться при необходимости явно указать тип).
4. После того как определено отношение = , на множестве формул и ^-морфизмов вводится структура X -категории. (В дальнейшем выражение ЕИе будет обозначать не только исчисление, но и эту -категорию). А именно* - это множество формул; если г\ и о - формулы, то Ьож
А, В)
- это множество классов эквивалентности Е/Зг: А"^ В ; единица для объекта А - это ^а^-'А^А ; функции с1ош. и сос1 определяются тривиальным образом; 1 - выделенный объект; композиция на £ -морфизмах задается правилом сечения (правилом (I) Ейс ); функторы => и Д на объектах ( Е -морфизмах) определяются условиями: А^В
А (А, В) ^ А л В , . Корректность^ переноса этих операций на классы' эквивалентности обуславливается непосредственно определением ("устойчивостью" относительно применения соответствующих правил).
Естественные преобразования (кроме ЛГ^ОГ"1/ ) задаются схемами аксиом, точнее, например, ¿:А,В,С сЗ^- и т.д. Естественные преобразования СГГ , ОТ"1 , ( > задаются на мах соответствующими правилами ЕИ г . Как и в случае функторов, определение = обуславливает корректность переноса этого определения с представителей ( Л. -морфизмов) на классы эквивалентности. Процесс построения исчисления со структурой 2-категории, описанный в пл. 1-4, может рассматриваться как частный случай общей схемы, которая впервые, по-видимому, была проведена И.Ламбеком ( [10] , {II] ), а в настоящее время стала стандартной (так, она систематически применяется в книге [17] , ср. также [3] , [13] , а для КЗ-категорий - [29] ). Категория Ей^ является свободной ¿ -категорией, порожденной дискретной категорией (а.1,. ,. ^ ( [И] .'[17] ¿'[29] ).
5. Интерпретацией будет называться всякий ¿-функтор -> К » гДе ^ ~ I-категория. Так как ЕИЕ имеет структуру свободной 2 -категории, то интерпретация 3 : ЕИг -> К полностью определяется своими значениями на переменных а,,. а.^,. , и обратно, всякое отображение (гц,.,^,. ] -»ОКЮ может быть единственным образом продолжено до интерпретации (это очевидно и непосредственно).
Отметим, что отображение ¿ьЬс1к определяет интерпретации ЕЙсмз в Шкз и ЕИДЗ,
6. Важную роль будет играть операция подстановки формул вместо переменных. Пусть А^ >., А^ - произвольные формулы, ап., а^ - произвольные попарно различные переменные. Выражение ^д^" будет называться подстановкой (формул А .,>., А^ вместо переменных ). Пусть Л - некоторое синтаксическое выражение. Тогда выражение СЛ!^ ' ^ ) будет обозначать результат одновременной подстановки А1 вместо всех вхождений в вместо всех вхождений в Л (внешние скобки часто будут опускаться) . Иногда удобно допускать случай /г = 0 (в этом случае никакая подстановка в действительности не делается).
Выражение вида будет обозначать список ^ всли , и пустой список, если и.- О (это обозначение будет использоваться и тогда, когда ^ 13. - ^ Л^ не являются синтаксическими объектами).
Перечислим некоторые свойства подстановок. I Л|-гЯ I
Если уд -подстановки, переменные
ЬГА, попарно различны, то 1 д^' - подстановка.
Пусть Л >Л>1 * . ? А*, - некоторые синтаксические выражения, и Я ^ Л1Лг . Л^ . Тогда для любой подстановки К • где А[ Вчаотности, если ец , не входят в Д) , то Л} (
Пусть а 1,., а и , Ц ,.Ьуч. - попарно различные переменные, А„.,АЛ~ произво.пьные формулы (очевидно, в этом случае ,и ^ь,'!^ - подстановки). Пусть Л - произвольное синтаксическое выражение, Ь^. , не входят в Л . Тогда
Пусть Л - некоторое синтаксическое выражение, и подстановки, причем переменные отличны от переменных и не входят в формулы А^- уДь* пусть В'ь н~п')
Легко видеть, что выводы в ЕИГ переходят при подстановке в выводы ЕИе . Любая подстановка ¿д,/^ определяет интерпретацию ЕИ^ -> ЕИг , если положить ПСя^-) =. Д^ (1 & £ $ и,) и И С а.) = сь для остальных переменных (формулы и 2] -морфизмы переходят при этой интерпретации в результат подстановки в них формул А*.,. » А и, вместо переменных л,,). В частности, имеет место
ЛЕММА 2.1. (а) Если £ - ^-морфизм типа А , то
-морфизм типа ; (б) дня любых ¿.-морфизмов
Будем называть переименованием переменных в синтаксическом выражении Л применение к нему всякой подстановки вида , где Ь 1 , •••, У г* ~ попарно различные переменные, отличные от всех переменных, входящих в Л (кроме, может быть, ).
СЛЕДСТВИЕ 2.1 % Если -морфизмы и д' получаются из 2 -морфизмов / и ^ в результате некоторого переименования переменных, то ^ ^ <'"==^>/
§
7. -морфизм ^ : Д —> В будет называться 2 -изоморфизмом, если существует 2 -морфизм ^ : В ~А в ЕИ^. такой, что ¿р-д. = 4в и • Если существует 2 -изоморфизмто формулы А и В будут называться ¿'-изоморфными. Выражение будет обозначать, что форму-А Е -изоморфна о . Распространим отношение на секвенции вида (т.е. на типы ¿-морфизмов), положив А —^ В ^ А В тогда и только тогда, когда А и В ^ В . Очевидно, что - отношение эквивалентности, содержится в ^ и
Если К - Е-категория, то ¿-каноническими морфизмами (или просто I -морфизмами) в К будут называться образы 2-морфизмов при всевозможных интерпретациях 3 : ЕИГ -> К -морфизмы называются равными (в экстенсиональном смысле), если равны вое их интерпретации в любой Л -категории • Оказывается, что отношение экстенсионального равенства I] -морфизмов совпадает с отношением ^ . Имеет место следующая лемма (ор. [3] , лемма 2.1): ЛЕММА 2.2. Пусть £ , - цроизвольные Е -морфизмы. Тогда / <=т> для любой Е «категории К и любой интерпретации Т-Шг К имеет место равенство ) в К
ДОКАЗАТЕЛЬСТВО. Достаточно заметить, что ^ т ^ влечет для любой интерпретации л , и в то же время само отношение ^ определяет равенство морфизмов в
Лемма 2.2 показывает, что коммутативность некоторой диаграммы X -морфизмов равносильна коммутативности всех диаграмм, получающихся из нее при всевозможных интерпретациях.
3. Назовем вхождение подформулы в формулу А положительным (отрицательным) , если для четного (нечетного) числа вхождений в А различных подформул вида В ^ С оно происходит от некоторого вхождения в В . (Положительные вховдения называют иногда ковариантны-ми, а отрицательные - контравариантными - ср. [18] ). Если число таких подформул равно нулю, то вхоздение называется существенно положительным. Заметим, что если формула А1 входит в формулу А г а формула А^ входит в формулу А3 • то знак вхождения А1 в А3 , происходящего от рассматриваемого вховдения Ат в А2 через рассматриваемое вхождение Аг в , может быть определен по знакам этих последних с помощью "правила произведения".
Здесь и далее символ О будет обозначать конец доказательства.
Вхождению формулы в секвенцию вида А припишем тот же знак, что и соответствующему вхоадению в формулу А ^В • Вхоаде-ния одной и той же формулы в формулу или секвенцию, имеющие противоположные знаки, будут иногда называться соцряженными.
ПРИМЕР 2,1. В следущей секвенции указаны знаки вхождений переменных, подчеркнуты существенно положительные вхождения формул в секвенцию : (С ее ^ 15 с) л с
Будем использовать символ УЬ (о индексами или без) для обозначения вхоаденжй произвольных синтаксических выражений, а символы ю , 1Г ,1хг (о индексами или без) - для обозначения вховдений переменных исчислений Ей £ . Если - вхождение, то VI будет обозначать выражение, вхождением которого оно является (и аналогично для вхождений переменных).
Пусть 1Л/ - некоторое вхоадение формулы или секвенции Л в синтаксическое выражение <3 (не обязательно линейное - например, в древовидный вывод). Для любого вхождения какой-либо формулы в 3 цроисходящего от вхоадения в Л через ^Ь , определяется его знак относительно VI , как знак соответствующего вхоадения в Л
Пусть Л - произвольное синтаксическое выражение. Тогда ]/СЛ) будет обозначать множество вхождений переменных исчисления ЕИ^ в Л . Если Л - формула или секвенция (т.е. оцределены знаки вхождений), то
ГШ У(Ю ж УТЛ) будут обозначать соответственно множества положительных, отрицательных и существенно положительных вхождений переменных в Л . Если при этом УЬ - вхоадение Л в некоторое объемлющее выражение, то V (ВД, У (VI) и V (VI) будут обозначать соответственно множества положительных, отрицательных и существенно положительных относительно /Щ<> вхождений в объемлющее выражение. В том случае, когда Л - линейное выражение, и упомянутые множества задаются посредством списков (например,
-^иг} или \/(Л)= [и^ъ } ) будет предполагаться, что порядок вхождений в списках совпадает с их порядком в А
Назовем секвенцию А В квазиуравновешенной, если каждая переменная входит в нее не более двух раз, уравновешенной, если каждая переменная, которая входит в нее, входит ровно двазды, и притом о противоположными знаками» I- уравновешенной , если она уравновешена и в любой ее подформуле С ° В , где 0 - постоянная (не содержащая вхождений переменных) формула, \у также постоянна.
Сформулируем (в терминологии, введенной выше) некоторые известные результаты о когерентности. а) Случай СМЗ-категорий.
ТЕОРЕМА 2.1. Если и А-*В - СМЗ-морфнзмы, и секвенция А В 1-уравновешенна, то ^^^
Эта теорема впервые доказана в [18] (теорема 2.4) и обычно называется теоремой когерентности Келли-Маклейна.
Центральными изоморфизмами называются СМЗ-изоморфизмы, которые строятся из \ , об , р , у , сГ' , при помощи композиции и
А . Пусть С, Т) - формулы, построенные из переменных а*, -, 4ц. и константы X при помощи А и скобок, в каждую из которых (кь) входит ровно один раз. С помощью теоремы 2.1 легко доказывается следующая теорема (впервые она была доказана раньше теоремы 2.1).
ТЕОРЕМА 2.2. Существует единственный с точностью до г центральный изоморфизм . (С&1. [I] , теорема 5.1, [18] теорема 3.4).
Если секвенция А В не является 1-уравновешенной, то
9 ' ' о могут существовать неэквивалентные СМЗ-морфизмы типа |5 , однако их конечное число (см. [17] , 8.6.7 и 8.6.14). б) Случай ДЗ-категорий.
З^цесь наличие схемы аксиом 0Л: А^Х и правила вывода заметно усложняет ситуацию. Для некоторых секвенций А -> I? существует бесконечно много попарно неэквивалентных ДЗ-морфизмов типа например, для секвенции Са^а-Ма—> - см. [17]
9.6.7).
Г.Е.Минцем в [13]| был доказан аналог теоремы 2.2 для ДЗ-морфизмов, построенных из \} л,.0 цри помощи только А > и композиции (без помощи , ОТ и Л"1 ).
Автором (й независимо, А.Вабаевым) доказана теорема когерентности, утвервдаицая, что любые два ДЗ-морфизма £ , ^ типа АВ , где А^В - квазиуравновешенная секвенция, ДЗ-эквива-лентны» (В [20] мы называли такие секвенции уравновешенными). Ее доказательство, принадлежащее автору, приводится ниже (см. теорему 14 Л). с) В случае КЗ-категорий наш интерес будет в основном сосредоточен на описании произвольных естественных преобразований. Относительно когерентности для КЗ-канонических морфизмов см. [ 29]
§ 3. Вспомогательные исчисления генценовского типа
Исчисления, рассмотренные в предыдущем параграфе, не лишены, с точки зрения теории исчислений, некоторых существенных недостатков (не устранимо сечение, выводы громоздки). йце Ламбек [ю] ввел вспомогательные исчисления генценовского типа и воспользовался устранимостью сечения в этих исчислениях для получения теорем о канонических морфизиах. В этом параграфе будут рассмотрены исчисления играющие роль, аналогичную исчислениям, рассмотренных Ламбеком, по отношению к!СН1 и ЕИЛз . Что касается Ей^ , то в построении вспомогательного генценовского исчисления в этой случае не будет необходимости, поскольку наличие аксиом £дв 'А^ВВлГА^ ) и , не являющихся тавтологиями, позволит ограничиться рассмотрением очень простых секвенций и обойтись без устранения сечения при получении интересующих нас теорем.
Генценовскив исчисления, связанные с ЕИсиз> (с Ейдъ ) будут обозначаться через ГИСМЗ (соответственно, через ). СимволЕ на протяжении этого параграфа будет обозначать СМЗ или ДЗ.
I. Формулы в ГИ^ те же, что и в ЕИ^ • Выводимыми объектами Тй^ будут секвенции вида Г-^ А , где А - формула, Г -список формул; для обозначения списков формул будут использоваться греческие буквы Г , Д , П . . • (с индексами или без). В секвенции Г-^А список Г называется антецедентом, А - сукцеден-том; вхождения формул в качестве членов списка Г - антецедентными членами. Говоря о ГИСМЗ и Гйдз , мы часто будем называть А конъюнкцией, аз- импликацией. Буквой р (с индексами или без) будут обозначаться выводы в ГЙ^- . Запись будет обозначать, вывод р I секвенции Г А
Перечислим аксиомы и правила вывода исчисления
Аксиомы.
I) А-*А ; (2) —X
Правила вывода:
Г-А ; . В,г-Сл
Г,Л-А*В А лВ,Г-СА£ Щ^Г1'' Г-А В,А-С " г.
Г-А-В А=В,Г,Д-С ' сокращение); сечение). или будут, как обычно, называться логическими, а остальные правила - структурными. Рядом о формулировками правил помещены их обозначения (для структурных правил - также их названия), которые будут играть вспомогательную роль.
Описанное только что исчисление несущественно отличается от (Л, ^) -фрашента интуиционистского исчисления высказываний с константой "истина".
Исчисление ГИСМЪ отличается от ГИдз, по трем пунктам: в нем нет цравила 1-* ; правила А е-* заменяются на правило
А ; правило Ь заменяется на правило ^ -> (так называемую ограниченную форму утончения [3] ). Здесь А -> и 9 - следующие адг—с . д-1 г->е~ правила: / ' -к-*- ; —--'-- ч ->
Фрагменты исчислений Гй ^ , в которых не применяется сечение, будут обозначаться через ГИ~
2. Напомним некоторые термины из теории логического вывода ( [27] [32] ). Под "вхождением" мы сейчас будем понимать явно указанное в формулировках правил вхождение. Пусть ^ - применение одного из правил, рассмотренных выше. Если ^ - применение сечения, то вхождения А в посылки называются формулами сечения. Если ^ -применение П , то вхождения А и В в посылку и в заключение называются формулами перестановки. Для остальных правил, вхождения те(гтэтнвние); хг^г^
ШЩп* (перестановка); Г-А А.А-С
Г,ВАМ Г,А-С
Правила, применениями которых вводятся вхождения А
Д , В в посылку (посылки) называются боковыми формулами, вхождение , где о обозначает А или (если оно имеется), либо вхождение А в заключение называется главной формулой. Вховдения формул в Г\ Д называются параметрическими.
3. Отметим, что правила л и У являются производными правилами ГЙДз . Они моделируются следующими последовательностями переходов:
А,В,ГЧЛ , г-с
1Щ Л.Г-1-(ое,внив)
АаВЛВГЧ АлВ,Г-*С
В ряде случаев удобно рассматривать всякий Гисмз -вывод одновременно как ГИдз -вывод; в этом случае мы будем предполагать, что каждое применение л ^ или У представлено соответствущей фигурой. В ГИ Дз удобно пользоваться также следующим; производным правилом:
Оно моделируется фигурой, состоящей из утончения и применения для которого главная формула У служит боковой формулой. Присоединим это правило к основным правилам ГЙД5 .В случае необходимости мы будем считать, что оно служит просто удобным сокращением для соответствующей фигуры вывода. В будет считаться единственной боковой формулой -»• . Определения из п.^ распространяются на автоматически.
4. По каядому ), -морфизму /: А В может быть построен вывод р секвенции Д-*В в ГИ^ . Для этого в выводе (единственном) Е-морфизма АВ каждая аксиома заменяется
ГИ„ -выводом, каждое применение правила вывода - некоторой фигу-£ рой вывода в Гй£ . Например, акоиома д в о А в-В А-^А |Д удв:пАР"^иАп заменяется на вывод ^ д £>дД „ ААВ-ВАА применение цравипа вида -11112— заменаетоя на фштру
А1-В д
-,----* Л
А,А-*ВАС С ^
А-ВдС
В дальнейшем используется в основном факт существования такого перевода, поэтому ограничимся этими примерами. (Подробности см. в [17] ).
Пусть Г - произвольный список формул. Если Г-А^и." » то а(Г) будет обозначать формулу (.(А.,л.)л А^ . Если же Г пуст, то Л (Г) будет обозначать X . (Аналогичные обозначения будут применяться для ¿-морфизмов .Если
Опишем перевод , при котором ГИ^. -выводы переходят в морфизмы, цричем Гй Е «выводы секвенции Г А переходят в X -морфизмы типа
Л(Г)-*]\ и для любого Е-мррфизма А( П А найдется вывод р секвенции Г —» Д , т.ч. -О^с^) iе £ ( Заметим, что любая формула может быть представлена в виде А С Г; для некоторого списка Р ). Наличие делает ГИ£ эффективным средством для изучения 2 -морфизмов. В описании мы в основном следуем [17] , используя некоторые уточнения из '¡13] , [15] . Для любой секвенции положим На выводах исчисления ГИЕ перевод ^с^- будет определен рекурсией по цроцессу построения ГИ^ -вывода.
При определении существенную роль сыграют центральные изоморфизмы (см. п*2.10). Пусть Г^ > Г^ - некоторые списки форяул, Г| Гь. - некоторые их перестановки. Если Г*, состоят из попарно различных переменных, то по теореме 2.2 существует единственный о точностью до центральный изоморфизм типа • Если П Пе. состоят из произвольных формул, то существует единственный о точностью до = центральный изоморфизм, получающийся из центрального изоморфизма описанного выше вида в результате очевидной подстановки формул вместо переменных. Зафиксируем для любых списков ;П, Г*. и их перестановок Г^ ,. , Г^ некоторый такой центральный изоморфизм типа
Л(Л(К),.,Л(ГГ* ) и обратный к нему. В приводимых ниже определивших равенствах для через обозначаются эти фиксированные центральные изоморфизмы (их типы легко определяются по типам остальных X -морфизмов).
В п.п. (1)-(7) й обозначает , где Е ^ СМЗ, ДЗ. Скобки в записи композиции не указываются (можно считать, что они группируются влево).
1) ^(А-А)ИД:А-А; м • £ • Фср, > А \т )■//.• Г, А ) С. ; es) Г^А В,А* С А=В,Г,А-»С
QWc-^-d П'-МА^Г.АМ; в) - Од Ч&р)* НмШ-- AÍ Гн С ;
7, Öf СМД^ ), Q f : ЛСГ, В, А# А) - С í
1Г,В,А,Д-С/
- рг)'(Рлсг/)Глп)1 )-íQo»íPiíaVj)•£:л(А,Гьс ; ю) ÖAS)^„ф^лО^с л(ИГ)-С ; Ш) ^Д' (щ^ bO^tf. л V,)* Xf АлВ, Г ЬС з
13, Яз =
Отметим, что если перевод отличается от только выбором изоморфизмов то для любого ГИ^ -вывода р (р) =
Ср) .В этом смысле перевод определен однозначно(с точностью до = ) . Отметим, что мевду ^сиь и ^аз есть согласованность, в том смысле что, можно показать, для любого ГИСМЪ -вывода р и ГИЛЗ -вывода р/ , получающегося, если заменить в р каждое применение У и на соответствующую фигуру вывода в ГИДЗ см. п.3.3) , ^дз ( Ш Яе (■ Р
ЗАМЕЧАНИЕ 3.1. Чтобы упростить описание конкретных выводов в исчислении ГИХ , расширим его всевозможными производными правилами^ каждое из которых можно получить при' помощи фигуры, состоящей из одного применения некоторого правила ГИ ^ (за исключением правила перестановки), которому предшествуют и за которым следуют некоторые применения правила перестановки. Зафиксируем для каждого из этих производных правил некоторую "представлявшую" его фигуру. Распространим перевод на выводы в расширенном исчислении. Если р - произвольный вывод в расширенном исчислении, то заменим все применения производных пра вил указанного вида на представляющие их фигуры и затем применим . Как показывают п. (7) определения перевода и теорема 2.2, при другом выборе фигур, представляющих рассматриваемые производные правила (они могут отличаться лишь применениями перестановок), результатом применения будет Е-морфизм, отличающийся от полученного первоначально только заменой некоторых центральных изоморфизмов на эквивалентные, и, следовательно, эквивалентный ему. В этом смысле распространение на выводы в расширенном исчислении определено однозначно с точностью до = независимо от вида фигур, "цредставляпцих" эти правила. В тех случаях, когда не будет поводов для недоразумений, эти производные правила будут обозначаться так же, как используемые в представляющих их фигурах правила, отличные от П-> . Такие правила часто будут использоваться при построении конкретных выводов (ср. примеры 3.2 и 3.3 ниже).
6. Используя перевод можно перенести на секвенции исчислений ГИ^ понятие знака вхождения. Будем считать, что знак вхождения в секвенцию вида Г —* А совпадает со знаком соответствующего вхождения в секвенцию вида л(Г) А » в (А ) . Автоматически переносятся и все связанные с этим понятия (см. п. 2.9).
Перевод иццуцирует на выводах исчисления ГИ^ отношение эквивалентности, которое мы, как и в случае исчисления Ей^ будем обозначать через = (и говорить, если р 1 р; , что выводы р ир' £ -эквивалентны).
Имеется следующая важная теорема:
ТЕОРЕМА 3.1. Для каждого ¿-морфизма Л( ГД найдется вывод р секвенции Г А в исчислении ГИ^ , такой, что
17] » теоремы 8.5.2 и 9.5.1).
Во многих случаях будет достаточно такой более слабой теоремы:
ТЕОРЕМА 3.2. Секвенция Л(Г)~* А выводима в исчислении ЕИ^ тогда и только тогда, когда секвенция Г А выводима в исчислении ГИ г . (По теореме 3.1 выводимость секвенции Г А в ГИ ^ следует из существования ¿-морфизма Л(Г) ^ А (т.е. ее выводимости в Ей^ ). Обратное следует из того, что по определению перевода ^^ , для любого вывода Р А в исчислении ГИ Я (р)- А(Г) А 2 - морфизм).
7. Прежде чем рассмотреть устранение сечения в ГИ^ , приведем некоторые цримеры.
ПРИМЕР 3.1. (ГиЕ —вывод и соответствущий ему Е-морфизм.)
Рассмотрим следующий ГИг -вывод р :
Имеем цри некотором выборе центральных изоморфизмов Гр) ^
Следующие примеры иллюстрируют использование Ги? -выводов для задания Ц -адзмов.
ПРИМЕР 3.2. Сомрьк. Ч йсмз Ср) , где р - следующий вывод
I) |> с а си к Ь^С ->£
CL , Сй.э Ь),(Ьэс ) ->с
-—--, о- =>Ь j bz>c. -> а. =>с
-д —>
Пусть а.,Ь,а -различные переменные. Тогда по теореме когерентности Келли-Маклейна (теорема 2.1) СМЗ-морфизм 7" (аос ) единствен (с точноотью до == ). в дальнейшем через будет обозначаться СМЗ-морфизм (Сож|)аЬс) •
Привлекая теорему когерентности, цри помощи ГИ ^ -выводов можно определять также обладающие различными свойствами обратимости (например, Хдодваш).
ПРИМЕР 3.3, Пусть р^ , pz - следующие выводы в ГИСн2(л$ Ь, с - различные сс-ъ-а. \> Ь а / Ь а. л Ь
--— "
--л —> ^(Ь^с) (алЬ)^с
Рассмотрим ШЗ-морсоизмы По теореме 2.
Поскольку подстановка определяет интерпретацию ЕИсмг в Ейсцз , имеем (для любых формул АД С ) ((Qí,2Ср^с
Шг ((^смэ «3 С^о ь и аналогично для другой композиции. Следовательно, -О^Р^а'в.с и Й:мз ^ являются взаимно-обратными СМЗ-изоморфизмами. В дальнейшем они будут обозначаться соответственно через /4д с/\аВ; = с
8. В Шсмз и ГИдт, в оледупцем смысле устранимо сечение: ТЕОРБМА. 3.3. Для любого вывода \> в ГИСЮ (в ГИДЗ ) найдется вывод р' в этом исчислении, с той же конечной секвенцией, не содержащий применений оечения и такой, что ¡> (что р'ц /> ). Для Гиснз это теорема 8.6.1, а для - теорема 9.6.
17] . Теорема 3.3 для ГИСМЗ вытекает также из теоремы об устранимости сечения более ранней работы [23] (ср. [3] ), а для Шдъ из теоремы 6.7 работы [13] и теоремы 6.5 [34] . (В [13] рассматривается исчисление натурального типа, а в [34] - перевод генценовс-ких выводов в натуральные). Теорема 3.3 показывает, что если выводы в ГИ ^ изучаются с точностью до = , то можно ограничиться рассмотрением исчисления ГИ~ . Выводы в ГИ^ обладают тем свойством, что всякая формула, появляющаяся в выводе, входит в конечную секвенцию (кроме, может быть, формулы I в ГИ~г ).
ЗАМЕЧАНИЕ 3.2. В силу теорем 3.1 и 3.3 всякое утверждение о когерентности (об эквивалентности между собой всех) ^орфизмов т.ч. а( Г ) —г* А равносильно утверждению об эквивалентности ' всех выводов секвенции А в ГИ~ ;
Рекомендованный список диссертаций по специальности «Математическая логика, алгебра и теория чисел», 01.01.06 шифр ВАК
Классифицирующие пространства алгебраических групп и их инварианты2015 год, кандидат наук НЕШИТОВ Александр Юрьевич
Стереотипные алгебры и двойственность для групп Штейна2009 год, доктор физико-математических наук Акбаров, Сергей Саидмузафарович
Обобщенное функциональное исчисление в векторных решетках2013 год, кандидат наук Тасоев, Батрадз Ботазович
Производные категории эквивариантных когерентных пучков и когерентных пучков на стеках2009 год, кандидат физико-математических наук Елагин, Алексей Дмитриевич
Явные конструкции в теории формальных групп и конечных групповых схем и их приложения к арифметической геометрии2006 год, доктор физико-математических наук Бондарко, Михаил Владимирович
Введение диссертации (часть автореферата) на тему «Применения логических исчислений к изучению естественных преобразований в категориях»
I. Одаой из важных тем общей теории категорий является изучение естественных преобразований б категориях, снабженных дополнительной структурой, состоящей из выделенных объектов, выделенных функторов (чаще всего в этой роли фигурировали функторы типа тензорного произведения, внутреннего 1гопг -функтора, прямой суммы или прямого произведения) и выделенных естественных преобразований (типа естественного изоморфизма коммутативности тензорного произведения, естественного изоморфизма сопряженности тензорного произведения и внутреннего К^-функтора, или естественных проекций прямого произведения), при условии, что все эти данные подчиняются определенным соотношениям (скажем, ОС - \ где С обозначает естественный изоморфизм коммутативности тензорного произведения).
В диссертации к проблемам этой тематики применяется ряд методов и конструкций, "подсказанных" математической логикой (теорией доказательств, теорией формальных систем) и на этой основе решен ряд конкретных задач, касающихся естественных преобразований суперпозиций выделенных функторов в категориях с дополнительной структурой.
История воцроса восходит к началу 60-х годов (см. [I] ). Естественные преобразования в категориях с дополнительной структурой активно изучались с того времени С.Маклейном, С. Эйленбергом, И.Ламбе-ком и рядом других математиков (см., например, [2] [3] [5] [8] [18] [29] [30] ). 4Рассматривались в основном задачи, связанные с естественными преобразованиями, которые могут быть представлены некоторыми термами, построенными из символов выделенных естественных, преобразований при помощи символов выделенных функторов и символа композиции (тавив естественные преобразования мы будем называть, в духе работ С.Маклейна [2] [25] каноническими естественными преобразованиями; их точное определение для рассматриваемых в этой работе типов категорий дается ниже, в § 2), в частности задачи о корегентнооти канонических естественных цреобразований (верно ли, что все диаграммы в том иди ином классе диаграмм канонических естественных цреобразований комздутативны).
Полученные результаты находили применение в различных областях математики: ври построении бесконечнократннх пространств петель в алгебраической топологии (см. [2] [4] [5] ); при построении "длинных точных последовательностей" в гомологической алгебре [6]; при определении операций Стинрода в абелевых категориях [7] и т.д. Н.П.Титов нашел неожиданные применения результатов о когерентности к вопросам описания работы систем ЭВМ [8 ] •2. В ряде случаев для решения задач упомянутых типов с успехом применялась теория исчислений. Связующим звеном между теорией категорий и теорией исчислений служит тот факт, что с классом категорий, имеющих заданную дополнительную структуру, может быть связано (вообще говоря, многими способами) некоторое исчисление секвенциального типа, которое оказывается свободной категорией того же класса при следующем "распределении ролей": формулы играют роль объектов; роль морсоизмов из А в В отводится класоам эквивалентных друг другу выводов секвенции А-В (или их кодов) при некотором отношении эквивалентности =■ оцределяемом на основании соотношений, выполнение которых требуется в рассматриваемом классе категорий (в частности, класс эквивалентности аксиомы А^А играет роль единичного морфизма); роль композиции играет правило сечэния ——^—^ ; роль функторов играют пропозициональныеА Сусвязки (на объектах) и правила введения соответствующей связки(на морфизмах); роль естественных преобразований играют схемы аксиом или иногда (например, для изоморфизмов сопряженности) правила вывода.
Впервые, по-видимому, начал применять исчисления для изучения канонических естественных преобразований И.Ламбек (см. [9] - [И]), обнаруживший не только связь мевду исчислениями и категориями, имевшую описанный выше характер, но и то, что исчислениям, рассматриваемым в связи со шогими интересными классами категорий, можно придать формулировку, допускающую применение хорошо известных методов теории доказательств, например, устранение сечения. Ряд дальнейшие результатов можно найти в статьях [з] [12] - [16] и в книге [17] • В [17] описываются исчисления, отвечающие большинству представленных в литературе вариантов дополнительной структуры в категориях. (В основном эти исчисления оказались близки к различным фрагментам интуиционистского исчисления высказываний).
3. Однако предоставляемые теорией исчислений возможности использовались не в полном объеме. Привлекаемая в этих работах техника теории исчислений сводилась в основном к различным вариантам теорем об устранимости сечения (в исчислениях генценовокого) типа и о нормализуемости выводов (в исчислениях натурального типа, чему соответствовала возможность обойтись без композиций (за исключением некоторых специальных случаев) в термах, представлящих канонические естественные преобразования.
В данной диссертации рассматривается и решается ряд новых задач теории категорий (и некоторые ранее известные); при этом используются некоторые методы теории исчислений, которые раньше в этой связи не применялись. Среди новых задач теории категорий рассматривается* например, задача описания всех (а не только канонических) естественных преобразований всевозможных суперпозиций виделенных функторов над данной категорией. В тех случаях, когда удается решить ее (скажем, для категории конечнопорозденных проективных модулей над кашутативным кольцом 1 с I и суперпозиций &х и кот; ) теория исчислений помогает свести общий случай к сравнительно несложным алгебраическим теоремам. Из ранее не применявшихся в такш направлении методов теории исчислений отметим преобразования выводов, включающие (в отличие от процедуры устранения сечения) преобразование конечной секвенции (особую роль будут играть операции, обладающие некоторыми свойствами обратимости); анализ "зацеплений" вхождений переменных в секвенцию; метод оценок (придания истинных значений пропозициональным переменным).
Рассматриваются три класса категорий о дополнительной структурой. Это, прежде всего, класс так называемых симметрических моно-дцальных замкнутых (далее - СМЗ-) категорий, и два подкласса класса СМЗ-категорий (дополнительная структура категорий, принадлежащих этим подклаосам, получается в результате обогащения структуры ШЗ-категорий в двух различных направлениях: класс компактных замкнутых (далее - КЗ-) категорий, и класс декартово замкнутых (далее - ДЗ-) категорий. Охарактеризуем коротко эти классы (определения даются в § I).
В СМЗ-категориях выделенными функторами являются коммутативное и ассоциативное с точностью до естественных изоморфизмов "тензорное произведение" и сопряженный к нему справа внутренний кот -функтор. Мы будем обозначать эти функторы через Лиз соответственно (существует значительное сходство мезвду свойствами этих функторов и свойствами конъюнкции и импликации в логике; ср. [II] [13] [Г?] ). Имеется выделенный объект, обозначаемый обычно через Т который является (с точностью до естественного изоморфизма) "тензорной единицей". Выделенными являются также некоторые естественныеизоморфизмы, обеспечивающие выполнение перечисленных условий на I, Л и о. Эти естественные изоморфизмы должны удовлетворять определенным соотношениям.
В КЗ-категориях треюуется, кроме того, чтобы для любых объектов X Y объекты а также и были естественно изоморфны (к выделенным в СМЗ-категориях естественным изоморфизмам добавляются соответствующие естественные изоморфизмы, на которые накладываются некоторые дополнительные соотношения).
В ДЗ-категориях вместо этого требуется, чтобы функтор Л был произведением в обычном категорнсм смысле олова, а объект 1 - правым нулем (терминальным объектом). К структуре ШЗ-категории добавляются соответствующие данные, на которые накладываются определенные соотношения (выражащие терминальность 1 и т.п.).
Типичным примеров ШЗ-категории может служить категория модулей над коммутативным кольцом 1 о I, с функторами и 1готг в качестве А и "з соответственно [30} (эта категория будет обозначаться далее через МОД-I); примером КЗ-категории - подкатегория конечнопоровденных проективных модулей категории МОД-I со структурой СМЗ-категории, индуцированной структурой MOft-I, и двумя дополнительными (стандартными для таких модулей) естественными изоморфизмами указанного выше вида [29] (эта категория будет обозначаться через ШОД-1). Функторы X и (vom. вместе со стандартная! естественными цреобразованиями определяют структуру ДЗ-категории на категории множеств и отображений (эта категория будет обозначаться через Se-i* ). ДЗ-категориями являются также топосы. В § 15 будет указан еще ряд примеров СМЗ-, КЗ- и ДЗ-категорий.
Исчисление, на котором вводится структура ДЗ-категории, цредс-тавляет собой (л, э; -фрагмент интуиционистского исчисления высказываний с константой "истина". Для СМЗ-категорий подобную роль играет исчисление, получаемое из этого фрагмента некоторым ослаблением структурных правил. Исчисление для КЗ-категорий не является логический в том смысле, что в нем выводимы не только тавтологии; оно, по-видимому, ранее не рассматривалось. Исчисление для КЗ-категорий содержит исчисление для СМЗ-категорий.
4. Опишем коротко структуру диссертации и распределение содержания по главам.
Диссертация состоит из Введения и 4-х глав. Гл.1 носит вводный, в основном обзорный характер. В гл.2 рассматриваются некоторые операции над каноническими морфизмами и над естественными преобразованиями, связанные с операциями над выводами в соответствующих исчислениях. В гл.З рассматриваются связи между свойствами "зацеплений" вхождений переменных в секвенцию и ее выводимостью. В гл.4 при помощи теорем глав 2 и 3 изучаются свойства цроизвольных естественных преобразований суперпозиций функторов А и о в СМЗ-и КЗ-категориях (§§ 11-13) и канонических морфизмов в ДЗ-категори-ях (§ 14). § 15 гл.4 содержит примеры применений теорем, полученных в §§ 11-14«
Похожие диссертационные работы по специальности «Математическая логика, алгебра и теория чисел», 01.01.06 шифр ВАК
Операдные и категорные методы в теории многообразий универсальных алгебр2011 год, доктор физико-математических наук Тронин, Сергей Николаевич
Производные категории когерентных пучков и эквивалентности между ними2002 год, доктор физико-математических наук Орлов, Дмитрий Олегович
Категории модулей: Некоторые аддитивные функторы и двойственность1998 год, кандидат физико-математических наук Звягина, Марина Берговна
Компактификации схем модулей стабильных векторных расслоений на поверхности локально свободными пучками2016 год, доктор наук Тимофеева Надежда Владимировна
Конечные подгруппы в группе Кремоны над полем вещественных и комплексных чисел2018 год, кандидат наук Ясинский Егор Андреевич
Список литературы диссертационного исследования кандидат физико-математических наук Соловьев, Сергей Владимирович, 1984 год
1. Mac Lane S. Natural associativity and commutativity. - Bice Univ.Studies, 1963, v.49, ТВ 4, p.28-46.
2. Mac bane S. Topology and logic as a source of algebra. Bull. Amer.Math.Soc., 1976, v.82, Ж 1, p.1-40.
3. Минц.Г.Е. Замкнутые категории и теория доказательств,- Зап. научн.семин.ЛОМИ, 1977, т.68, с.83-114.
4. Ддамс Д&. Бесконечнократные цространства петель. М.: "Мир", 1982, 198 с.
5. May J.P. Е^ -spaces, group completions, and permutative categories. "New developments in topology", bond.Math.Soc.Lect. Uotes, N 11, Cambr.Univ.Press, 1974, p.61-93.
6. Villamayor O.E., Zelinsky D. Brauer groups and cohomology for general commutative rings extensions. J.Pure and Appl.Algebra, 1977, v.11.
7. Epstein D.B.A. Punctors between tensored categories, Invent. Math., 1966, v.1, p.221-228.
8. Титов Н.П. Когерентность естественных изоморфизмов в категориях алгебр и модулей.- Авторефер.дисеерт. на соискание учен.ст. канд. физ.-матем.наук, М., 1981, 16 о.
9. Mann C. !Che connection between equivalence of proofs and cartesian closed categories. Proc.Lond.Math.Soc., 1975, v.31, N 3, p.289-310.
10. Минц Г.Е. Теория категорий и теория доказательств,- В кн.:Актуальные цроблемы логики и методологии науки. Киев, 1979, с.252-278.
11. Бабаев A.A. Равенство морфизмов и теорема когерентности для бизамкнутых категорий.- Зап.научн.семин.ЛОМИ, 1981, т.105, с.3-10.
12. Бабаев A.A. Равенство морфизмов в замкнутых категориях.- Изв. АН Азерб.ССР, сер. физ.-тех. и мат.наук, 1981, № I, с.3-10.
13. Бабаев A.A. Равенство морфизмов в замкнутых категориях.- Изв. АН Азерб.ССР, сер. физ.-тех. и мат.наук, 1981, № 2, с.3-9.
14. Szabo М.Е. Algebra of proofs. Studies in Log.and the Fondations of Math., North-Holland P.C., 1978, v.88, 297 p.
15. Kelly. G.M., Mac Lane S. Coherence in closed categories. « J.Pure and Appl.Algebra, 1971» v.1, p.97-140.
16. Соловьев C.B. Новые приложения теории доказательств к теории категорий.- 6 Всесогозн. конферен. по матем. логике. Тезисы, Тбилиси, 1982, с.173.
17. Бабаев A.A., Соловьев C.B. Теорема когерентности для канонических морфизмов в декартово замкнутых категориях.- Зап.научн. семин.ЛОМИ, 1979, т.88, с.3-29.
18. Соловьев C.B. Сохранение эквивалентности выводов цри редукции глубины формул.- Зап.научн.семин.ЛОМИ, 1979, т.88, с.197-208.
19. Соловьев C.B. 0 естественных преобразованиях в компактных замкнутых категориях.- 17 Всесоюзн. алгебр, конферен. Тезисы сообщений, 4.2. Минск, 1983, с.225.
20. Минц Г.Е. Теорема об устранимости сечения для релевантных логик.» Зап.научн.семин.ЛОМИ, 1972, т.32, с.90-98.
21. Eilenberg S., Kelly G.M. A generalisation of the Functorial Calculus, J.of Algebra, 1966, v.3, p.366-375.
22. Mac Lane S. Categories for the working mathematician*Berl.Springer, 1972, 262 p.
23. Фейс К. Алгебра: кольца, модули и категории. I. М.: "Мир", 1977, 688 с.
24. Клини С.К. Математическая логика. М.: "Мир", 1973, 480 с.
25. Карри Х.Б. Основания математической логики. М.: "Мир", 1969, 568 с.
26. Kelly G.M., Laplaza М. Coherence for compact closed categories. J.Pure and Appl.Alg., 1980, nv.19, p.193-213«
27. Eilenberg S., Kelly G.M. Closed cagegories. Proc.of the conf.on Categorical Algebra, La Jolla, 1965, p.421-562.
28. Szabo M.E. A counter-example to coheren e in cartesian closed categories, Canad.Mathem.Bull., 1975, v.18, p.111-114*
29. Kleene S.C. Permutability of inferences in Gentzen's calculi LKand LJ. Memoirs Amer.Math.Soc., 1952, N 10, p.1-26.
30. Соловьев С.В. Выводимость секвенции критерий существования естественного преобразования в категории модулей.- 16 Всесо-юзн. алгебр, конферен. Тезисы, ч.1, Л., 1981, с.150-151.
31. Pottinger G. Normalisation as a homomorphic image of cutelimination. Ann.of Math.bog., 1977, v.12, 323-357.
32. Шанин H.A., Давыдов Г.В., Маслов С.Ю., Минц Г.Е., Оревков В.П., Слисенко А.О. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний.- М.-Л.: "Наука", 1965, 39 с.
33. Голота Я.Я. Сети меток и выводимость в интуиционистском исчислении высказываний.- Зап.научн.семин.ЛОМИ, 1969, т.16,с.28-43.
34. Голота Я.Я. Некоторые приемы, упрощающие построение сетей меток.- Зап.научн.семин.ЛОМИ, 1969, т.16, с.44-53.
35. Голота Я.Я. Матричный способ записи сетей меток.- Зап.научн. семин.ЛОМИ, 1974, т.40, с.4-9.
36. Харари Ф. Теория графов. М.: "Мир", 1973, 300 с.
37. Оревков В.П. Три способа выявления несущественных формул в секвенциях.- Зап.научн.семин.ЛОМИ, т.88, с. 163-176.
Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.