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

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

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

УДК 681.3.06

ТЕОРІЯ ІНТЕГРОВАНИХ КОМПОЗИЦІЙНО-НОМІНАТИВНИХ

МОДЕЛЕЙ ПРОГРАМ

01.05.03 - математичне та програмне забезпеченняобчислювальних машин і систем

Автореферат

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

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

НІКІТЧЕНКО Микола Степанович

Київ - 2001



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

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

Науковий консультант: академік НАН України,доктор фізико-математичних наук, професор РЕДЬКО В.Н., Київський національний університет імені Тараса Шевченка, завідувач кафедри теорії програмування.

Офіційні опоненти: доктор фізико-математичних наук, професор КАПІТОНОВА Ю. В., Інститут кібернетики НАН України, м. Київ, завідувач ідділу теорії цифрових автоматів;

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

доктор фізико-математичних наук, професор ПРОВОТАР О. І., Київський державний лінгвістичний університет, завідувач кафедри інформатики.

Провідна організація: Інститут програмних систем НАН України, відділ теорії комп'ютерних обчислень, м. Київ.

Захист відбудеться 4 жовтня 2001 р. о 14 год. на засіданні спеціалізованої вченої ради Д 26.001.09 у Київському національному університеті імені Тараса Шевченка за адресою: 03127, Київ, пр. Глушкова, 2, корп. 6, ф-т кібернетики, ауд. 40. (Тел.252-58-83. Факс 252-59-77. E-mail: rada@unicyb.kiev.ua)

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

Автореферат розiсланий " 7 " серпня 2001 р.

Вчений секретар

спецiалiзованої вченої ради В.П.Шевченко



Нікітченко М.С. Теорія інтегрованих композиційно-номінативних моделей програм.- Рукопис. обчислюваний програма алгебраїчний

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

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

Ключові слова: моделі програм, специфікації програм, композиції програм, математична логіка, теорія обчислюваності.



НИКИТЧЕНКО Н.С. Теория интегрированных композиционно-номинативных моделей программ.- Рукопись.

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

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

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

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

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

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

Построенные композиционно-номинативные модели программ применены для описания языков программирования и языков баз данных, а также для моделирования транспортных систем.

Ключевые слова: модели программ, спецификации программ, композиции программ, математическая логика, теория вычислимости.



NIKITCHENKO M.S. Theory of integrated composition nominative program models.- Manuscript.

Thesis for a doctor's degree of physics and mathematics by speciality 01.05.03 - mathematical and program software of computers and systems. Kyiv Taras Shevchenko national university, Kyiv, 2001.

A general theory of program models, based on principles of development, compositionality and nominativity is developed. A formalism of composition nominative systems, which represent program models of various abstraction and generality levels and which permits program adequate specification and effective realisation, is proposed and investigated. Subclasses of such systems, which represent infinitary predicate logics of various types, are investigated. Classical problems of correctness and completeness are solved for such logics. Program computability methods, which generalise traditional approaches to computability, are defined and investigated. The complete classes of computable functions and compositions over nominative data of various abstraction and generality levels are defined and algebraic representations of such classes are constructed.

Key words: program models, program specifications, program compositions, mathematical logic, computability theory.



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

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

Справді, розроблені моделі програмних систем (програм) традиційно розділяють на три відносно незалежні групи: денотаційні, операційні та аксіоматичні моделі. Для кожної групи увага акцентується переважно на одному аспекті програм. Зокрема, денотаційні моделі орієнтовані перш за все на такий засіб побудови програм, як оператор найменшої нерухомої точки (рекурсія); операційні моделі - на пристрої, що забезпечують обчислення програм; аксіоматичні моделі - на логічні формалізми специфікації програм. Така різнорідність типів моделей утруднює розробку багатоаспектних (інтегрованих) технологій конструювання програм. Безумовно, ця обставина усвідомлюється багатьма фахівцями, які намагаються об'єднати різноманітні теорії програмування і моделі програм. Проте роботи в цьому напрямку фактично обмежуються демонстрацією взаємної трансляції моделей при деяких умовах. Осторонь залишаються найважливіші питання методологічного обгрунтування моделей, повноти, взаємозалежності і розвитку. Більше того, можна стверджувати, що навіть дуже детально розроблені моделі вказаних класів вельми неадекватно відображають специфіку програмування. Для такої неадекватності є об'єктивні обставини. Справа в тому, що всі вказані типи моделей спираються на традиційні математичні формалізми - теорію алгоритмів, математичну логіку й універсальну алгебру. Проте ці формалізми були в основному сформовані до 40-х років 20-го сторіччя, тобто раніше, ніж програмування набуло значного поширення. Тому немає нічого надзвичайного в тому, що ці формалізми та побудовані на їхній основі моделі програм не враховують істотних особливостей програмування. Серед цих особливостей зазначимо такі.

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

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

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

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

5. Традиційні формалізми орієнтовані на клас n-арних однозначних (часто всюди визначених) відображень, у той час як в програмуванні використовується і більш широкий клас номінативних часткових недетермінованих відображень. Крім того, традиційні формалізми звичайно базуються на фінітарних побудовах, у той час як в мовах специфікацій програм дедалі частіше застосовуються інфінітарні побудови, причому як для структур даних, так і для самих специфікацій.

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

Сучасний етап розвитку програмування висуває нові вимоги до моделей програм. Головними з цих вимог є такі:

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

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

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

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

Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконувалася в рамках комплексної наукової програми Київського національного університету імені Тараса Шевченка "Перспективні інформаційні технології, прилади комплексної автоматизації, системи зв'язку" (теми "Дослідження універсальних та спеціалізованих програмних логік", 1996-2000, номер держреєстрації 197U003444, і "Логіко-математичні та програмологічні засоби інформаційних технологій", 2001-2005, номер держреєстрації - 0101U002163), а також у рамках госпдоговірної теми "Розробка об'єктно-орієнтованих моделей баз даних", 1993-1996, номер держреєстрації 0195U008132.

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

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

- розробка нових методологій моделювання програм;

- розробка і дослідження поняття композиційно-номінативної системи, що дозволяє побудувати ієрархії моделей програм різних рівнів абстракції та загальності;

- виділення підкласів композиційно-номінативних систем, які формалізують семантичні аспекти логік різноманітних типів;

- виділення підкласів композиційно-номінативних систем, які описують повні класи обчислюваних функцій і композицій над різноманітними структурами даних;

- застосування розроблених методів і моделей для формалізації предметних областей.

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

Головним методологічним методом є метод сходження від абстрактного до конкретного. Головні математичні методи включають методи формальної логіки, теорії алгоритмів та універсальної алгебри.

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

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

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

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

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

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

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

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

- Побудовано композиційно-номінативні моделі програм, які застосовано для опису мов програмування та мов баз даних, а також для моделювання транспортних систем.

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

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

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

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

Результати проведених досліджень були також використані в проектах, підтриманих грантами Міжнародного інституту інформаційних технологій Університету Об'єднаних Націй - UNU/IIST (1996), INTAS-94-1817 (1995-1998), Датської Дослідницької Академії DRA N1997-125-0031 (1997-1998).

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

Апробація роботи. Основні результати роботи пройшли апробацію в провідних наукових колективах України, Росії, Данії, Німеччини, Голландії. Вони доповідались на засіданнях семінарів "Теорія мов і процесорів", "Теорія автоматів та її застосування", "Програмологія та її застосування" (Київ, 1982-2001), Всесоюзних конференціях "Проблеми теоретичної кібернетики" (Іркутськ, 1985, Горький, 1988, Волгоград, 1990), Всесоюзних конференціях з прикладної логіки (Новосибірськ, 1985 і 1988), Міжнародному семінарі "Software Construction - Foundation and Application" (Dagstuhl, Germany, 1992), First International Symposium of Formal Methods Europe (Odense, Denmark, 1993), Second International East-West Database Workshop (Klagenfurt, Austria, 1994), International Workshop on Advances in Databases and Information Systems (Москва, 1995, 1996), Міжнародних науково-практичних конференціях з програмування (Київ, 1998, 2000).

Публікації. За темою дисертації опубліковано 30 наукових праць. Основні результати дисертації повно викладені в роботах [1-22], надрукованих у виданнях, які затверджені ВАК України. Серед цих робіт 11 опубліковано без співавторів.

Структура і обсяг роботи. Дисертаційна робота складається із вступу, п'ятьох розділів, висновків, списку використаних джерел (159 найменувань). Загальний обсяг дисертації становить 312 сторінок, основний текст роботи викладено на 297 сторінках.

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

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

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

У першому підрозділі формулюються основні принципи композиційно-номінативного підходу. Центральним з них є наступний принцип.

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

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

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

Принцип прагматичності програм: на абстрактному рівні розгляду основним призначенням програм є їхня корисність (прагматичність) для вирішення проблем користувача.

Наступний крок розвитку полягає в визначенні такого поняття, що забезпечує єдність понять "проблема" і "програма". Таким поняттям є програмування, яке здійснює їх єдність, тобто програмування мусить привести до такої програми, яка адекватно задає рішення проблеми.

Принцип адекватності програмування: на абстрактному рівні розгляду процес програмування повинний бути орієнтований на побудову програми, що адекватно задає рішення заданої проблеми.

Таким чином, введено чотири поняття - користувач, проблема, програма і програмування, які утворюють тетраду основних понять програмування.

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

Принцип інформаційності проблеми: на абстрактному рівні розгляду основною властивістю проблеми, релевантною програмуванню, є властивість інформаційності.

Поняттю інформації відповідає в області програм поняття даних. Отже, основною (істотною) властивістю програм є властивість аплікативності.

Принцип аплікативності (функціональності): на гранично високому рівні абстракції програми доцільно розглядати як функції, що при застосуванні до вхідних даних можуть виробляти вихідні дані.

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

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

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

Принцип композиційності [В.Н. Редько]: програми (функції) будуються з більш простих програм за допомогою композицій.

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

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

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

Введених понять достатньо для побудови багатих моделей програм.

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

Принцип обчислюваності: програми і композиції є обчислюваними відображеннями.

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

Наступний підрозділ першого розділу присвячений формалізації введених програмних понять.

Традиційно для формалізації програмних понять використовують теоретико-множинний підхід, часто в дуже специфічній формі. Наприклад, такі методи формальної розробки програм, як Z і B, безпосередньо спираються на аксіоматичну теорію множин Цермело-Френкеля. Композиційно-номінативний підхід орієнтується на теоретико-функціональну формалізацію.

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

Функції трактуються як часткові багатозначні функції. Клас таких функцій із D у R позначається DR. Клас тотальних (всюди визначених) функцій - DR.

Наводиться приклад теоретико-функціональної формалізації простої програми.

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

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

Визначення 1.1 Композиційною системою (КС) називається об'єкт Cm(Z) = <D, F, C> де D - довільна множина, яка називається множиною даних,

F - довільна підмножина класу DD усіх часткових багатозначних функцій на D, яка називається множиною функцій КС,

Z - довільна множина, яка називається множиною імен аргументів композицій,

C - довільна підмножина класу (ZF) F усіх часткових багатозначних відображень із ZF у F, яка називається множиною Z-номінативних композицій над F.

Клас StDes інфінітарних стандартних дескрипцій програм визначається індуктивно на основі множин імен базових функцій Fn, композицій Cn і аргументів композицій Z. Для виділення спеціальних класів стандартних дескрипцій вводиться відповідна програмна система.

Визначення 1.2 Стандартною номінативною (дескриптивною) системою називається об'єкт Nm(Z) = <Fn, Cn, Ds> де Fn - довільна множина імен базових функцій,

Cn - довільна множина імен базових композицій,

Z - довільна множина імен аргументів композицій,

Ds StDes - довільна підмножина множини стандартних дескрипцій.

Відношення денотації для композиційної системи Cm(Z) і номінативної системи Nm(Z) конкретизується як відображення den: DsF. В силу індуктивної побудови дескрипцій, достатньо задати відношення денотації для імен базових функцій та імен композицій: den_fn: FnF і den_cn: CnC. У цьому випадку стандартну систему денотації можна задати таким визначенням.

Визначення 1.3 Стандартною денотаційною системою над композиційною системою Cm(Z) = <D, F, C> і стандартною номінативною системою Nm(Z) = <Fn, Cn, Ds> називається об'єкт Dn(Z)= <den_cn, den_fn>, де den_cn: CnC - відображення денотації імен базових композицій, den_fn: FnF - відображення денотації імен базових функцій.

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

Визначення 1.4 Стандартною композиційно-номінативною системою (КНС) Z-номінативного типу називається об'єкт CNS = <Cm(Z), Nm(Z), Dn(Z)>, де

Cm(Z) = <D, F, C> - довільна композиційна система,

Nm(Z) = <Fn, Cn, Ds> - довільна стандартна номінативна система,

Dn(Z) = <den_cn, den_fn> - стандартна денотаційна система над Cm(Z) і Nm(Z).

КНС, як видно з наведеного визначення, є спеціальними мовними системами, призначеними для опису різноманітних класів функцій. Їх можна також називати композиційно-номінативними мовами функцій. Такі системи тісно пов'язані з алгебрами функцій і даних. Ці системи побудовані в семантико-синтаксичному стилі і спираються на парадигми композиційності, номінативності і розвитку. Відмінності від традиційних систем (моделей програм) полягають у наступному:

1) формалізація ведеться на основі теоретико-функціонального підходу,

2) замість традиційних класів однозначних n-арних функцій розглядаються часткові багатозначні номінативні відображення,

3) структури даних є похідними номінативних структур.

Переваги такого підходу:

1) побудовані моделі програм є математично простими, але більш адекватними для опису семантики програм,

2) є можливість широкого використання методів універсальної алгебри, математичної логіки і теорії алгоритмів для дослідження програм,

3) введені моделі програм є параметричними і дозволяють природним чином задавати програми різних рівнів абстракції і загальності.

Наступний підрозділ першого розділу присвячений класифікації і властивостям композиційно-номінативних систем.

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

Дані розглядаються на трьох рівнях: абстрактному, бульовому і номінативному.

На номінативному рівні дані трактуються як номінативні дані. Клас ND(V,W) інфінітарних номінативних даних над множиною V базових імен та множиною W базових значень може бути заданий таким рекурсивним визначенням: ND(V,W) = W (VND(V,W)).

У програмуванні клас номінативних даних обмежується класом ієрархічно побудованих скінченних відображень. Тому виділяються такі основні класи інфінітарних номінативних даних:

однозначні номінативні дані [В.Н. Редько] (скінченні однозначні відображення), що називаються іменними даними і задаються рекурсивним визначенням Nam(V,W) = W (VNam(V,W)),

багатозначні номінативні дані (скінченні багатозначні відображення), що називаються просто номінативними даними (або мульти-іменними даними) і задаються рекурсивним визначенням Nom(V,W) = W (VNom(V,W)).

Іменні дані дозволяють формалізувати структури даних, що використовуються в програмуванні і характеризуються однозначністю іменування своїх компонент. Це такі структури даних, як записи, масиви, файли і т.п. Номінативні дані дозволяють задавати структури даних, котрим властива неоднозначність іменування своїх компонент, такі як множини, мультимножини, реляції, сукупності і т.п.

Принцип репрезентативної повноти номінативних даних: структури даних мов програмування можуть розглядатися як конкретизації номінативних даних.

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

Композиції класифікуються за рівнями розгляду даних і функцій, а також за типом їх аргументів. Найважливішим типом композицій є клас ^ZFF - Z-квазіарних композицій, де ^ZF = ZF. Дається експлікація цього класу композицій, що відповідає гранично абстрактному розгляду функцій як слабко аплікативних функцій. Таке уточнення будується на основі поняття детермінанту композиції, що задається відображенням спеціального типу. Отриманий клас композицій називається класом аплікативних композицій. Він задає дуже багатий клас засобів конструювання програм. Доводиться теорема про збіжність класу таких композицій із класом монотонних композицій.

Визначаються найбільш важливі аплікативні композиції абстрактного, бульового і номінативного рівнів. Це дозволяє ввести базисну композиційно-номінативну мову BACON(V,W), в основі якої лежить n-арна КС BCS(V,W) = <D, F, BC>, де - D = Nam(V,W) - множина іменних даних над V і W,

- F = DD - множина недетермінованих (багатозначних) функцій над D,

- BC - множина базових композицій (і функцій), що складається з параметричних функцій іменування v, розіменування v, предиката наявності значення v!, недетермінованої функції вибору і композицій множення , циклювання і накладення .

Похідні композиції і функції задаються за допомогою нерекурсивних визначень.

Незважаючи на простоту, мова BACON(V,W) має велику виразну потужність, а її композиції незалежні.

Теорема 1.3 У будь-якій мові BACON (V, W) виразима будь-яка частково рекурсивна функція.

Теорема 1.4 Композиції множини BC взаємно незалежні.

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

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

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

гранично абстрактний рівень розгляду предикатів, на котрому припустиме використання тільки властивості аплікативності предикатів,

конкретний рівень розгляду імен аргументів композицій, на котрому припустиме використання всіх їхніх властивостей,

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

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

Обгрунтовується і вводиться клас детермінантів пропозиційних композицій K(Z) = ^ZBoolBool (визначення 2.2), де ^ZBoolBool - клас відображень, які зберігають значення при розширеннях аргументів. Такі відображення називаються еквітонними. На основі поняття детермінанту визначається клас CPR(Z,D) пропозиційних композицій (визначення 2.3).

Для дослідження класу пропозиційних детермінантів і композицій вводиться інфінітарна пропозиційна алгебра Кліні AK(Z) = <K(Z), _K, _K, _K>, де _K і _K фактично є множинними інфінітарними аналогами операцій сильної диз'юнкції і сильної кон'юнкції Кліні, а _K є операція заперечення. Наступна теорема задає базис цієї алгебри.

Теорема 2.1 Всюди невизначена функція {_K} і множина функцій розіменування {'z_K |z Z} є базисом інфінітарної Z-пропозиційної алгебри Кліні AK(Z).

Таким чином, операції алгебри Кліні разом з функціями базису утворюють повний для класу K(Z) набір композицій, подібно до того, як вони (у їх скінченноарному варіанті) є функціонально повним набором для класу тотальних бульових функцій.

На основі алгебри AK(Z) будується алгебра пропозиційних композицій ACPR(Z,D). З теореми про базис випливає, що відповідна множина TK(Z) термів алгебри Кліні задає усі детермінанти. Далі доводиться, що ці терми також задають усі пропозиційні композиції. Для таких термів можна визначити спеціальну позитивно-негативну нормальну форму. Для побудови повної системи тотожних перетворень вводиться спеціальний варіант інфінітарного екваційного числення з відношенням вивідності |-.

Система тотожностей задається такими схемами аксіом.

K1: { { X_ij | j J_i } | iI} = { X_ij | jJ_i, iI} - асоціативність.

K2: {X} = X - ідемпотентність.

K3: { {X_ij | jJ_i } | iI} = { {X_{i ( i )} | iI } | _iI J_i }

- цілком дистрибутивність.

K4: {X, {X, X'}} = X - поглинання.

K5: X = X - інволюція.

K6: {X_i | i I } = { X_i | iI } - закон де Моргана.

K7: = - нерухома точка.

K8: { {X, X}, {X', X'}} = {X, X} - нормальність.

Центральним твердженням підрозділу є така теорема.

Теорема 2.4 Для будь-якого непорожнього D

1) терми множини TK(Z) задають усі пропозиційні композиції класу CPR(Z,D),

2) система тотожностей (K1-K8) є повною і коректною системою тотожностей, тобто для будь-яких t,t 'TK(Z)

ACPR(Z,D) |= t=t' (K1-K8) |- t=t' .

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

Дається визначення класу E(Z, D) детермінантів сингулярних композицій і будується спеціальна детермінантна алгебра Кліні AE(Z, D) = <E(Z, D), _E, _E,_E>. Для опису базису цієї алгебри додатково вводяться параметричні характеристичні функції _E.

Теорема 2.6 Множина функцій {_E} {'(z,d)_E | (z,d) (Z D)} {_E| d D} є базисом інфінітарної детермінантної алгебри Кліні AE(Z, D).

Далі визначається спеціальна інфінітарна алгебра сингулярних (аплікативних) композицій Кліні AA(Z,D) = <A(Z,D), _C, _C, _C> як образ алгебри детермінантів. Крім того, визначається відповідна множина TCK(Z) термів цієї алгебри.

Вводяться додаткові тотожності, що задають властивості функцій із базису.

K9: ' = F, якщо d d'- нерівність даних.

K10: = {' | d' d, d'D} - позитивізація.

K11: { | dD} = T - покриття.

Теорема 2.8 Система тотожностей (K1-K11) є повна і коректна система тотожностей в алгебрі аплікативних композицій AA(Z,D), тобто для будь-яких t,t'TCK(ZD) AA(Z,D)|= t=t' (K1-K11) |- t=t' .

Далі досліджуються властивості таких композицій. Доводиться їх монотонність та формулюються необхідні і достатні умови коректності правила modus ponens в алгебрах Кліні. Для цього потрібно, щоб в аналізованому класі предикатів слабка рівність була відношенням еквівалентності (умова еквітранзитивності).

Теорема 2.9 Нехай AP(D,P) - довільна алгебра Кліні. Тоді для класу P умови еквітранзитивності і modus ponens еквівалентні.

Теорема 2.10 Нехай AP(D,P) - довільна алгебра Кліні. Тоді клас P є еквітранзитивним класом тоді і тільки тоді, коли на D може бути визначене відношення часткового порядку , для якого множина tot(P) тотальних елементів мажорує множину part(P) часткових елементів і всі предикати з P є еквітонними предикатами.

У четвертому підрозділі другого розділу розглядаються композиції номінативного рівня, який може трактуватися як синтез двох попередніх рівнів. Номінативний рівень характеризується тим, що дані розглядаються як однозначні номінативні (іменні) дані класу D = V A, тобто як однозначні часткові функції з множини предметних імен V у множину базових (предметних) значень A. При цьому множина імен V розглядається на гранично конкретному рівні, а множина A - на гранично абстрактному.

Проведена конкретизація дозволяє ввести нові параметричні композиції предикатів - реномінацію (перейменування) R_P ( VV) і квантори x_P, x_P (xV). Отриману алгебру APIFO (V, A, Q) = <Q, _P, _P, _P, R_P, x_P , x_P > природно назвати інфінітарною предикатною алгеброю першого порядку.

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

Теорема 2.14 Нехай - формула неокласичної логіки. Тоді |=_NC |- _NC .

Останній підрозділ присвячений дослідженню пропозиційних логік недетермінованих предикатів типу DBool. Такі логіки значно складніші, ніж логіки однозначних предикатів. Адже для недетермінованих предикатів не виконуються такі важливі закони, як дистрибутивність диз'юнкції і кон'юнкції та закони поглинання. Для опису класу детермінантів NE(Z) потрібно додатково ввести композицію ангельського вибору _K.

Теорема 2.16 Множина функцій {'z_K | zZ} є базисом пропозиційної алгебри недетермінованих бульових предикатів ANE(Z) = <NE(Z), _K, _K, _K, _K >.

Дається опис повного класу пропозиційних композицій і будується повна і коректна система тотожних перетворень (теорема 2.18).

Третій розділ "Абстрактна обчислюваність у композиційно-номінативних системах" вводить спеціальну обчислюваність функцій.

Поняття обчислюваності є одним із найважливіших у теоретичному програмуванні. Значні успіхи теорії алгоритмів мимоволі створюють враження, що питання про обчислюваність програм достатньо зрозуміле, принаймні, у принциповому плані, і не вимагає подальшого прояснення. Вважається, що практично всі мови програмування є універсальними мовами в тому сенсі, що вони можуть задавати всі обчислювані функції. Істотним обгрунтуванням такої позиції служить теза Чьорча, що зводить поняття обчислюваної функції до поняття частково рекурсивної функції (або функції, обчислюваної за Тьюрінгом). Водночас існує досить багато обставин, які засвідчують той факт, що питання обчислюваності програм не є очевидним і дійсно вимагає певного прояснення. По-перше, мови програмування визначають функції, задані не тільки на натуральних числах або словах, але і на інших типах даних, як на базових, наприклад, на дійсних числах, так і на структурних, наприклад, на масивах, файлах, списках, множинах, реляціях і т.п. Теорія обчислюваності на таких типах даних розроблена досить слабко. По-друге, програми під час своєї роботи часто використовують інші програми (процедури) для отримання потрібних результатів. Це фактично говорить про те, що обчислюваність програм відносна. По-третє, широке використання в програмуванні недетермінованих процесів вимагає теорії обчислюваності, яку можна застосувати і в цьому випадку. Така обчислюваність називається абстрактною. Орієнтація роботи на композиційно-номінативні моделі програм вимагає визначення абстрактної обчислюваності функцій над номінативними даними.

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

Визначення 3.1 Класом інваріантно обчислюваних функцій над множиною Nam({v₀,... ,v_n}, W) називається клас функцій, що задається мовою BACON({v₀,... , v_n}, W).

Визначення 3.2 Нехай D, B - довільні множини, V = {v₀,... ,v_n} - довільна скінченна множина, nom: DNam(V, B) - довільне всюди визначене багатозначне ін'єктивне відображення, яке називається відображенням номінативізації. Тоді множина D називається множиною номінативно скінченних даних відносно множини базових елементів B, множини імен V і відображення номінативізації nom (позначається D NFD(V, B, nom)).

Визначення 3.3 Нехай D NFD(V, B, nom) - довільна множина номінативно скінченних даних. Тоді функція f: DD називається номінативно обчислюваною (відносно V, B, nom), якщо є інваріантно обчислювана функція g:Nam(V, B) Nam(V, B) така, що f = nom g nom^-1.

Вводяться також варіанти номінативної обчислюваності над множиною ієрархічних послідовностей і множиною бінарних дерев.

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

Визначення 3.4 Нехай B - деяка множина. Тоді множиною натуральних даних над B називається множина Nat(B) = Nat B.

Визначення 3.5 Множина даних D називається множиною даних скінченної структури, якщо задана деяка множина B і усюди визначене багатозначне ін'єктивне відображення nat: DNat(B). Це відображення називається відображенням натуралізації, а часткове обернене відображення nat^-1 : Nat(B)D, що позначається denat, - відображенням денатуралізації.

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

Визначення 3.7 Функція f: DD називається натурально обчислюваною (відносно заданих відображень nat і denat), якщо існує кодово обчислювана функція g: Nat(B) Nat(B) така, що f = nat g denat.

Варто зауважити, що при B = кодова обчислюваність та інваріантна обчислюваність перетворюються в частково рекурсивну обчислюваність над Nat, а натуральна обчислюваність - у нумераційну обчислюваність (відносно відображень nat і denat). Тому введені поняття натуральної і номінативної обчислюваності є достатньо багатими.

Твердження 3.2 Всі функції, що представляються в мові BACON(V,W) із зліченною множиною імен V, натурально обчислювані.

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

Теорема 3.3 Повний клас однозначних натурально обчислюваних функцій над множиною V-скінченних W-абстрактних іменних даних збігається з класом функцій, отриманим замиканням множини функцій {v₀,... , v_m,v₀,... , v_m, v₀! ,... , v_m! } відносно множини композицій {, , }.

Для опису повного класу обчислюваних функцій над іменними даними із зліченною множиною імен V = {v₀, v₁,... } вводяться функції, які забезпечують роботу з іменами, що обчислюються. Це функції, які перераховують елементи множини V, а також бінарні функції іменування as, розіменування cn, видалення ex і предикат наявності компоненти ec такі, що для vV, dD маємо as(v,d) = v(d), cn(v,d) = v(d), ex(v,d) = \v(d), ec(v,d) = v! (d).

Теорема 3.4 Повний клас однозначних натурально обчислюваних функцій над множиною V-зліченних W-абстрактних іменних даних збігається з класом функцій, отриманим замиканням множини функцій {v₀, v₁, V, W, , =v₀, succ_V, pred_V, as, cn, ex, ec} відносно множини композицій {, , }.

Якщо множина W = {w₀, w₁,... } теж є зліченною, то для представлення повного класу необхідно додатково використовувати функції, що перелічують множину W:, =w₀, succ_W, pred_W.

Теорема 3.5 Повний клас однозначних натурально обчислюваних функцій над множиною (V,W)-зліченних іменних даних збігається з класом функцій, отриманим замиканням множини функцій {v₀, v₁, V, W, ,=v₀, succ_V, pred_V, , =w₀, succ_W, pred_W, as, cn, ex, ec} відносно множини композицій {, , }.

Для опису повних класів обчислюваних багатозначних функцій додатково вводиться функція вибору .

Теорема 3.6 Повні класи багатозначних натурально обчислюваних функцій над множинами іменних даних, перерахованих в теоремах 3.3 - 3.5, збігаються з класами функцій, отриманими замиканням відповідних множин функцій, поповнених функцією вибору , відносно відповідних множин композицій.

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

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

У наступних підрозділах досліджується питання про обчислюваність аплікативних композицій. Незважаючи на те, що такі композиції утворюють власний підклас класу всіх композицій, цей підклас занадто багатий для практичного використання в програмуванні. Тому необхідна подальша його конкретизація, яка утворюється введенням різноманітних властивостей фінітності, що дозволяє перейти до визначення обчислюваних композицій. Спроба застосування традиційних визначень обчислюваного оператора (композиції) наштовхується на труднощі. Суть їх полягає в тому, що багато підходів постулюють виконуваність таких вимог, які, по-перше, далеко не очевидні і самі вимагають обгрунтування, як, наприклад, вимога про наявність універсальної обчислюваної функції (підходи Стронга, Фрідмана, Московакіса), а по-друге, вони не можуть бути застосовані до певних структур даних, як, наприклад, вимога про наявність нумерації даних (нумераційний підхід Мальцева) або вимога гьоделізації (підхід Вагнера). Крім того, необхідно ввести обчислюваність, задану в термінах іменних даних, функцій і композицій, що спрямована на вирішення програмістських задач.