Compositional logics of nominative data
Logics that are oriented on program specification are proposed. These logics are constructed in a semantic-syntactic style on a basis of composition nominative approach. The first logic (neoclassical compositional logic) is the logic of equitone predicates over infinitary named data; it preserves th...
Gespeichert in:
| Datum: | 2015 |
|---|---|
| Hauptverfasser: | , |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
PROBLEMS IN PROGRAMMING
2015
|
| Schlagworte: | |
| Online Zugang: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/17 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Institution
Problems in programming| id |
pp_isofts_kiev_ua-article-17 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/f4/2d1098774d12c2a4b7258419554685f4.pdf |
| spelling |
pp_isofts_kiev_ua-article-172018-10-02T21:31:22Z Compositional logics of nominative data Композиційні логіки номінативних даних Композиційні логіки номінативних даних Nikitchenko, M.S. Shkilniak, S.S. UDC 510.6, 681.3.06 УДК 510.6, 681.3.06 УДК 510.6, 681.3.06 Logics that are oriented on program specification are proposed. These logics are constructed in a semantic-syntactic style on a basis of composition nominative approach. The first logic (neoclassical compositional logic) is the logic of equitone predicates over infinitary named data; it preserves the main properties of classical logic. The second logic (over finitary nominative data) is a concretization of the first one; the class of multi-valued naturally (abstractly) computable functions over nominative data is defined on its basis. Пропонуються логіки, орієнтовані на специфікації програм. Логіки будуються в семантико-синтаксичному стилі на основі композиційно-номінативного підходу. Перша з них (неокласична композиційна логіка) є логікою еквітонних предикатів над нескінченними іменними множинами, вона зберігає основні властивості класичної логіки предикатів. Друга логіка (над скінченними номінативними даними) є конкретизацією першої, на її основі визначається клас багатозначних натурально (абстрактно) обчислюваних функцій над номінативними даними. Пропонуються логіки, орієнтовані на специфікації програм. Логіки будуються в семантико-синтаксичному стилі на основі композиційно-номінативного підходу. Перша з них (неокласична композиційна логіка) є логікою еквітонних предикатів над нескінченними іменними множинами, вона зберігає основні властивості класичної логіки предикатів. Друга логіка (над скінченними номінативними даними) є конкретизацією першої, на її основі визначається клас багатозначних натурально (абстрактно) обчислюваних функцій над номінативними даними. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2015-07-01 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/17 PROBLEMS IN PROGRAMMING; No 3 (2003) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 3 (2003) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 3 (2003) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/17/21 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T21:31:22Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
UDC 510.6 681.3.06 |
| spellingShingle |
UDC 510.6 681.3.06 Nikitchenko, M.S. Shkilniak, S.S. Compositional logics of nominative data |
| topic_facet |
UDC 510.6 681.3.06 УДК 510.6 681.3.06 УДК 510.6 681.3.06 |
| format |
Article |
| author |
Nikitchenko, M.S. Shkilniak, S.S. |
| author_facet |
Nikitchenko, M.S. Shkilniak, S.S. |
| author_sort |
Nikitchenko, M.S. |
| title |
Compositional logics of nominative data |
| title_short |
Compositional logics of nominative data |
| title_full |
Compositional logics of nominative data |
| title_fullStr |
Compositional logics of nominative data |
| title_full_unstemmed |
Compositional logics of nominative data |
| title_sort |
compositional logics of nominative data |
| title_alt |
Композиційні логіки номінативних даних Композиційні логіки номінативних даних |
| description |
Logics that are oriented on program specification are proposed. These logics are constructed in a semantic-syntactic style on a basis of composition nominative approach. The first logic (neoclassical compositional logic) is the logic of equitone predicates over infinitary named data; it preserves the main properties of classical logic. The second logic (over finitary nominative data) is a concretization of the first one; the class of multi-valued naturally (abstractly) computable functions over nominative data is defined on its basis. |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/17 |
| work_keys_str_mv |
AT nikitchenkoms compositionallogicsofnominativedata AT shkilniakss compositionallogicsofnominativedata AT nikitchenkoms kompozicíjnílogíkinomínativnihdanih AT shkilniakss kompozicíjnílogíkinomínativnihdanih |
| first_indexed |
2025-07-17T09:43:56Z |
| last_indexed |
2025-07-17T09:43:56Z |
| _version_ |
1850410205284663296 |
| fulltext |
Теоретические и методологические основы программирования
© М.С. Нікітченко, С.С. Шкільняк, 2003
ISSN 1727-4907. Проблемы программирования. 2003. № 3 29
УДК 510.6, 681.3.06
М.С. Нікітченко, С.С. Шкільняк
КОМПОЗИЦІЙНІ ЛОГІКИ НОМІНАТИВНИХ ДАНИХ∗
Пропонуються логіки, орієнтовані на специфікації програм. Логіки будуються в
семантико-синтаксичному стилі на основі композиційно-номінативного підходу. Пер-
ша з них (неокласична композиційна логіка) є логікою еквітонних предикатів над не-
скінченними іменними множинами, вона зберігає основні властивості класичної логі-
ки предикатів. Друга логіка (над скінченними номінативними даними) є конкретиза-
цією першої, на її основі визначається клас багатозначних натурально (абстрактно)
обчислюваних функцій над номінативними даними.
∗ Робота виконана в рамках проекту INTAS 2000-447.
Вступ
Математична логіка і теорія об-
числюваності, які формують математи-
чні підвалини теорії програмування,
також знаходять у програмуванні одне
з потужних джерел їхнього власного
розвитку. В даній статті ми визначаємо
і досліджуємо спеціальні логіки, що
виникають як формалізми специфіка-
цій програм. Ми також розглядаємо
спеціальне поняття абстрактної обчис-
люваності і вивчаємо його зв'язок із
запропонованими логіками. Побудову
аксіоматичних систем над номінатив-
ними даними було започатковано в
[1, 2]. Такі системи визначались на базі
класичної логіки предикатів. В даній
статті викладаються результати відпо-
відних досліджень, проведених в рам-
ках композиційно-номінативних логік.
Формальні методи побудови про-
грам звичайно пропонують послідовне
зведення абстрактних специфікацій
програм до більш конкретних специфі-
кацій. Для ефективного використання
таких методів повинні бути визначені
адекватні формалізми специфікацій
програм різних рівнів абстракції. Відо-
мі мови специфікацій, наприклад VDM,
RSL, Z та B, базуються на традиційному
теоретико-множинному підході до про-
грамних формалізмів, при цьому здебі-
льшого використовується аксіоматична
теорія множин Цермело—Френкеля.
Застосування такого могутнього фор-
малізму для побудови програм дає змо-
гу досить ефективно вирішувати деякі
прикладні проблеми. Але багато питань
відносно точних визначень програм
(особливо аспекту недетермінованості
програм) і використання логічних фор-
малізмів для мов специфікацій зали-
шаються відкритими. Це робить актуа-
льним розвиток нових підходів, що ве-
дуть до побудови більш адекватних
формалізмів специфікацій програм.
Пропонована стаття базується на ком-
позиційно-номінативному підході [3, 4]
до формалізації поняття програми.
1. Композиційно-номінативний підхід
Основна мета підходу полягає в
побудові ієрархії формальних моделей
програм різних рівнів абстракції та за-
гальності. Такий підхід може розгляда-
тися як подальший розвиток компози-
ційного програмування, запропонова-
ного [5] В.Н. Редьком.
Для полегшення розуміння робо-
ти наведемо основні визначення і по-
няття.
Композиційно-номінативні сис-
теми. Поняття композиційно-номіна-
тивної системи (КНС) є основним ма-
тематичним поняттям композиційно-
номінативного підходу. Така система
може розглядатися як трійка прості-
ших систем: композиційної, дескрип-
тивної, денотаційної. Композиційна ви-
значає семантичні аспекти програм,
дескриптивна – дескрипції або описи
програм (синтаксичні аспекти), денота-
ційна – значення (денотати) дескрип-
цій. У даній статті подамо тільки ви-
значення композиційної системи.
Теоретические и методологические основы программирования
30
Під композиційною системою бу-
демо розуміти кортеж Cm = <D, Fn, C>,
де D – множина даних; Fn ⊆ D →m D
– деяка множина часткових багато-
значних функцій; C – множина ком-
позицій на Fn.
КНС можуть трактуватися як
спеціальні мовні системи для визна-
чення різних класів функцій. Такі сис-
теми тісно пов'язані з (нетрадиційни-
ми) алгебрами даних і функцій.
Для багатозначної функції запис
f(a)↓ = r означає, що f може бути визна-
чена на a (пишемо f(a)↓) з результатом
r; запис f(a)↑ означає, що f може бути
невизначеною на a.
Множину натуральних чисел бу-
демо позначати Nat.
Під (частковим багатозначним)
предикатом розуміємо довільну част-
кову багатозначну функцію вигляду
р : D →m Bool. Тут Bool = {T, F} – мно-
жина істиннісних значень.
КНС можуть використовуватися
для побудови формальних моделей рі-
зноманітних класів програм та мов
маніпулювання даними. Моделі про-
грам, подані КНС, математично прос-
ті, але визначають семантику програм
досить адекватно. Такі моделі параме-
тричні, що дає змогу природним чи-
ном подавати програми різних рівнів
абстракцій. Окрім того, є можливість
подати на основі КНС поняття спеці-
альної абстрактної обчислюваності та
різних аксіоматичних формалізмів.
КНС можна класифікувати відповідно
до рівнів абстракції їхніх параметрів:
даних, функцій, композицій, імен.
Номінативні дані. Дані розгля-
даються на трьох рівнях: абстрактно-
му, булевому і номінативному [3, 4].
Дані третього рівня називаються номі-
нативними даними. Вони будуються
індуктивно із множини імен V та
множини базових значень W. Дамо
рекурсивне визначення класу номіна-
тивних даних:
ND(V, W) = W ∪(V →m ND(V, W)).
Hомінативні дані будемо запису-
вати у вигляді d = [vi аi | i ∈ I]. Відно-
шення номінативної належності позна-
чаємо ∈n. Таким чином, vi аi ∈n d озна-
чає, що d(vi)↓ = аi. Клас ND(V, W) \ W на-
зивається класом власне номінативних
даних. Щоб підкреслити ієрархічну
структуру номінативних даних, будемо
їх також називати ієрархічними номі-
нативними даними. Однорівневі одно-
значні номінативні дані називатимемо
іменними множинами.
Операції та композиції над но-
мінативними даними. Ми визначимо
тільки такі операції, що необхідні для
даної статті.
Основні унарні операції над но-
мінативними даними з ім'ям v як пара-
метром: іменування ⇒v, розіменування
v⇒, перевіркa v!. При застосовуванні
до даного d операція іменування ⇒v
видає як результат номінативне дане,
що складається з єдиної компоненти з
іменем v та значенням d; операція ро-
зіменування v⇒ видає як результат од-
не (довільно вибране) значення імені v,
якщо принаймні одна компонента з
іменем v знаходиться в d; операція пе-
ревірки v! видає як результат порожнє
номінативне дане ∅, якщо в d містить-
ся принаймні одна компонента з іме-
нем v, та видає як результат d, якщо в d
немає компонент з іменем v.
Основні бінарні операції над но-
мінативними даними: накладення ∇,
об'єднання ∪, різниця \. При застосову-
ванні до номінативних даних d і d' опе-
рація накладення видає як результат
нове номінативне дане, що має як
компоненти усі компоненти d' та ті
компоненти d, імена яких не містяться
в d'; операція об'єднання видає як ре-
зультат нове дане, що має усі компо-
ненти аргументів; операція різниці \
видаляє з d ті компоненти, що нале-
жать d'.
Введемо також спеціальну опе-
рацію недетермінованого вибору
choice: при застосовуванні до довільно-
Теоретические и методологические основы программирования
31
го номінативного даного d choice видає
як результат або d, або ∅.
Функції множини Fn = ND(V, W) →m
→m ND(V, W) називаються номінатив-
ними функціями.
Основні композиції, визначені на
Fn, – це бінарні композиції, описані
такими співвідношеннями:
1) множення (функціональна ком-
позиція): (f○g)(d) = g(f(d)).
Зауважимо, що спочатку засто-
совується f, потім застосовується g;
2) ітерація. Рекурсивне визна-
чення композиції ітерації таке:
(f∗g)(d) =
, ( )
( )( ( )), ( )
d f d
f g g d f d
= ∅
∗ ≠ ∅
якщо ,
якщо ;
3) накладення: ( f ∇g)(d) = f(d)∇g(d);
4) сума: ( f Ug)(d) = f(d) ∪ g(d);
5) різниця: (f – g)(d) = f(d) \ g(d),
де f, g∈Fn, d∈ND(V, W).
В усіх випадках, коли деяке за-
стосування функції до певних даних у
правій частині співвідношення неви-
значене, результат лівої частини спів-
відношення також невизначений.
Абстрактна обчислюваність над
номінативними даними. Будучи фор-
мальними моделями програм, КНС до-
зволяють визначити і досліджувати ос-
новні властивості програм. Одна з та-
ких властивостей – обчислюваність
програми.
Традиційні мови програмування
звичайно називають універсальними.
Проте більш повне дослідження зму-
шує засумніватися в цьому, воно вка-
зує на низку труднощів, що виникають
при такому трактуванні поняття обчис-
люваності програм. Як правило, під
ним розуміють обчислюваність n-арних
функцій, визначених на цілих числах
або на словах. Таку обчислюваність
можна назвати Тьюринговою. Але про-
грами також працюють з іншими стру-
ктурами даних, тому для цих структур
мови програмування, що розглядають-
ся як універсальні, вже такими не бу-
дуть, оскільки не можуть подавати усі
обчислювані функції, визначені на цих
структурах [3]. Отже, уточнення по-
няття обчислюваності програми – не-
тривіальна проблема, яка вимагає спе-
ціального дослідження. Потрібне нам
поняття обчислюваності мусить бути
також застосовне до структур даних
різних рівнів абстракції. Така обчис-
люваність називається абстрактною.
Спеціальний тип абстрактної обчислю-
ваності, орієнтований на композицій-
но-номінативні системи, називається
натуральною обчислюваністю [6, 7].
Ми не будемо тут деталізувати це пи-
тання, подамо тільки один результат,
що описує повний клас обчислюваних
функцій над номінативними даними
(теорема 5 [6]). Цей результат буде ви-
користовуватися при вивченні логік
над номінативними даними.
Нехай V = {v0, …, vm} – скінченна
множина (m > 0), W – абстрактна мно-
жина. В цьому випадку ND(V, W) назве-
мо множиною V-скінченних W-абстракт-
них номінативних даних.
Теорема 1. Повний клас натура-
льно обчислюваних часткових багато-
значних функцій на множині ND(V, W)
V-скінченних W-абстрактних номінати-
вних даних збігається з класом функ-
цій, отриманих замиканням множини
функцій {⇒v0, …, ⇒vm, v0⇒, …, vm⇒, v0!,
…, vm!, choice} за допомогою множини
композицій {○, ∗, U, –}.
Специфікації програм. Деклара-
тивні методи специфікації програм
розглядаються як більш абстрактні, ніж
імперативні. Існують різні підходи до
специфікації програм. Тут ми прийме-
мо традиційну точку зору, згідно з
якою для специфікації програм вико-
ристовуються предикати. Труднощі по-
лягають у тому, що ми розглядаємо ча-
сткові багатозначні функції. Щоб пода-
вати такі функції, необхідно розвинути
спеціальні часткові логіки. У цьому на-
прямку зроблені тільки перші кроки.
Введемо наступне визначення.
Нехай p : D2→Bool – бінарний преди-
кат, f∈D' →m D' – часткова багато-
значна функція (тут D' ⊆ D). Тоді пре-
дикат p реляційно подає функцію f,
Теоретические и методологические основы программирования
32
якщо графік функції f збігається з
множиною {(a, r) | p(a, r) = Т, a, r ∈ D'}.
Композиційно-номінативні пре-
дикатні системи. КНС можуть також
використовуватися для визначення
класів предикатів. Відповідні КНС на-
зиваються предикатними (ПКНС) [8].
Для випадку ПКНС композиційні сис-
теми мають вигляд <D, Рr, C>, де D –
множина даних, Рr ⊆ D →m Bool – де-
яка множина (часткових багатознач-
них) предикатів, C – множина компо-
зицій на Pr.
Ми розглядаємо ПКНС на трьох
рівнях, індукованих відповідними рів-
нями абстракції даних: ПКНС над абс-
трактними даними, нескінченними
іменними множинами та ієрархічними
номінативними даними. ПКНС є семан-
тичною основою для спеціальних логік
предикатів (композиційних логік). Ло-
гіки абстрактного рівня називаються
пропозиційними. Інфінітарні пропози-
ційні логіки для різних класів частко-
вих і недетермінованих предикатів бу-
ли введені в [8]. У даній статті ми про-
понуємо дві логіки предикатів: над
іменними множинами та над номіна-
тивними даними.
2. Композиційна логіка над іменними
множинами
Ця логіка буде аналогом класич-
ної логіки предикатів, тому ми назвемо
її неокласичною композиційною логі-
кою предикатів (НКЛП), або неокласи-
чною логікою.
Щоб мотивувати наші визначен-
ня, мусимо спочатку проаналізувати
основні поняття класичної логіки [9],
до яких можна віднести:
1) мову LCL, що описує множину
формул FrCL над множиною Vr предме-
тних змінних та n-aрною предикатною
сигнатурою σCL = (Ps, ar), де Ps – мно-
жина предикатних символів, ar : Ps →
→ Nat – відображення арності;
2) відношення вивідності (довід-
ності) |–CL ⊆ CLFr2 ×FrCL формули з мно-
жини аксіом;
3) поняття моделі (інтерпрета-
ції) IntCL, базоване на понятті
алгебраїчної системи (АС) заданої
раїчної системи (АС) заданої сигна-
тури A(σCL) = (A, Ps
CLµ ), де відображення
Ps
CLµ : Ps → ∪
Natn
n BoolA
∈
→ )( узгоджується з
відображенням арності ar;
4) відношення істинності |=CL ⊆
⊆ IntCL×FrCL формули на моделі.
Проведений в [10] аналіз класич-
ної логіки дозволяє зробити наступні
висновки:
— до побудови класичної логіки
застосовується синтактико-семантич-
ний підхід;
— трактування пропозиційних
зв'язок і атомарних формул орієнтоване
на використання n-aрних предикатів;
— семантика кванторів та фор-
мул задається за допомогою інтерпре-
тацій.
З погляду композиційно-номіна-
тивного підходу семантичні аспекти
важливіші за синтаксичні, тому синта-
ктико-семантичний стиль побудови ло-
гіки повинен бути змінений на семан-
тико-синтаксичний. Це означає, що ми
спочатку фіксуємо рівень абстракції
розгляду предметних областей; потім
будуємо відповідні обраному рівню аб-
стракції композиційні системи (алгеб-
ри), які задають семантичні аспекти,
після цього визначаємо мову і відно-
шення істинності, індуковане компози-
ційними системами; нарешті, задаємо
відношення виведення, яке узгоджу-
ється з властивостями композиційних
систем, та відношення істинності.
Основним семантичним понят-
тям логіки є поняття предикату. Тради-
ційно досліджувані предикати тракту-
ються як тотальні n-aрні предикати ти-
пу An → Bool. Але якщо ми спробуємо
подати значення формул як тотальні n-
aрні предикати, тоді зіштовхнемося з
багатьма труднощами. Зокрема, таке
подання не є композиційним за Фреге
[8]. Зазначені факти дають підставу
замість тотальних n-aрних предикатів
розглядати часткові предикати над
іменними даними. Такі часткові преди-
кати, визначені на множині VrА = Vr → А,
називаються Vr-квазіарними. Зауважи-
мо, що фактично цей клас предикатів
Теоретические и методологические основы программирования
33
індукований семантикою Тарського
класичної логіки.
Розглянемо наступний приклад.
Нехай Vr = {x, y, z, ...}. Тотальний преди-
кат на множині цілих чисел, описаний
формулою x > y, може розглядатися як
Vr-aрний предикат, визначений на не-
скінченній іменній множині вигляду
[x а1, y а2, z а3, …], де а1, а2, а3, ... –
цілі числа. Зрозуміло, що для цього
предикату тільки змінні x та y є істот-
ними, інші змінні неістотнi. Це озна-
чає, що ми можемо також поставити у
відповідність формулі x > y частковий
Vr-квазіарний предикат замість тоталь-
ного предикату. Цей частковий преди-
кат буде визначений на всіх нескін-
ченних та скінченних іменних множи-
нах, які мають компоненти з іменами x
та y, наприклад, на іменній множині
[x а2, y а1, z а4]. На іменних мно-
жинах, що не мають компоненти з
іменем x або y, цей предикат невизна-
чений. Розглянутий предикат має на-
ступні дві властивості. По-перше, якщо
він визначений на деякій іменній мно-
жині d (в цьому випадку d містить ком-
поненти з іменами x та y), тоді він буде
також визначений на будь-якій іншій
іменній множині d', яка є розширенням
d. По-друге, цей предикат завжди буде
визначеним на будь-якій максимальній
іменній множині, тобто на іменній
множині, в якій кожна змінна має зна-
чення.
Формалізація цих двох властиво-
стей веде до наступних визначень
[3, 11].
Предикат p∈VrA → Bool назвемо
eквітонним, якщо (p(d)↓ & (d ⊆ d')) ⇒
⇒ (p(d')↓ = p(d)) для будь-яких d, d'∈VrA.
Предикат p∈VrA → Bool назвемо
повнототальним, якщо p(d)↓ для будь-
яких d∈AVr.
Еквітонні повнототальні преди-
кати називаються Vr-повними преди-
катами.
Неважко показати, що формули
класичної логіки мають як значення
Vr-повні предикати. Це твердження є
безпосереднім наслідком відомої леми
збігу (coincidence lemma). Зазначений
факт дуже важливий для побудови
неокласичної композиційної логіки,
яка базується на класі Pc(Vr, А) Vr-
повних предикатів. Для таких класів
часткових предикатів пропозиційні
зв'язки і квантори доцільно трактувати
як композиції.
Композиції предикатів. Спочатку
визначимо композиції диз'юнкції ∨ та
заперечення ¬ на класі Pr = D → Bool
наступними співвідношеннями (тут
p, q∈Pr, d∈D):
( ) ( )
( ) ( )( )( )
у
T p d T q d T
F p d F q d Fp q d
↓= ↓=
↓= ↓=∨ =
, якщо або ,
, якщо та ,
невизначене в сіх інших
випадках;
( )
( )( ) ( )
( )
T p d F
p d F p d T
p d
↓=
¬ = ↓=
↑
, якщо ,
, якщо ,
невизначене, якщо .
Ці композиції є аналогами силь-
них зв'язок Кліні. Вони є композиціями
абстрактного рівня.
На наступному рівні визначаємо
D як VrA. На цьому рівні можна визна-
чити нову параметричну композицію
реномінації R n
n
vv
xx
,...,
,...,
1
1
та екзистенційний
квантор (квантор існування) ∃x (тут
p, q∈Pr, d∈VrA, v1, ..., vn, х1, ..., хn ∈Vr, при-
чому v1, ..., vn – попарно відмінні імена):
R ))((,...,
,...,
1
1
dpn
n
vv
xx = p([v a | v a ∈n d, v∉{v1,
..., vn}]∇[vi ai | xi ai ∈n d, i∈{1,…, n}]);
: (
)
( )( )( )
у
T b A p d x
b T
F p d x a Fp d
a A
∈ ∇
↓=
∇ ↓=∃ =
∈
, якщо існує
,
, якщо
для всіх ,
невизначене в сіх інших
випадках.
x
Похідні композиції &, →, ↔, ∀x
визначаються традиційним способом.
Теоретические и методологические основы программирования
34
Ввівши позначення вигляду y для
y1, ..., yn, замість R n
n
vv
xx
,...,
,...,
1
1
також писати-
мемо Rvx .
Нехай клас предикатів Pr ⊆
VrA →
→ Bool замкнений відносно введених
композицій. Композиційна система
< VrA, Pr, {∨, ¬, Rvx , ∃x}> називається ба-
зовою композиційною системою пер-
шого порядку і далі буде подаватися як
алгебра APFO(Vr, A, Pr) = <Pr, ∨, ¬, Rvx , ∃x>.
Назвемо її базовою предикатною алге-
брою першого порядку. Зазначені алге-
бри формують семантичну основу
композиційної логіки першого порядку.
Неважко довести наступне твер-
дження [11].
Теорема 2. Клас Vr-повних пре-
дикатів Pc(Vr, А) замкнений відносно
композицій ∨, ¬, Rvx , ∃x.
Таким чином, APFO(Vr, A, Pc(Vr, А))
– предикатна алгебра першого поряд-
ку. Для цієї алгебри зберігаються осно-
вні властивості традиційних пропози-
ційних зв'язок і кванторів. Тому обме-
жимося розглядом дистрибутивної вла-
стивості реномінації:
Rvx (¬р) = ¬Rvx (р) — дистрибутив-
ність реномінації щодо заперечення;
Rvx (p∨q) = Rvx (p)∨Rvx (q) — дистри-
бутивність реномінації щодо диз'юнкції;
Rvu (∃xр) = ∃хRvu (р) за умови х∉{v ,
u } — обмежена дистрибутивність ре-
номінації щодо кванторів.
Обмежена дистрибутивность не
дає змоги просунути реномiнацію
вглиб формули і перетворити формулу
до класичноподібного вигляду. Щоб це
стало можливим за умови х∈{v1, ..., vn, u1,
..., un}, необхідно замінити кванторну
змінну х на таку змінну z, яка не вхо-
дить до {v1, ..., vn, u1,..., un}. Тоді вираз ∃хp
можна замінити виразом ∃zR x
z p. Проте
при обчисленні p така заміна змінює
значення z, яке може бути істотним для
p. Отже, щоб заміна була коректною,
треба вимагати неістотності z для p. За-
гальне визначення неістотності таке.
Змінна z∈Vr неістотна для пре-
дикату р∈VrA→ Bool, якщо для будь-яких
d, d'∈VrA, які відрізняються тільки зна-
ченнями змінної z, із р(d)↓ та р(d')↓ ви-
пливає р(d) = р(d').
Наступне питання: як можна
одержати неістотні змінні? Видається
розумним постулювати існування та-
ких змінних для базових предикатів і
потім виводити цю властивість для
предикатів, які є значеннями структу-
рованих формул. Змінні, неістотні для
базових предикатів, називаються син-
тетично неістотними. Змінні, неістот-
ність яких виводиться, називаються
аналітично неістотними. Таким чином,
постулюючи існування нескінченної
множини синтетично неістотних змін-
них, ми можемо просувати реномi-
націю вглиб формули до предикатних
символів. Отримані формули природно
назвати псевдокласичними.
Основні визначення і властивос-
ті неокласичної композиційної логіки.
Неокласична композиційна логіка пре-
дикатів – спеціальна композиційна ло-
гіка першого порядку. Основні поняття
НКЛП будемо звичайно позначати, ви-
користовуючи CPL як нижній індекс.
Композиційно-номінативні пре-
дикатні системи. Композиційні логіки
базуються на ПКНС (предикатних ал-
гебрах) першого порядку, що індуку-
ють семантичні та синтаксичні власти-
вості таких логік.
Мова. Алфавіт мови НКЛП скла-
дається з множини Vr предметних
змінних, множини Ps предикатних си-
мволів (символів базових предикатів)
та символів базових композицій ∨, ¬,
R vx , ∃x. Для кожного символу Ps мно-
жина синтетично неістотних змінних
визначається за допомогою тотального
відображення ne : Ps→2Vr. Пару σCPL =
= (Ps, ne) назвемо предикатною сигна-
турою. Вимагається, щоб множина
∩
Psp
pne
∈
)( , яку назвемо множиною тота-
льно неістотних змінних, була нескін-
ченною. Таке визначення сигнатури
Теоретические и методологические основы программирования
35
аналогічне визначенню сигнатури кла-
сичної логіки предикатів σCL = (Ps, ar).
Проте на противагу випадку класичної
логіки для НКЛП сигнатура не впливає
на множину формул, а обмежує тільки
клас інтерпретацій. Тому множина фо-
рмул НКЛП є множиною термів пре-
дикатної алгебри першого порядку.
Позначимо її FrCPL.
Звичайним способом вводимо сим-
воли похідних композицій →, &, ↔, ∀х.
Інтерпретації задають значення
предикатних символів, узгоджене з їх
сигнатурою. Це означає: µCPL
Ps : Ps →
→ PC(Vr, A) є відображенням денотації
(інтерпретації) предикатних символів
таким, що для будь-якого p∈Ps змінні
множини ne(p) є неістотними для пре-
дикату µCPL
Ps(р). Пара Е(σCPL) = (A, µCPL
Ps)
називається алгебраїчною системою Vr-
повних предикатів, або неокласичною
АС. Така алгебраїчна система – аналог
класичної АС n-aрних предикатів
А(σCL) = (A, µCL
Ps). Якщо сигнатури зрозу-
мілі з контексту, їх опускаємо. Відобра-
ження µCPL
Ps природним чином продов-
жується до відображення µCPL
: FrCPL →
→ PC(Vr, A).
Відношення істинності |=CPL. Фор-
мула Φ∈FrCPL частково істинна (не-
спростовна) в E, що позначаємо
E |=CPLΦ, якщо для кожного d∈VrA маємо
µCPL(Φ)(d)↓ ⇒ µCPL(Φ)(d) = T. Формула Φ
всюди істинна, що позначаємо |=CPLΦ,
якщо E |=CPLΦ для кожної неокласичної
АС E.
Відношення вивідності |−CPL. Від-
ношення вивідності для НКЛП можна
задати формально-аксіоматичними сис-
темами Гільбертівського типу [12].
Враховуючи властивості предикатних
алгебр першого порядку, визначимо
наступну множину логічних аксіом:
АхРr) ¬Φ∨Φ – пропозиційні ак-
сіоми;
АхR∃x) )(,...,
,...,
1
1
Φn
n
vv
xxR → ∃v1...∃vnФ –
аксіоми підстановки;
АхR¬) ↔Φ¬ )(vxR ))(( Φ¬ v
xR – R¬-
дистрибутивність;
АхR∨) ( ( )R Φv
x ( ))R∨ Ψ ↔v
x (R Φ ∨v
x
)Ψ∨ – R∨-дистрибутивність;
АхRR) ↔Φ))(( u
z
v
x RR )(Φu
z
v
xR —
згортка реномінацій [10, 11];
АхR∃) ↔Φ∃ )( xRvu )(Φ∃ v
uxR при х∉
∉{ v , u } — обмежена R∃-дистрибутив-
ність;
АхRT) ↔Φ)(z
zR Φ — згортка пар
однакових імен в реномінаціях;
Ах∃∃) ∃x∃yΦ → ∃y∃xΦ — комута-
тивність ∃-префіксів;
АхN∃) ∃xΦ → ∀x∃xΦ — аналітична
неістотність квантифікованих імен;
АхNR) )()( Φ→Φ∃ x
z
х
z RхR при х ≠ z
— аналітична неістотність верхніх імен
в реномінаціях;
АхNР) p → ∀xp, де р∈Ps, — синте-
тична неістотність імен для базових
предикатів
(тут Φ, Ψ∈FrCPL).
Множина правил виведення
складається з таких правил:
П1) Φ |−Ψ∨Φ — правило розши-
рення;
П2) Φ∨Φ |−Φ — правило скоро-
чення;
П3) Φ∨(Ψ∨Ξ) |−(Φ∨Ψ)∨Ξ — пра-
вило асоціативності;
П4) Φ∨Ψ, ¬Φ∨Ξ |−Ψ∨Ξ — прави-
ло перетину;
П5) Φ→Ψ, Ψ→∀xΨ |−∃xΦ→Ψ — пра-
вило ∃∀;
П6) Ф→∀уФ |− ↔Φ)(,
,
v
x
y
zR )(Φv
xR —
правило згортки по неістотному імені
(тут Φ, Ψ, Ξ∈FrCPL).
Розглянемо основні властивості
НКЛП: коректність та повноту. Корек-
тність можна довести, показуючи іс-
тинність аксіом в предикатних алгеб-
рах першого порядку та збереження
істинності правилами виведення. Пов-
ноту НКЛП можна довести безпосере-
дньо. Таке доведення проводиться на
основі секвенційних числень неокла-
сичних логік, запропонованих та дослі-
джених в [13, 14]. Вкажемо тут в пев-
ному розумінні більш сильний резуль-
Теоретические и методологические основы программирования
36
тат щодо взаємної трансляції (моделю-
вання) класичної та неокласичної логік.
Універсальне моделювання кла-
сичної логіки в неокласичній. Зафік-
суємо деяку мову класичної логіки
першого порядку сигнатури σCL. Спо-
чатку промоделюємо сигнатуру σCL у
НКЛП. Виділимо в Vr зліченну послідо-
вність різних змінних u1, ..., un, …, що
будуть грати роль стандартних імен
1, 2, ..., і збудуємо сигнатуру σCРL =
= (Ps, ne), взявши ne(p) = Vr \ {u1,..., un}, де
n = ar(p), для довільного p∈Ps. Тепер
промоделюємо класичні АС в НКЛП.
Взявши довільну класичну АС А(σCL) =
= (A, µCL
Ps), збудуємо відповідну неокла-
сичну АС Е(σCPL) = (A, µCPL
Ps), поклавши
µCPL(р)(d)↓ = b ⇔ µCL(p)(a1, ..., an)↓ = b & [u1
a1, …, un an] ⊆ d для довільних p∈Ps,
d∈VrA, b∈Bool. Побудовану АС позна-
чимо nc(A). Нарешті, моделюємо фо-
рмули класичної логіки в композицій-
ній. Для цього збудуємо відображення
nc : FrCL(σCL) → FrCРL(σCРL), замінюючи в
ϕ∈FrCL всі атомарні формули вигляду
p(x1, ..., xm) формулами R m
m
uu
xx
,...,
,...,
1
1
(р). Така
трансляція зберігає істинність формул
та всюди істинність класичних формул
в обох логіках.
Всі аксіоми класичної логіки ви-
водяться в НКЛП, правила виведення
класичної логіки моделюються в
НКЛП. Звідси отримуємо моделювання
виведень формул класичної логіки в
НКЛП. Отже, можемо говорити про
ізоморфне вкладення класичної логіки
в НКЛП.
Теорема 3. Нехай А(σCL) – дові-
льна класична АС та ϕ∈FrCL. Тоді
1) А(σCL) |=CL ϕ ⇒ nc(A) |=CPL nc(ϕ);
2) |=CL ϕ ⇒ |=CPL nc(ϕ);
3) |−CL ϕ ⇒ |−CPL nc(ϕ).
Обмежене моделювання неокла-
сичної логіки в класичній. Універсаль-
ного моделювання класу формул
НКЛП в класі формул класичної логіки
не існує. Причина полягає в тому, що
множини істотних змінних для формул
НКЛП можуть бути нескінченними.
Проте можемо зробити обмежене мо-
делювання, тому що будь-яку формулу
НКЛП можна звести до еквівалентної
їй псевдокласичної форми, використо-
вуючи додаткові змінні.
Теорема 4. Нехай Φ∈FrCРL. Тоді
існує формула Φ(с) в псевдокласичній
формі така, що |=CPL Φ ⇔ |=CPL Φ (с) та
|−CPL Φ ⇔ |−CPL Φ(с).
Всюди істинність Φ(с) можна пе-
ревірити на її класичному аналогу ϕ(с).
Крім того, можна моделювати виве-
дення таких формул в обох логіках
[12]. Отже, справджується
Теорема 5. Нехай Φ(с)∈FrCРL та
ϕ(с)∈FrCL – її класичний аналог. Тоді
|=CPL Φ(с) ⇔ |=CL ϕ(с) та |−CPL Φ(с) ⇔ |−CL ϕ(с).
З теорем 3—5 і коректності та
повноти класичної логіки випливає те-
орема коректності та повноти неокла-
сичної композиційної логіки:
Теорема 6. Нехай Φ∈FrCРL. Тоді
|=CPL Φ ⇔ |−CPL Φ.
Підсумуємо відмінність та подіб-
ність класичної логіки і неокласичної
композиційної логіки. Основна відмін-
ність полягає в тому, що НКЛП буду-
ється в семантико-синтаксичному стилі
на основі поняття композиційно-
номінативної системи. Це веде до про-
стішої семантики, що задається преди-
катною алгеброю першого порядку, та
дозволяє безпосередньо використову-
вати потужний апарат алгебри для до-
слідження НКЛП. Пропозиційні зв'яз-
ки та квантори набувають явного се-
мантичного статусу композицій. Клас
моделей НКЛП істотно багатший за
клас моделей класичної логіки. В той
же час класична і композиційна логіки
дуже близькі. Ми можемо говорити
про ізоморфне моделювання класичної
логіки в НКЛП та обмежене моделю-
вання НКЛП в класичній логіці.
3. Композиційна логіка предикатів над
номінативними даними
Предикатна алгебра першого
порядку над номінативними даними.
Неокласична композиційна логіка пре-
дикатів побудована згідно припущення,
що дані були іменними множинами,
Теоретические и методологические основы программирования
37
тобто однорівневими номінативними
даними класу VrA. На наступному рівні
абстракції елементи A можна розгляда-
ти як ієрархічні номінативні дані над V
і W. Ми також включаємо до A множи-
ну V, інакше прийдеться будувати дво-
сортну аксіоматичну теорію номінати-
вних даних. Проте ми воліємо розгля-
дати односортну теорію, тому A визна-
чимо як V ∪ ND(V, W). Припускаємо та-
кож, що V містить принаймні m + 1 (m > 0)
попарно різних імен v1, ..., vm . Побудова-
ну композиційну логіку назвемо логі-
кою номінативних даних (ЛНД).
Введемо спеціальні параметричні
предикати типу Pc(Vr, V ∪ ND(V, W)):
— предикат номінативної належ-
ності х у ∈n z;
— предикат рівності x = y;
— характеристичний предикат
W~ (х) для множини W;
— характеристичний предикат
V~ (х) для множини V;
— характеристичний предикат
iv~ (х) для елемента vі∈V, де і∈{0, ..., m}
(тут x, y, z∈Vr).
Такі позначення роблять форму-
ли будованої логіки дуже близькими до
традиційної форми. Крім того, обме-
жимо у формулах явне використання
реномінації.
Таким чином, розглядаємо алгеб-
ру APND(Vr, V, W) = < Pс(Vr, V ∪ ND(V, W)),
∨, ¬, Rvx , ∃x, х у ∈n z, x = y, W~ (х), W~ (х),
0
~v (х), …, mv~ (х)>.
Властивості відношення номіна-
тивної належності. Зрозуміло, що від-
ношення номінативної належності по-
дібне до відношення належності теорії
множин. Тому при побудові аксіомати-
чної теорії номінативних даних можна
керуватись ідеями, що застосовуються
в теорії множин. Тут ми будемо орієн-
туватись на теорію допустимих мно-
жин [15, 16], яка має деякі специфічні
особливості.
По-перше, ця теорія використо-
вує праелементи (базові елементи) для
побудови структур даних. Відомо, що
аксіоматична теорія множин ZF Цер-
мело—Френкеля дозволяє робити пра-
елементи непотрібними. ZF є елегант-
ним та могутнім засобом організації
математики, але вона занадто потужна
для теорії програмування. Теорія допу-
стимих множин більш слабка порів-
нянно з ZF стосовно принципів існу-
вання множин, вона, зокрема, не допу-
скає застосування аксіоми побудови
множини всіх підмножин. У той же час
ця теорія дозволяє праелементи, які ін-
терпретуються як базові дані. Це дає
змогу природним чином будувати скла-
дні структури даних, що добре узго-
джується з практикою програмування.
По-друге, ця теорія не настільки
потужна, як ZF, але вона достатньо си-
льна, щоб породжувати функції, які
використовуються в теорії баз даних і
програмуванні.
Враховуючи зазначені моменти,
будуємо ЛНД у стилі теорії допустимих
множин.
Аксіоматична теорія номінатив-
них даних. Деякі зауваження стосовно
позначень. По-перше, використовуємо
традиційний запис ϕ(x) для позначення
формули )(ϕz
xR , утвореної з ϕ пере-
йменуванням z на х, якщо ім'я z зрозу-
міле з контексту і не вимагає пояснень.
По-друге, припускаємо, що змінні a, b,
c приймають значення в класі власне
номінативних даних, тобто справджу-
ються формули ¬W~ (а)&¬V~ (а), ¬W~ (b) &
& ¬V~ (b), ¬W~ (c)&¬V~ (c). Це дає змогу
легко вказувати належність до номіна-
тивних даних чи до базових даних. На-
приклад, формула ∃а∃х∃у(х у∈n а) ствер-
джує, що існують непорожні номінати-
вні дані.
Введемо поняття обмежених кван-
торів. Записи
∀x y∈n a ϕ та ∃x y∈n a ϕ
розглядаємо як скорочені позначення
формул ∀x∀y(x y∈n a → ϕ) та ∃x∃y(x
y∈n a & ϕ) відповідно.
Строге включення визначаємо
формулою a ⊂ b ↔ (a ≠ b) & ∀x∀y(x y∈n a →
→ x y∈n b).
Теоретические и методологические основы программирования
38
Поняття ∆0-формули та Σ-форму-
ли вводимо традиційним [15, 16] спосо-
бом (див. також [1, 2]). Клас Σ-формул
буде використовуватися при вивченні
обчислюваності в ЛНД.
Спеціальні аксіоми ЛНД розділе-
ні на три групи. Перша група описує
властивості рівності:
AxRf) x = x – рефлексивнiсть рів-
ності;
AxEq) x1 = y1 & … & xn = yn → R n
n
vv
xx
,...,
,...,
1
1
ϕ
↔ R n
n
vv
yy
,...,
,...,
1
1
ϕ – заміна рівних.
Друга група аксіом описує влас-
тивості власне номінативних даних:
AxEx) ∀x∀y(x y∈n a ↔ x y∈n b) →
→ a = b – eкстенсійність;
AxFn) (∀a(∀x y∈n a ϕ(x) & ϕ(y) →
→ ϕ(a))) → ∀a ϕ(a) – фундованість (ін-
дукція за ∈n);
AxIn) (∀a(∀b⊂ a ϕ(b) → ϕ(a))) → ∀a ϕ(a)
– індукція за включенням;
AxSp) ∃b∀x∀y(x y∈n b ↔ x y∈n a &
& ϕ(a)) – виділення;
AxNm) ∃c(x y∈n c) – іменування;
AxUn) ∃c(a ⊆ c & b ⊆ c) – об'єд-
нання;
AxNT) ∃a∃x∃y(x y∈n a) – нетри-
віальність власне номінативних даних;
ANV) (x y∈n u) → V
~ (х) – тільки
елементи V можуть використовуватися
як імена.
Третя група аксіом описує влас-
тивості множин базових імен і даних:
AxAt) V~ (z)∨W~ (z) → ∀x∀y(x y∉n z)
— атомарність базових імен і даних;
AxCN) ( iv~ (х) & iv~ (y) → x = y, де i∈
∈{0, …, m} – єдиність опису імені ха-
рактеристичним предикатом;
AxDN) ∃u0…∃um–1∃um ( 0
~v (u0) & … &
& 1
~
−mv (um–1) & mv~ (um) & u0 ≠ u1 & …& u0 ≠ um &
& … & um–1 ≠ um) – існування m + 1 різ-
них імен.
Теорема 7. Аксіоматична теорія
номінативних даних несуперечлива.
Для доведення теореми треба по-
казати, що клас предикатів над A = V ∪
∪ ND(V, W) – модель для цієї теорії,
звідки теорія несуперечлива.
ЛНД досить потужна, вона дає
змогу подавати всі натурально обчис-
лювані функції над номінативними да-
ними.
Подання обчислюваних функцій.
Покажемо, що кожна натурально об-
числювана функція над номінативними
даними може бути реляційно подана
предикатом, описаним деякою Σ-фор-
мулою. Такі предикати назвемо Σ-пре-
дикатами. Для доведення цього твер-
дження будуємо подання всіх основних
функцій, зазначених в теоремі 1, та
всіх функцій, отриманих за допомогою
композицій, наведених в цій теоремі.
Строгий запис всіх предикатів техніч-
но досить складний, тому допускаємо
деякі синтаксичні вільності, а саме,
"подаємо" функції записами вигляду
f(x) = y ≡ ϕ(x, у). Зауважимо, що тут фор-
мула f(x) = y розглядається як скорочен-
ня формули ϕ(x, у). Введення констант
обґрунтовується формулами вигляду
∃!x k(x). Зокрема, формула ∃!a ∀x
y∈n a (x ≠ x), яка засвідчує існування
єдиного елемента, що є власне номіна-
тивним даним і не містить жодних
компонент, описує порожнє номінати-
вне дане ∅. Тоді z = ∅ є скороченням
формули ∀x y∈n z (x ≠ x). Нові преди-
катні символи вводяться записами ви-
гляду Q(x) ≡ ψ(x). Можна використову-
вати попередньо подані символи. Зви-
чайно, коректність таких введень му-
сить бути доведена.
Існування імен обґрунтовується
виразами вигляду ∃!x iv~ (х) для імені vi,
i∈{0, …, m}.
Подаємо параметричні іменуван-
ня, розіменування і функції перевірки
такими виразами:
⇒vi(x) = y ≡ (∃z z'∈n y (z = vi & z' =
= x)) & (∀z z'∈n y (z = vi & z' = x));
vi⇒(x) = y ≡ (∃z z'∈n x (z = vi & z' = y);
Теоретические и методологические основы программирования
39
vi!(x) = y ≡ (∃z z'∈n x (z = vi → y = ∅) &
& (∀z z'∈n x (z ≠ vi) → y = x).
Операція вибору: choice(x) = y ≡ (y =
= ∅ ∨ y = x).
Покажемо, як можна подавати
функції, побудовані за допомогою ком-
позицій.
Нехай функції f та g подані фор-
мулами P(x, y) та Q(x, y), тоді для мно-
ження, сумування та різниці цих фун-
кцій можна використати наступні ви-
рази:
(f g)(x) = y ≡ ∃zP(x, z) & G(z, y);
(f U g)(x) = y ≡ ∃a∃b(P(x, a) & G(x, b) &
& (∀z z'∈n y (z z'∈n a ∨ z z'∈n b)) & (∀z
z'∈n a (z z'∈n y)) & (∀z z'∈n b (z z'∈n y)));
(f – g)(x) = y ≡ ∃a∃b(P(x, a) & G(x, b) &
& (∀z z'∈n y (z z'∈n a & ∨ z z'∉n b)) &
& (∀z z'∈n a (z z'∉n b → z z'∈n y))).
Для ітерації ситуація складніша.
Спочатку ми повинні подати множини,
oрдинали, натуральні числа і послідов-
ності номінативних даних, потім пода-
ти індексні операції над послідовнос-
тями та операцію наступника для нату-
ральних чисел.
Множина {d1, ..., dn} подається як
номінативне дане [v0 d1, …, v0 dn]. По-
слідовність <d1, ..., dn> – як номінативне
дане [v0 [v0 1, v1 d1], …, [v0 [v0
n, v1 dn]].
Усі необхідні побудови можуть
бути зроблені в стилі [15,16] з викори-
станням тільки Σ-формул. Отже, справ-
джується
Теорема 8. Клас натурально об-
числюваних функцій над класом номі-
нативних даних може бути поданий за
допомогою Σ-предикатів ЛНД.
Таким чином, побудовані компо-
зиційні логіки номінативних даних до-
сить потужні, вони дозволяють подати
клас всіх натурально обчислюваних
функцій, отже, такі логіки неповні згід-
но теореми Гьоделя про неповноту.
Теорема 9. Аксіоматична теорія
номінативних даних неповна.
Висновки
У цій статті ми запропонували
дві спеціальні логіки, орієнтовані на
специфікації програм. Вони побудовані
в семантико-синтаксичному стилі і є
композиційними за Фреге. Часткові
предикати над номінативними даними
використовуються для подання денота-
тів формул. Перша логіка (неокласична
композиційна логіка) була визначена
як логіка еквітонних предикатів над
нескінченними іменними множинами,
вона зберігає основні властивості кла-
сичної логіки предикатів. Друга логіка
(над скінченними номінативними да-
ними) є конкретизацією композиційної
логіки предикатів. На основі цієї логіки
визначається клас багатозначних нату-
рально (абстрактно) обчислюваних фу-
нкцій над номінативними даними.
1. Аксиоматические системы спецификаций
программ над номинативными данными /
Н.С. Никитченко, Л.Л. Омельчук, С.С. Шкиль-
няк, О.И. Янченко // Пробл. программирова-
ния. – 2000. – № 1—2. – С. 259—272.
2. Нікітченко М.С., Шкільняк С.С., Омель-
чук Л.Л. Програми над ідентифікованими
даними та їх Σ-визначеність. – Київ, 1999.
– Деп. в ДНТБ України 01.10.99, N 242—
Ук99. – 82 с.
3. Nikitchenko N. A Composition Nominative
Approach to Program Semantics: Technical
Report IT—TR: 1998—020. – Denmark: Tech-
nical University of Denmark, 1998. – 103 p.
4. Никитченко Н.С. Композиционно—номи-
нативный подход к уточнению понятия про-
граммы // Пробл. программирования. –
1999. – № 1. – С. 16—31.
5. Редько В.Н. Композиции программ и компо-
зиционное программирование // Програм-
мирование. – 1978. – № 5. – С. 3—24.
6. Nikitchenko N.S. Abstract Computability of
Non-deterministic Programs over Various
Data Structures // Perspectives of Systems In-
formatics: Proc. of A.Ershov Fourth Intern.
Conf., Novosibirsk, 2001. – LNCS 2244
(2001). – P. 471—484.
7. Басараб И.А., Никитченко Н.С., Редько В.Н.
Композиционные базы данных. – Киев:
Либiдь. – 1992. – 191 с.
8. Никитченко Н.С. Предикатные композици-
онно—номинативные системы // Пробл.
программирования. – 1999. – № 2. –
С. 3—19.
9. Шенфилд Дж. Математическая логика. –
М.: Наука, 1975. – 527 с.
10. Никитченко Н.С., Шкильняк С.С. Неоклас-
сические логики предикатов // Пробл.
Теоретические и методологические основы программирования
40
программирования. – 2000. – № 3—4. –
С. 3—17.
11. Нікітченко М.С., Шкільняк С.С. Алгебри
еквітонних функцій та їх властивості //
Вісн. Київ. Ун. Сер.: фіз.-мат. науки. –
1998. – Вип 2. – С. 222—232.
12. Нікітченко М.С., Шкільняк С.С. Чисті
композиційно-номінативні числення // Там
же. – 2000. – Вип 3. – С. 290—303.
13. Нікітченко М.С., Шкільняк С.С. Неокласич-
ні логіки та секвенційні числення. – Деп.
в ДНТБ України 22.07.2002, № 114-Ук2002.
– 46 с.
14. Шкільняк С.С. Неокласичні секвенційні чи-
слення. – Вісн. Київ. Ун. Сер.: фіз.-мат.
науки, 2002. – Вип 4. – С. 261—274.
15. Barwise J. Admissible sets and structures. –
Berlin: Springer—Verlag, 1975. – 394 p.
16. Ершов Ю.Л. Определимость и вычисли-
мость. – Новосибирск: Науч. кн., 1996.
– 300 с.
Отримано 03.09.03
Про авторів
Нікітченко Микола Степанович
доктор фіз.-мат. наук, зав. кафедрою
теорії програмування
Шкільняк Степан Степанович
канд. фіз.-мат. наук, доцент кафедри
теорії програмування
Місце роботи авторів:
Київський національний університет ім. Тараса
Шевченка
вул. Володимирська, 60, Київ, Україна
Тел. (044) 259 0519
E-mail: nikitchenko@unicyb.kiev.ua
sssh@unicyb.kiev.ua
|