First-order composition-nominative logics with predicates of weak equality and of strong equality
Development of the new software-oriented logical formalisms is a topical problem. The paper introduces logics of partial predicates with predicate complement and equality predicates, we denote them LCE. They extend logics of quasiary predicates with equality and logics with predicate complement. T...
Збережено в:
| Дата: | 2019 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2019
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/365 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-365 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/99/672c6314b88c06adff637f145fd11599.pdf |
| spelling |
pp_isofts_kiev_ua-article-3652024-04-28T11:05:26Z First-order composition-nominative logics with predicates of weak equality and of strong equality Первопорядковые композиционно-номинативные логики с сущностями слабой и строгой равности Першопорядковi композиційно-номінативні логіки з предикатами слабкої та строгої рівності Shkilniak, S.S. logic; predicate; composition; equality; logical consequence UDC 004.42:510.69 логика; композиция; предикат; равенство; логическое следствие УДК 004.42:510.69 логіка; частковий предикат; композиційна алгебра; логічний наслідок УДК 004.42:510.69 Development of the new software-oriented logical formalisms is a topical problem. The paper introduces logics of partial predicates with predicate complement and equality predicates, we denote them LCE. They extend logics of quasiary predicates with equality and logics with predicate complement. The composition of the predicate complement is used in Floyd-Hoare program logics’ extensions on the class of partial predicates. We define predicates of weak equality and of strong equality. Thus, LCE with predicates of weak equality (denoted by LCEw) and LCE with predicates of strong equality (denoted by LCEs) can be specified. LCE can be studied on the first order and renominative levels. We consider composition algebras of LCE, investigate properties of their compositions and describe first order languages of such logics. We concentrate on the properties related to the equality predicates and the composition of the predicate complement. Various variants of logical consequence relations for the first order LCE are introduced and studied: P|=T, P|=F, R|=T, R|=F, P|=TF, R|=TF, P|=IR. In particular, we obtained that LCEw are somewhat degenerate, as for them all the relations are incorrect except for the irrefutability logical consequence relation under the conditions of undefinedness |=IR^. At the same time, all of the listed relations are correct for LCEs. Properties of the logical consequence relations are the semantic basis for construction of the respective calculi of sequential type. Further investigation of logical consequence relations for LCE includes adding the conditions of undefinedness and constructing the corresponding sequent calculi; it is planned to be displayed in the forthcoming articles. Problems in programming 2019; 3: 28-44 В работе исследованы новые программно-ориентированные логические формализмы – композиционно-номинативные логики с предикатами равенства и композицией предикатного дополнения, такие логики названы LCE. Можно выделить предикаты слабого равенства и строгого равенства. Отсюда получаем LCE с предикатами слабого равенства, их назовем LCEw, и LCE с предикатами строгого равенства, их назовем LCEs. LCE можно рассматривать на первопорядковом уровне и реноминативном уровне. Рассмотрены композиционные алгебры LCE, исследованы свойства их композиций, описаны первопорядковые языки этих логик. Основное внимание сосредоточено на исследовании свойств, связанных с предикатами равенства и композицией предикатного дополнения. Введен и исследован ряд отношений логического следствия в первопорядковых LCE, рассмотрены их особенности. В частности, установлена определенная вырожденность LCEw, для которой корректным оказывается только отношение неопровержимого логического следствия в условиях неопределенности. Подробное исследование в LCE отношений логического следствия в условиях неопределенности будет проведено в последующих роботах. Свойства отношений логического следствия в LСE является семантической основой построения соответствующих исчислений секвенциального типа. Такое построения тоже планируется осуществить в последующих роботах.Problems in programming 2019; 3: 28-44 Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивостіцих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої наявності, наведено властивості декомпозиції формул та елімінації кванторів.Problems in programming 2019; 3: 28-44 Інститут програмних систем НАН України 2019-08-21 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/365 10.15407/pp2019.03.028 PROBLEMS IN PROGRAMMING; No 3 (2019); 28-44 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 3 (2019); 28-44 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 3 (2019); 28-44 1727-4907 10.15407/pp2019.03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/365/367 Copyright (c) 2019 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2024-04-28T11:05:26Z |
| collection |
OJS |
| language |
Ukrainian |
| topic |
logic predicate composition equality logical consequence UDC 004.42:510.69 |
| spellingShingle |
logic predicate composition equality logical consequence UDC 004.42:510.69 Shkilniak, S.S. First-order composition-nominative logics with predicates of weak equality and of strong equality |
| topic_facet |
logic predicate composition equality logical consequence UDC 004.42:510.69 логика композиция предикат равенство логическое следствие УДК 004.42:510.69 логіка частковий предикат композиційна алгебра логічний наслідок УДК 004.42:510.69 |
| format |
Article |
| author |
Shkilniak, S.S. |
| author_facet |
Shkilniak, S.S. |
| author_sort |
Shkilniak, S.S. |
| title |
First-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_short |
First-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_full |
First-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_fullStr |
First-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_full_unstemmed |
First-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_sort |
first-order composition-nominative logics with predicates of weak equality and of strong equality |
| title_alt |
Первопорядковые композиционно-номинативные логики с сущностями слабой и строгой равности Першопорядковi композиційно-номінативні логіки з предикатами слабкої та строгої рівності |
| description |
Development of the new software-oriented logical formalisms is a topical problem. The paper introduces logics of partial predicates with predicate complement and equality predicates, we denote them LCE. They extend logics of quasiary predicates with equality and logics with predicate complement. The composition of the predicate complement is used in Floyd-Hoare program logics’ extensions on the class of partial predicates. We define predicates of weak equality and of strong equality. Thus, LCE with predicates of weak equality (denoted by LCEw) and LCE with predicates of strong equality (denoted by LCEs) can be specified. LCE can be studied on the first order and renominative levels. We consider composition algebras of LCE, investigate properties of their compositions and describe first order languages of such logics. We concentrate on the properties related to the equality predicates and the composition of the predicate complement. Various variants of logical consequence relations for the first order LCE are introduced and studied: P|=T, P|=F, R|=T, R|=F, P|=TF, R|=TF, P|=IR. In particular, we obtained that LCEw are somewhat degenerate, as for them all the relations are incorrect except for the irrefutability logical consequence relation under the conditions of undefinedness |=IR^. At the same time, all of the listed relations are correct for LCEs. Properties of the logical consequence relations are the semantic basis for construction of the respective calculi of sequential type. Further investigation of logical consequence relations for LCE includes adding the conditions of undefinedness and constructing the corresponding sequent calculi; it is planned to be displayed in the forthcoming articles. Problems in programming 2019; 3: 28-44 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2019 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/365 |
| work_keys_str_mv |
AT shkilniakss firstordercompositionnominativelogicswithpredicatesofweakequalityandofstrongequality AT shkilniakss pervoporâdkovyekompozicionnonominativnyelogikissuŝnostâmislabojistrogojravnosti AT shkilniakss peršoporâdkovikompozicíjnonomínativnílogíkizpredikatamislabkoítastrogoírívností |
| first_indexed |
2024-09-16T04:07:54Z |
| last_indexed |
2024-09-16T04:07:54Z |
| _version_ |
1818527922231705600 |
| fulltext |
Теоретичні та методологічні основи програмування
© О.С. Шкільняк, 2019
28 ISSN 1727-4907. Проблеми програмування. 2019. № 3
УДК 004.42:510.69 https://doi.org/10.15407/pp2019.03.028
C.С. Шкільняк
ПЕРШОПОРЯДКОВI КОМПОЗИЦІЙНО-НОМІНАТИВНІ
ЛОГІКИ З ПРЕДИКАТАМИ СЛАБКОЇ
ТА СТРОГОЇ РІВНОСТІ
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) преди-
катного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень
логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості
цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему
про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої
наявності, наведено властивості декомпозиції формул та елімінації кванторів.
Ключові слова: логіка, частковий предикат, композиційна алгебра, логічний наслідок.
Вступ
Поняття і методи математичної ло-
гіки засвідчують високу ефективність при
розв'язанні широкого спектра задач інфор-
матики й програмування (див., напр., [1]).
Особливе місце серед них посідають зада-
чі, пов’язані з розробкою надійного про-
грамного забезпечення, найперше, із побу-
довою систем специфікації та верифікації
програм. До найпоширеніших логічних
формалізмів, які успішно використовують-
ся в системах верифікації, належать логіки
Флойда-Хоара [2, 3. Такі логіки базуються
на класичній логіці предикатів, яка в недо-
статній мірі враховує неповноту, частко-
вість інформації про предметну область.
Традиційні логіки Флойда-Хоара викорис-
товують тотальні перед- та після-умови
(предикати), тому було запропоновано
(див., напр., [4, 5]) їх узагальнення на випа-
док часткових предикатів. Важливим на-
прямком такого узагальнення стало вве-
дення спеціальної немонотонної операції
(композиції) предикатного доповнення [5.
Композиційно-номінативні логіки частко-
вих квазіарних предикатів, розширені
композицією предикатного доповнення,
названо LC. Пропозиційні LC детально
описано в [6, чисті першопорядкові LC в
розглянуто [7, відношення логічного нас-
лідку в LC досліджено в [8].
В даній роботі запропоновано роз-
ширити композицією предикатного допов-
нення першопорядкові композиційно-номі-
нативні логіки з предикатами рівності. Та-
кі нові логіки названо LCE.
Спеціальні предикати рівності да-
ють змогу ототожнювати й розрізняти зна-
чення предметних імен. Композиційно-
номінативні логіки з предикатами рівності
вивчалися в [9. Можна виділити два різ-
новиди цих предикатів: слабкої рівності та
строгої рівності. Такі предикати можна ро-
зглядати на реномінативному рівні та на
чистому першопорядковому (кванторно-
му) рівні. Це дає принаймі 4 різновиди
LCE: з предикатами слабкої рівності та з
предикатами строгої рівності, які розгля-
даємо на реномінативному рівні та на чис-
тому першопорядковому рівні.
В роботі описано композиційні ал-
гебри та мови цих різновидів LCE. Основ-
ну увагу зосереджено на вивченні власти-
востей, пов’язаних з предикатами слабкої
рівності й строгої рівності та з компози-
цією предикатного доповнення. Введено та
досліджено низку відношень логічного на-
слідку в першопорядкових LCE.
Поняття, які в роботі не визнача-
ються, тлумачимо в сенсі [6, 9, 10].
1. Kомпозиційні алгебри логік з
предикатним доповненням та
рівністю
Розглядаємо квазіарні предикати
реляційного типу, або R-предикати [10.
V-A-квазіарний R-предикат – це ча-
сткова неоднозначна функція вигляду
Q :
V
A {T, F}, де {T, F} – множина іс-
тиннісних значень,
V
A – множина всіх V-A-
https://doi.org/10.15407/pp2019.03.0
Теоретичні та методологічні основи програмування
29
іменних множин. Тут V та A – множини
предметних імен та базових значень.
Позначаємо Q[d] множину всіх зна-
чень, які R-предикат Q може приймати на
аргументі d
V
А. Така Q[d] може бути од-
нією з множин , {T}, {F}, {T, F}. Отже,
кожний R-предикат Q можна задати за до-
помогою множин T(Q) = {d | TQ[d]} та
F(Q) = {d | FQ[d]}, які називають облас-
тю істинності та областю хибності преди-
ката Q. Для R-предикатів область невизна-
ченості визначається множинами T(Q) та
F(Q): )()()()()( QFQTQFQTQ .
R-предикат Q монотонний, якщо
d1 d2 Q[d1] Q[d2].
R-предикат Q антитонний, якщо
d1 d2 Q[d1] Q[d2].
R-предикат Q частковий однознач-
ний або P-предикат, якщо T(Q)F(Q) = .
R-предикат Q тотальний, або T-пре-
дикат, якщо T(Q)F(Q) =
V
A.
Для P-предиката Q запис Q(d)
означає, що Q(d) визначене, запис Q(d)
означає, що Q(d) невизначене.
Можна виділити [10] 4 константнi
R-предикати T, F, , :
T(T) = F(F) =
V
А, T(F) = F(T) = ,
T( ) = F( ) = , T() = F() =
V
А.
Предикати T, F, , відповідають
множинам значень {T}, {F}, , {T, F}, які
R-предикат може прийняти на вхідному
даному.
Предикати T, F, , монотонні й
антитонні, при цьому T, F, однозначні.
Класи V-A-квазіарних R-предикатів
та P-предикатів позначимо Pr
V–A
та PrP
V–A
.
Характерною особливістю LC є на-
явність спеціальної немонотонної 1-арної
композиції предикатного доповнення
(див. [6). Для R-предикатів задамо так:
( ) ( ) ( ) ( ),T Q Q T Q F Q
( )F Q .
Звідси ( ) ( ) ( )Q T Q F Q .
Для P-предикатів композицію
можна задати [6 так:
, якщо ( ) ,
( )( )
невизначене, якщо ( )
T Q d
Q d
Q d
Із визначень випливає, що збе-
рігає однозначність R-предикатів
Таким чином, класи P-предикатів та
R-предикатів замкнені щодо композиції .
Водночас композиція не зберігає
тотальність R-предикатів.
Твердження 1. Для кожного преди-
ката QPr
V–A
маємо QPrP
V–A
;
для кожного QPrT
V–A
маємо Q .
Звідси випливає, що клас T-преди-
катів незамкнений щодо .
Це означає, що для T-предикатів LC
не мають смислу.
Таким чином, можна розглядати LC
R-предикатів та LC P-предикатів.
LC R-предикатів реномінативного
рівня далі називаємо L
RC
; LC P-предикатів
реномінативного рівня називаємо L
RCP
;
LC R-предикатів чистого першопо-
рядкового (кванторного) рівня називаємо
L
QC
; LC P-предикатів чистого першопо-
рядкового рівня називаємо L
QCP
.
В логіках квазіарних предикатів
ототожнювати й розрізняти значення пре-
дметних імен можна за допомогою спеці-
альних 0-арних композицій – параметризо-
ваних за іменами предикатів рівності. Роз-
глядають [9] два різновиди цих предикатів:
– слабкої (з точністю до визначено-
сті) рівності =ху ;
– строгої (точної) рівності xy .
Предикати =ху та ху задаємо так:
T(=xy) = {d | d(x), d(y) та d(x) = d(y)},
F(=xy) = {d | d(x), d(y) та d(x) d(y)};
T(xy) = {d | d(x), d(y) та d(x) = d(y)}
{d | d(x) та d(y)},
Теоретичні та методологічні основи програмування
30
F(xy) = {d | d(x), d(y), d(x) d(y)}
{d | d(x), d(y) або d(x), d(y)}.
Предикати =xy та xy традиційно та-
кож позначають x
=
y та x
y.
Предикати xy тотальні однозначні,
вони [9 немонотонні й неантитонні.
Водночас предикати =xy часткові
однозначні, монотонні й еквітонні.
Неістотним для предикатів =xy та xy
є кожне zV \{x, y}.
КНЛ з предикатами рівності назве-
мо LE. Зокрема, LE з предикатами слабкої
рівності назвемо LEw, LE з предикатами
строгої рівності назвемо LEs.
На реномінативному й першопоряд-
ковому рівнях можна виділити [9 низку
різновидів LE. Зокрема, для R-предикатів
та P-предикатів маємо такі різновиди.
На реномінативному рівні:
– L
RE
– LEw R-предикатів;
– L
REP
– LEw P-предикатів;
– L
REs
– LEs R-предикатів;
– L
REsP
– LEs P-предикатів.
На чистому першопорядковому
(кванторному) рівні:
– L
QE
– LEw R-предикатів;
– L
QEP
– LEw P-предикатів;
– L
QEs
– LEs R-предикатів;
– L
QEsP
– LEs P-предикатів.
LC з предикатами рівності назвемо
LCE. Зокрема, LCE з предикатами слабкої
рівності назвемо LCEw, LCE з предика-
тами строгої рівності назвемо LCEs.
Маємо такі різновиди LCE.
На реномінативному рівні:
– L
RCE
– LCEw R-предикатів;
– L
RCEP
– LCEw P-предикатів;
– L
RCEs
– LCEs R-предикатів;
– L
RCEsP
– LCEs P-предикатів.
На чистому першопорядковому рівні:
– L
QCE
– LCEw R-предикатів;
– L
QCEP
– LCEw P-предикатів;
– L
QCEs
– LCEs R-предикатів;
– L
QCEsP
– LCEs P-предикатів.
Спільними базовими композиціями
зазначених вище різновидів КНЛ є логічні
зв’язки та , композиції реномінації R v
x
,
композиції квантифікації x для першопо-
рядкових логік. Для КНЛ зі слабкою рівні-
стю до них додаються предикати слабкої
рівності =ху , а для КНЛ зі строгою рівніс-
тю – предикати строгої рівності =ху . Для
LC та LCE додаємо композицію предикат-
ного доповнення .
Стисло нагадаємо (див. [6]) визначення
композицій , , ,R v
x x.
Задамо , , x через області істин-
ності й хибності відповідних предикатів:
T(P) = F(P);
F(P) = T(P);
T(PQ) = T(P)T(Q);
F(PQ) = F(P)F(Q);
T(xP) = {d | d x a T(Р) для деякого
aA};
F(xP) = {d | d x a F(Р) для всіх
aA}.
Композицію v
xR задаємо умовою:
))(r())((R dPdP v
x
v
x для всіх d
V
А.
Традиційним є використання похід-
них композицій , &, х, вони задаються
так:
PQ = PQ; P&Q = (PQ);
хР = хР.
Підсумовуючи, для зазначених ви-
ще різновидів КНЛ маємо такі множини
базових композицій.
CRE = {, , ,R v
x =ху} – для L
RE
та L
REP
;
CREs = {, , ,R v
x ху} – для L
REs
та L
REsP
;
CQE = {, , ,R v
x x, =ху} – для L
QE
та L
QEP
;
CQEs = {, , ,R v
x x, ху} – для L
QEs
та L
QEsP
;
Теоретичні та методологічні основи програмування
31
CRС = {, , ,R v
x } – для L
RC
та L
RCP
;
CQС = {, , ,R v
x x, } – для L
QC
та L
QCP
;
CRСE = {, , ,R v
x , =ху} – для L
RCE
та L
RCEP
;
CRСEs = {, , ,R v
x ,ху} – для L
RCEs
та
L
RCEsP
;
CQСE = {, , ,R v
x x, , =ху} – для L
QCE
та
L
QCEP
;
CQСEs = {, , ,R v
x x, ,ху} – для L
QCEs
та
L
QCEsP
.
Семантичною основою КНЛ є ком-
позиційні предикатні системи вигляду
(
V
A, Pr
V–A
, CLС), де CB – множина базових
композицій. Така композиційна система
задає дві алгебри: алгебру (алгебраїчну си-
стему) даних (
V
A, Pr
V–A
) та композиційну
алгебру предикатів (
V
A, Pr
V–A
, CB).
Композиційну систему (
V
A, Pr
V–A
,
CQE) назвемо чистою першопорядковою
композиційною системою R-предикатів зі
слабкою рівністю.
Композиційну алгебру A
QE
= (Pr
V–A
,
CQE) назвемо чистою першопорядковою
композиційною алгеброю R-предикатів зі
слабкою рівністю.
Композиційну систему (
V
A, Pr
V–A
,
CQEs) назвемо чистою першопорядковою
композиційною системою R-предикатів зі
строгою рівністю.
Композиційну алгебру A
QEs
= (Pr
V–A
,
CQEs) назвемо чистою першопорядковою
композиційною алгеброю R-предикатів зі
строгою рівністю.
Композиційну систему (
V
A, Pr
V–A
,
CQС), назвемо чистою першопорядковою
композиційною системою R-предикатів з
предикатним доповненням.
Композиційну алгебру A
QC
= (Pr
V–A
,
CQС) назвемо чистою першопорядковою
композиційною алгеброю R-предикатів з
предикатним доповненням.
Композиційну систему (
V
A, Pr
V–A
,
CQСE) назвемо чистою першопорядковою
композиційною системою R-предикатів зі
слабкою рівністю та предикатним допов-
ненням.
Композиційну алгебру A
QCE
= (Pr
V–A
,
CQСE) назвемо чистою першопорядковою
композиційною алгеброю R-предикатів зі
слабкою рівністю та предикатним допов-
ненням.
Композиційну систему (
V
A, Pr
V–A
,
CQСEs) назвемо чистою першопорядковою
композиційною системою R-предикатів зі
строгою рівністю та предикатним допов-
ненням.
Композиційну алгебру A
QCEs
= (Pr
V–A
,
CQСEs) назвемо чистою першопорядковою
композиційною алгеброю R-предикатів зі
строгою рівністю та предикатним допов-
ненням.
Композиційні алгебри зі слабкою
рівністю також називатимемо композицій-
ними E-алгебрами, зі строгою рівністю –
композиційними Es-алгебрами, з компози-
цією предикатного доповнення – компози-
ційними С-алгебрами, з композицією пре-
дикатного доповнення та слабкою рівніс-
тю – композиційними СE-алгебрами, з
композицією предикатного доповнення та
строгою рівністю – композиційними СEs-
алгебрами.
Наприклад, A
QCEs
– композиційна
СEs-алгебра R-предикатів.
Клас P-предикатів замкнений щодо
базових композицій CQE, CQEs, CQС, CQСE,
CQСEs.
Таким чином, в алгебрах A
QE
, A
QEs
,
A
QC
, A
QCE
, A
QCEs
виділено підалгебри:
– A
QEP
= (PrP
V–A
, CQE) – чистa
першопорядковa композиційна E-алгебра
P-предикатів;
– A
QEsP
= (PrP
V–A
, CQEs) – чистa
першопорядковa композиційна Es-алгебра
P-предикатів;
– A
QCP
= (PrP
V–A
, CQС) – чистa
першопорядковa композиційна C-алгебра
P-предикатів;
– A
QCEP
= (PrP
V–A
, CQСE) – чистa
першопорядковa композиційна CE-алгебра
P-предикатів;
Теоретичні та методологічні основи програмування
32
– A
QCEsP
= (PrP
V–A
, CQСEs) – чистa
першопорядковa композиційна СEs-ал-
гебра P-предикатів.
Подібним чином отримуємо компо-
зиційні предикатні системи та компози-
ційні алгебри КНЛ на реномінативних
рівнях. Маємо такі композиційні алгебри:
A
RE
= (Pr
V–A
, CRE),
A
REP
= (PrP
V–A
, CRE);
A
REs
= (Pr
V–A
, CREs),
A
REsP
= (PrP
V–A
, CREs);
A
RC
= (Pr
V–A
, CRС),
A
RCP
= (PrP
V–A
, CRС);
A
RCE
= (Pr
V–A
, CRСE),
A
RCEP
= (PrP
V–A
, CRСE);
A
RCEs
= (Pr
V–A
, CRСEs),
A
RCEsP
= (PrP
V–A
, CRСEs).
2. Bластивості композицій
Властивості пропозиційних компо-
зицій в LE, LC та LCE аналогічні власти-
востям пропозиційних композицій класич-
ної логіки, вони наведені в [6].
В LE, LC та LCE основні властиво-
сті композицій квантифікації, не пов'язані
з реномінацією, в цілому аналогічні відпо-
відним властивостям кванторів класичної
логіки. Зокрема, це
– комутативність однотипних кван-
торів;
– закони де Моргана для кванторів;
– неістотність квантифікованих імен:
Властивості, пов’язані з композиці-
ями реномінації та квантифікації в LE, LC
та LCE, аналогічні відповідним власти-
востям традиційної логіки квазіарних пре-
дикатів (див. [10]). Зокрема, це властивості
R, RI, RU, R, R, RR, Ren, Rs, R.
Для опису в перщопорядкових логі-
ках властивостей елімінації кванторів до-
датково використовують спеціальні 0-арні
композиції – предикати-індикатори Ez, які
визначають наявність у вхідних даних
компоненти з відповідним іменем zV.
Предикати Ez задаються [5] так:
T(Ez) = {d | d(z)}; F(Ez) = {d | d(z)}.
Предикати-індикатори Ez тотальні,
однозначні, немонотонні, неантитонні.
Кожне xV таке, що x z, неістотне для Ez.
Твердження 2. Маємо xx = T та
xy xy = T.
Звідси xx = F та xy & xy = F.
Отже, носій кожної підалгебри
алгебр A
QEs
, A
QEsP
, A
REs
, A
REsP
, A
QCEs
, A
QCEsP
,
A
RCEs
, A
RCEsP
містить константні предикати
T та F.
Позначимо [Pr]Cm замикання мно-
жини предикатів Pr щодо множини компо-
зицій Cm
{T, F} = [{T, F}{xy | x, yV]CQEs –
це найменша множина R-предикатів, замк-
нена щодо базових композицій CQEs та
CREs. Таким чином, в LEs можна виділити
сингулярні композиційні алгебри предика-
тів ({T, F}, CQEs) та ({T, F}, CREs).
Подібним чином задаємо множини
з константними предикатами { , T, F},
{, T, F}, { , , T, F}, вони замкнені що-
до базових композицій CQEs та CREs. Тому:
Твердження 3. 1) В першопорядко-
вих LEs R-предикатів виділяємо сингуляр-
ні композиційні алгебри ({T, F}, CQEs)
({ , T, F}, CQEs), ({, T, F}, CQEs) та
({ , , T, F}, CQEs).
2) В першопорядкових LEs P-пре-
дикатів виділяємо сингулярні композицій-
ні алгебри ({T, F}, CQEs), ({ , T, F}, CQEs).
Подібні сингулярні композиційні
алгебри виділяємо в реномінативних LEs.
[E]= = [{=xy | x, yV}]CRE замкнена
щодо CRE ; { } = [{ }{=xy | x, yV}]CQE
вже замкнена щодо CQE. Аналогічно зада-
мо замкнені щодо CQE множини з констан-
Теоретичні та методологічні основи програмування
33
тними предикатами {}=, { , }=, {T, F}=,
{ , T, F}=, {, T, F}=, { , , T, F}=. Звідси:
Твердження 4. 1) В першопоряд-
кових LEw R-предикатів можна виділити
сингулярні композиційні алгебри
({ } , CQE), ({}=, CQE), ({ , }=, CQE),
({T, F}=, CQE), ({ , T, F}=, CQE),
({, T, F}=, CQE), ({ , , T, F}=, CQE).
2) В першопорядкових LEw P-пре-
дикатів залишаються сингулярні алгебри
({ } , CQE), ({T, F}=, CQE), ({ , T, F}=, CQE).
Подібні сингулярні композиційні
алгебри виділяємо в реномінативних LEw.
Згідно твердження 1 T F .
З іншого боку, маємо
Твердження 5. = T та .
Справді, маємо ( )F ,
( ) ( ) ( ) ( )T T F
V
A;
далі маємо ( )F ,
( ) ( ) ( ) ( )T T F .
Отже, носій кожної підалгебри
алгебр A
QС
, A
QСP
, A
RС
, A
RСP
, A
QCEs
, A
QCEsP
,
A
RCEs
, A
RCEsP
, A
QCE
, A
QCEP
, A
RCE
, A
RCEP
містить константні предикати , T, F;
носій кожної підалгебри алгебр A
QС
, A
RС
,
A
QCEs
, A
RCEs
, A
QCE
, A
RCE
містить константні
предикати , , T, F. Звідси маємо таке.
Множини { , T, F} та { , , T, F}
замкнені щодо CQС та CRС. Множини
TF = [{ , T, F}{xy | x, yV}]CQСEs та
TF = [{ ,, T, F}{xy | x, yV}]CQCEs
замкнені щодо CQСEs. Подібним чином за-
даємо замкнені щодо CQСE множини TF =
та TF = . Таким чином:
Твердження 6. 1) В першопорядко-
вих LС, в першопорядкових LCEw та в
першопорядкових LCEs можна відповідно
виділити сингулярні композиційні алгебри
({ , T, F}, CQС), ( TF =, CQСE) та
( TF , CQСEs).
2) В першопорядкових LС R-пре-
дикатів, в першопорядкових LCEw та в
першопорядкових LCEs R-предикатів та-
кож можна відповідно виділити сингулярні
композиційні алгебри ({ , , T, F}, CQС),
( TF =, CQСE) та ( TF , CQСEs).
Аналогічні сингулярні композицій-
ні алгебри можна виділити в реномінатив-
них LС та LCE.
Розглянемо тепер властивості ком-
позиції .
Теорема 1. Для кожного R-
предиката Q маємо Q Q Q = T.
Справді, для кожного QPr
V–A
T(Q Q Q ) = T(Q)T(Q) ( )T Q =
= T(Q)F(Q) ( ) ( )T Q F Q =
V
A;
F(Q Q Q ) = F(Q)F(Q) ( )F Q =
= F(Q)T(Q) = .
Таким чином, Q Q Q = T.
Наслідок 1. Для кожного R-преди-
ката Q маємо
(Q Q Q ) = F;
(Q Q Q ) = .
Твердження 7 (див. також [6]).
1) Для кожного QPr
V–A
маємо:
( ) ( )F P T P ( ) ( ) ( )P T P F P ;
( ) ( )T P F P ;
( )P ( ) ( ) ( )P T P F P .
2) Для кожного QPr
V–A
маємо:
Q Q ; Q Q ; Q Q .
3) Для кожного QPrP
V–A
додатково
маємо: Q Q Q .
Розглянемо зв'язок між композиці-
ями предикатного доповнення, реномінації
та квантифікації. Згідно визначень маємо:
(R ( ))v
xT P = ( (R ( )))v
xT P ;
(R ( ))v
xF P = ( (R ( )))v
xF P = ;
Теоретичні та методологічні основи програмування
34
(R ( ))v
x P = ( (R ( )))v
x P .
Звідси отримуємо властивість R -
дистрибутивності:
R ) R ( )v
x P R ( )v
x P .
Із визначень отримуємо:
( ) ( )T xP xP ; ( )F xP ;
( ) ( ) ( )xP T xP F xP .
Розглянемо дію композиції на
спеціальні предикати-індикатори та пре-
дикати слабкої й строгої рівності.
Предикати ху та Ez є тотальними.
Враховуючи твердження 1, отримуємо:
Твердження 8.
ху = ; Ez = .
Твердження 9. Для предикатів
слабкої рівності маємо таке подання:
=ху = Ex Ey = Ex Ey ху.
Справді, для кожного d
V
A маємо:
=ху(d) =
, якщо = ( ) ,
невизначене, якщо = ( )
xy
xy
T d
d
, якщо ( ) ( ) ,
невизначене, якщо ( ) & ( )
T Ex d Ey d T
Ex d Ey d T
= Ex(d) Ey(d) (d).
Нагадаємо (див. [9]) властивості,
пов’язані з предикатами рівності.
Твердження 10. Маємо
xy = (=xy & Ex & Ey) (Ex & Ey).
Отже, предикати xy можна подати
через предикати =xy та Ez.
Наведемо властивості реномінації
предикатів рівності.
RD) Маємо
yxu
wzv
,,
,,R (=xy) = =zw та
yxu
wzv
,,
,,R (xy) = zw;
за умови { }y u маємо
xu
zv
,
,R (=xy) = =zy та
xu
zv
,
,R (xy) = zy;
за умови , { }x y u маємо
u
vR (=xy) = =xy та u
vR (xy) = xy.
Для =xy та xy маємо властивості ре-
флективності, симетричності, транзитив-
ності.
RfP) Кожний предикат вигляду =xx є
неспростовним;
кожний предикат вигляду xx є то-
тожно істинним, тобто xx = T.
SmP) Для кожного d
V
A маємо
=xy(d) = =yx(d) та xy(d) = yx(d).
TrP) Для кожного d
V
A маємо:
=xy(d) = T та =yz(d) = T =xz(d) = T;
xy(d) = T та yz(d) = T xz(d) = T.
Звідси отримуємо:
Наслідок 2. Кожний предикат ви-
гляду =xy & =yz =xz неспростовний;
кожний предикат вигляду
xy & yz xz тотожно істинний, тобто
xy & yz xz = T.
Для =xy та xy маємо властивість за-
міни рівних.
ER) Для кожних PPr
А
та d
V
A ма-
ємо:
=xy(d) = T , ,
, ,R ( )( ) R ( )( )u v u v
z x z yP d P d ;
xy(d) = T , ,
, ,R ( )( ) R ( )( )u v u v
z x z yP d P d .
Квантифікація предикатів строгої
рівності та слабкої рівності має (див. також
[9]) певні особливості.
Теорема 2. 1) x xy = Ey;
2) якщо |А| 2, то x xy = Т; якщо
|А| = 1, то x xy = Ey.
Доводимо п.1. x xy(d) = T існує
aА таке, що d(y) = a d(y) Ey(d) = T.
x xy(d) = F для кожного aА
невірно, що d(y) = a d(y) Ey(d) = F.
Доводимо п.2. x xy(d) = T іс-
нує aА таке, що невірно d(y) = a. Якщо
|А| 2, то це так; якщо |А| = 1, то це вимагає
d(y), тобто Ey(d) = T;
Теоретичні та методологічні основи програмування
35
x xy(d) = F для кожного aА
маємо d(y) = a. Якщо |А| 2, то це не так;
якщо |А| = 1, то це вимагає d(y), тобто
Ey(d) = T, звідки Ey(d) = F.
Наслідок 3. В L
QCEs
предикати-
індикатори є похідними.
Теорема 3. 1) x =xy = Ey ;
2) якщо |А| 2, то x =xy = Ey ;
якщо |А| = 1, то x =xy = Ey & .
Доводимо п.1. x (=xy)(d) = T іс-
нує aА таке, що d(y) = a d(y)
Ey(d) = T;
x =xy(d) = F d(y) та для кожного
aА невірно, що d(y) = a, а це неможливо;
x =xy(d) d(y). Таким чином,
x =xy = Ey .
Доводимо п.2. x =xy = F для
кожного aА маємо d(y)= a. Якщо |А| 2,
то це неможливо; якщо |А| = 1, то це озна-
чає d(y), тобто Ey(d) = T, звідки
Ey(d) = F.
x =xy(d) = T існує aА таке, що
d(y) та d(y) a. Якщо |А| 2, то це так за
умови d(y); якщо |А| = 1, то це неможливо.
x =xy(d) для кожного aА
маємо d(y) = a або d(y), причому немож-
ливо d(y)= a для кожного aА; якщо
|А| 2, то це буде при d(y); якщо |А| = 1, то
це буде при d(y).
Отже, x =xy(d) d(y).
Таким чином:
– якщо |А| 2, то x =xy(d) = T при
d(y) та x =xy(d) при d(y); звідси
x =xy = Ey .
– якщо |А| = 1, то x =xy(d) = F при
d(y) та x =xy(d) при d(y); звідси
x =xy = Ey & .
3. Мови LCE
Мови LE та мови LC єокремими
випадками мов LCE. Мови першопоряд-
кових LE детально описано в [9]. Мови
пропозиційних LC досліджено в [6], мови
першопорядкових LC введено в [7]. Тому в
даній роботі в першу чергу зосередимося
на дослідженні мов чистих першопоряд-
кових LCE.
Детально розглянемо мову L
QCEs
.
Алфавiт мови:
– множина V предметних імен (змінних),
– множина Ps предикатних символів,
– множина CsQLCEs = {, , ,v
xR x, , =ху}
символів базових композицій.
Дамо індуктивне визначення мно-
жини Fr формул мови:
– кожний рPs та кожний ху є фо-
рмулою; такі формули назвемо атомар-
ними;
– нехай , Fr; тоді Fr,
Fr, ,FrRv
x xFr, Fr
Для L
QCEs
задамо множину VT
V
імен, неістотних для всіх рPs – множину
тотально неістотних [5] імен
Для визначення множин гарантова-
но неістотних для формул імен таку про-
довжуємо до : Fr2
V
таким чином:
() = (Ф);
() = ()();
)(
,...,
,...,
1
1
n
n
vv
xx
R =
= ((){v1,...,vn})
\
{xi | vi(), 1,i n };
(x) = (){x};
( ) ( ) ;
(ху) = V \{x, y}.
Розширена сигнатура мови L
QCEs
– це
= (V, VT, CsQLCEs, Ps).
Якщо х(), то (див. [3]) ім’я х не-
істотне для формули .
Для довільної
Fr вводимо такі
позначення:
– () – це множина всіх рРs, які
входять до складу ;
Теоретичні та методологічні основи програмування
36
– nm() – це множина всіх xV, які
фігурують у формулax ;
–
)()( , fu() = VT \ nm().
Інтерпретуємо мову L
QCEs
на компо-
зиційних системах CS = (
V
A, Pr
V–A
, CQСEs).
Задаємо тотальне однозначне
I : Ps Pr
V–A
, яке продовжимо до відобра-
ження інтерпретації формул I : Fr Pr
V–A
:
I() = (I()),
I() = (I(), I()),
))((R)( IRI v
x
v
x ,
I(х) = х(I())
( ) ( ( )),I I
I(ху) = ху.
Трійку J = (CS, , I) назвемо інтерп-
ретацією мови L
QCEs
. Cкорочено інтерпре-
тації мови позначаємо як (A, I).
Предикат I() – значення формули
при інтерпретації J – позначимо J .
Предметне ім'я xV неістотне для
формули , якщо при кожній інтерпретації
J ім'я x неістотне для предиката J .
Мова L
QCE
визначається аналогічно
мові L
QCEs
лише замість символів ху пи-
шемо символи =ху .
Подібним чином описуємо мови ре-
номінативних логік L
RCEs
та L
RCE
, опус-
каючи пункти для х.
При визначенні мов L
QC
та L
RC
опу-
скаємо пункти, де фігурують символи пре-
дикатів рівності.
При визначенні мов L
QEs
, L
QE
, L
REs
,
L
RE
опускаємо пункти, де фігурують сим-
воли композиції предикатного доповнення.
Виділення в LCE підалгебр P-пре-
дикатів виділяє загальний клас R-інтер-
претацій та підклас P-інтерпретацій. Такі
класи інтерпретацій називають семантика-
ми, їх позначаємо R та P.
Нехай – деякий клас інтерпрета-
цій (семантика).
Формула неспростовна (частково
істинна) при інтерпретації J (позн. J
|=
),
якщо предикат J – неспростовний.
Формула неспростовна (частково
істинна) в , що позначаємо
|=
, якщо
J
|=
при кожній J.
Формула тотожно істинна при ін-
терпретації J (позн. J
|=id ), якщо преди-
кат J – тотожно істинний.
Формула тотожно істинна в
(позн.
|=id ), якщо J
|=id при кожній
J.
Якщо семантика зафіксована, то
замість
|=,
|=id пишемо |=, |=id .
Формула виконувана при інтер-
претації J, якщо предикат J – виконува-
ний.
Формула виконувана в , якщо
виконувана при деякій J.
Твердження 11. J
|=id J
|=
;
|=id |=
.
Приклад 2. Маємо
|= x = x та
|= x = y y = x (тут – R чи P).
Приклад 3. Маємо
|=id x x та
|=id x y y x (тут – R чи P).
Із твердження 8 отримуємо:
Твердження 12. Для кожної інтер-
претації J маємо
( ху)J = ;
( Ez)J = .
Із теореми 1 отримуємо:
Твердження 13. Для кожних Fr
та інтерпретації J маємо
( )J = T;
( )J = F;
( )J = .
Наслідок 4. Для кожної Fr
|=id (тут – R чи P).
Теоретичні та методологічні основи програмування
37
Отже, в LC та LCE в семантиках R
та P множини тотожно істинних формул та
неспростовних формул непорожні.
4. Відношення логічного наслідку
Для формалізації фундаментального
поняття логічного наслідку в логіках квазі-
арних предикатів запропоновано (див.
[10, 9]) низку відповідних відношень.
Спочатку задаємо відношення нас-
лідку для двох формул при фіксованій ін-
терпретації J.
1) Істиннісний, або T-наслідок J|=T :
J|=T T(J) T(J).
2) Хибнісний, або F-наслідок J|=F :
J|=F F(J) F(J).
3) Cильний, або TF-наслідок J|=TF :
J|=TF J|=T та J|=F .
4) Неспростовнісний, або IR-нас-
лідок J|=IR : J|=IR T(J)F(J) = .
5) Дуальний до IR, або DI-наслідок
J|=DI : J|=DI F(J)T(J) =
V
A.
Відповідні відношення логічного
наслідку в семантиці задаємо за схемою:
|= , якщо J|= для кожної J.
В загальному випадку логік квазі-
арних предикатів (реляційного типу) та LE
можна розглядати (див. [10, 9]) семантики
R, P, T, TS; при цьому семантики P та T
дуальні, семантики R та TS автодуальні.
Для зазначених відношень маємо
[10, 9] такі властивості:
– в TS-семантиці усі ці відношення
збігаються і стають єдиним відношенням
TS|= ;
–
P
|=DI =
T
|=IR =
R
|=IR =
R
|=DI = ;
–
P
|=IR =
T
|=DI =
TS
|= ;
–
P
|=T =
T
|=F ;
P
|=F =
T
|=T ;
–
P
|=TF =
T
|=TF;
R
|=T =
R
|=F =
R
|=TF.
Серед цих відношень маємо лише 5
різних:
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF.
При цьому:
–
P
|=T
P
|=F та
P
|=F
P
|=T;
–
R
|=TF
P
|=TF =
P
|=T
P
|=F;
–
P
|=T
P
|=IR та
P
|=F
P
|=IR .
Відношення логічного наслідку інду-
кують відношення логічної еквівалентності.
Відношення еквівалентності при ін-
терпретації J JT , JF , JTF , JIR визначає-
мо за такою схемою:
J , якщо J|= та J|= .
Відношення логічної еквівалентно-
сті
P
IR,
P
T,
P
F,
P
TF,
R
TF визначаємо так:
, якщо
|= та
|= .
При цьому:
J для кожної J.
Особливе значення має відношення
J TF . Це випливає з наступного:
JTF T(J) = T(J) та F(J) = F(J).
Отже, JTF означає:
J та J – це один і той же предикат.
Основою еквівалентних перетво-
рень формул є [10] теорема еквівалентнос-
ті. Вона формулюється для відношень
R
TF,
P
TF,
P
IR . Для
P
T та
P
F теорема невірна.
Теорема 4. Нехай ' отримано з
формули заміною деяких входжень
1, ..., n на 1, ..., n. Якщо 1
1, ...,
n
n, то
'.
Тут
одне з
R
TF,
P
TF,
P
IR.
Відношення логічного наслідку по-
ширюються на пари множин формул.
Нехай , Fr, J – інтерпретація.
Далі позначаємо
)( JT як T
(J),
)( JF як F
J),
)( JT як T
(J),
)( JF як F
(J).
є IR-наслідком при J (позн. J|=IR ),
якщо T
(J) F
(J) = .
є T-наслідком при J (позн. J|=T ),
якщо T
(J) T
(J).
Теоретичні та методологічні основи програмування
38
є F-наслідком при J (позн. J|=F ),
якщо F
(J) F
(J).
є TF-наслідком при J (позн. J|=TF ),
якщо J|=T та J|=F .
Відповідні відношення логічного
наслідку визначаємо за схемою:
|= , якщо J|= для кожної J.
Аналогом теореми 4 для множин
формул є теорема заміни еквівалентних.
Теорема 5. Нехай , тоді:
, |= , |= ;
|= , |= , .
Тут – одне з
R
TF,
P
TF,
P
IR; |= –
одне з відношень
R
|=TF,
P
|=TF,
P
|=IR.
Нагадаємо (див. [10, 9]) основні вла-
стивості відношень логічного наслідку для
множин формул. Надалі, якщо інше не за-
значене, |= – це одне з
R
|=TF,
P
|=TF,
P
|=T,
P
|=F,
P
|=IR.
M) Нехай та , тоді
|= |= (монотонність).
Декомпозиція формул:
L) , |= , |= .
R) |= , |= , .
L) , |= , |= та , |= .
R) |= , |= , , .
L) (), |= , , |= .
R) |= , () |= , та
|= , .
Для
P
|=IR також маємо (це невірно
[10] для
R
|=TF,
P
|=TF,
P
|=T,
P
|=F):
L) ,
P
|=IR
P
|=IR , .
R)
P
|=IR , ,
P
|=IR .
Властивості еквівалентних перетво-
рень, пов'язані з реномінацією, отриму-
ються на основі властивостей R, RI, RU,
RR, R, R (див. [10]). Кожна з них про-
дукує 4 відповідні властивості для відно-
шення логічного наслідку, коли виділена
формула чи її заперечення знаходиться у
лівій чи правій частині цього відношення.
Для першопорядкових логік маємо
[10] властивості елімінації кванторів, пер-
вісного означення та E-розподілу; вони
справджуються також для LE та LСE.
Властивості елімінації кванторів:
L) х, |= ,),( EzRx
z |=
за умови zfu(, , х));
RL) ),( xRu
v |= ,),(,
, EzR xu
zv |=
за умови ))(,,( xRfuz u
v ;
R) |= х, , Ez |= ),(x
zR
за умови zfu(, , х));
RR) |=
),( xRu
v
, Ez |=
),(,
,
xu
zvR
за умови ( , , ( ))u
vz fu R x ;
vR) , Ey |= х,
, Ey |= х, ),(x
yR ;
RvR) , Ey |= )(, xRu
v
, Ey |= )(),(, ,
, xu
yv
u
v RxR ;
vL) х, Ey, |=
,),(, EyRx x
y |= ;
RvL) ,),( EyxRu
v |=
,),(),( ,
, EyRxR xu
yv
u
v |= .
Властивості E-розподілу та первіс-
ного означення:
Ed) |= |= , Ey та Ey, |= ;
Ev) |= Ez, |= , де zfu(, ).
Гарантують (див. [10]) наявність то-
го чи іншого відношення логічного наслід-
ку властивості С, СL, СR, СLR.
Для усіх відношень маємо:
С) , |= , .
Додатково гарантують наявність
відповідного відношення такі властивості:
СL) , ,
P
|=T ;
СR)
P
|=F , , ;
Теоретичні та методологічні основи програмування
39
СLR) , ,
P
|=TF , , .
Властивості С, СL, СR, СLR справ-
джуються для LE та LСE.
Зауважимо, що відношення, які ми
позначаємо одним символом (напр.,
P
|=T),
різні в LE, LС, LСE, але з контексту буде
зрозуміло, про яке відношення йде мова.
5. Особливості відношень
логічного наслідку в LE та в LСE
Розглянемо особливості відношень
логічного наслідку в LE, пов’язані з наяв-
ністю предикатів рівності.
Опишемо властивості LEw, пов’я-
зані з предикатами слабкої рівності.
На основі Sm маємо властивості:
SmL) x = y, |= x = y, y = x, |= ;
SmR) |= , x = y |= , x = y, y = x.
Tr індукує властивості:
TrL) x = y, y = z, |=
x = y, y = z, x = z, |=
(тут |= – це
P
|=IR чи
P
|=T);
TrR) |= , x = y, y = z
|= , x = y, y = z, x = z
(тут |= – це
P
|=IR чи
P
|=F).
Справді, T(x = y) T(y = z) =
= T(x = y) T(y = z) T(x = z).
Теорема 6. TrL невірна для |=F;
TrR невірна для |=T.
Справді, для d = [x a, z b]
dF(x = y) F(y = z) = F(x = y & y = z);
проте dF(x = z), тому
dF(x = z) F(x = y) F(y = z) =
= F(x = y & y = z & x = z).
Звідси x = y & y = z
P
|F x = y & y = z & x = z.
Проте
P
|=F
P
|=T , тому
x = y y = z x = z
P
|T x = y y = z.
Водночас x = y & y = z
P
|=T x = y & y = z & x = z,
x = y y = z x = z
P
|=F x = y y = z.
Таким чином, транзитивність слаб-
кої рівності порушується для відношень
P
|=F та
P
|=T, тому й для
P
|=TF та
R
|=TF. Тому в
LEw ці відношення некоректні.
Наслідок 5. Для LEw коректним за-
лишається лише відношення
P
|=IR.
Властивість RD індукує властивості
реномінації рівності для відношення
P
|=IR.
RDL) ),( yxRu
v
P
|=IR x = y,
P
|=IR
за умови , { }x y u ;
),(,
, yxR xu
zv
P
|=IR z = y,
P
|=IR
за умови { }y u ;
),(
,,
,, yxR
yxu
uzv
P
|=IR z = u,
P
|=IR .
RDR) ),(| yxRu
vIR
P
P
|=IR , x = y за умови , { }x y u ;
),(| ,
, yxR xu
zvIR
P
P
|=IR , z = y
за умови { }y u ;
),(|
,,
,, yxR
yxu
uzvIR
P
P
|=IR , z = u.
Властивість ER індукує властивості
заміни рівних для відношення
P
|=IR :
ERL) ),(, ,
,
zu
xvRyx
P
|=IR
),(),(, ,
,
,
,
zu
yv
zu
xv RRyx
P
|=IR ;
ERR) ),(|, ,
,
zu
xvIR
P Ryx
),(),(|, ,
,
,
,
zu
yv
zu
xvIR
P RRyx .
Властивість Rf індукує спеціальну
умову наявності відношення
P
|=IR :
СRf)
P
|=IR x = x, .
Опишемо властивості LEs, пов’яза-
ні з предикатами строгої рівності. Далі |= –
це одне з
R
|=TF,
P
|=TF,
P
|=T,
P
|=F,
P
|=IR.
Для відношень типу T, F, TF зніма-
ти заперечення, переносячи з лівої час-
тини відношення у праву як і навпаки,
взагалі кажучи, не можна. Проте це можна
робити для предикатів строгої рівності:
ELR) |= x y, x y, |= та
x y, |= |= x y, ;
ERLR) ),(| yxRu
v
Теоретичні та методологічні основи програмування
40
|),( yxRu
v та
|),( yxRu
v ),(| yxRu
v .
Властивості, індуковані Sm та Tr:
SmS) x y, |= x y, y x, |= ;
TrS) x = y, y = z, |=
x = y, y = z, x = z, |= .
Властивість RD індукує властивості
реномінації рівності.
RDSL) |),( yxRu
v
, | x y за умови , { }x y u ;
|),(,
, yxR xu
zv , | z y
за умови { }y u ;
|),(
,,
,, yxR
yxu
uzv , | z u ;
RDSR) ),(| yxRu
v | , x y
за умови , { }x y u ;
),(| ,
, yxR xu
zv | , z y
за умови { }y u ;
),(|
,,
,, yxR
yxu
uzv | , z u .
Властивість ER індукує такі власти-
вості заміни рівних:
ERSL) |)(,, ,
,
zu
xvRyx
|)(),(,, ,
,
,
,
zu
yv
zu
xv RRyx ;
ERSR) ),(|, ,
,
zu
xvRyx
),(),(|, ,
,
,
,
zu
yv
zu
xv RRyx .
Властивість Rf індукує спеціальну
умову наявності кожного з відношень
R
|=TF,
P
|=TF,
P
|=T,
P
|=F,
P
|=IR:
СRfS) |= x x, .
Підсумовуючи, в LEw маємо такі
властивості відношення
P
|=IR :
– декомпозиції L, R, L, R;
– еквівалентних перетворень на осно-
ві R, RI, RU, RR, R, R;
– елімінації кванторів L, RL, vR,
RvR;
– E-розподілу Ed та первісного озна-
чення Ev;
– пов’язані з предикатами слабкої
рівності SmL, TrL, RDL, RDR, ERL, ERR;
– властивості С та СRf гарантованої
наявності відношення
P
|=IR .
Подібні властивості відношення
P
|=IR маємо в LEs; відмінність тільки в за-
міні символів =xy на символи xy, що дає
такі властивості:
– пов’язані з предикатами строгої рі-
вності SmS, TrS, RDSL, RDSR, ERSL, ERSR;
– властивості С та СRfS гарантованої
наявності відношення
P
|=IR .
Властивості відношень
R
|=TF,
P
|=TF,
P
|=T,
P
|=F в LEs:
– декомпозиції формул L, R, L,
R, L, R;
– еквівалентних перетворень на осно-
ві R, RI, RU, RR, R, R;
– елімінації кванторів L, RL, R,
RR, vR, RvR, vL, RvL;
– E-розподілу і первісного означення;
– пов’язані з предикатами строгої
рівності властивості ELR, ERLR, SmS, TrS,
RDSL, RDSR, ERSL, ERSR;
– властивості С, СL, СR, СLR, СRfS
гарантованої наявності відношення логіч-
ного наслідку.
Детальніше щодо виконання цих
властивостей щодо різних відношень:
– С, СL, СRfS для
P
|=T ;
– С, СR, СRfS для
P
|=F ;
– С, СLR, СRfS для
P
|=TF ;
– С, СRfS для
R
|=TF .
В LC та в LCE відношення логічно-
го наслідку вводимо так, як описано вище.
Водночас композиція предикатного допов-
нення має специфічні особливості, що ві-
дображається на властивостях відношень
логічного наслідку.
Теоретичні та методологічні основи програмування
41
В LC, тому і в LCE, змістовними є
лише R-семантика та P-семантика, тому
малозмістовними є відношення типу DI.
Для відношення
R
|=IR рефлексив-
ність порушується як в традиційних логі-
ках квазіарних предикатів, так і в LC, LE,
LCE. Справді, для довільного pPs маємо
p
Rс
|IR p (беремо JR таку, що pJ = ). То-
му вироджене відношення
R
|=IR ; далі не
розглядаємо.
Для LEw відношення типів T, F, TF
для пар формул нетранзитивні (теорема 6),
нетранзитивними вони залишаться і для
LСEw. Тому для LСEw коректним може
бути лише відношення
P
|=IR.
Відношення логічного наслідку в LC
детально досліджено в [8]. Зокрема, пока-
зано, що відношення
P
|=IR в LC коректно
ввести неможливо. Причиною цього є не-
можливість коректно задати умови деком-
позиції формул вигляду . Зумовлено це
тим, що декомпозиція формули вима-
гає подання області невизначеності фор-
мули через її області істинності та хиб-
ності за допомогою лише та . Як пока-
зано в [8], це неможливо.
Таким чином, для LC відношення
P
|=IR неадекватне. Це мотивує перехід від
відношення
P
|=IR до загальнішого відно-
шення |=IR
неспростовнісного логічного
наслідку за умов невизначеності. Відно-
шення |=IR
в LC досліджено в [6, 7].
Неадекватність відношення
P
|=IR в
LC робить його і неадекватним і в LCE.
Отже,
P
|=IR буде неадекватним в
LСEw та LСEs. Враховуючи, що в LСEw
відношення типів T, F, TF теж неадекватні,
LСEw до певної міри вироджена, для неї
може працювати лише відношення |=IR
.
Стисло опишемо відношення типів
T та F в LС та LСEs. Це відношення
P
|=T і
R
|=T, які також будемо позначати |=T, та
відношення
P
|=F і
R
|=F, які також познача-
тимемо |=F.
Для цих відношень в LС та LСEs
справджуються відповідні властивості де-
композиції формул, еквівалентних пере-
творень, елімінації кванторів, E-розподілу
та первісного означення, які мають місце
для традиційних логік квазіарних предика-
тів (див. [10]). Справджуються також на-
ведені в [10] умови, які гарантують наяв-
ність того чи іншого відношення логічного
наслідку. Водночас в LС з’являються (див.
[8]) нові властивості, пов’язані з компози-
цією предикатного доповнення.
Для відношень |=T додатково маємо
наступні властивості.
Умова гарантованої наявності |=T :
)C , |=T .
Декомпозиція формул типу :
LT) , |=T |=T , , .
RT) |=T ,
, |=T та , |=T .
El) |=T , |=T .
Властивість El – це фактично
елімінація .
Для відношень |=F додатково маємо
наступні властивості.
Умова гарантованої наявності |=F :
)C | ,F .
Декомпозиція формул типу :
RF) |=F , , , |=F .
LF) , |=F
|=F , та |=F , .
El) , |=F |=F .
Властивість El – це фактично елі-
мінація .
Як випливає з цих співвідношень,
для відношень типу |=T та типу |=F маємо
різні властивості декомпозиції формул ви-
гляду , їх не можна подати як спільну
властивість для відношень типу |=TF.
Це означає, що в LC відношення
R
|=T,
R
|=F,
R
|=TF різні, водночас в традицій-
ній логіці квазіарних предикатів маємо
R
|=T =
R
|=F =
R
|=TF.
Властивості декомпозиції формул
вигляду для відношень типу |=TF отри-
муємо, поєднуючи наведені вище відпові-
дні властивості для |=T та |=F : LT та El,
Теоретичні та методологічні основи програмування
42
RT та ,C C та LF, El та RF :
LTF) , |=TF
|=T , , та |=F ;
RTF) |=TF ,
, |=T та , |=T ;
LTF) , |=TF
|=F , та |=F , ;
RTF) |=TF ,
|=T та , , |=F .
Аналогічні властивості відношень
типів |=T та |=F, пов’язані з композицією
предикатного доповнення, маємо в LСEs.
Звідси, зокрема, випливає, що в в
LСEs усі відношення
P
|=T,
P
|=F,
P
|=TF,
R
|=T,
R
|=F,
R
|=TF є різними.
В LСEs також виконуються наведе-
ні вище властивості LEs, пов’язані з пре-
дикатами строгої рівності. Новими є від-
ношення, які пов’язують та предикати
строгої рівності.
Згідно твердження 12 для кожної
інтерпретації J маємо
T(( х у)J) = F(( х у)J) = .
Звідси умови гарантованої наявнос-
ті |=T та гарантованої наявності |=F :
LC ) х у, |=T ;
RC ) |=F , х у.
При взаємній заміні |=T та |=F маємо
властивості спрощення – елімінації ху :
LEl ) х у, |=F |=F ;
REl ) |=T , х у |=T .
Підсумовуючи, в LСEs маємо такі
властивості відношень
R
|=T,
R
|=F,
P
|=T,
P
|=F .
Спільні для
R
|=T,
R
|=F,
P
|=T,
P
|=F влас-
тивості:
– декомпозиції формул L, R,
L, R, L, R;
– еквівалентних перетворень на ос-
нові R, RI, RU, RR, R, R, R ;
– елімінації кванторів L, RL, R,
RR, vR, RvR, vL, RvL;
– пов’язані з предикатами строгої
рівності властивості ELR, ERLR, SmS, TrS,
RDSL, RDSR, ERSL, ERSR.
Для відношень |=T додатково маємо:
– властивості LT, RT, El де-
композиції формул типу ;
– властивість REl елімінації ху .
Властивості гарантованої наявності
відношення
P
|=T : С, СL, СRfS, ,C LC .
Властивості гарантованої наявності
відношення
R
|=T : С, СRfS, ,C LC .
Для відношень |=F додатково маємо:
– властивості RF, LF, El де-
композиції формул типу ;
– властивість LEl елімінації ху .
Властивості гарантованої наявності
відношення
P
|=F : С, СR, СRfS, ,C RC .
Властивості гарантованої наявності
відношення
R
|=F : С, СRfS, ,C RC .
Такі ж властивості відношень
R
|=T,
R
|=F,
P
|=T,
P
|=F справджуються в LС, але при
цьому ми опускаємо властивості, в яких
фігурують символи предикатів строгої рів-
ності.
Наявність в LC та в LСE композиції
предикатного доповнення дає змогу визна-
чити відношення логічного наслідку за
умови невизначеності. Для LC такі відно-
шення вивчались в [6–8]. Для LСE дослі-
дження відношень логічного наслідку за
умови невизначеності буде зроблено в нас-
тупних статтях.
Висновки
В роботі досліджено нові програм-
но-орієнтовані логічні формалізми – ком-
позиційно-номінативні логіки з предика-
тами рівності та композицією предикатно-
го доповнення, такі логіки названо LCE.
Можна виділити предикати слабкої рівно-
сті та строгої рівності, це дає LCE з преди-
катами слабкої рівності, які названо LCEw,
Теоретичні та методологічні основи програмування
43
та з предикатами строгої рівності, які на-
звано LCEs. LCE можна розглядати на
першопорядковому рівні та реномінатив-
ному рівні. Розглянуто композиційні алге-
бри LCE, досліджено властивості їх ком-
позицій, описано першопорядкові мови
цих логік. Основну увагу зосереджено на
вивченні властивостей, пов’язаних з пре-
дикатами рівності та композицією преди-
катного доповнення. Введено та дослідже-
но низку відношень логічного наслідку в
першопорядкових LCE, розглянуто їх осо-
бливості. Зокрема, встановлено певну ви-
родженість LCEw, для якої коректним є
лише відношення неспростовнісного логі-
чного наслідку за умов невизначеності.
Детальне дослідження відношень логічно-
го наслідку за умови невизначеності в LСE
буде зроблено в наступних роботах.
Властивості відношень логічного
наслідку є семантичною основою побудо-
ви в LСE відповідних першопорядкових
числень секвенційного типу. Таку побудо-
ву теж планується здійснити робити в на-
ступних роботах.
Література
1. Handbook of Logic in Computer Science /
Edited by S. Abramsky, Dov M. Gabbay and
T. S. E. Maibaum. – Oxford University Press,
Vol. 1–5. 1993–2000.
2. Hoare C. An axiomatic basis for computer
programming, Comm. 1969. ACM. 12(10).
P. 576–580.
3. Apt K. Ten years of Hoare’s logic: a survey –
part I, ACM Trans. Program. Lang. Syst. 3(4)
(1981). P. 431–483.
4. Ivanov I., Nikitchenko M. On the sequence
rule for the Floyd-Hoare logic with partial
pre- and post-conditions. In Proceedings of
the 14
th
International Conference on ICT.
2018. Vol. 2104. of CEUR Workshop Proc.
P. 716–724.
5. Ivanov I., Nikitchenko M. Inference Rules
for the Partial Floyd-Hoare Logic Based on
Composition of Predicate Complement,
Comm. in Computer and Information
Science, 2019. Vol. 1007. Springer, Cham,
P. 71–88.
6. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С., Мамедов Т.А. Пропозиційні логіки
часткових предикатів з композицією пре-
дикатного доповнення. Проблеми програ-
мування. 2019. № 1. C. 3–13.
7. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С. Чисті першопорядкові логіки квазіар-
них предикатів з композицією предикатно-
го доповнення. Dynamical systems
modelling and stability investigation: in-
ternational conference: proceeding. К., 2019.
C. 371–373.
8. Шкільняк О.С. Відношення логічного на-
слідку в логіках часткових предикатів з
композицією предикатного доповнення.
Проблеми програмування. 2019. № 3.
C. 11–27.
9. Нікітченко М.С., Шкільняк С.С. Чисті
першопорядкові квазіaрні логіки з преди-
катами рівності. Проблеми програмування.
2017. № 2. C. 3–23.
10. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С. Чисті першопорядкові логіки квазіар-
них предикатів. Проблеми програмування.
2016. № 2–3. C. 73–86.
References
1. ABRAMSKY, S., GABBAY, D. and
MAIBAUM, T. (editors). (1993–2000).
Handbook of Logic in Computer Science
Oxford University Press, Vol. 1–5.
2. HOARE, C. (1969). An axiomatic basis for
computer programming, Comm. ACM 12(10),
576–580, 1969.
3. APT, K. (1981). Ten years of Hoare’s logic: a
survey – part I, ACM Trans. Program. Lang.
Syst. 3(4), pp. 431–483.
4. IVANOV, I. and NIKITCHENKO, M.
(2018). On the sequence rule for the Floyd-
Hoare logic with partial pre- and post-
conditions. In Proceedings of the 14
th
International Conference on ICT. Vol 2104 of
CEUR Workshop Proc., pp. 716–724.
5. IVANOV, I. and NIKITCHENKO, M.
(2019). Inference Rules for the Partial
Floyd-Hoare Logic Based on Composition
of Predicate Complement. In
Communication. in Computer and
Information Science. Vol. 1007. Springer,
Cham, pp. 71-88.
6. NIKITCHENKO, M., SHKILNIAK, O.,
SHKILNIAK, S. and MAMEDOV, T. (2019).
Propositional logics of partial predicates with
composition of predicate complement. In
Problems in Progamming. No 1. P. 3–13 (in
ukr).
Теоретичні та методологічні основи програмування
44
7. NIKITCHENKO, M., SHKILNIAK, O. and
SHKILNIAK, S. (2019). Pure first-order
logics of quasiary predicates with the
composition of predicate complement. In
Proceedings of the XIX
h
International
Conference “Dynamical systems modelling
and stability investigation”, pp. 371–373 (in
ukr).
8. SHKILNIAK, O. (2019). Relations of logical
consequence in logics of partial predicates
with composition of predicate complement.
In Problems in Progamming. No 3 (in ukr).
9. NIKITCHENKO, M. and SHKILNIAK, S.
(2017). Pure first-order quasiary logics with
equality predicates. In Problems in
Progamming. No 2. P. 3–23 (in ukr).
10. NIKITCHENKO, M., SHKILNIAK, O. and
SHKILNIAK, S. (2016). Pure first-order
logics of quasiary predicates. In Problems in
Progamming. No 2–3. P. 73–86 (in ukr).
Одержано 10.06.2019
Про автора:
Шкільняк Степан Степанович,
доктор фізико-математичних наук,
професор, професор кафедри Теорії
та технології програмування.
Кількість наукових публікацій в
українських виданнях – понад 240,
у тому числі у фахових виданнях –
понад 100.
Кількість наукових публікацій в
зарубіжних виданнях – 22.
Scopus Author ID: 36646762300
h-індекс (Google Scholar): 7 (5 з 2014).
http://orcid.org/0000-0001-8624-5778.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 05 19.
http://orcid.org/0000-0001%20-8624-5778
|