Моделі та методи дослідження абстрактних обчислювальних структур в категорній аксіоматиці

Размещено на http://www.allbest.ru/

Київський національний університет

імені Тараса Шевченка

УДК 004.42:510.65:512.58

МОДЕЛІ ТА МЕТОДИ ДОСЛІДЖЕННЯ

АБСТРАКТНИХ ОБЧИСЛЮВАЛЬНИХ СТРУКТУР

В КАТЕГОРНІЙ АКСІОМАТИЦІ

01.05.01 - теоретичні основи інформатики та кібернетики

АВТОРЕФЕРАТ

дисертації на здобуття наукового ступеня

кандидата фізико-математичних наук

Ченцов Олексій Ілліч

Київ - 2007

Дисертацією є рукопис.

Робота виконана на кафедрі інформаційних систем факультету кібернетики Київського національного університету імені Тараса Шевченка

Науковий керівник:доктор фізико-математичних наук, професор Провотар Олександр Іванович, Київський національний університет імені Тараса Шевченка, завідувач кафедри інформаційних систем

Офіційні опоненти:доктор фізико-математичних наук, старший науковий співробітник, Глазунов Микола Михайлович, Національний авіаційний університет МОН України, м. Київ, професор, завідувач кафедри

кандидат фізико-математичних наук, старший науковий співробітник,Єршов Сергій Володимирович, Інститут кібернетики НАН України, старший науковий співробітник

Провідна установа:Дніпропетровський національний університет, кафедра обчислювальної математики та математичної кібернетики

Захист дисертації відбудеться “5” квітня 2007 року о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 в Київському національному університеті імені Тараса Шевченка (03127, м. Київ, пр. Глушкова, 2, корп. 6, ф-т кібернетики, ауд. 40. Тел. 521-33-66. Факс 259-70-44)

З дисертацією можна ознайомитися в Науковій бібліотеці Київського національного університету імені Тараса Шевченка (01033, м. Київ, вул. Володимирська, 58)

Автореферат розісланий “5” березня 2007 року.

Учений секретар спеціалізованої вченої ради Д.Я. Хусаінов

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Обчислювальні структури належать до засадничих інструментів формалізації в комп'ютерних науках. Проблеми, пов'язані з обчислювальними структурами, виникають в таких областях як, моделювання, інформаційний пошук, теорія графів, обробка символьної інформації, трансляція програм та інші. Класичні обчислювальні структури описуються в термінах інтуїтивної теорії множин і є досить добре вивченими. Із розвитком некласичних логік виникли питання про засоби дослідження структур, що використовувались в цих логіках. Одним з найбільш зручних формалізмів для дослідження таких логік є теорія категорій з інструментарієм для опису різноманітних математичних структур - локальних теорій. Тому опис та дослідження абстрактних обчислювальних структур в термінах теорії категорій є актуальним на сьогодні питанням. Фундамент в дослідженнях абстрактних структур заклали відомі вчені А.І. Мальцев, А.П. Єршов, В.М. Глушков, І. Ламбек, Д. Скот, Дж. Гоген.

Використання категорного підходу для опису обчислювальних структур зумовлене кількома обставинами. По-перше, це потреба у розробці спільних підходів до вивчення, на перший погляд, різних проблем інформатики та кібернетики. По-друге, одержані абстрактні моделі обчиcлювальних структур, у випадку конкретних категорій, можуть утворювати нові, досі невивчені обчислювальні об'єкти. Причому властивості загальної категорної моделі залишаються справедливими для кожної конкретної інтерпретації.

Слід зазначити, що в цьому напрямку одержано ряд суттєвих результатів. А саме, одержані моделі опису індуктивних типів за допомогою ініціальних T-алгебр, на базі ефективних топосів побудовані системи, всі конструкції яких є обчислюваними, одержані ізоморфізми обчислювальних структур для різних класів замкнених категорій, що моделюють певні числення.

Разом з тим, використання апарату екваціональних теорій та методів математичної логіки є, іноді, не досить зручним, а то і взагалі відносно неможливим, як, наприклад, у випадку відсутності адекватного категорного тлумачення (категорної формалізації) певних логічних конструкцій.

Отже, важливими і актуальними є дослідження абстрактних обчислювальних структур, що спиралися б не на сукупність аксіом для внутрішньої мови, а на доволі елементарні факти, задані в термінах співвідношень між морфізмами, що можуть бути виражені комутативними діаграмами. Саме цій проблематиці присвячено дисертаційне дослідження.

Зв'язок роботи з науковими програмами, планами, темами. Дисертація виконана на кафедрі інформаційних систем Київського національного університету імені Тараса Шевченка в рамках тем “Створення теоретичних основ, методів та засобів інтелектуалізації інформаційно-комунікаційних технологій та розподілених комп'ютерних систем” (номер держреєстрації 0106U005860), “Розробка систем інтелектуалізації інформаційних технологій та дистанційного навчання” (номер держреєстрації 0101U002170).

Мета і завдання дослідження. Метою даної роботи є побудова моделей абстрактних обчислювальних структур в категорній аксіоматиці, та визначення співвідношень та умов еквівалентності цих структур. Для досягнення цієї мети визначено такі основні завдання:

* провести аналіз сучасного стану в області категорних моделей абстрактних обчислювальних структур;

* розробити методи побудови морфізмів та індуктивні методи доведення їх властивостей для категорій з об'єктом натуральних чисел;

* побудувати обчислювальну структуру натуральних чисел на об'єктах скінченних сум, декартових добутків, зчисленних сум об'єктів натуральних чисел;

* одержати умови ізоморфності об'єкта натуральних чисел та області нескінченного підоб'єкта об'єкта натуральних чисел, знайти конструкцію ізоморфізму;

* визначити загальні співвідношення для структури підоб'єкту, та за їх допомогою дослідити можливість категорного узагальнення теореми Кантора-Бернштейна.

Об'єктом дослідження є абстрактні обчислювальні структури.

Предметом дослідження є теоретико-категорні моделі абстрактних обчислювальних структур, співвідношення між різними структурами та умови їх еквівалентності.

Методи дослідження. Достовірність одержаних результатів забезпечують використані теоретично та науково обґрунтовані методи математики та метаматематики. В ході дослідження застосовувалися конструктивні методи теоретико-категорного аналізу, індуктивні та дедуктивні методи математичної логіки.

Наукова новизна одержаних результатів. Основні результати, які визначають наукову новизну та виносяться на захист, такі:

* Введено поняття ітеративного морфізму з інваріантним підоб'єктом та запропонований спосіб категорної реалізації конструкції while.

* Одержані умови, за яких на об'єктах скінченних сум, декартових добутків та зчисленних сум об'єктів натуральних чисел може бути утворена обчислювальна структура натуральних чисел.

* Запропоновано і доведено ізоморфність нумерації пар чисел в категорній аксіоматиці, що спирається виключно на ітерацію та властивість парності.

* Для довільної категорії з об'єктом натуральних чисел сформульовані та доведені умови, за яких область нескінченного підоб'єкту об'єкту натуральних чисел є ізоморфною об'єкту натуральних чисел.

* Узагальнена теорема Кантора-Бернштейна. Вперше доведено теорему за умови, коли в алгебрах підоб'єктів наявні -об'єднання. Дане доведення не використовує кванторні співвідношення і може бути поширене на категорії відмінні від топосів.

Практичне значення одержаних результатів. Дисертаційна робота носить теоретичний характер. Одержані результати є новими і можуть бути використані для категорної інтерпретації, аналізу, та розв'язання проблем в обчислювальних системах із підкласами та ітеративними конструкціями, що спираються на натуральні числа. Одержані ізоморфізми для об'єктів натуральних чисел можуть бути використані як аксіоми для розширення екваціональних систем, що описують ізоморфізми типів для звуженого класу категорій. Основне призначення таких систем - ефективний пошук в бібліотеках функцій.

Особистий внесок здобувача. Всі результати дисертації отримано автором особисто. В роботах, які опубліковано зі співавторами, особистий внесок дисертанта такий. В роботах [1,2,5] О.І. Провотарю належить постановка задачі, дисертанту - формулювання та доведення допоміжних тверджень, отримання доведення категорного узагальнення теореми Кантора-Бернштейна, конструкція та доведення ізоморфізму для бінарного декартового добутку об'єктів натуральних чисел. В роботі [4] дисертант поглибив результати попередніх досліджень співавтора.

Апробацiя результатів дисертації. Результати дисертацiйної роботи доповідалися і обговорювалися на семінарах факультету кібернетики Київського національного університету імені Тараса Шевченка; на V Міжнародній науково-практичній конференції ``Системний аналіз та інформаційні технології'' (Київ, 2003); на I, II Міжнародних конференціях ``Theoretical and Applied Aspects of Program Systems Development'' (Київ, 2004, 2005);

Публiкацiї. Основні результати дисертації опубліковано в 6 роботах; з них 4 - статті в наукових фахових виданнях, 2 - тези доповідей.

Структура та об'єм дисертації. Дисертаційна робота складається зі вступу, чотирьох роздiлiв, висновків та переліку використаних джерел, що містить 71 найменування. Загальний обсяг дисертації - 118 сторінок, обсяг основного тексту - 111 сторінок.

ОСНОВНИЙ ЗМІСТ РОБОТИ

У вступі наведено загальну характеристику та цілі роботи, обґрунтовано її актуальність і наукову новизну.

У першому розділі дисертації подано огляд літератури за тематикою категорної абстракції обчислювальних структур. Розглянуті елементарні факти про ізоморфізм. Категорні моделі функціонального програмування та ізоморфізми типів в них.

У другому розділі розглядаються структури алгебр підоб'єктів та співвідношення між алгебрами для об'єктів, пов'язаних мономорфізмами.

У підрозділах 2.1 та 2.2 сформульоване теоретико-категорний варіант теореми Кантора--Бернштейна. Приведені загальні міркування стосовно виконання теореми для топосів передпучків та точкових топосів.

У підрозділі 2.3 досліджені співвідношення між алгебрами підоб'єктів для об'єктів, сполучених мономорфізмом. Для мономорфізму m:A>D множина Sub(D)|m={f:fm} разом з відношенням , що є обмеженням відношення із Sub(D), утворюють гратку. Мономорфізм індукує відображення між алгебрами підоб'єктів, що сформульовано у вигляді леми:

Лема 1. Мономорфізм індукує ізоморфізм граток Sub(A)Sub(D)|m у наступний спосіб .

У підрозділі 2.4 приведене теоретико-категорне доведення теореми Кантора--Бернштейна.

Теорема (Кантора-Бернштейна). Нехай в булевому топосі в алгебрах підоб'єктів існують -об'єднання. Тоді якщо для об'єктів X та Y існують мономорфізми l:Y>X та v:X>Y, то ці об'єкти ізоморфні, тобто XY.

Доведення спирається на лему 1, -об'єднання, а також властивість когерентності доповнень в алгебрах підоб'єктів, що має місце в булевих топосах. Таким чином для виконання теореми Кантора-Бернштейна не обов'язково щоби категорія була булевим топосом, достатньо присутності в ній когерентних доповнень, та відповідних -об'єднань.

Також у підрозділі розглянуто можливість переходу від задачі на ізоморфність пари об'єктів, пов'язаних мономорфізмами, до задачі, в якій були би виконані вихідні умови доведеного варіанту теореми Кантора-Бернштейна. Показано, що засобів алгебр Гейтинга для такого переходу недостатньо.

У підрозділі 2.5 розглянуті умови виконання теореми Кантора - Бернштейна для похідних категорій. На можливість поширення теореми з відносної категорії на вихідну категорію вказує таке твердження.

Твердження 1. Для того, щоби в категорії виконувалась теорема Кантора--Бернштейна достатньо аби вона виконувалася в відносній категорії для деякого непорожнього об'єкту X.

Вважається, що наявність глобальних елементів є надто сильною вимогою для робочої категорії. Це зрозуміло, бо, наприклад, хоча в відносних топосах термінальний елемент визначається дуже просто, знаходження глобальних елементів є проблемним, окрім, зрозуміло, випадку, де роль об'єктів грає проекція декартового добутку, а для нетривіальних конструкцій, таких як класифікатор часткових морфізмів, використовуються локальні елементи. Відомі категорії (часткові топоси), що не містять термінального об'єкту. Для таких категорій отримане твердження.

Твердження 2. Якщо в виконується теорема Кантора--Бернштейна і визначені підоб'єкти, то існує ізоморфізм h, що переводить один підоб'єкт в інший:.

Відповідно, якщо існують вказані в умовах твердження 2 перетини в алгебрах підоб'єктів, то теорема Кантора-Бернштейна виконана в вихідній категорії. Для того щоб застосувати дані міркування до певної категорії необхідно, щоб в ній існував такий об'єкт ?, для якого існують бієкції між Sub(A) та Hom(A,?), та для довільних мономорфізмів v, l виконувалася рівність (vl)v=(vl)індекс, за яким береться компонента , вважається відомим за аргументом. Друга вимога може бути виражена як

.

У третьому розділі розглядаються методика реалізацій ітеративних алгоритмів та проведення доведень на абстрактній обчислювальній структурі, що моделюється об'єктом натуральних чисел.

У підрозділі 3.1 розроблені методи доведення за індукцією тверджень в категоріях з об'єктом натуральних чисел. Відомий принцип індукції, що виконується для об'єкта натуральних чисел, є доволі загальним. Здебільшого його використання можливо лише після певних підготовчих кроків, пов'язаних з обранням підоб'єкту об'єкту N. В даному підрозділі були досліджені типові застосування принципу індукції, що сформульовані у вигляді тверджень. Одні твердження стосуються умови рівності морфізмів для різних категорій. Інші стосуються умов мажорантності. Для прикладу наведемо одне з тверджень про доведення рівності морфізмів в декартово-замкненій категорії.

Твердження 3. Нехай f, g: XNY. Тоді якщо виконуються положення:

;

для довільного з комутативності (діаграма) слідує комутативність

то

f=g.

У підрозділі 3.2 введено та досліджується поняття інваріантів ітеративних морфізмів. Вони призначені для отримання властивостей ітеративних морфізмів та моделювання конструкції імперативного програмування циклу while.

Визначення 1. Назвемо морфізм u:XY інваріантним ендоморфізму f:XX, якщо є також ендоморфізмом на у категорії .

Твердження 4. Якщо морфізм інваріантний f і морфізм h:NZX визначений за аксіомою NNO морфізмами h₀:ZX, , то має місце

.

Нехай задано мономорфізм (невідомо чи є в нього булеве доповнення). Припустимо є деякий морфізм alg:ZNX, для якого комутує діаграма.

Накладемо умову на морфізм :

(1)

Позначимо =alg^-1[m]:EZN. Інтуїція підказує, що коли результат такого морфізму потрапляє у підоб'єкт m, то за збільшення кількості ітерацій він залишатиметься у m. Це формалізується таким твердженням.

Твердження 5. Має місце

де .

Для доведення використовується узагальнені співвідношення в алгебрах підоб'єктів та принцип індукції.

Наслідок 1. Якщо для деякого морфізму f:YZN виконується і для деякого морфізму g:YN виконується gf_N, то .

Наслідок 2. Якщо , то - ізоморфізм, та, відповідно, образ морфізму потрапляє в m.

Визначення 2. Назвемо підоб'єкт m інваріантним ендоморфізму f, якщо f є також ендоморфізмом на m у , тобтоУ разі , f слід скорегувати на відповідний автоморфізм fm=m.

Зауважимо, що інваріантність підоб'єкту та інваріантність його характеру незалежні.

Тепер розглянемо ітеративний морфізм, для якого підоб'єкт m є інваріантним кроку ітерації step. Очевидно, що для морфізму step виконується умова (1) Показано, що в даному випадку можна ще точніше вказати значення ітеративного морфізму за умов, аналогічних твердженню 5.

Лема 2 (про стабілізацію). Якщо m є інваріантним step підоб'єктом, то

(2)

Доведення проводиться за індукцією з використанням загальної властивості, викладеної в твердженні 5.

Наслідок. Якщо для деякого морфізму f:YZN виконується , і для деякого морфізму g:YN виконується gf_N, то

Твердження 6. Якщо , то .

Морфізми, вказаного типу, можна синтезувати в випадку коли підоб'єкт має когерентне доповнення. Тоді враховуючи, що доповнення визначає конструкцію бінарної суми, можна задавати морфізм кроку ітерації покомпонентно. Зрозуміло, що складова на m тотожня. В свою чергу складова на другій ін'єкції визначає логіку дії морфізму. Досить часто такими підоб'єктами є підоб'єкти, що пов'язані із відношенням порядку на об'єкті натуральних чисел, тому на категорію накладається вимога на розв'язність даного відношення.

У підрозділі 3.3 розглянуто проблему замикання ітеративних морфізмів з інваріантним підоб'єктом. Під замиканням ми розуміємо перехід до деякого підоб'єкту об'єкту Z, для якого ітерація стабілізується. Ітеративний морфізм можна замкнути, коли заздалегідь відома кількість ітерацій, за яких морфізм досягає підоб'єкту m, що задається мажоруючим морфізмом n:Z'N, де . Відповідно, замиканням морфізму буде морфізм algn,l.

Побудуємо підоб'єкт об'єкту Z, що складається з “елементів”, для яких морфізм досягає значення в m. Його можна отримати застосуванням функтору існування до . Отже це підоб'єкт (p_Z). Аби мати змогу відтворити за його елементом кількість ітерацій необхідно, щоб даний морфізм пропускався через проекцію p_Z:ZNZ. Досягнути цього можна, коли епіскладова морфізму p_Z є розщепленим епіморфізмом. Тоді існує :EE, такий, що (p_Z)_e=id_E. Це дає змогу скомпонувати морфізм :EZN. Відповідно замиканням морфізму є h=alg.

Умова наявності розщеплення є занадто сильною і має сумнівну конструктивність. У підрозділі 3.4 показано, як отримати замикання в випадку, коли відносна категорія є топосом.

Припустимо, що підоб'єкт має когерентне доповнення. Побудуємо на XN як на вершині суми морфізм кроку ітерації, таким чином, що на mN він тотожній, а на (-mN) за X веде себе як step, а за N робить інкремент - . Побудуємо допоміжний ітеративний морфізм , для якого комутує діаграма.

Морфізм має ряд властивостей. Вихідний морфізм є складовою даного: . Декартовим підйомом морфізму mN вздовж є . Можна замінювати другу компоненту значення на вході на його композицію із і при цьому результат дії морфізму не зміниться, тобто .

Позначимо , . Якщо розглядати як підоб'єкт об'єкту p_E:ENE у відносній категорії і ця категорія топос, то виконуватиметься . А це має наслідком існування морфізму x:EEN, що пропускається крізь r, та для якого p_Ex=id_E. Оскільки , то відповідно . Маємо діаграму.

Для часткових топосів доведено таку лему.

Лема 3. З кожним ітеративним морфізмом alg:ZNX, крок ітерації якого має інваріантний доповнюваний підоб'єкт, пов'язаний морфізм _alg:EN такий, що .

У четвертому розділі побудовані ізоморфізми об'єкта натуральних чисел граничним та кограничним конструкціям на об'єктах натуральних чисел.

Ізоморфність вершини деякої конструкції та об'єкта натуральних чисел має два аспекти. З одного боку, це наділяє дану конструкцію структурою натуральних чисел - відповідно, наявні морфізми початку і слідуванні. З іншого, ми переносимо структуру даної конструкції на об'єкт натуральних чисел, що дає змогу надалі працювати з ним, як з відповідною конструкцією з певними властивостями універсальності.

Було розглянуто декілька граничних конструкцій на об'єктах натуральних чисел: скінченні суми, декартові добутки, зчисленні суми, та нескінченні підоб'єкти.

У підрозділі 4.1 розглянуто бінарну суму об'єктів натуральних чисел. Як відомо, суми є категорною інтерпретацією варіантних утворень. Нехай в категорії існує об'єкт суми NN. Розглянемо ітеративний морфізм, що визначається ітеративною діаграмою.

Твердження 7. Морфізм enum є ізоморфізмом NNN із зворотним , де морфізм подвоєння.

Приведені два доведення. Одне спирається на існування суми і можливість визначення морфізма [i₂,i₁s], що інкрементує значення після подвійного застосування. Друге спирається на властивості морфізмів у алгебрі підоб'єктів та морфізму максимуму. Якщо в категорії виконані умови другого доведення, то в ній можна безпосередньо побудувати бінарну суму N+N.

Наслідок. Трійка утворює конструкцію бінарної суми, а для діаграми має місце аксіома NNO.

У підрозділі 4.2 розглянуто об'єкт цілих чисел. За визначенням, це сума об'єктів натуральних чисел, в якій ототожнено нулі для складових. Спираючись на твердження 7 доведено

Твердження 8. У категорії з об'єктом натуральних чисел виконується ZN.

У підрозділі 4.3 конструкцію підрозділу 4.1 поширено на -суму об'єктів натуральних чисел. Роль вкладення об'єкта суми грає морфізм . Зворотний морфізм будується за аксіомою NNO за діаграмою, де . Ідея є узагальненням випадку двох складових, а саме - зсув відбувається на кожен крок і є циклічним, а інкремент відбувається лише на кожний n-й крок. Має місце

Твердження 9. Морфізми em та enum є зворотними ізоморфізмами один до одного.

У підрозділі 4.4 за допомогою лінійних морфізмів узагальнено представлення об'єкта N у вигляді суми.

У підрозділі 4.6 розглянуто бінарний декартів добуток NN. Конструкція ізоморфізму така. Морфізм em:NN N визначається комутативною діаграмою.

Зворотний до нього морфізм базується на замиканні ітеративного морфізму alg із інваріантним підоб'єктом . Відповідно, на другій ін'єкції крок виконує операцію ділення на два, тобто . Цей ітеративний морфізм виділяє ступінь двійки та непарний множник, з якого вже легко отримати один з аргументів за допомогою морфізму ділення div2. Показано, що для замикання можна використати діагональний морфізм.

За своєю побудовою step має інваріантний морфізм, де є морфізм, пов'язаний з ітеративною схемою. Використовуючи це та властивості ітеративних морфізмів з інваріантами доведено:

Твердження 10.em є ізоморфізмом,.

У підрозділі 4.7 розглянуто нескінченні підоб'єкти об'єкта натуральних чисел. Вважатимемо підоб'єкт m:XN нескінченним, якщо він має підоб'єктом об'єкт натуральних чисел l:NX.

Умова 1 (монотонності).

,

де .

Для категорій з розв'язним відношенням порядку на об'єкті натуральних чисел було доведено таке твердження.

Твердження 11 (₀-теорема Кантора--Бернштейна). Якщо для нескінченного доповнюваного підоб'єкта об'єкта натуральних чисел виконано умову 1, то його область ізоморфна об'єкту натуральних чисел.

Морфізм початку і слідування ізоморфної нумерації є категорними аналогами алгоритмів пошуку першого числа в m, починаючи з заданого числа.

ВИСНОВКИ

В дисертації запропоновано теоретичне узагальнення та новий підхід до побудови моделей абстрактних обчислювальних структур в категорній аксіоматиці, досліджені співвідношення та умови еквівалентності таких структур. Основними результатами дисертації є наступні:

* Розроблено індуктивну методику доведення співвідношень для морфізмів, областю (чи кообластю) яких є об'єкт натуральних чисел.

* Запропоноване поняття ітеративних морфізмів з інваріантами, спосіб та умови реалізації конструкції циклу while за допомогою таких морфізмів.

* Побудовані ізоморфізми об'єкта натуральних чисел в об'єкти скінченних та зчисленних сум об'єктів натуральних чисел, а також в об'єкт цілих чисел.

* Запропоновано і доведено ізоморфність нумерації абстрактної структури пар натуральних чисел в категорній аксіоматиці. На відміну від традиційної нумерації, дана спирається виключно на ітерацію та властивість парності.

* Одержані умови ізоморфності області нескінченного підоб'єкта об'єкта натуральних чисел об'єктові натуральних чисел, тобто умови виконання ₀-варіанту теореми Кантора-Бернштейна. Одержано конструкцію ізоморфізму.

* Одержані ізоморфні ітератори для систем з базовим типом N (для довільних композитних типів). Вони є категорними реалізаціями простих та зрозумілих узагальнених алгоритмів.

* Доведено категорне узагальнення теореми Кантора-Бернштейна за умови існування в алгебрах підоб'єктів -об'єднань та когерентних доповнень.

* Досліджено умови виконання теореми Кантора-Бернштейна для відносних категорій. Показано, що якщо теорема має місце для відносної категорії , де об'єкт X непорожній, то вона також матиме місце для вихідної категорії .

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Ченцов А.И., Провотар А.И. Обобщение теоремы Кантора - Бернштейна для булевых топосов // Компьютерная математика. - 2003. - № 2. - С. 45-53.

2. Ченцов А. И., Провотар А. И. Конечные декартовы произведения объектов натуральных чисел в топосах // Компьютерная математика. - 2004. - № 2.- С. 136-143.

3. Ченцов А.И. Суммы объектов натуральных чисел в топосах // Компьютерная математика. - 2005. - № 2.- С. 34-143.

4. Ченцов А.И., Провотар А.И. Обобщение линейных морфизмов на N в топосах // Кибернетика и системный анализ. - 2005. - № 5.- С. 66-72.

5. Ченцов О.І., Провотар О.І. Теорема Кантора - Бернштейна в контексті проблеми ідентифікації об'єктів // Тези доп. міжн. конф. “Системний аналіз та інформаційні технології”. - Київ: ІПСА, 2003. - С. 120-121.

6. Ченцов О.І. Ітератори кортежів натуральних чисел в конструктивних абстракціях функціонального програмування // Тези доп. міжн. конф. “Теоретичні та прикладні аспекти побудови програмних систем”. - Київ: НаУКМА, 2004. - С.76-79.

абстрактний ізоморфність обчислювальний натуральний

АНОТАЦІЇ

Ченцов О.І. Моделі та методи дослідження абстрактних обчислювальних структур в категорній аксіоматиці. -- Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук зі спеціальності 01.05.01 - теоретичні основи інформатики та кібернетики. - Київський національний університет імені Тараса Шевченка. - Київ, 2007.

В дисертації описано теоретико-категорні моделі абстрактних обчислювальних структур, співвідношення між абстрактними обчислювальними структурами та умови їх еквівалентності. Досліджено загальну структуру підоб'єкту та одержані співвідношення між алгебрами підоб'єктів пов'язаних мономорфізмом об'єктів. Доведено категорне узагальнення теореми Кантора-Бернштейна для категорій, в алгебрах підоб'єктів яких існують -об'єднання та когерентні доповнення.

Отримано ряд тверджень для доведення різних властивостей морфізмів за допомогою принципу індукції. Розширено метод побудови морфізмів в термінах імперативної мови програмування. Для категорної реалізації конструкції while введено поняття ітеративних морфізмів з інваріантами.

За допомогою розвинутих методів побудовано ізоморфізми об'єкта натуральних чисел та різних структур, похідних від об'єкта натуральних чисел. А саме для скінченних сум, скінченних декартових добутків, зчисленних сум та нескінченних підоб'єктів об'єкту натуральних чисел. Отримані достатні умови для існування цих ізоморфізмів в конкретній категорії.

Ключові слова: абстрактні обчислювальні структури, ізоморфізм, алгебра підоб'єктів, теорема Кантора-Бернштейна, об'єкт натуральних чисел, ітеративні морфізми з інваріантними підоб'єктами, індуктивні методи доведення.

Ченцов A.И. Модели и методы исследования абстрактных вычислительных структур в категорной аксиоматике. -- Рукопись.

Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.01 - теоретические основы информатики и кибернетики. -- Киевский национальный университет имени Тараса Шевченко. - Киев, 2007.

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

Исследована структура алгебр подобъектов и отношения между алгебрами, соответствующими объектам, связанным мономорфизмами. Получено доказательство теоремы Кантора--Берштейна для категорий, в которых алгебры подобъектов имеют когерентные дополнения и счетные объединения. Предложен способ построения для объектов, связаных мономорфизмом, приближений удовлетворяющих теореме Кантора-Бернштейна. Рассмотрены условия переноса теоремы Кантора--Бернштейна из исходной категории в ее производные категории и наоборот. Показано, что достаточным условием для выполения теоремы Кантора-Бернштейна в исходной категории является ее выполнение в относительной категории для непустого объекта X.

На основе принципа индукции разработан метод доказательства утверждений, касающихся морфизмов на объекте натуральных чисел, определены рамки его применения. Введено понятие итеративных морфизмов с инвариантными подобъектами. Инвариантные подобъекты - это такие подобъекты кообласти итеративных морфизмов, на которых шаг итерации совпадает с пустым оператором. При попадании результата итеративного морфизма в инвариантный подобъект последующие итерации его не меняют, что формализовано леммой о стабилизации. Можно говорить о замыкании итеративного морфизма, как о получение стабилизированного значения по заданому значению аргумента. Соответствующий морфизм является категорной реализацией цикла, заканчивающегося по условию: конструкции while. Для замыкания необходимо указать количество итераций, достаточное для достижения стабилизации. Показано, что достаточным условием для замыкания является выполнение для категории аксиомы выбора. Наконец, для категорий, имеющих достаточно развитые логические средства, доказана возможность замыкания итеративного морфизма в случае, когда подобъект имеет когерентное дополнение.

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

Ключевые слова: абстрактные вычислительные структуры, изоморфизм, алгебра подобъектов, теорема Кантора-Бернштейна, объект натуральных чисел, итеративные морфизмы с инвариантными подобъектами, индуктивные методы доказательства.

Chentsov O.I. Models and Research Methods for Abstract Computational Structures within Categorical Axiomatics. -- Manuscript.

Thesis for obtaining Candidate of Science (Physics and Mathematics) degree (Ph.D) speciality 01.05.01 - Theoretical Foundations of Informatics and Cybernetics. - Kyiv Taras Shevchenko National University. - Kyiv, 2007.

In the thesis categorical abstract computational structures were considered. The general structure of subobject is described and relations between subobject algebras induced by monomorphism is derived. Category theory generalization of Cantor-Bernstein theorem is investigated and proof for categories with -complete subobject algebras is given.

Proving methods for morphism structures involving natural number object are developed. Reasoning technique using iterative morphism invariant subobject is proposed. It allows constructing morphisms that correspond to algorithms available in algorithmic language.

Using developed methods isomorphisms for various structures based on natural number object are derived. Namely isomorphisms between natural number object and n-ary coproduct, binary cartesian product and domain of infinite subobject of natural number object. Sufficient conditions for such isomorphisms to exist in concrete category are obtained.

Key words: abstract computational structures, isomorphism, subobject algebra, Cantor-Bernstein theorem, natural number object, iterative morphism invariant subobject, inductive proving.

Размещено на Allbest.ru

...