Композиційно-номінативні логіки з непрямим іменуванням
We construct sequent calculi for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multi-ple-valued quasi-ary predicates of quantifier level. The defined calculi are proposed for a general case of logics of quasi-ary predicates, for logics of singl...
Збережено в:
| Дата: | 2015 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2015
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/51 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-51 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/74/7a6cb2a18908e7da750b9f634cafdf74.pdf |
| spelling |
pp_isofts_kiev_ua-article-512018-10-02T21:22:00Z Композиційно-номінативні логіки з непрямим іменуванням Rossada, T.V. Shkilniak, О.С. композиційно-номінативні логіки We construct sequent calculi for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multi-ple-valued quasi-ary predicates of quantifier level. The defined calculi are proposed for a general case of logics of quasi-ary predicates, for logics of single-valued equitone predicates and for logics of total multiple-valued antytone predicates. For the introduced calculi soundness and completeness theorems are proved. Досліджено композиційно-номінативні логіки, базовані на іменних множинах з непрямим іменуванням. Запропоновано та дослі-джено операції над такими множинами, зокрема, операції реномінації. На цій основі побудована логіка реномінативного рівня.In this paper composition-nominative logics based on name sets with indirect nomination are studied. We introduce and investigate operations on such sets, in particular operations of renomination. On this basis we specify a logic of renominative level. Інститут програмних систем НАН України 2015-09-10 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/51 PROBLEMS IN PROGRAMMING; No 2-3 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/51/52 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2018-10-02T21:22:00Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
|
| spellingShingle |
Rossada, T.V. Shkilniak, О.С. Композиційно-номінативні логіки з непрямим іменуванням |
| topic_facet |
композиційно-номінативні логіки |
| format |
Article |
| author |
Rossada, T.V. Shkilniak, О.С. |
| author_facet |
Rossada, T.V. Shkilniak, О.С. |
| author_sort |
Rossada, T.V. |
| title |
Композиційно-номінативні логіки з непрямим іменуванням |
| title_short |
Композиційно-номінативні логіки з непрямим іменуванням |
| title_full |
Композиційно-номінативні логіки з непрямим іменуванням |
| title_fullStr |
Композиційно-номінативні логіки з непрямим іменуванням |
| title_full_unstemmed |
Композиційно-номінативні логіки з непрямим іменуванням |
| title_sort |
композиційно-номінативні логіки з непрямим іменуванням |
| description |
We construct sequent calculi for first-order composition-nominative logics of partial single-valued, total multiple-valued and partial multi-ple-valued quasi-ary predicates of quantifier level. The defined calculi are proposed for a general case of logics of quasi-ary predicates, for logics of single-valued equitone predicates and for logics of total multiple-valued antytone predicates. For the introduced calculi soundness and completeness theorems are proved. |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2015 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/51 |
| work_keys_str_mv |
AT rossadatv kompozicíjnonomínativnílogíkizneprâmimímenuvannâm AT shkilniakos kompozicíjnonomínativnílogíkizneprâmimímenuvannâm |
| first_indexed |
2025-07-17T09:41:03Z |
| last_indexed |
2025-07-17T09:41:03Z |
| _version_ |
1838499835762704384 |
| fulltext |
Теоретичні та методологічні основи програмування
44
УДК 004.42:510.69
КОМПОЗИЦІЙНО-НОМІНАТИВНІ ЛОГІКИ З НЕПРЯМИМ
ІМЕНУВАННЯМ
Т.В. Россада, О.С. Шкільняк
Київський національний університет імені Тараса Шевченка
01601, Київ, вул. Володимирська, 60
тел.: (044) 259 0511
e-mail: t.rossada@gmail.com, me.oksana@gmail.com
Досліджено композиційно-номінативні логіки, базовані на іменних множинах з непрямим іменуванням. Запропоновано та дослі-
джено операції над такими множинами, зокрема, операції реномінації. На цій основі побудована логіка реномінативного рівня.
In this paper composition-nominative logics based on name sets with indirect nomination are studied. We introduce and investigate
operations on such sets, in particular operations of renomination. On this basis we specify a logic of renominative level.
Вступ
Апарат математичної логіки лежить в основі сучасних інформаційних і програмних систем. Такі систе-
ми, як правило, базуються на класичній логіці предикатів. Проте класична логіка, незважаючи на її безперечні
позитивні якості, має низку обмежень (див., напр., [1]), що ускладнює застосування цієї логіки при розв’язанні
нових задач і проблем, що виникають в програмуванні. Тому дуже важливою є проблема розробки нових, про-
грамно-орієнтованих логічних формалізмів. Такими є композиційно-номінативні логіки, які будуються на базі
спільного для логіки і програмування композиційно-номінативного підходу [2]. На його основі побудовано [1]
широкий спектр логічних систем на різних рівнях абстрактності й загальності. Такі рівні відрізняються тракту-
ванням рівня розгляду даних.
Найважливішим типом даних для програмування є номінати – дані, побудовані на основі відношення
ім’я значення. Імена розглядаються гранично конкретно ("білі" скриньки), значення – абстрактно ("чорні"
скриньки). Поняття номінату лежить в основі визначення універсуму NomD(V,W) номінативних даних, який
будується індуктивно на основі елементів множини імен V та сукупності (передмножини) базових значень W.
У роботі [3] запропонована типологія номінативних даних, яка базується на класифікації фундаментального
відношення ім’я значення:
a
a
– значення класифікуються як прості (неструктуровані) та складні (структуровані),
– імена класифікуються як прості (неструктуровані) та складні (структуровані),
– імена та значення можуть бути незалежними (пряме іменування), або залежними (можливе непряме
іменування).
Зазначені три параметри дають вісім типів номінативних даних. Таку класифікацію названо [3] типоло-
гічним кубом номінативних даних. Найпростішими є типи TND1 (прості імена, прості значення, пряме імену-
вання) та TND2 (прості імена, прості значення, непряме іменування), найскладнішим – тип TND8 (складні імена,
складні значення, непряме іменування).
Особливо важливим класом номінатів є однозначні – іменні множини. Поняття іменної множини (інколи
під іншими назвами) активно використовується в математиці й програмуванні. До іменних множин можна
віднести [4] кортежі, послідовності, індексовані множини тощо. Традиційно іменними множинами (ІМ)
називають множини пар, перша компонента яких – ім’я, а друга – його значення. Формально V-іменну множину
над A можна визначити [1] як однозначну функцію вигляду δ : V→A, де V та A – множини предметних імен та
предметних значень. Якщо (в логіці зазвичай так і роблять) вважати V ∩ A = ∅, то такі іменні множини є
номінативними даними типу TND1 (прості імена та значення, пряме іменування). Водночас в програмуванні
досить поширеним є непряме іменування, яке часто називають непрямою адресацією.
Непряма адресація є важливою особливістю розробленої К.Л. Ющенко мови адресного програмування,
яка була однією з перших мов програмування (див. [5]). Непряма адресація означає, що в комірці пам’яті ком-
п’ютера може знаходитись нова адреса. Наявність операторів та композицій, що опирались на непряму адре-
сацію, дозволило істотно підвищити виразну потужність мови. Адресне програмування дало змогу за допомо-
гою відносно простої мови програмування розробити низку алгоритмів для розв’язку широкого кола задач.
Мова адресного програмування успішно використовувалась для побудови інтерпретаторів і трансляторів для
перших вітчизняних електронно-обчислювальних машин.
Таким чином, розробка логічних формалізмів, основою яких є іменні множини з непрямим іменуванням,
має велике значення для програмування. Саме такі логічні формалізми вивчаються в даній роботі, ідея їх побу-
дови запропонована М.С. Нікітченком. Метою роботи є дослідження іменних множин з непрямим іменуванням
та операцій над ними, побудова базованих на них композиційно-номінативних логік реномінативного рівня.
Поняття, які в роботі не визначаються, будемо трактувати в сенсі [1].
© Т.В. Россада, О.С. Шкільняк, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 2-3. Спеціальний випуск
mailto:t.rossada@gmail.com
Теоретичні та методологічні основи програмування
1. Іменні множини з непрямим іменуванням
V-іменною множиною з непрямим іменуванням над множиною базових даних A називатимемо
однозначну функцію вигляду δ : V→V∪A. Такі множини будемо традиційно подавати у вигляді
[v1at1,...,vnatn,...], де vі∈V, tі∈V ∪ A, vі ≠ vj при і ≠ j. Іменні множини з непрямим іменуванням скорочено
називатимемо ІМН. Значеннями предметних імен в ІМН можуть бути як предметні імена, так і базові значення.
Клас всіх V-ІМН над A позначаємо V(V∪A). Клас всіх скінченних V-ІМН над A позначатимемо V(V∪A)F .
Предикат вигляду Р : V(V∪A) → {T, F} назвемо V-A-квазіарним предикатом.
Клас V-A-квазіарних предикатів позначимо PrV,A.
Багатократне застосування звичайних ІМ як функцій до певного предметного імені v вже на другому
кроці гарантовано дає невизначеність, адже до базових даних ІМ незастосовні. Водночас для ІМН таке засто-
сування означає рух іменною множиною.
Приклад 1. Нехай d = [xay, yaz, zaa, vab], де x, y, z, v∈V, a, b∈A;
тодi d(x) = y, d(d(x)) = z, d(d(d(x))) = a, d(d(d(d(x))))↑.
Для ІМН введемо позначення d(n)(v), де v∈V, таким чином:
d(0)(v) = v,
d(n+1)(v) = d(d(n)(v)), де n ≥ 0.
Далі, в стилі деномінаційних функцій, d(n)(v) позначатимемо також як (n)v(d).
Зокрема, d(v) позначатимемо як (1)v(d) та 'v(d), d(2)(v) позначатимемо як (2)v(d) та ''v(d) і т. д.
Шляхом в ІМН d назвемо послідовність (v1, v2 ,… vn ) таку, що vi avi+1 ∈ d, i∈{1,…, n–1}.
Шлях (v1, v2 ,… vn ) позначатимемо також v1av2a…avn .
Циклічний шлях v1av2a…avnav1av2a… будемо позначати { v1av2a…avn}.
Шлях v1av2a…aa термінальний, якщо a∈A. Шлях v1av2a…av нетермінальний, якщо v∈V.
Зокрема, пара vas∈d термінальна, якщо s∈A, та нетермінальна, якщо s∈V.
Ефект циклічного іменування притаманний ІМН.
Приклад 2. Нехай d = [xay, yaz, zax, vay, tas, uaw, waa], де a∈A, інші імена ∈V.
Тоді маємо циклічні шляхи {xayaz}, {yazax}, {zaxay}.
Окрім того, маємо також шляхи va{yazax}, tas, uawaa, waa.
Введемо розгорнуту форму подання ІМН, яку назвемо розгорткою ІМН. Для цього замість кожної пари
vat∈d записуємо шлях в d, який починається іменем v.
Приклад 3. Наведена в прикладі 2 ІМН [xay, yaz, zax, vay, tas, uaw, waa] має розгортку
[{xayaz}, {yazax}, {zaxay}, va{yazax}, tas, uawaa, waa ].
ІМН термінально еквівалентні, якщо їх розгортки мають однакові множини термінальних шляхів.
Надалі приймемо такий природний постулат:
на термінально еквівалентних ІМН предикати приймають однакові значення.
Розгортку ІМН назвемо термінальною, якщо вона містить лише термінальні шляхи.
ІМН, розгортка якої містить лише термінальні шляхи, є мінімальною в множині термінально еквіва-
лентних ІМН у тому розумінні, що не містить "зайвих" компонент, на які не реагують предикати.
Наприклад, серед ІМН, термінально еквівалентних наведеній вище ІМН прикладу 2, такою мінімальною
буде ІМН [uaw, waa], розгортка якої – [uawaa, waa].
Операції над ІМН. Для ІМН як для бінарних відношень на V × (V∪A) можна ввести традиційні операції
проекції за координатами:
pr1(d) = {v∈V | vat∈d для деякого t∈V∪A};
pr2(d) = {t∈V∪A | vat∈d для деякого v∈V}.
Можна також ввести традиційні теоретико-множинні операції перетину ∩ та різниці \.
Водночас операція об’єднання ∪ не завжди є визначеною, адже при об’єднанні ІМН може порушитись
умова однозначності.
ІМН d1 та d2 назвемо диз’юнктними, якщо pr1(d1)∩pr2(d2) = ∅.
Для диз’юнктних ІМН операція об’єднання ∪ вже коректна.
Надалі для операції об’єднання диз’юнктних ІМН вживатимемо також символ +.
Зауважимо, що операції перетину та різниці можна ввести і для розгорток ІМН, при цьому розгортка
перетину та перетин розгорток, взагалі кажучи, різні. Те саме має місце і для операції різниці.
Приклад 4. Нехай d1 = [xay, yaz, zax, vay, tas, uaw, waa], d2 = [yaz, zax, vay, xav, waa].
Тоді d1∩d2 = [yaz, zax, vay, waa].
Розгортка δ1 ІМН d1 наведена в прикладі 3. Розгортка ІМН d2 має вигляд
δ2 = [{yazaxav}, {zaxavay}, {vayazax}, { xavayaz}, waa ].
Розгортка ІМН d1∩d2 має вигляд δ = [yazax, zax, vayazax, waa ].
45
Теоретичні та методологічні основи програмування
46
Тоді δ1∩δ2 = [waa].
Операцію проекції за множиною імен X⊆V визначаємо традиційно:
d ║Х = {vat∈d | v∈X}.
Замість d ║(V \Х) та d ║(V \{x}) будемо cкорочено писати d ║–Х та d ║–x .
Операцію накладки для ІМН вводимо так:
δ1∇δ2 = (δ1 ||(pr1(d2)) + d2.
2. Операція реномінації та її властивості
Визначення операції реномінації (перейменування) для випадку ІМН істотно ускладнюється порівняно із
визначенням (див. [1]) операції реномінації звичайних ІМ.
Параметризовану за множиною пар імен операцію реномінації r : 1 1[ ,..., ]n nv x v xa a VА →
VA визначають так:
r (d) = [v1 1[ ,..., ]n nv x v xa a
1a d(x1),...,vnad(xn)]∪(d║(V\{v1,...,vn})).
Це можна записати у вигляді
r (d) = d║–{v1 1[ ,..., ]n nv x v xa a
1,...,vn} + [v1ad(x1),...,vnad(xn)].
Замість r зазвичай вживають дещо коротше позначення r1 1[ ,..., ]n nv x v xa a 1
1
,...,
,...,
n
n
v v
x x .
Замість y1,…, yn також скорочено пишуть y . Тоді r можна скорочено позначати як r1 1[ ,..., ]n nv x v xa a [ ]v xa .
Операція реномінації ІМН мусить враховувати той факт, що імена, які набувають нові значення (ліві
компоненти пар імен) та самі ці значення (задаються правими компонентами пар імен) можуть задаватися опо-
середковано, за допомогою ІМН, до якої застосовується реномінація.
В загальному вигляді операція реномінації ІМН позначається так: r . 1 11 1[ ,..., ]m nm n k kk kv x v xa a
Тут позначення означає n-кратне застосування вхідної ІМН d (аргумент операції реномінації) до
предметного імені z. Зокрема, у випадку n
n z
= 0 маємо саме ім’я z, у випадку n = 1 будемо також писати 'z,
у випадку n = 2 писатимемо ''z і т.д.
Зауважимо, що в таких позначеннях операція реномінації звичайних ІМ r подаватиметься
у вигляді r .
1 1[ ,..., ]n nv x v xa a
1 1[ ' ,..., ' ]n nv x v xa a
Дамо визначення операції реномінації ІМН r : 1 11 1[ ,..., ]m nm n k kkv x v xa a k
k k
V(V∪A) →
V(V∪A).
ІМН r (d), яка є результатом застосування операції r до ІМН d,
задамо таким чином.
1 11 1[ ,..., ]m nm n k kkv x v xa a 1 11 1[ ,..., ]m nm n k kkv x v xa a
Для кожного vi, i∈{1,..,k}, обчислюємо . При цьому можливі три випадки: отримуємо деяке z( ) ( )im
id v i∈V,
отримуємо деяке b∈A, або маємо ( ) ( )im
id v ↑ , тобто значення невизначене. Останні два випадки
непродуктивні. Формуємо послідовність q = (z
( ) ( )im
id v
1,…, zl) так отриманих предметних імен, тут zj відповідає ,
jiv де
1 ≤ i1 ≤…≤ il ≤ k. Зрозуміло, що в цій послідовності можливі повтори, це відповідає ситуації
∈V для різних i,( )( ) ( ) ( )ji mm
id v d v= j j∈{1,..,k}. Нехай Z – множина всіх імен послідовності q (зрозуміло, що
повтори в множині неможливі).
Для кожного zj обчислюємо відповідне
( )
( ),i j
j
n
id x j∈{1,..,l}. Якщо
( )
( ) ,i j
j
n
id x ↑ то вилучаємо відповідне
zj з послідовності q. Отримуємо послідовність q', в якій залишаються лише імена zj із обчисленими значеннями
( )
( )i j
j
n
j is d x= . Далі формуємо множину пар zjasj для всіх таких zj∈q'. Перші компоненти в цих парах можуть
повторюватися, водночас ІМН – однозначні. Тому треба залишити в такій множині лише такі zjasj, для яких у
цій множині немає пари zpasp із zj = zp та sj ≠ sp . Інакше кажучи, із цієї множини пар вилучаємо всі пари з
однаковими першими та різними другими компонентами. В результаті отримуємо іменну множину таких пар
η = 1 1
[ ,..., ]
tj j j jz s z sa a
t
k
k ]
. Тепер остаточно маємо r (d) = d1 11 1[ ,..., ]m nm n k kkv x v xa a
║–Z + η .
Операцію реномінації r скорочено позначатимемо r1 11 1[ ,..., ]m nm n k kkv x v xa a 1 1[ ,..., k kα β α βa a , де αi та βi позна-
чають вирази для обчислення непрямих імен та їх значень. Зовсім стисло позначаємо реномінацію як r [ ]α βa .
Приклад 5. Обчислимо δ = r ['xa''''y, ''xaz, 'ya''z, ua'y, 'ua'z] (d), де d = [xap, yap, zau, uab, pav, vaa], a, b∈A
та x, y, p, z, u, v ∈V. Маємо 'x(d) = d(x) = p, ''''y(d) = d(4)(y)↑, ''x(d) = d(d(x)) = v, 'y(d) = d(y) = p, ''z(d) = d(d(z)) = b,
'u(d) = d(u) = b, 'z(d) = d(z) = u. Тоді послідовність продуктивних імен q = (p, v, p, u), множина таких імен
Z = {p, v, u}. Для p маємо два входження в послідовність, проте для першого входження його значення ''''y(d)↑.
Таким чином, отримуємо ІМН пар η = [vaz, pab, uap]. Звідси результуюча ІМН δ = d ║–Z + η має вигляд:
δ = [xap, yap, zau, vaz, pab, uap].
Теоретичні та методологічні основи програмування
Властивості операції реномінації. Операція реномінації ІМ r [ ] монотонна за розширенням даних:
для всіх d
v xa
1, d2 ∈VA маємо d1 ⊆ d2 ⇒ r [v xa ] (d1) ⊆ r [v xa ] (d2). Це вже не так для операції реномінації ІМН r [ ]α βa .
Приклад 6. Нехай ρ = r ['xa'u, 'ya'v]. Візьмемо ІМН d1 = [xaz, uaa, vab] та d2 = [xaz, yaz, uaa, vab], де
a, b∈A та x, y, z, u, v ∈V. Маємо 'x(d1) = z, 'y(d1)↑, 'u(d1) = a, 'v(d1) = b; 'x(d2) = z, 'y(d2) = z, 'u(d2) = a, 'v(d2) = b. Тоді
ρ(d1) = d1 ║–z + [zaa] = [xaz, uaa, vab, zaa], водночас ρ(d2) = d2 ║–z + ∅ = [xaz, uaa, vab]. Таким чином,
d1 ⊂ d2 та ρ(d1) ⊃ ρ(d2) – монотонності для ρ немає.
Візьмемо тепер d3 = [xaz, uaa, vab, zab], d4 = [xaz, yaz, uaa, vab, zab]. Тоді d3 ⊂ d4 . Тепер маємо
ρ(d3) = d3 ║–z + [zaa] = [xaz, uaa, vab, zaa], ρ(d4) = d4 ║–z + ∅ = [xaz, yaz, uaa, vab], тому знову моно-
тонності немає, адже невірно ρ(d3) ⊆ ρ(d4).
Таким чином:
Твердження 1. Операція реномінації ІМН r [ ]α βa не є монотонною.
На відміну від операцій реномінації ІМ, для операцій реномінації ІМН вже не можна робити їх згортку,
тобто однотипно, незалежно від вхідної ІМН, замінювати послідовне застосування двох і більше реномінацій на
застосування однієї – їх згортки. Для реномінації ІМ r [v xa ] та r [u ya ] їх згортка r [ ] [v x u ya o a ] залежить лише
від пар імен початкових реномінацій. Проте неявне, непряме задання імен в реномінаціях ІМН веде до залеж-
ності реномінації – результату послідовного застосування кількох реномінацій – не тільки від них, а й від
конкретної ІМН, до якої ведеться застосування цих реномінацій. Це засвідчує наступний
Приклад 7. Нехай d1 = [yau, uab, zaa], d2 = [yav, vab, zaa], де a, b∈A та x, y, z, u, v ∈V.
Розглянемо послідовне застосування реномінацій r [ua'z] та r [xa''y] до d1 та до d2 .
Маємо r [xa''y](r [ua'z](d1)) = r [xa''y]([yau, uaa, zaa] = [yau, uaa, zaa, xaa] = r [ua'z, xa'z](d1);
r [xa''y](r [ua'z](d2)) = r [xa''y]([yav, vab, zaa, uaa]) = [yav, vab, zaa, uaa, xab] = r [ua'z, xa''y](d2).
У випадку d1 згортка r [ua'z] та r [xa''y] подається як r [ua'z, xa'z], у випадку d2 – як r [ua'z, xa''y].
3. Реномінативна логіка з непрямим іменуванням
Семантичними моделями композиційно-номінативних логік реномінативного рівня є [1] композиційні
системи квазіарних предикатів реномінативного рівня, де множина композицій визначається базовими компо-
зиціями пропозиційного рівня та композицією реномінації. Досліджувались [1] традиційні реномінативні ло-
гіки, в яких композиція реномінації визначається через відповідну операцію реномінації ІМ. У даній роботі
пропонуються реномінативні логіки, в яких композиція реномінації R [ ]α βa визначається операцією реномінації
r [α βa ] іменних множин з непрямим іменуванням. Такі логіки назвемо реномінативними логіками з непрямим
іменуванням (РНЛН). Семантичними моделями цих логік є композиційні системи вигляду (V(V∪A), PrV,A, C), де
C визначається множиною базових композицій ¬, ∨ та R [ ]α βa .
1-арна параметрична реномінації R [ ]α βa : PrV,A →PrV,A кожному предикату зіставляє V-A-квазіарний
предикат R [ ] ( ),Pα βa значення якого для кожного d∈V(V∪A) задається так:
R [ ] ( )( )P dα β =a P(r [ ] ( ))dα βa .
Твердження 2. Композиція R [α βa ] не зберігає еквітонність (монотонність) V-A-квазіарних предикатів.
Задамо V-A-квазіарний предикат P наступним чином: P(d) = T, якщо z∈pr1(d), та P(d)↑, якщо z∉pr1(d).
Такий предикат P – еквітонний. Розглянемо тепер предикат R ['xa'u, 'ya'v](P). Цей предикат нееквітонний.
Справді, візьмемо ІМН d3 = [xaz, uaa, vab, zab] та d4 = [xaz, yaz, uaa, vab, zab] прикладу 5. Тоді:
R ['xa'u, 'ya'v](P)(d3) = P(r['xa'u, 'ya'v](d3)) = P([xaz, uaa, vab, zaa]) = T,
R ['xa'u, 'ya'v](P)(d4) = P(r['xa'u, 'ya'v](d4)) = P([xaz, yaz, uaa, vab])↑.
Маємо d3 ⊂ d4 , R ['xa'u, 'ya'v](P)(d3) = T та R ['xa'u, 'ya'v](P)(d4)↑. Отже, предикат R ['xa'u, 'ya'v](P) нееквітонний.
Наведемо основні властивості композицій R [ ]α βa .
R¬) R [ ] (α βa ¬P) = ¬R [ ] ( )Pα βa ;
R∨) R [ ] (α βa P∨Q) = R [ ] ( )Pα βa ∨ R [ ] ( )Qα βa .
Аналогічно можна записати властивості R→, R&, R↔ для похідних логічних зв’язок →, &, ↔.
RR) R [ ] (α βa R [ ] ( ))( )P dγ η =a P(r [ ] (γ ηa r [ ] ( ))dα βa ) для кожного d∈V(V∪A).
На відміну від традиційних РНЛ предикатів над ІМ, тут властивість RR записується в слабкій формі.
Неможливість виконувати згортку композицій реномінації V-A-квазіарних предикатів випливає з неможливості
виконувати згортку операцій реномінації для ІМН.
Специфічний вигляд має також властивість згортки тотожного перейменування RT.
RT) R
( ) ( 1)[ , ] ( )
n nx x P
+ α β =a a R [ ] ( )Pα βa .
47
Теоретичні та методологічні основи програмування
48
Предикатна композиційна система (V(V∪A), PrV,A, C) задає дві алгебри: алгебру даних (А, PrV,A) та алгебру
предикатів (PrV,A, C), терми якої трактуються як формули мови РНЛН.
Мова РНЛН. Опишемо мову РНЛН. Алфавіт мови: множина V предметних імен, множина Ps предикат-
них символiв; символи базових композицій ¬, ∨, [ ]R α βa .
Множина Fr формул мови визначається індуктивно:
1) кожний p∈Ps є формулою; такi формули назвемо атомарними;
2) нехай Φ та Ψ – формули; тодi ¬Φ та ∨ΦΨ – формула;
3) нехай Φ – формулa; тодi [ ]R α β Φa – формула.
Задамо відображення інтерпретації формул J : Fr→PrV,A визначається за допомогою тотального одно-
значного відображення I : Ps → PrV,A, яке виділяє базові предикати, позначаючи їх символами Рs.
1) J(р) = I(p) для кожного р∈Ps;
2) J(¬Φ) = ¬(J(Φ)), J(∨ΦΨ) = ∨(J(Φ), J(Ψ));
3) J [ ]( )R α β Φa = R [α βa ] (J(Φ)).
Об’єкти вигляду ((A, Pr V,A), I) називають [1] алгебраїчними системами (АС) з доданою сигнатурою. Відо-
браження I : Ps → PrV,A прив’язує алгебру даних (А, PrV,A) до мови РНЛН, тому така АС визначає композиційну
систему (V(V∪A), PrV,A, C). Таким чином, АС з доданою сигнатурою є інтегрованими семантичними моделями,
які пов’язують мову логіки з алгебрами даних. Такі АС скорочено позначають A = (A, I).
Традиційно позначаємо ΦA предикат J(Φ) – значення формули Φ при інтерпретації на моделі мови A.
Стандартним чином (див. [1]) вводимо поняття (частково) істинної при інтерпретації на моделі мови A та
виконуваної при інтерпретації на A формули, всюди істинної та виконуваної формули.
Формула Φ частково істинна при інтерпретації на A = (A, I) (позначаємо A |= Φ) якщо предикат ΦA –
частково істинний. Формула Φ всюди iстинна (позначаємо |= Φ), якщо A |= Φ для кожної моделі мови A.
Семантичні властивості РНЛН. На множинi формул мови РНЛН стандартним чином (див. [1]) вводять-
ся відношення логiчного наслiдку |=, слабкого логiчного наслiдку ||=, логiчної еквiвалентностi ∼; визначаються
поняття тавтології, тавтологічного наслідку. Відношення логічного наслідку поширюється на множини формул.
Для РНЛН справджуються відомі [1] теореми еквівалентності та заміни еквівалентних.
Теорема 1 (еквівалентності). Нехай формула Φ' отримана з формули Φ заміною деяких входжень формул
Φ1, ..., Φn на формули Ψ1, ..., Ψn вiдповiдно. Якщо Φ1 ∼ Ψ1, ..., Φn ∼ Ψn, то Φ ∼ Φ'.
Теорема 2 (заміни еквівалентних). Нехай Φ ∼ Ψ. Тоді: Φ, Γ |= Δ ⇔ Ψ, Γ |= Δ та Γ |= Δ, Φ ⇔ Γ |= Δ, Ψ.
Семантичні властивості пропозиційного рівня аналогічні відповідним властивостям традиційної реномі-
нативної логіки та класичної пропозиційної логіки (див. [1]). Наведемо властивості, пов’язані з композицією
реномінації. Вони записуються згідно відповідних властивостей композиції реномінації V-A-квазіарних
предикатів над ІМН і мають таку ж назву.
R¬) [ ] ( )R α β ¬Φa
∼
[ ] ( )R α β¬ Φa .
R∨) [ ] ( )R α β Φ ∨Ψa
∼
[ ] [ ]( ) ( )R Rα β α βΦ ∨ Ψa a .
Узагальнюючи R¬ та R∨, отримуємо властивості RR¬ та RR∨.
RR¬) [ ] [ ](... ( )...)R Rα β γ η ¬Φa a
∼
[ ] [ ](... ( )...)R Rα β γ η¬ Φa a .
RR∨) [ ] [ ](... ( )...)R Rα β γ η Φ ∨Ψa a
∼
[ ] [ ] [ ] [ ](... ( )...) (... ( )...)R R R Rα β γ η α β γ ηΦ ∨ Ψa a a a .
RT)
( ) ( 1)[ , ] ( )
n nx xR
+ α β Φa a
∼
[ ] ( )R α β Φa .
Записати властивість RR в аналогічному вигляді, із використанням ∼, вже неможливо. Можна лише пере-
писати властивість RR композиції реномінації:
RR_С) для кожних A = (A, I) та d∈V(V∪A) маємо [ ] [ ] [ ] [ ]( ( )( ) (r (r ( ))A AR R d dα β γ η γ η α βΦ = Φa a a a .
Кожну формулу мови РНЛН можна звести до класичноподібної нормальної форми, коли реномінації
просунуті максимально вглиб формули.
Формулу вигляду [ ] [ ](... ( )...)R R pα β γ ηa a , де р∈Ps та в реномінаціях згорнуті тотожні перейменування,
назвемо примітивною.
Формулу мови РНЛН назвемо нормальною, якщо вона утворена із примітивних формул за допомогою
символів пропозиційних композицій.
Про нормальну формулу кажуть, що вона знаходиться в нормальній формі.
Подібні нормальні форми введені [1] для формул традиційної реномінативної логіки.
Теорема 3. Для кожної формули Φ можна збудувати нормальну формулу Ψ таку, що Φ ∼ Ψ.
Використовуючи R¬ та R∨, просуваємо реномінації вглиб формули. Використовуючи RT, згортаємо то-
тожні перейменування. Кожний такий крок веде до формули, логічно еквівалентної попередній. Згідно теореми
еквівалентності, отримана таким перетвореннями нормальна формула еквівалентна початковій.
Існує алгоритм, який дозволяє для кожної формули Φ мови РНЛН з’ясувати, чи є Φ всюди iстинною.
Теоретичні та методологічні основи програмування
Без обмежень загальності, згідно теореми 3, можна розглядати лише нормальні форми.
Нехай нормальна формула Φ така, що |≠ Φ. Тоді для Φ існує контрмодель (A, d) – така модель мови
A = (A, I) та ІМН d∈V(V∪A), що ΦA(d) = F. Нехай nm(Φ) – множина всіх предметних імен, які фігурують в
символах реномінації формули Φ. Такі імена назвемо явними. Враховуючи непряме іменування, при обчисленні
значень предикатів, заданих примітивними формулами, можуть задіюватися неявні для Φ імена, вони фігу-
рують в d. Їх кількість залежить від кількості застосувань d до предметних імен, що описується параметрами
реномінації, але для конкретної Φ вона завжди скінченна. Таким чином, для кожної контрмоделі (A, d) в ІМН d
задіюється не більше певної кількості m елементів (пар ім’я значення), таке m залежить від Φ. Тому для по-
шуку контрмоделі розглядаємо лише скінченну кількість ІМН, які мають не більше m елементів. Компонентами
пар будуть імена nm(Φ) та неявні імена, таких неявних імен не більше 2m. Для термінальних пар друга
компонента (значення) є дублером першої (імені). Для кожного такого d розглядаємо всеможливі значення, які
можуть приймати на ньому елементарні підформули Φ (можлива і невизначеність). Для кожного такого набору
значень знаходимо (згідно законів пропозиційної логіки часткових предикатів) значення Φ
a
A . Якщо хоч один раз
для ΦA отримаємо значення F, то |≠ Φ, в іншому випадку |= Φ.
Таким чином, отримуємо:
Твердження 3. Множина всюди істинних формул РНЛН алгоритмічно розв’язна відносно множини всіх
формул мови.
Аналогічне твердження про розв’язність множини всюди істинних формул справджується [1] і для тра-
диційної реномінативної логіки.
Висновки
У роботі вивчаються композиційно-номінативні логіки, базовані на іменних множинах з непрямим
іменуванням. Запропоновано та досліджено операції над такими множинами, особливу увагу приділено
операції реномінації. На цій основі побудована реномінативна логіка з непрямим іменуванням. Дослідження
планується продовжити в напрямках побудови числень реномінативних логік та побудови першопорядкових
логік з непрямим іменуванням.
1. Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы // Проблеми програмування. – 1999. – № 1.
– С. 16–31.
2. Нікітченко М.С., Шкільняк С.С. Математична логіка та теорія алгоритмів. – К.: ВПЦ Київський університет, 2008. – 528 с.
3. Никитченко Н.С. Композиционно-номинативные аспекты адресного программирования // Кибернетика и системный анализ. – 2009. –
№ 6. – С. 24–35.
4. Басараб И.А., Никитченко Н.С., Редько В.Н. Композиционные базы данных. – К.: Либідь, 1992. –192 с.
5. Гнеденко Б.В., Королюк В.С., Ющенко Е.Л. Элементы программирования. – М.: Физматгиз, 1961. – 348 с.
49
|