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

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

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

Звідси випливає, що описи повних класів композицій утворюються безпосередньо з теореми 3.8 і теорем 3.3 - 3.6. Наприклад, для екваційних номінативних даних має місце такий результат ( - композиція з'єднання).

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

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

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

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

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

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

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

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

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

Поняття запитуючої програми можна підсилити до поняття сильнозапитуючої програми (підрозділ 4.3), яка може не тільки запитувати значення даних, але і визначати їхню наявність. Отримані при цьому класи функцій вже не будуть монотонними (еквітонними). Проте вдається перенести всі основні результати про запитуючі програми на клас сильнозапитуючих програм (теореми 4.2 - 4.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: D²Bool - бінарний предикат, а f DD - часткова багатозначна функція. Тоді предикат p реляційно представляє функцію f, якщо її графік збігається з областю істинності предикату.

Для визначення предикатів використовуються спеціальні - предикатні - КНС (ПКНС), визначені в другому розділі. Розглядаються системи, які базуються на фінітарних предикатних алгебрах першого порядку виду APFO(V, A, ^VA) = <^VA, _P, _P, _P, R_P, x_P, x_P>. Множина A конкретизується як клас метаномінативних даних, а за базові предикати вибираються предикати номінативної належності (_n) , рівності на класі метаномінативних даних (=) і належності множині базових елементів (W). Вказана конкретизація визначає нову ПКНС, що називається системою специфікації номінативних даних. Ця система досліджується як у семантичному, так і в синтаксичному (аксіоматичному) аспекті. З цією метою будується спеціальна аксіоматична теорія метаномінативних даних (ТМНД) із рівністю і тернарною зв'язкою (предикатом) номінативної належності.

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

ТМНД будується як односортна теорія з унарним предикатом U, істинним на елементах базової множини W. Аксіоми ТМНД діляться на декілька груп. Аксіоми екстенсійності, фундування (індукції за зв'язкою належності - вертикальної індукції) і індукції за зв'язкою включення (горизонтальної індукції) стосуються фундаментальних властивостей МНД. Аксіоми виділення, іменування та об'єднання пов'язані з допустимими принципами конструювання МНД. Інші аксіоми задають нетривіальність класу МНД і властивості базових елементів.

Спеціальні аксіоми ТМНД є універсальними замиканнями наступних формул, де - довільна формула, а ₀ - довільна ₀-формула, що не має вільних входжень b.

- Екстенсійність: x y (x y_n a x y_n b) a = b.

- Фундованість (індукція за належністю):

(a (x y_n a ( x) ( y) (a))) a (a) .

- Індукція за включенням: (a (b a (b) (a))) a (a).

- ₀-виділення: b x y (x y_n b x y_n a ₀(a)) .

- Іменування: c x y_n c.

- Об'єднання: c (a c b c ).

- Нетривіальність: a x y (x y_n a) .

- Базові елементи: (x y_n u) .

Теорема 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) належності пари елементів бінарному відношенню. Це дозволяє застосувати розроблену у попередньому розділі аксіоматичну систему специфікацій програм для опису транспортних систем, і в рамках таких описів перейти до їх дослідження і подальшої конкретизації, що веде до створення програмних транспортних систем.

ВИСНОВКИ

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

Основними науковими результатами дисертації є такі.

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

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

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

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

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

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

1. Задорожный В.И., Никитченко Н.С. Алгебраический подход к формализации дедуктивных языков запросов к базам данных // Программирование.- 1992.- N.6.- C. 29-47.

2. Задорожный В.И., Калиниченко Л.А., Никитченко Н.С. Взаимодополняющие формализации дедуктивных языков запросов // Кибернетика и системный анализ.- 1993.- N.2.- С. 94-110.

3. Никитченко Н.С. Композиционная семантика языков программирования // Программирование.- 1982.- N.6.- С. 9-18.

4. Никитченко Н.С., Шкильняк С.С. Программные дефиниторы // Программирование.- 1983.- N.1.- С. 3-10.

5. Никитченко Н.С. Вычисляемые композиции и универсальные императивные программные логики // Программирование.- 1983.- N.6.- С. 3-14.

6. Никитченко Н.С., Редько В.Н. Композиционное и функциональное программирование: сравнительный анализ // Программирование.- 1985.- N.2.- С. 15-28.

7. Никитченко Н.С. Композиции программ, индуцирующих монотонные функции специального вида // Программирование.- 1987.- N.1.- С. 3-17.

8. Никитченко Н.С. Семантическое конструирование программ согласующими композициями // Программирование.- 1987.- N.6.- С. 14-27.

9. Никитченко Н.С., Трубчанинов Г.Г. Полиморфные модели программ // Кибернетика.- 1991.- N.1.- С. 29-34.

10. Никитченко Н.С. Объектно-ориентированные расширения композиционных баз данных // Управляющие системы и машины.- 1994.- N.6.- С. 48-53.

11. Никитченко Н.С. Построение систем композиционного программирования на основе отношения идентификации // Кибернетика и системный анализ.- 1995.- N.6.- С. 38-44.

12. Нікітченко М.С., Шкільняк С.С. Алгебри еквітонних функцій та їх властивості // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 2.- Київ, 1998.- С. 222-232.

13. Нікітченко М.С., Шкільняк С.С. Принципи -рефлексії та -параметризації в логіках структурованих даних // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 4.- Київ, 1998.- С. 169-179.

14. Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы // Проблемы программирования.- 1999.- N.1.- С. 16-31.

15. Никитченко Н.С. Предикатные композиционно-номинативные системы // Проблемы программирования.- 1999.- N 2.- С. 3-19.

16. Никитченко Н.С. Пропозициональные композиции частичных предикатов // Кибернетика и системный анализ.- 2000.- N.2.- С. 3-19.

17. Нікітченко М.С., Шкільняк С.С. Композиційно-номінативні логіки еквітонних предикатів // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 2.- Київ, 2000.- С. 300-314.

18. Никитченко Н.С. Вычислимость недетерминированных программ над номинативными данными // Проблемы программирования.- 2000.- N. 1-2.- С. 49-62.

19. Никитченко Н.С., Шкильняк С.С. Неоклассические логики предикатов // Проблемы программирования.- 2000.- № 3-4.- С. 3-17.

20. Нікітченко М.С., Шкільняк С.С. Чисті композиційно-номінативні числення // Вісник Київського університету. Серія: фіз.-мат. науки. Вип 3.- Київ, 2000.- С. 290-303.

21. Никитченко Н.С. Аппликативные композиции частичных предикатов // Кибернетика и системный анализ.- 2001.- N.2.- С. 14-33.

22. Редько В.Н., Никитченко Н.С. Композиционные аспекты программологии // Кибернетика.- Часть 1, 1987.- N.5.- С. 49-56; часть 2, 1988.- N.1.- С. 28-34.

23. Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных.- Киев: Либiдь.- 1992.- 191 с.

24. Никитченко Н.С. Абстрактная вычислимость в языках программирования // Модели и системы обработки информации. Республиканский межведомственный научный сборник.- Киев: Либiдь.- 1991.- с. 94-99.

25. Никитченко Н.С. Построение абстрактных транспортных моделей на основе систем композиционного программирования // Проблемы программирования. Сборник научных трудов. Киев: ИПС НАНУ.- Выпуск 2, 1997.- С. 20-26.

26. 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.- 1994.- P. 221-230.

27. 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 .- 1995.- P. 12-23.

28. 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.-1996.- P. 52-56.

29. Hansen B.S., Nikitchenko N.S. Abstract Transport Systems: Compositions and Description Languages // Перша міжнародна науково-практична конференція з програмування УкрПРОГ'98 - Праці.- Україна, Київ.- 1998.- С. 59-67.

30. 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.- 1993.- P. 428-441.

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