Если у вас возникли сложности с курсовой, контрольной, дипломной, рефератом, отчетом по практике, научно-исследовательской и любой другой работой - мы готовы помочь.
Предоплата всего
Подписываем
31
\NikitchenkoÌàíüêî
Київський національний університет
імені Тараса Шевченка
НІКІТЧЕНКО Микола Степанович
УДК 681.3.06
ТЕОРІЯ ІНТЕГРОВАНИХ КОМПОЗИЦІЙНО-НОМІНАТИВНИХ
МОДЕЛЕЙ ПРОГРАМ
.05.03 – математичне та програмне забезпеченняобчислювальних машин і систем
Автореферат
дисертації на здобуття наукового ступеня
доктора фізико-математичних наук
Дисертац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 Київського національного
університету імені Тараса Шевченка за адресою:
, Київ, вул. Володимирська, 58.
Автореферат розiсланий " 7 " серпня 2001 р.
Вчений секретар спецiалiзованої вченої ради В.П.Шевченко
Актуальність теми. Необхідність постійного розширення сфери застосування інформаційних технологій наштовхується на значні труднощі в розробці потрібного математичного та програмного забезпечення. Відставання в створенні програмних систем стає особливо помітним у порівнянні з бурхливим розвитком елементної бази обчислювальних машин. Ненадійність програмних систем, відсутність чітких критеріїв ефективності програмного забезпечення, труднощі його супроводу змушують деяких фахівців стверджувати про наявність кризи в комп'ютерних науках. Причини такого стану справ різноманітні і торкаються як економічних, соціальних, психологічних, так і науково-технічних аспектів створення та використання інформаційних технологій. Серед наукових проблем особливе місце займає проблема моделювання програмних систем і пов'язана з нею проблема моделювання предметних областей. На теперішній момент отримано цілий ряд значних результатів з вказаних проблем. Проте, незважаючи на безсумнівні досягнення в цій області, слід визнати, що адекватна й ефективна теорія моделювання програмних систем і предметних областей ще не розроблена. Наявні моделі є різнорідними, описують лише окремі аспекти, не забезпечують єдиного розуміння досліджуваних проблем.
Справді, розроблені моделі програмних систем (програм) традиційно розділяють на три відносно незалежні групи: денотаційні, операційні та аксіоматичні моделі. Для кожної групи увага акцентується переважно на одному аспекті програм. Зокрема, денотаційні моделі орієнтовані перш за все на такий засіб побудови програм, як оператор найменшої нерухомої точки (рекурсія); операційні моделі –на пристрої, що забезпечують обчислення програм; аксіоматичні моделі –на логічні формалізми специфікації програм. Така різнорідність типів моделей утруднює розробку багатоаспектних (інтегрованих) технологій конструювання програм. Безумовно, ця обставина усвідомлюється багатьма фахівцями, які намагаються об'єднати різноманітні теорії програмування і моделі програм. Проте роботи в цьому напрямку фактично обмежуються демонстрацією взаємної трансляції моделей при деяких умовах. Осторонь залишаються найважливіші питання методологічного обгрунтування моделей, повноти, взаємозалежності і розвитку. Більше того, можна стверджувати, що навіть дуже детально розроблені моделі вказаних класів вельми неадекватно відображають специфіку програмування. Для такої неадекватності є об'єктивні обставини. Справа в тому, що всі вказані типи моделей спираються на традиційні математичні формалізми –теорію алгоритмів, математичну логіку й універсальну алгебру. Проте ці формалізми були в основному сформовані до 40-х років 20-го сторіччя, тобто раніше, ніж програмування набуло значного поширення. Тому немає нічого надзвичайного в тому, що ці формалізми та побудовані на їхній основі моделі програм не враховують істотних особливостей програмування. Серед цих особливостей зазначимо такі.
. Традиційні формалізми і моделі переважно орієнтовані на екстенсійні аспекти програм, у той час як у програмуванні усе більшу роль відіграють інтенсійні аспекти.
. Поняття розглядаються у статиці, у той час як постійне збагачення методів програмування вимагає розгляду програмних понять у їх розвитку.
. Традиційні формалізми використовують дуже обмежені засоби конструювання об'єктів, але такі засоби в програмуванні вельми різноманітні, до того ж вони знаходяться на різних рівнях абстракції, що утруднює їх дослідження.
. Традиційні формальні моделі програм грунтуються на понятті множини, хоча для програмування більш суттєвим є поняття функції.
. Традиційні формалізми орієнтовані на клас n-арних однозначних (часто всюди визначених) відображень, у той час як в програмуванні використовується і більш широкий клас номінативних часткових недетермінованих відображень. Крім того, традиційні формалізми звичайно базуються на фінітарних побудовах, у той час як в мовах специфікацій програм дедалі частіше застосовуються інфінітарні побудови, причому як для структур даних, так і для самих специфікацій.
Таке становище робить актуальною проблему розробки інтегрованих моделей програм, що адекватно враховують їх головні аспекти й забезпечують їх ефективну реалізацію. Вказана проблема є дуже складна і вимагає поетапного підходу для її вирішення. Значні результати з моделювання програмних систем і предметних областей були отримані в роботах В.М. Глушкова і його колег Ю.В. Капітонової, О.А. Летичевського, П.І. Андона, І.В. Сергієнка, А.О. Стогнія, Г.О. Цейтліна, К.Л. Ющенко й ін. Суттєвий крок у створенні розвинутих моделей програм був зроблений у роботах з композиційного програмування В.Н. Редька.
Сучасний етап розвитку програмування висуває нові вимоги до моделей програм. Головними з цих вимог є такі:
–необхідно розробити методологічно обгрунтовані методи моделювання програм і сформувати на цій основі систему понять програмування;
–моделі програм повинні задавати різноманітні їх аспекти, що можна здійснити тільки шляхом побудови ієрархії моделей програм різних рівнів абстракції і загальності, що дозволяють як адекватну специфікацію програм, так і ефективну їх реалізацію;
–теорія моделей програм повинна бути інтегрована з дисциплінами, що її підтримують, такими, як теорія алгоритмів, математична логіка та універсальна алгебра.
Серед різноманітних методологічних підходів до побудови моделей програм, що задовольняють названим вимогам, у дисертаційній роботі розробляється підхід, заснований на принципі розвитку як сходженні від абстрактного до конкретного, принципі композиційності, який акцентує увагу на засобах конструювання програм, та принципі номінативності, який розкриває важливість конкретизацій відношень іменування в процесі конструювання програм. Вказані принципи дозволяють говорити про композиційно-номінативний підхід до побудови моделей програм.
Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконувалася в рамках комплексної наукової програми Київського національного університету імені Тараса Шевченка "Перспективні інформаційні технології, прилади комплексної автоматизації, системи зв'язку" (теми "Дослідження універсальних та спеціалізованих програмних логік", 1996–, номер держреєстрації 197U003444, і "Логіко-математичні та програмологічні засоби інформаційних технологій", 2001–, номер держреєстрації –U002163), а також у рамках госпдоговірної теми "Розробка об'єктно-орієнтованих моделей баз даних", 1993–, номер держреєстрації 0195U008132.
Мета і задачі дослідження. Метою дисертаційної роботи є розробка композиційно-номінативного підходу до побудови багатоаспектних математичних моделей програмних систем, створення на цій основі ієрархії моделей програм різних рівнів абстракції та загальності, дослідження таких моделей та їх застосування в математичній логіці, теорії алгоритмів і моделюванні предметних областей.
Враховуючи основні вимоги до моделей програм і відповідно до сформульованої мети в дисертації ставляться і вирішуються такі задачі:
–розробка нових методологій моделювання програм;
–розробка і дослідження поняття композиційно-номінативної системи, що дозволяє побудувати ієрархії моделей програм різних рівнів абстракції та загальності;
–виділення підкласів композиційно-номінативних систем, які формалізують семантичні аспекти логік різноманітних типів;
–виділення підкласів композиційно-номінативних систем, які описують повні класи обчислюваних функцій і композицій над різноманітними структурами даних;
–застосування розроблених методів і моделей для формалізації предметних областей.
Проведені в дисертаційній роботі дослідження грунтуються на сукупності загальнометодологічних та математичних методів.
Головним методологічним методом є метод сходження від абстрактного до конкретного. Головні математичні методи включають методи формальної логіки, теорії алгоритмів та універсальної алгебри.
Наукова новизна одержаних результатів, що виносяться на захист, полягає в наступному.
–Запропоновано новий композиційно-номінативний підхід до побудови інтегрованих семантико-синтаксичних моделей програм, методологічною основою якого є метод сходження від абстрактного до конкретного.
–Розроблено і досліджено теоретико-функціональний формалізм композиційно-номінативних систем, що адекватно описують моделі програм різних рівнів абстракції і загальності.
–Визначено і досліджено предикатні композиційно-номінативні системи, призначені для специфікації логік предикатів. На їхній основі розроблені нові логічні системи абстрактного, сингулярного і номінативного рівнів, що узагальнюють традиційні пропозиційні логіки і логіки предикатів на класи часткових і недетермінованих предикатів. Для побудованих аксіоматичних систем вирішені класичні проблеми коректності і повноти.
–Розроблено і досліджено нові підходи до визначення абстрактної обчислюваності програм (номінативна і натуральна обчислюваність), які узагальнюють традиційні визначення обчислюваності функцій.
–Описані повні класи обчислюваних функцій і композицій над номінативними даними різних рівнів абстракції і загальності та побудовані алгебраїчні представлення таких класів.
–Визначені і досліджені спеціальні класи узгоджуючих композицій програм, що спрощують їх конструювання.
–Побудована і досліджена аксіоматична система специфікацій програм, що дозволяє специфікувати усі абстрактно обчислювані функції над номінативними даними.
–Побудовано композиційно-номінативні моделі програм, які застосовано для опису мов програмування та мов баз даних, а також для моделювання транспортних систем.
Таким чином, у дисертаційній роботі вперше висунута і розроблена теорія композиційно-номінативних моделей програм, що дає можливість інтегрального опису головних аспектів програм і служить теоретичною основою для розробки програмних систем різноманітного призначення.
Практичне значення одержаних результатів. Теорія композиційно-номінативних моделей програм, яка побудована в дисертаційній роботі, забезпечує можливість її практичного застосування для розробки надійних і ефективних програмних систем. Ця теорія дозволяє підтримувати головні етапи життєвого циклу програмних систем, починаючи з їх декларативних специфікацій і аж до ефективних процедурних програм.
Отримані результати з формалізації мов програмування і мов запитів баз даних були реалізовані в інтерактивній інформаційній системі Комбад, розробленій в Київському університеті.
Методологічні та теоретичні результати дисертаційної роботи були застосовані в нормативних курсах з програмування та теоретичних основ програмування, а також в спеціальних курсах з семантичного конструювання програм та композиційних логік, які читаються студентам факультету кібернетики Київського національного університету імені Тараса Шевченка.
Результати проведених досліджень були також використані в проектах, підтриманих грантами Міжнародного інституту інформаційних технологій Університету Об'єднаних Націй –UNU/IIST (1996), INTAS-94-1817 (1995–), Датської Дослідницької Академії DRA N1997-125-0031 (1997–).
Особистий внесок здобувача. Всі результати, які складають суть дисертаційної роботи, одержані здобувачем самостійно. З робіт, виконаних із співавторами, на захист виносяться лише результати, одержані особисто здобувачем.
Апробація роботи. Основні результати роботи пройшли апробацію в провідних наукових колективах України, Росії, Данії, Німеччини, Голландії. Вони доповідались на засіданнях семінарів "Теорія мов і процесорів", "Теорія автоматів та її застосування", "Програмологія та її застосування" (Київ, 1982–), Всесоюзних конференціях "Проблеми теоретичної кібернетики" (Іркутськ, 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–], надрукованих у виданнях, які затверджені ВАК України. Серед цих робіт 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).
КНС, як видно з наведеного визначення, є спеціальними мовними системами, призначеними для опису різноманітних класів функцій. Їх можна також називати композиційно-номінативними мовами функцій. Такі системи тісно пов'язані з алгебрами функцій і даних. Ці системи побудовані в семантико-синтаксичному стилі і спираються на парадигми композиційності, номінативності і розвитку. Відмінності від традиційних систем (моделей програм) полягають у наступному:
) формалізація ведеться на основі теоретико-функціонального підходу,
) замість традиційних класів однозначних n-арних функцій розглядаються часткові багатозначні номінативні відображення,
) структури даних є похідними номінативних структур.
Переваги такого підходу:
) побудовані моделі програм є математично простими, але більш адекватними для опису семантики програм,
) є можливість широкого використання методів універсальної алгебри, математичної логіки і теорії алгоритмів для дослідження програм,
) введені моделі програм є параметричними і дозволяють природним чином задавати програми різних рівнів абстракції і загальності.
Наступний підрозділ першого розділу присвячений класифікації і властивостям композиційно-номінативних систем.
КНС класифікуються відповідно до рівнів розгляду їх параметрів, насамперед даних, функцій і композицій.
Дані розглядаються на трьох рівнях: абстрактному, бульовому і номінативному.
На номінативному рівні дані трактуються як номінативні дані. Клас 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} і множина функцій розіменування {'zK |z Z} є базисом інфінітарної Z-пропозиційної алгебри Кліні AK(Z).
Таким чином, операції алгебри Кліні разом з функціями базису утворюють повний для класу K(Z) набір композицій, подібно до того, як вони (у їх скінченноарному варіанті) є функціонально повним набором для класу тотальних бульових функцій.
На основі алгебри AK(Z) будується алгебра пропозиційних композицій ACPR(Z,D). З теореми про базис випливає, що відповідна множина TK(Z) термів алгебри Кліні задає усі детермінанти. Далі доводиться, що ці терми також задають усі пропозиційні композиції. Для таких термів можна визначити спеціальну позитивно-негативну нормальну форму. Для побудови повної системи тотожних перетворень вводиться спеціальний варіант інфінітарного екваційного числення з відношенням вивідності |–.
Система тотожностей задається такими схемами аксіом.
K1: { { Xij | j Ji } | iI} = { Xij | jJi, iI} –асоціативність.
K2: {X} = X –ідемпотентність.
K3: { {Xij | jJi } | iI} = { {Xi( i) | iI } | iI Ji }
–цілком дистрибутивність.
K4: {X, {X, X'}} = X –поглинання.
K5: X = X –інволюція.
K6: {Xi | i I } = { Xi | iI } –закон де Моргана.
K7: = –нерухома точка.
K8: { {X, X}, {X', X'}} = {X, X} –нормальність.
Центральним твердженням підрозділу є така теорема.
Теорема 2.4 Для будь-якого непорожнього D
1) терми множини TK(Z) задають усі пропозиційні композиції класу CPR(Z,D),
) система тотожностей (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 –на гранично абстрактному.
Проведена конкретизація дозволяє ввести нові параметричні композиції предикатів –реномінацію (перейменування) RP ( VV) і квантори xP, xP (xV). Отриману алгебру APIFO (V, A, Q) = <Q, P, P, P, RP, xP , xP > природно назвати інфінітарною предикатною алгеброю першого порядку.
Предикатні алгебри першого порядку утворюють семантичну основу логік першого порядку. Однієї з таких логік є фінітарна логіка часткових еквітонних повнототальних предикатів. Цю логіку природно назвати неокласичною логікою, оскільки вона зберігає основні властивості класичної логіки предикатів (теорема 2.11), але істотно розширює клас моделей. Для неокласичної логіки будується аксіоматична система гільбертового типу, для якої має місце теорема коректності і повноти.
Теорема 2.14 Нехай –формула неокласичної логіки. Тоді |=NC |–NC .
Останній підрозділ присвячений дослідженню пропозиційних логік недетермінованих предикатів типу DBool. Такі логіки значно складніші, ніж логіки однозначних предикатів. Адже для недетермінованих предикатів не виконуються такі важливі закони, як дистрибутивність диз'юнкції і кон'юнкції та закони поглинання. Для опису класу детермінантів NE(Z) потрібно додатково ввести композицію ангельського вибору K.
Теорема 2.16 Множина функцій {'zK | zZ} є базисом пропозиційної алгебри недетермінованих бульових предикатів ANE(Z) = <NE(Z), K, K, K, K >.
Дається опис повного класу пропозиційних композицій і будується повна і коректна система тотожних перетворень (теорема 2.18).
Третій розділ "Абстрактна обчислюваність у композиційно-номінативних системах" вводить спеціальну обчислюваність функцій.
Поняття обчислюваності є одним із найважливіших у теоретичному програмуванні. Значні успіхи теорії алгоритмів мимоволі створюють враження, що питання про обчислюваність програм достатньо зрозуміле, принаймні, у принциповому плані, і не вимагає подальшого прояснення. Вважається, що практично всі мови програмування є універсальними мовами в тому сенсі, що вони можуть задавати всі обчислювані функції. Істотним обгрунтуванням такої позиції служить теза Чьорча, що зводить поняття обчислюваної функції до поняття частково рекурсивної функції (або функції, обчислюваної за Тьюрінгом). Водночас існує досить багато обставин, які засвідчують той факт, що питання обчислюваності програм не є очевидним і дійсно вимагає певного прояснення. По-перше, мови програмування визначають функції, задані не тільки на натуральних числах або словах, але і на інших типах даних, як на базових, наприклад, на дійсних числах, так і на структурних, наприклад, на масивах, файлах, списках, множинах, реляціях і т.п. Теорія обчислюваності на таких типах даних розроблена досить слабко. По-друге, програми під час своєї роботи часто використовують інші програми (процедури) для отримання потрібних результатів. Це фактично говорить про те, що обчислюваність програм відносна. По-третє, широке використання в програмуванні недетермінованих процесів вимагає теорії обчислюваності, яку можна застосувати і в цьому випадку. Така обчислюваність називається абстрактною. Орієнтація роботи на композиційно-номінативні моделі програм вимагає визначення абстрактної обчислюваності функцій над номінативними даними.
Перший підрозділ вводить поняття номінативної обчислюваності функцій. Спочатку визначається обчислюваність, інваріантна відносно базових елементів.
Визначення 3.1 Класом інваріантно обчислюваних функцій над множиною Nam({v,... ,vn}, W) називається клас функцій, що задається мовою BACON({v,... , vn}, W).
Визначення 3.2 Нехай D, B –довільні множини, V = {v,... ,vn} –довільна скінченна множина, 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,... , vm,v,... , vm, v! ,... , vm! } відносно множини композицій {, , }.
Для опису повного класу обчислюваних функцій над іменними даними із зліченною множиною імен 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, succV, predV, as, cn, ex, ec} відносно множини композицій {, , }.
Якщо множина W = {w, w,... } теж є зліченною, то для представлення повного класу необхідно додатково використовувати функції, що перелічують множину W:, =w, succW, predW.
Теорема 3.5 Повний клас однозначних натурально обчислюваних функцій над множиною (V,W)-зліченних іменних даних збігається з класом функцій, отриманим замиканням множини функцій {v, v, V, W, ,=v, succV, predV, , =w, succW, predW, as, cn, ex, ec} відносно множини композицій {, , }.
Для опису повних класів обчислюваних багатозначних функцій додатково вводиться функція вибору .
Теорема 3.6 Повні класи багатозначних натурально обчислюваних функцій над множинами іменних даних, перерахованих в теоремах 3.3 –.5, збігаються з класами функцій, отриманими замиканням відповідних множин функцій, поповнених функцією вибору , відносно відповідних множин композицій.
Таким чином, використання введених понять номінативної і натуральної обчислюваності дозволяє дати прості описи повних класів обчислюваних функцій у класах однозначних і багатозначних функцій над різними видами іменних даних. Ці описи можуть бути використані для доведення повноти різноманітних мов програмування і баз даних.
При переході від обчислюваності функцій над іменними даними до обчислюваності над номінативними даними необхідно понизити рівень абстракції множини W введенням предикату рівності. Такий рівень називається W-екваційним номінативним рівнем. Для цього випадку також доводиться теорема 3.7 про опис повного класу обчислюваних функцій.
У наступних підрозділах досліджується питання про обчислюваність аплікативних композицій. Незважаючи на те, що такі композиції утворюють власний підклас класу всіх композицій, цей підклас занадто багатий для практичного використання в програмуванні. Тому необхідна подальша його конкретизація, яка утворюється введенням різноманітних властивостей фінітності, що дозволяє перейти до визначення обчислюваних композицій. Спроба застосування традиційних визначень обчислюваного оператора (композиції) наштовхується на труднощі. Суть їх полягає в тому, що багато підходів постулюють виконуваність таких вимог, які, по-перше, далеко не очевидні і самі вимагають обгрунтування, як, наприклад, вимога про наявність універсальної обчислюваної функції (підходи Стронга, Фрідмана, Московакіса), а по-друге, вони не можуть бути застосовані до певних структур даних, як, наприклад, вимога про наявність нумерації даних (нумераційний підхід Мальцева) або вимога гьоделізації (підхід Вагнера). Крім того, необхідно ввести обчислюваність, задану в термінах іменних даних, функцій і композицій, що спрямована на вирішення програмістських задач.
Запропоновані уточнення вводяться на основі операційного підходу, тобто передбачається, що програма обчислювана, якщо є пристрій (дискретна система) спеціального вигляду, що обчислює її значення на вхідних даних. Функціонування цього пристрою задається спеціальним відображенням, що називається детермінантом. У цьому випадку обчислюваність аплікативних композицій зводиться до обчислюваності детермінантів. Це дозволяє використовувати результати про номінативну і натуральну обчислюваність функцій для представлення обчислюваних композицій.
Теорема 3.8 Будь-який детермінантно обчислюваний оператор (композиція) може бути представлений у мові BACON, що поповнена функціями натуралізації і денатуралізації.
Звідси випливає, що описи повних класів композицій утворюються безпосередньо з теореми 3.8 і теорем 3.3 –.6. Наприклад, для екваційних номінативних даних має місце такий результат ( –композиція з'єднання).
Теорема 3.10 Повний клас детермінантно обчислюваних композицій над класом V-скінченних W-екваційних номінативних даних збігається з класом композицій, отриманих замиканням множини композицій {v,... , vm, v,... , vm, v! ,... , vm! , , =W, , , } відносно суперпозиції.
Таким чином, введені поняття детермінантної та натуральної обчислюваності дозволяють дати прості описи класів обчислюваних композицій і функцій над різними типами номінативних даних.
У четвертому розділі розглядаються композиційно-номінативні системи, орієнтовані на конструювання і специфікацію програм.
У композиційно-номінативному підході (КНП) до програмування відношенням іменування та їхньому використанню в побудові даних, функцій і композицій приділяється значна увага. Можна стверджувати, що ці відношення займають центральне місце в КНП. Щоб додатково підкреслити важливість відношень іменування в програмуванні, бажано порівняти КНП з іншими підходами, у котрих іменуванню приділяється другорядна роль. Таким підходом є функціональне програмування (ФП) Дж. Бекуса, у якому відсутність явного іменування розглядається як перевага підходу. Порівнювані підходи дуже близькі на рівні принципів функціональності і композиційності. Основна відмінність –використання у ФП послідовностей як основної структури даних, тоді як у КНП використовують номінативні структури даних.
Розглядаються приклади, що демонструють труднощі модифікації програм у функціональному програмуванні Дж. Бекуса. Причини труднощів викликані тим, що структури даних типу послідовності знаходяться на більш низькому рівні абстракції, ніж структури номінативних даних, і це відбивається як на функціях, що працюють із такими даними, так і на композиціях над такими функціями. У ФП робота з компонентами даних ведеться через позицію компоненти в об'єкті, і оскільки при зміні об'єкта часто змінюється і позиція компоненти, то ці зміни потрібно враховувати явно, постійно стежити за ними. Що ж стосується зміни значень компонент, то для цього потрібно писати цілу програму, що особливо важко при частій зміні структури об'єкту. Імена ж компонент, як правило, не змінюються при зміні даного. "Позиція" за рівнем абстракції розташована нижче, ніж "ім'я", тому що співвідноситься з іншими позиціями сильніше, ніж співвідноситься ім'я з іншими іменами. Таким чином, необхідність у ФП постійних узгоджень вхідних і вихідних об'єктів, складність зміни компонент даних і неадекватність засобів конструювання утруднюють побудову програм.
Оскільки "ручне" узгодження даних істотно утруднює програмування, то доцільно ввести спеціальні композиції, які здійснюють таке узгодження автоматично (підрозділ 4.2). Щоб це було можливо, виділяється спеціальний клас програм, названих запитуючими програмами. Для цих програм результат обчислюється на основі тільки тих значень даних, що були запитані самою програмою. Клас таких програм дуже широкий. Властивість запитувати є фактично властивість слабкої аплікативності. Такі програми уточнюються як еквітонні функції.
Однією із найважливіших властивостей запитуючих програм є те, що для обчислення їхніх результатів достатньо знати тільки запитувану частину вхідних даних, у той час як інша частина залишається надлишковою. Тому з запитуючими програмами поряд із класом еквітонних функцій доцільно зв'язувати інший клас функцій, у яких відзначена надмірність вхідних даних відсутня або, принаймні, зменшена. Зрозуміло, що такі функції, що називаються екстрактами, є спеціальними звуженнями еквітонних функцій. Екстракти уточнюються як еквісумісні функції (значення яких на сумісних елементах рівні).
Поняття екстракту є корисним для вирішення низки задач програмування. Наприклад, можливість визначення за допомогою екстракту необхідних даних дозволяє підвищити ефективність обробки даних за рахунок попереднього перенесення їх на більш швидкі запам'ятовуючі пристрої, якщо, скажімо, дані знаходяться в розподілених базах даних і для їх пошуку потрібно багато часу.
Будуються класи композицій, задані на екстрактах еквітонних функцій. Ці композиції здійснюють автоматичне узгодження даних. Будується алгебра таких композицій і доводиться теорема 4.1 про гомоморфізм алгебри з традиційними композиціями в алгебру з узгоджуючими композиціями. Значення теореми полягає в тому, що вона дозволяє проводити семантичне конструювання програм в алгебрі узгоджуючих композицій (які спрощують програмування, але ускладнюють обчислення програм), а обчислення проводити в більш простій алгебрі традиційних композицій.
Поняття запитуючої програми можна підсилити до поняття сильнозапитуючої програми (підрозділ 4.3), яка може не тільки запитувати значення даних, але і визначати їхню наявність. Отримані при цьому класи функцій вже не будуть монотонними (еквітонними). Проте вдається перенести всі основні результати про запитуючі програми на клас сильнозапитуючих програм (теореми 4.2 –.3).
Таким чином, застосовуючи узгоджуючі композиції можна виграти у простоті конструювання програм вказаних класів, практично не програючи в складності їх обчислення.
Останній підрозділ присвячений аксіоматичним методам специфікації програм. Для побудови більш багатих класів програм над номінативними даними необхідно припустити, щоб деякі імена могли іменувати інші імена (бути метаіменами). Це фактично означає, що імена можуть виступати як значення, тобто VW . Забезпечити наявність метаімен можна різними способами. При трактуванні імен як структурованих об'єктів (як номінативних даних) утворюється клас метаномінативних даних (МНД), який можна задати рівнянням
MND = W (MNDMND).
Для опису повного класу обчислюваних функцій використовується натуральна обчислюваність.
Теорема 4.5 Повний клас натурально обчислюваних функцій над класом MND метаномінативних даних збігається з класом функцій, отриманим замиканням множини функцій { 0 , 1 , , W , , \, =W , as , cn , } відносно множини композицій {, , } .
Теорема мотивує визначення такої КНС, що називається імперативною КНС. Для цієї КНС композиційна система Cm(Z) = <D, F, C> конкретизується таким чином, що D = MND –множина метаномінативних даних над W, F = DD –множина часткових багатозначних функцій над MND, Z = Nat, C = {, , }. Параметри дескриптивної та денотаційної систем задаються очевидним чином.
Поряд з імперативними способами завдання програм (функцій) часто використовуються декларативні методи завдання (специфікації) програм. Є різні підходи до цієї проблеми. У роботі приймається традиційна точка зору, за якою специфікація програм (функцій) провадиться за допомогою предикатів. А саме, нехай p: DBool –бінарний предикат, а f DD –часткова багатозначна функція. Тоді предикат p реляційно представляє функцію f, якщо її графік збігається з областю істинності предикату.
Для визначення предикатів використовуються спеціальні –предикатні –КНС (ПКНС), визначені в другому розділі. Розглядаються системи, які базуються на фінітарних предикатних алгебрах першого порядку виду APFO(V, A, VA) = <VA, P, P, P, RP, xP, xP>. Множина A конкретизується як клас метаномінативних даних, а за базові предикати вибираються предикати номінативної належності (n) , рівності на класі метаномінативних даних (=) і належності множині базових елементів (W). Вказана конкретизація визначає нову ПКНС, що називається системою специфікації номінативних даних. Ця система досліджується як у семантичному, так і в синтаксичному (аксіоматичному) аспекті. З цією метою будується спеціальна аксіоматична теорія метаномінативних даних (ТМНД) із рівністю і тернарною зв'язкою (предикатом) номінативної належності.
Природно, що при побудові аксіоматичної теорії зв'язки номінативної належності можна спиратися на різні аксіоматики теорії множин. Аксіоматика ТМНД будується в дусі теорії допустимих множин, що має певні переваги: з одного боку, ця теорія достатньо потужна, щоб породжувати обчислювані функції над різними структурами даних, з іншого ж боку, вона не настільки обмежувальна, як різні варіанти конструктивних логік.
ТМНД будується як односортна теорія з унарним предикатом U, істинним на елементах базової множини W. Аксіоми ТМНД діляться на декілька груп. Аксіоми екстенсійності, фундування (індукції за зв'язкою належності –вертикальної індукції) і індукції за зв'язкою включення (горизонтальної індукції) стосуються фундаментальних властивостей МНД. Аксіоми виділення, іменування та об'єднання пов'язані з допустимими принципами конструювання МНД. Інші аксіоми задають нетривіальність класу МНД і властивості базових елементів.
Спеціальні аксіоми ТМНД є універсальними замиканнями наступних формул, де –довільна формула, а –довільна -формула, що не має вільних входжень b.
–Екстенсійність: x y (x yn a x yn b) a = b.
–Фундованість (індукція за належністю):
(a (x yn a ( x) ( y) (a))) a (a) .
–Індукція за включенням: (a (b a (b) (a))) a (a).
–-виділення: b x y (x yn b x yn a (a)) .
–Іменування: c x yn c.
–Об'єднання: c (a c b c ).
–Нетривіальність: a x y (x yn a) .
–Базові елементи: (x ynu) .
Теорема 4.6 Теорія метаномінативних даних несуперечлива.
Обчислювані предикати можуть бути задані -формулами (з одним необмеженим квантором існування).
Теорема 4.7 Клас натурально обчислюваних функцій над множиною метаномінативних даних реляційно представляється -предикатами ТМНД.
Доведена теорема свідчить про велику виразну силу побудованої аксіоматичної системи метаномінативних даних. Водночас, можливість представлення натурально обчислюваних функцій, і зокрема, всіх частково рекурсивних функцій, свідчить про те, що для ТМНД виконуються умови теореми Гьоделя про неповноту.
Теорема 4.8 Теорія метаномінативних даних неповна.
Розділ 5 "Застосування композиційно-номінативних систем для моделювання транспортних областей" демонструє можливість застосування розробленої теорії композиційно-номінативних систем для такої предметної області, як транспорт. Ця область, що є однією з найважливіших для економіки будь-якої країни, піддається моделюванню і вивченню на протязі багатьох років. Водночас необхідність створення ефективних і надійних програмних систем висуває нові вимоги до транспортних моделей (ТМ), їх опису і дослідження. В даний час, відповідно до методів строгої (формальної) розробки програмних систем, акцент переноситься з проблем алгоритмічного опису предметних областей на їх специфікацію. У зв'язку з цим переглядаються вимоги і до транспортних моделей. Тепер необхідно побудувати на єдиній методологічній основі ієрархію моделей різних рівнів абстракції і розробити методи коректного переходу від абстрактних моделей до більш конкретних. Ця задача у свою чергу вимагає розробки спеціальних мов (логік) опису транспортних моделей та їх дослідження.
У розділі виділяються основні транспортні абстракції і будуються різноманітні транспортні моделі шляхом конкретизації виділених абстракцій. Запропоновані моделі орієнтовані на композиційно-номінативні системи, що дозволяє застосовувати розроблені в КНП методи для дослідження транспортних моделей і створення відповідних програмних систем.
Для виділення абстракцій необхідно проаналізувати предметну область. З визначення транспорту як "перевезення людей і вантажів з одного місця на інше" випливає, що основні транспортні абстракції –це "місця", "люди і вантажі" та "перевезення". Найбільш важливим із них є поняття "перевезення", яке краще розглядати більш абстрактно як "рух". Стосовно транспортної області можна говорити про рух (зміну) транспортної області в цілому (найбільш абстрактний рух) і про рух транспортних засобів усередині області (більш конкретний рух). Математичне уточнення цих понять дає абстрактні моделі транспортних областей.
Спочатку вводиться найбільш абстрактна модель, що дозволяє описати зміну предметної області як єдиного цілого. У цьому випадку множина станів предметної області задається деякою множиною St, а зміна станів –відношенням переходів tr St St. Природно вважати, що відношення tr є частковий порядок. Множина станів, лінійно впорядкована стосовно tr, називається еволюцією. Еволюція задає послідовність змін одного стану.
Визначення 5.1 Еволюційною системою (моделлю) називається трійка <St, tr, Ev >, де
St –деяка абстрактна множина станів,
tr –відношення переходів (частковий порядок на St),
Ev –деяка підмножина всіх лінійно упорядкованих підмножин St (множина еволюцій).
Еволюційна система є занадто абстрактною моделлю щоб відобразити специфіку транспортної області. Для побудови моделей транспортної області необхідно здійснити конкретизацію еволюційної системи поняттями, що відображають істотні особливості цієї області.
З цією метою вводиться абстракція транспортного об'єкту. Нехай Rs –абстрактна множина. Елементи цієї множини, які називаються транспортними об'єктами, представляють місця, пасажирів, вантажі, шляхи і т.д. Основне відношення для транспортних моделей є тернарне відношення зв'язування tk, задане на Rs Rs St. Якщо об'єкт rs зв'язаний з об'єктом rs' у стані st, тобто tk(rs, rs', st), то об'єкт rs' називається місцем (перебування) об'єкту rs у стані st. Ці поняття приводять до наступної моделі.
Визначення 5.2 Абстрактною транспортною системою (АТC) називається
кортеж < St, tr, Ev, Rs, tk>, де
параметри St, tr, Ev мають той же зміст, що й у визначенні 5.1,
Rs –деяка абстрактна множина (об'єктів),
tk –тернарне відношення зв'язування на Rs Rs St.
Тепер можна визначити рух об'єкта. А саме, об'єкт рухається в еволюції, якщо він змінює місця свого перебування в еволюції. Точне визначення таке.
Визначення 5.3 Об'єкт rs рухається в еволюції ev, якщо
rs'Rs stev st'ev (tk(rs,rs',st) tk(rs,rs',st')).
Незважаючи на те, що поняття руху об'єктів дуже абстрактне і нерозвинене, воно дозволяє в процесі його розвитку (сходженні від абстрактного до конкретного) визначити інші конкретні характеристики транспортних областей, зокрема, простір, вулиці, транспортні засоби і т.д., і таким чином, звести їх різноманіття і багатство до обмежень на об'єкти і їх рух. Цю важливу обставину можна коротко сформулювати так: транспорт є рух об'єктів.
Прийняття цієї тези має ряд важливих наслідків. Один з них полягає в тому, що стани абстрактної транспортної системи можна конкретизувати як деякі елементи, побудовані з транспортних об'єктів. Далі, відношення між транспортними об'єктами можна обмежити тільки відношенням зв'язування, що можна тлумачити як відношення іменування одного транспортного об'єкта іншим. Прийняття цих абстракцій дозволяє розглядати стани транспортної системи як відображення, визначені на множині транспортних об'єктів. Такі відображення можна трактувати як номінативні дані. Прийняття цих положень дозволяє ввести таку конкретизацію АТС, яка називається транспортною системою.
Визначення 5.4 Транспортною системою (ТC) називається кортеж < Rs, St, tr, Ev >, де
Rs –деяка абстрактна множина (транспортних об'єктів),
St Rs –деяка підмножина часткових багатозначних відображень, заданих на Rs,
параметри tr, Ev мають той же зміст, що й у визначенні 5.1.
При створенні програмних транспортних систем звичайно обмежуються використанням таких моделей, у яких стани являють собою спадково скінченні бінарні відношення, а еволюції –скінченні множини станів. Виникаючі в цьому випадку дані подібні до номінативних даних, а відношення переходів можуть розглядатися як багатозначні відображення над такими відношеннями. Визначаючи ці відношення за допомогою композицій, можемо говорити про транспортні моделі як спеціалізації КНС.
Для специфікації транспортних систем звичайно застосовують декларативні (логічні) методи. В останньому підрозділі будується декларативна система, заснована на тернарному відношенні (зв'язці) tk(x,y,a) належності пари елементів бінарному відношенню. Це дозволяє застосувати розроблену у попередньому розділі аксіоматичну систему специфікацій програм для опису транспортних систем, і в рамках таких описів перейти до їх дослідження і подальшої конкретизації, що веде до створення програмних транспортних систем.
ВИСНОВКИ
У дисертаційній роботі вперше висунута і розроблена теорія композиційно-номінативних моделей програм, що дає можливість інтегрального опису основних аспектів програм і є теоретичною основою для розробки програмних систем різноманітного призначення.
Основними науковими результатами дисертації є такі.
. Запропоновано новий композиційно-номінативний підхід до побудови інтегрованих семантико-синтаксичних моделей програм, методологічною основою якого є метод сходження від абстрактного до конкретного. Розроблено і досліджено теоретико-функціональний формалізм композиційно-номінативних систем, що адекватно описують моделі програм різного рівня абстракції і загальності.
. Визначені і досліджені предикатні композиційно-номінативні системи, призначені для специфікації логік предикатів. На їх основі розроблені нові логічні системи абстрактного, сингулярного і номінативного рівнів, що узагальнюють традиційні пропозиційні логіки і логіки предикатів на класи часткових і недетермінованих предикатів. Для побудованих аксіоматичних систем вирішені класичні проблеми коректності і повноти.
. Розроблені і досліджені нові підходи до визначення абстрактної обчислюваності програм, що узагальнюють традиційні визначення обчислюваності функцій. Описано повні класи обчислюваних функцій і композицій над номінативними даними різних рівнів абстракції і загальності та побудовані алгебраїчні представлення таких класів.
. Визначені і досліджені спеціальні класи узгоджуючих композицій програм, що спрощують їх конструювання. Побудована і досліджена аксіоматична система специфікацій програм, що дозволяє специфікувати усі абстрактно обчислювані функції над номінативними даними.
5. Побудовані композиційно-номінативні моделі програм застосовані для опису мов програмування і мов баз даних, а також для моделювання транспортних систем.
Список опублікованих праць за темою дисертації
Задорожный В.И., Никитченко Н.С. Алгебраический подход к формализации дедуктивных языков запросов к базам данных // Программирование.–.–N.6.–C. 29–.
Задорожный В.И., Калиниченко Л.А., Никитченко Н.С. Взаимодополняющие формализации дедуктивных языков запросов // Кибернетика и системный анализ.–.–N.2.–С. 94–.
Никитченко Н.С. Композиционная семантика языков программирования // Программирование.–.–N.6.–С. 9–.
Никитченко Н.С., Шкильняк С.С. Программные дефиниторы // Программирование.–.–N.1.–С. 3–.
Никитченко Н.С. Вычисляемые композиции и универсальные императивные программные логики // Программирование.–.–N.6.–С. 3–.
Никитченко Н.С., Редько В.Н. Композиционное и функциональное программирование: сравнительный анализ // Программирование.–.–N.2.–С. 15–28.
Никитченко Н.С. Композиции программ, индуцирующих монотонные функции специального вида // Программирование.–.–N.1.–С. 3–.
Никитченко Н.С. Семантическое конструирование программ согласующими композициями // Программирование.–.–N.6.–С. 14–.
Никитченко Н.С., Трубчанинов Г.Г. Полиморфные модели программ // Кибернетика.–.–N.1.–С. 29–.
Никитченко Н.С. Объектно-ориентированные расширения композиционных баз данных // Управляющие системы и машины.–.–N.6.–С. 48–.
Никитченко Н.С. Построение систем композиционного программирования на основе отношения идентификации // Кибернетика и системный анализ.–.– N.6.–С. 38–.
Нікітченко М.С., Шкільняк С.С. Алгебри еквітонних функцій та їх властивості // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 2.– Київ, 1998.– С. 222–.
Нікітченко М.С., Шкільняк С.С. Принципи -рефлексії та -параметризації в логіках структурованих даних // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 4.– Київ, 1998.–С. 169–.
Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы // Проблемы программирования.–.–N.1.–С. 16–.
Никитченко Н.С. Предикатные композиционно-номинативные системы // Проблемы программирования.–.–N 2.–С. 3–.
Никитченко Н.С. Пропозициональные композиции частичных предикатов // Кибернетика и системный анализ.–.–N.2.–С. 3–.
Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки еквітонних предикатів // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 2.–Київ, 2000.–С. 300–.
Никитченко Н.С. Вычислимость недетерминированных программ над номинативными данными // Проблемы программирования.–.–N. 1–.–С. 49–.
Никитченко Н.С., Шкильняк С.С. Неоклассические логики предикатов // Проблемы программирования.–.–№ 3–.–С. 3–.
Нікітченко М.С., Шкільняк С.С. Чисті композиційно-номінативні числення // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 3.–Київ, 2000.–С. 290–.
Никитченко Н.С. Аппликативные композиции частичных предикатов // Кибернетика и системный анализ.–.–N.2.–С. 14–33.
Редько В.Н., Никитченко Н.С. Композиционные аспекты программологии // Кибернетика.–Часть 1, 1987.–N.5.–С. 49–; часть 2, 1988.–N.1.–С. 28–.
Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных.–Киев: Либiдь.–.–с.
Никитченко Н.С. Абстрактная вычислимость в языках программирования // Модели и системы обработки информации. Республиканский межведомственный научный сборник.–Киев: Либiдь.–.–с. 94–99.
Никитченко Н.С. Построение абстрактных транспортных моделей на основе систем композиционного программирования // Проблемы программирования. Сборник научных трудов. Киев: ИПС НАНУ.–Выпуск 2, 1997.–С. 20–.
Basarab I.A., Gubsky B.V., Nikitchenko N.S., Red'ko V.N. Composition models of databases // Proc. Second Int. East/West Database Workshop, Klagenfurt, Austria, 1994.–London: Springer.–.–P. 221–230.
Basarab I.A., Gubsky B.V., Nikitchenko N.S. Composition approach to systematic development of database systems // Proc. Second Int. Workshop on Advances in Databases and Information Systems, Moscow, 1995.–London: Springer .–.– P. 12–23.
Basarab I.A., Gubsky B.V., Nikitchenko N.S. Declarative Languages of Composition Database Development Method // Proc. Third Int. Workshop on Advances in Databases and Information Systems, vol. 1.–Moscow.–.–P. 52–.
Hansen B.S., Nikitchenko N.S. Abstract Transport Systems: Compositions and Description Languages // Перша міжнародна науково-практична конференція з програмування УкрПРОГ'98 –Праці.–Україна, Київ.–.–С. 59–.
Kalinichenko L.A., Nikitchenko N.S., Zadorozhny V.I. Application of composition development method for definition of SYNTHESIS information resource query language semantics // Proc. First Int. Symp. of Formal Methods Europe, Odense, Denmark, 1993.–Berlin: Springer-Verlag.–.–P. 428–441.
У спільно виконаних роботах науковому консультанту В.Н. Редьку належить загальна постановка проблеми та формулювання принципів композиційного програмування [6, 22, 23, 26], С.С. Шкільняку –дослідження синтаксичних виведень [4] та побудова виведень формул у розроблених аксіоматичних численнях [12, 13, 17, 19, 20], І. А. Басарабу та Б.В. Губському –дослідження операцій запитів до композиційних баз даних [23, 26–], Л.А. Калініченку та В.Й. Задорожному –дослідження операцій запитів до дедуктивних баз даних [1, 2, 30], Г.Г. Трубчанінову –дослідження поліморфних композицій [9], Б.С. Хансену –формулювання методів інтерпретації формул [29].
НІКІТЧЕНКО М.С. Теорія інтегрованих композиційно-номінативних моделей програм.–Рукопис.
Дисертація на здобуття наукового ступеня доктора фізико-математичних наук за спеціальністю 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.