Relations of logical consequence in logics of partial predicates with composition of predicate complement
In this paper we study software-oriented logics of partial predicates with new special non-monotonic operation (composition) of the predicate complement. We denote these logics by LC and composition of the predicate complement by . Such operations are used in various versions of the Floyd-Hoare prog...
Збережено в:
| Дата: | 2019 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2019
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/364 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-364 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/63/de0f48969ddb5f114452aee8d7b31763.pdf |
| spelling |
pp_isofts_kiev_ua-article-3642024-04-28T11:05:26Z Relations of logical consequence in logics of partial predicates with composition of predicate complement Отношения логического следствия в логиках частичных предикатов с композицией предикатного дополнения Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Shkilniak, O.S. logic; partial predicate; composition algebra; logical consequence UDC 004.42:510.69 логика; частичный предикат; композиционная алгебра; логическое следствие УДК 004.42:510.69 логіка; частковий предикат; композиційна алгебра; логічний наслідок УДК 004.42:510.69 In this paper we study software-oriented logics of partial predicates with new special non-monotonic operation (composition) of the predicate complement. We denote these logics by LC and composition of the predicate complement by . Such operations are used in various versions of the Floyd-Hoare program logic with partial pre- and post-conditions. We describe first order composition algebras and LC languages. For LC, a number of logical consequence relations (Pc|=T, Pc|=F, Rc|=T, Rc|=F, Pc|=TF, Rc|=TF, Pс|=IR) and logical consequence relations under the conditions of undefinedness (P|=T^, P|=F^, R|=T^, R|=F^, P|=TF^, R|=TF^) are specified. Properties of the defined relations are investigated, differences and the relationship between them are given. For the introduced relations, we describe the conditions for their guaranteed presence, the decomposition conditions for formulas and the properties of quantifier elimination. The theorem of elimination of the conditions of undefinedness for the relations |=T^ and |=F is proved. Thus, the relations P|=T^, P|=F^, R|=T^ and R|=F^ can be expressed by Pc|=T, Pc|=F, Rc|=T and Rc|=F respectively. However, it is shown that |=IR^ cannot be expressed by Pс|=IR. Moreover, it is impossible to define correctly the decomposition conditions for formulas for Pс|=IR. Properties of decomposition conditions for formulas are different for the relations |=T and |=F, therefore properties of decomposition and equivalent transformations must be specified indirectly through the corresponding properties of |=T and |=F. First order sequent calculi for the introduced logical consequence relations for LC and logical consequence relations under the conditions of undefinedness will be constructed in in the forthcoming articles.Problems in programming 2019; 3: 11-27 В работе исследованы программно-ориентированные логики частичных предикатов, названные LC. Характерной их особенностью является наличие новой операции (композиции) предикатного дополнения . Операции такого типа используются в различных вариантах программных логик Флойда-Хоара с частичными перед- и после-условиями. Описаны композиционные алгебры и языки LC. Предложен ряд отношений логического следствия в LC (типов |=T, |=F, |=TF, а также отношение Pс|=IR) и отношений логического следствия в условиях неопределенности (типов |=T^, |=F^, |=TF^). Исследованы свойства этих отношений, установлены соотношения между ними. Для предложенных отношений описаны условия их гарантированного наличия, приведены свойства декомпозиции формул и свойства элиминации кванторов. Для отношений типов |=T и |=F доказана теорема элиминации условий неопределенности. Это позволяет свести отношения P|=T^, P|=F^, R|=T^, R|=F^ к отношениям Pc|=T, Pc|=F, Rc|=T, Rc|=F. В то же время отношение|=IR^ невозможно свести к отношению Pс|=IR. Более того, для Pс|=IR невозможно корректно определить условия декомпозиции формул . Установленные свойства LC свидетельствуют о ее существенном отличии от традиционной логики квазиарных предикатов. Для предложенных отношений логического следствия в LC и отношений логического следствия в условиях неопределенности в последующих работах планируется построение первопорядковых исчислений секвенциального типа.Problems in programming 2019; 3: 11-27 Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої наявності, наведено властивості декомпозиції формул та елімінації кванторів.Problems in programming 2019; 3: 11-27 Інститут програмних систем НАН України 2019-08-21 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/364 10.15407/pp2019.03.011 PROBLEMS IN PROGRAMMING; No 3 (2019); 11-27 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 3 (2019); 11-27 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 3 (2019); 11-27 1727-4907 10.15407/pp2019.03 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/364/366 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 partial predicate composition algebra logical consequence UDC 004.42:510.69 |
| spellingShingle |
logic partial predicate composition algebra logical consequence UDC 004.42:510.69 Shkilniak, O.S. Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| topic_facet |
logic partial predicate composition algebra logical consequence UDC 004.42:510.69 логика частичный предикат композиционная алгебра логическое следствие УДК 004.42:510.69 логіка частковий предикат композиційна алгебра логічний наслідок УДК 004.42:510.69 |
| format |
Article |
| author |
Shkilniak, O.S. |
| author_facet |
Shkilniak, O.S. |
| author_sort |
Shkilniak, O.S. |
| title |
Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_short |
Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_full |
Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_fullStr |
Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_full_unstemmed |
Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_sort |
relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_alt |
Отношения логического следствия в логиках частичных предикатов с композицией предикатного дополнения Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| description |
In this paper we study software-oriented logics of partial predicates with new special non-monotonic operation (composition) of the predicate complement. We denote these logics by LC and composition of the predicate complement by . Such operations are used in various versions of the Floyd-Hoare program logic with partial pre- and post-conditions. We describe first order composition algebras and LC languages. For LC, a number of logical consequence relations (Pc|=T, Pc|=F, Rc|=T, Rc|=F, Pc|=TF, Rc|=TF, Pс|=IR) and logical consequence relations under the conditions of undefinedness (P|=T^, P|=F^, R|=T^, R|=F^, P|=TF^, R|=TF^) are specified. Properties of the defined relations are investigated, differences and the relationship between them are given. For the introduced relations, we describe the conditions for their guaranteed presence, the decomposition conditions for formulas and the properties of quantifier elimination. The theorem of elimination of the conditions of undefinedness for the relations |=T^ and |=F is proved. Thus, the relations P|=T^, P|=F^, R|=T^ and R|=F^ can be expressed by Pc|=T, Pc|=F, Rc|=T and Rc|=F respectively. However, it is shown that |=IR^ cannot be expressed by Pс|=IR. Moreover, it is impossible to define correctly the decomposition conditions for formulas for Pс|=IR. Properties of decomposition conditions for formulas are different for the relations |=T and |=F, therefore properties of decomposition and equivalent transformations must be specified indirectly through the corresponding properties of |=T and |=F. First order sequent calculi for the introduced logical consequence relations for LC and logical consequence relations under the conditions of undefinedness will be constructed in in the forthcoming articles.Problems in programming 2019; 3: 11-27 |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2019 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/364 |
| work_keys_str_mv |
AT shkilniakos relationsoflogicalconsequenceinlogicsofpartialpredicateswithcompositionofpredicatecomplement AT shkilniakos otnošeniâlogičeskogosledstviâvlogikahčastičnyhpredikatovskompoziciejpredikatnogodopolneniâ AT shkilniakos vídnošennâlogíčnogonaslídkuvlogíkahčastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ |
| first_indexed |
2024-09-25T04:02:58Z |
| last_indexed |
2024-09-25T04:02:58Z |
| _version_ |
1818527440257941504 |
| fulltext |
Теоретичні та методологічні основи програмування
© О.С. Шкільняк, 2019
ISSN 1727-4907. Проблеми програмування. 2019. № 3 11
УДК 004.42:510.69 https://doi.org/10.15407/pp2019.03.011
О.С. Шкільняк
ВІДНОШЕННЯ ЛОГІЧНОГО НАСЛІДКУ В ЛОГІКАХ
ЧАСТКОВИХ ПРЕДИКАТІВ З КОМПОЗИЦІЄЮ
ПРЕДИКАТНОГО ДОПОВНЕННЯ
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) преди-
катного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень
логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості
цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему
про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої
наявності, наведено властивості декомпозиції формул та елімінації кванторів.
Ключові слова: логіка, частковий предикат, композиційна алгебра, логічний наслідок.
Вступ
Розвиток інформаційних технологій
та розширення сфери їх застосування роб-
лять першочерговою задачу створення на-
дійних і ефективних програмних систем.
Недавні авіакатастрофи з літаками Boeing
737 MAX 8 яскраво це засвідчують. В ос-
нові таких систем лежить апарат матема-
тичної логіки (див., напр., [1]). Зазвичай це
класична логіка [2] предикатів та базовані
на ній спеціальні логіки. Проте класична
логіка має [3] принципові обмеження, які
ускладнюють її використання. Тому про-
блема побудови нових, програмно-орієнто-
ваних логічних формалізмів набуває особ-
ливої актуальності. Такими формалізмами
є композиційно-номінативні логіки (КНЛ)
часткових квазіарних предикатів. Описано
та досліджено [3–6] низку класів КНЛ на
різних рівнях абстрактності й загальності.
Важливим різновидом програмно-
орієнтованих логік, які успішно застосо-
вуються в системах верифікації програм, є
логіки Флойда-Хоара [7. Ці логіки вико-
ристовують тотальні перед- та після-умови
(предикати), тому запропоновано [8, 9] їх
розширення на випадок часткових преди-
катів. Введення спеціальної операції (ком-
позиції) предикатного доповнення [9 є
продуктивним напрямком такого розши-
рення. КНЛ часткових предикатів з компо-
зицією предикатного доповнення запропо-
новано в [10, їх названо LC. Дослідженню
пропозиційних LC присвячена робота [10.
Метою даної роботи є вивчення се-
мантичних властивостей першопорядкових
LC. Запропоновано низку відношень логіч-
ного наслідку в LC та відношень логічного
наслідку за умови невизначеності. Дослі-
джено властивості цих відношень, встано-
влено співвідношення між цими. Для від-
ношень типів |=T та |=F доведено теорему
про елімінацію умов невизначеності. Для
цих відношень описано умови їх гаранто-
ваної наявності, наведено властивості де-
композиції формул та елімінації кванторів.
Поняття, які тут не визначаються,
будемо тлумачити в сенсі [3, 5].
1. Kомпозиційні системи логік з
предикатним доповненням
Під V-A-квазіарним предикатом ро-
зуміємо часткову неоднозначну функцію
вигляду Р :
V
A {T, F}. Тут {T, F} – мно-
жина істиннісних значень,
V
A – множина
всіх V-A-іменних множин.
Множину всіх значень, які неодно-
значний предикат P може приймати на ар-
гументі (даному) d
V
А, позначаємо P[d].
В цій роботі розглядаємо неодно-
значні (недетерміновані) предикати реля-
ційного типу, або R-предикати.
Кожний R-предикат Q можна одно-
значно задати за допомогою 2-х множин:
– область істинності T(Q) = {d | TQ[d]};
– область хибності F(Q) = {d | FQ[d]}.
Oбласть невизначеності R-предика-
тa Q визначається через T(Q) та F(Q) так:
( ) ( ) ( ) ( ) ( )Q T Q F Q T Q F Q .
https://doi.org/10.15407/pp2019.03.0
Теоретичні та методологічні основи програмування
12
V-A-квазіарний R-предикат Q:
– частковий однозначний або P-пре-
дикат, якщо T(Q)F(Q) = ;
– тотальний, або T-предикат, якщо
T(Q)F(Q) =
V
A; тоді (Q) = .
Для P-предикатів пишемо Q(d),
якщо значення Q(d) визначене, та пишемо
Q(d), якщо значення Q(d) невизначене.
Тому для P-предикатів:
T(Q) = {d | Q(d) = T},
F(Q) = {d | Q(d) = F}.
Тоді ( )Q {d | Q(d)}.
Класи V-A-квазіарних R-предикатів
та P-предикатів позначимо Pr
V–A
та PrP
V–A
.
Маємо [5] 4 константних R-предикати T, F,
, : T(T) = F(F) =
V
А, T(F) = F(T) = ,
T() = F() = , T() = F() =
V
А.
Опишемо композиції R-предикатів.
Композиції пропозиційного рівня
називають логiчними зв’язками. За базові
логічні зв’язки R-предикатів візьмемо та
, вони задаються так:
T(P) = F(P); F(P) = T(P);
T(PQ) = T(P)T(Q); F(PQ) = F(P)F(Q).
Композиції , & є похідними, вони
виражаються через базові композиції , :
P&Q = (PQ); PQ = PQ.
Для R-предикатів ( ) ( );Q Q
( ) ( ( ) ( )) ( ( ) ( )).P Q P T Q Q T P
1-арна композиція реномінації
:R v
x Pr AV Pr AV задається умовою:
)](r[])[(R dPdP v
x
v
x .
Тут v
x r – операція реномінації [3, 5].
v
xR можна визначити через області
істинності та хибності предиката )(R Pv
x :
T ))((R Pv
x = {d | )()(r PTdv
x };
F ))((R Pv
x = {d | )()(r PFdv
x }.
Визначальними для першопорядко-
вих логік є 1-арні композиції квантифіка-
ції. За базову візьмемо x, задамо її так:
T(xP) =
Aa
PTaxdd
)}(|{ ;
F(xP) =
Aa
PFaxdd
)}(|{ .
Композиція х є похідною:
хР = хР.
Маємо )( xP
)()()()( xPFxPTxPFxPT .
Звідси (xP) =
Aa
PPFaxdd )}()(|{
.)}(|{
Aa
Paxdd
Зокрема, для P-предикатів маємо
(xQ) =
Aa
TaxdQd })(|{
.)}(|{
Aa
Paxdd
Таким чином, для P-предикатів:
xQ(d) Q(dx b) для деяко-
го bA та неможливо xQ(d) = T.
Характерна особливість LC – наяв-
ність спеціальної немонотонної 1-арної
композиції предикатного доповнення .
Композицію можна задати так:
( )T P = ,)()()()()( PFPTPFPTP
( )F P .
Тоді маємо ( ) ( ) ( )P T P F P .
Для P-предикатів задається так:
, якщо ( ) ,
( )( )
невизначене, якщо ( ) .
T P d
P d
P d
Отже, композиція немонотонна.
Класи P-предикатів та R-предикатів
замкнені щодо композицій , , , &,
,R v
x xQ, хР, .
Q є P-предикатом для довільного
QPr
V–A
, тому клас T-предикатів незамк-
нений щодо . Отже, для T-предикатів LC
не мають смислу.
Теоретичні та методологічні основи програмування
13
Тому розглядаємо загальний клас
LC – логіки R-предикатів з композицією
, та їх підклас LCP – LC P-предикатів.
LC пропозиційного, реномінативно-
го, чистого першопорядкового рівнів нази-
ваємо PLC, RLC, QLC. LC P-предикатів
відповідних рівнів називаємо PLCP, RLCP,
QLCP. Множини базових композицій PLC,
RLC, QLC – це множини CPLС ={ , , } ,
CRLС ={ , ,R , }v
x , CQLС ={ , ,R , , }v
x x .
Семантичною основою LC є компо-
зиційні предикатні системи вигляду
CS = (
V
A, Pr
V–A
, CLС), де CLС – множина ба-
зових композицій відповідного рівня. От-
же, маємо композиційні LC-системи: про-
позиційну (
V
A, Pr
V–A
, CPLС), реномінативну
(
V
A, Pr
V–A
, CRLС), чисту першопорядкову
(
V
A, Pr
V–A
, CQLС). Відповідно отримуємо
композиційні LC-алгебри R-предикатів:
реномінативну APLC = (Pr
V–A
, CPLС), рено-
мінативну ARLC = (Pr
V–A
, CRLС), чисту
першопорядкову AQLC = (Pr
V–A
, CQLС).
Клас P-предикатів замкнений щодо
, тому в APLC, ARLC, AQLC виділені
підалгебри APLCP, ARLCP, AQLCP з но-
сієм PrP
V–A
– композиційні LC-алгебри
P-предикатів пропозиційного, реномінатив-
ного, чистого першопорядкового рівнів.
Опишемо основні властивості ком-
позицій LС.
Не пов’язані з властивості пропо-
зиційних композицій, композицій реномі-
нації та квантифікації в LC аналогічні вла-
стивостям цих композицій у традиційних
логіках квазіарних предикатів (див. [3–5]).
На пропозиційному рівні властивос-
ті композиції описано в [10]. Зокрема:
P P ; P P ; P P .
Для P-предикатів додатково маємо
P P P .
Твердження 1. Маємо
( ) ( )F P T P ( ) ( ) ( )P T P F P ,
( ) ( )T P F P ,
( )P ( ) ( ) ( )P T P F P ;
(R ( ))v
xT P = ( (R ( )))v
xT P ,
(R ( ))v
x P = ( (R ( )))v
x P ,
(R ( ))v
xF P = ( (R ( )))v
xF P = .
Твердження 2. Властивість R -ди-
стрибутивності:
R ) R ( )v
x P R ( )v
x P .
Твердження 3. Маємо
( ) ( ) ( )xP T xP F xP ;
( ) ( )T xP xP ; ( )F xP .
Твердження 4. Дія композиції на
константні предикати T, F, , :
( ) T ; (T) (F) ( ) .
Отже, множини SR = {T, F, , } та
SP = {T, F, } замкнені щодо ,,R,, xv
x .
Тому можна виділити підалгебри
AQsC = (SR, CQLС) та AQsCP = (SP, CQLС)
алгебр AQLC та AQLCP. Аналогічні
aлгебри APsC, ARsC з носієм SR та APsCP,
ARsCP з носієм SP виділяємо на пропо-
зиційному та реномінативному рівнях; для
них маємо APsC APLC, ARsC ARLC,
APsCP APLCP, ARsCP ARLCP.
Опишемо мови логік з композицією
предикатного доповнення. Розглядаємо за-
гальний випадок першопорядкових LC.
Алфавiт мови:
– множина V предметних імен
(змінних),
– множина Ps предикатних
символів,
– множина CQLC ={ , , , , }v
xR x
символів базових композицій.
Задамо множину Fr формул мови.
Маємо Ps Fr, далі задаємо індуктивно:
, Fr , , , ,v
xR x Fr .
Розширена сигнатура мови QLC – це
= (V, VT, CQLC, Ps), де VT
V – множина
тотально неістотних [5] імен.
Теоретичні та методологічні основи програмування
14
Інтерпретуємо мову на композицій-
них системах CS = (
V
A, Pr
V–A
, CQLС).
Задаємо тотальне однозначне
I : Ps Pr
V–A
, яке продовжимо до відобра-
ження інтерпретації формул I : Fr Pr
V–A
:
I() = (I()), I() = (I(), I()),
( ) ( ( )),I I
))((R)( IRI v
x
v
x , I(х) = х(I()).
Інтерпретація мови сигнатури –
це J = (CS, , I); скорочено її позначаємо
(A, I). Предикат J() позначимо J .
Для довільної
Fr позначимо
() множину всіх рРs, які входять до
складу ; позначимо nm() множину
всіх xV, які фігурують у формулax .
Для формул мови QLC визначимо
множини гарантовано неістотних імен за
допомогою відображення : Fr2
V
так, як
для традиційних логік квазіарних предика-
тів [3, 5], додаючи пункт ( ) ( ) .
Для довільної
Fr задаємо
)()( , fu() = VT \ nm().
Подібним чином, опускаючи пунк-
ти для х, описуємо мову RLC.
При описі мови PLC опускаємо пу-
нкти для v
xR та х, а також поняття,
пов’язані з неістотністю імен.
Виділення класів предикатів виді-
ляє відповідні класи інтерпретацій, які на-
зивають [3, 5] семантиками. Зокрема, це
R-семантика, P-семантика, T-семантика.
Клас T-предикатів незамкнений що-
до , тому для LC T-семантика малозміс-
товна. Змістовними для LC є R-семантика
та P-семантика, їх позначаємо RС та PС.
Фіксуючи пропозиційний, реномі-
нативний, чистий першопорядковий рівні
розгляду, отримуємо семантики RPС та PPС,
RRС та PRС, RQС та PQС.
Властивості композицій LC можна
подати із використанням формул мови.
Наведемо для прикладу основні
властивості, пов’язані з реномінацією.
R) R()J = J ;
RI) J
v
xJ
vz
xz RR )()(,
, ;
RU) J
v
xJ
vz
xy RR )()(,
, , де z();
R) J
v
xJ
v
x RR )()( ;
R) J
v
xJ
v
xJ
v
x RRR )()()( ;
RR) J
w
y
v
xJ
w
y
v
x RRR )())(( ;
R )
( )v
x JR ( )v
x JR
R ) ( )v
x JR ( )v
x JR
Ren) J
y
zJ Rzy )()( , де z();
Rs) J
v
xJ
v
x yRyR )()( ,
де { , }y v x ;
R) J
y
z
v
xJ
v
x RzyR )()( ,
де ))(( yRfuz v
x .
2. Відношення
логічного наслідку в LC
На множинах формул мови LC мо-
жна визначити низку відношень логічного
наслідку. Зокрема, на мову LC природним
чином поширимо відомі [5] відношення
P
|=IR,
P
|=T,
P
|=F,
P
|=TF,
R
|=TF. Такі відношення
в LC будемо позначати
Pс
|=IR,
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF. При цьому істотні
особливості вносить нова композиція пре-
дикатного доповнення.
Нехай деяка Fr, нехай J – інтер-
претація. Далі позначаємо:
)( JT як T
(J),
)( JF як F
(J),
)( J як
(J),
)( JT як T
(J),
)( JF як F
(J),
)( J як
(J).
У випадку, коли = , маємо:
T
(J) = F
(J) =
(J) = ,
Теоретичні та методологічні основи програмування
15
T
(J) = F
(J) =
(J) =
V
A.
Нехай , Fr.
є T-наслідком при інтерпретації
J (позн. J|=T ), якщо T
(J) T
(J).
є F-наслідком при інтерпретації
J (позн. J|=F ), якщо F
(J) F
(J).
є TF-наслідком при інтерпрета-
ції J (позн. J|=TF ), якщо
J|=T та J|=F .
є IR-наслідком при інтерпрета-
ції J (позн. J|=IR ), якщо
T
(J) F
(J) = .
Відповідні відношення логічного -
наслідку в семантиці задаємо за схемою:
|= , якщо J|= для кожної J.
Приклад 1. Нехай Ps. Візьмемо
JRС таку: J = ; тоді T(J)F(J) =
V
A,
тому J|IR , звідки
Rс
|IR .
Приклад 1 узагальнимо так.
Твердження 5. Нехай формули в
та не мають входжень , тоді
Rс
|IR .
Справді, візьмемо JRС таку, що
J = для кожного (), тоді маємо
J|IR , звідки
Rс
|IR .
Приклад 2. Для кожних Fr та
JRС маємо ( )JF , ( )JT .
Звідси
Rс
|=F ,
Rс
|=T ,
Rс
|=IR ,
Rс
|=IR .
Приклад 3. Для кожних Fr та
JRС маємо T(J) ( )JT = ( J ) та
F(J) ( )JF = ( J ).
Звідси
Pс
|T та
Pс
|F ,
тому й
Rс
|T та
Rс
|F .
Таким чином, в LC відношення
Rс
|=IR,
Rс
|=T,
Rс
|=F,
Rс
|=TF різні, водночас в
традиційній логіці квазіарних предикатів
маємо
R
|=IR = та
R
|=T =
R
|=F =
R
|=TF. При
цьому в LC
R
|=IR , проте має дуже ви-
роджений характер: якщо в та немає
входжень , то
Rс
|IR .
Приклад 4. Нехай , Ps. Візьме-
мо I, JRС такі: I = , I = , J = ,
J = ; тоді маємо: , I|T , та
, J|F , .
Звідси маємо: ,
Rс
|T , ;
,
Rс
|F , ; ,
Rс
|TF , .
Зокрема: ,
Rс
|T та
Rс
|T , ;
,
Rс
|F та
Rс
|F , .
Приклад 5. Для кожних , Fr та
JPС маємо , J|=TF , .
Звідси ,
Pс
|=TF , .
Приклад 6. Для кожних , Fr та
JPС маємо , J |=T та J|=F , .
Звідси ,
Pс
|=T та
Pс
|=F , .
Приклад 7. Нехай , Ps. Візьме-
мо I, JPС такі: I = , I = F, J = T,
J = ; тоді ,
Pс
|F та
Pс
|T , .
Звідси ,
Pс
|F та
Pс
|T , .
Приклад 8. Для довільних , Fr
маємо ()
Pc
|=IR ().
Для кожної JPС маємо:
T( ()J) = T( J ),
F( ()J) = F( J ).
Звідси T( ()J) F( ()J) =
= T( J ) F( J ) = .
Приклад 9. Маємо
()
Pc
|T () та
()
Pc
|F ().
Візьмемо ,Ps та JPС такі:
T(J)F(J) T(J), T(J)F(J) F(J).
Наприклад, J = Ez, J = . Тоді:
T( ()J) = T(J), T( ()J) =
= T(J)(T(J)F(J)) T(J);
F( ()J) = F(J), F( ()J) =
= F(J)(F(J)T(J)) F(J). Звідси:
T( ()J) T( ()J) та
F( ()J) F( ()J).
Теоретичні та методологічні основи програмування
16
Зведемо результати щодо наявності
логічного наслідку в таблицю.
Таблиця. Наявність логічного наслідку
1 2 3 4 5 6 7
|=1 + + + + + + +
|=2 – + – + + – +
|=3 – – + + + + –
|=4 – – – + + – –
|=5 – – – – – + +
|=6 – – – – + – +
|=7 – – – – + + –
|=8 – – – – + – –
Тут введено скороченi позначення:
|=1:
Pс
|=IR, |=2:
Pс
|=T,
|=3:
Pc
|=F, |=4:
Pc
|=TF,
|=5:
Rc
|=IR, |=6:
Rc
|=T,
|=7:
Rc
|=F, |=8:
Rc
|=TF;
1: () |= (),
2: , , |= ,
3: |= , , ,
4: , , |= , , ,
5: , |= , ,
6: ,
|= , ,
7: , |= , .
Теорема 1. Між розглянутими від-
ношеннями логічного наслідку в LC маємо
такі співвідношення:
Rc
|=TF
Rc
|=T
Pc
|=T;
Rc
|=TF
Rc
|=F
Pc
|=F;
Rc
|=TF
Pc
|=TF
Pc
|=F;
Rc
|=TF
Pc
|=TF
Pc
|=T;
Pc
|=TF =
Pc
|=T
Pc
|=F;
Rc
|=TF =
Rc
|=T
Rc
|=F;
Pc
|=T
Pс
|=IR;
Pc
|=F
Pс
|=IR;
Rc
|=IR
Pс
|=IR;
Rc
|=IR
Pc
|=T;
Rc
|=IR
Pc
|=F;
Rc
|=T
Pc
|=F та
Pc
|=F
Rc
|=T;
Rc
|=F
Pc
|=T та
Pc
|=T
Rc
|=F.
Графічно це можна подати так (тут
замість вживаємо стрілку ):
Rc
|=T
Pc
|=T
Rc
|=TF
Pc
|=TF
Pс
|=IR
Rс
|=IR
Rc
|=F
Pc
|=F
Вироджене відношення
Rс
|=IR далі
розглядати не будемо.
Надалі, якщо інше не зазначене
окремо, будемо вживати такі позначення:
|= – одне з відношень
Pс
|=IR,
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF;
J|= – одне з J|=IR, J|=T, J|=F, J|=TF;
Pс
|= – одне з
Pс
|=IR,
Pс
|=T,
Pc
|=F,
Pc
|=TF;
Rc
|= – одне з
Rc
|=T,
Rc
|=F,
Rc
|=TF;
|=T – одне з
Pс
|=T,
Rc
|=T;
|=F – одне з
Pc
|=F,
Rc
|=F;
|=TF – одне з
Pс
|=TF,
Rc
|=TF.
Відношення логічного наслідку ін-
дукують відповідні відношення логічної
еквівалентності між двома формулами.
Нехай , Fr. Відношення еквіва-
лентності при інтерпретації J задаємо за
схемою: J , якщо J|= та J|= .
Особливе значення має відношення
JTF строгої еквівалентності:
Твердження 6. J TF J = J,
тобто J та J – один і той же предикат.
Cправді, J TF T( J ) = T(J)
та F( J ) = F(J).
Задаємо відношення
Pс
TF та
Rс
TF:
Pс
TF , якщо J TF для кожної JPС;
Rс
TF , якщо J TF для кожної JRС.
Згідно PС RС для всіх , Fr:
Rс
TF
Pс
TF .
Теоретичні та методологічні основи програмування
17
Водночас (приклад 4) невірно
Pс
TF
Rс
TF .
Основою еквівалентних перетво-
рень формул є теорема еквівалентності.
Для LC та LCP вона формулюється так:
Теорема 2. Нехай ' отримана з
заміною деяких входжень 1 , ..., n на
1 , ..., n .
Якщо 1
Rс
TF 1 , ..., n
Rс
TF n ,
то
Rс
TF ';
якщо 1
Pс
TF 1 , ..., n
Pс
TF n ,
то
Pс
TF '.
Теорема еквівалентності доводиться
індукцією за побудовою формули подібно
до відповідного доведення в традиційній
логіці квазіарних предикатів [3, 4].
Теорема заміни еквівалентних для
множин формул формулюється так.
Теорема 3. Нехай
Rc
TF , тоді:
, |= , |= ;
|= , |=|= , .
Нехай
Pc
TF , тоді:
,
Pc
|= ,
Pc
|= ;
Pc
|= ,
Pc
|=|= , .
Дослідимо відношення
Pс
|=IR,
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF.
Властивості, в яких не фігурує ком-
позиція предикатного доповнення, в ціло-
му аналогічні відповідним властивостям
[3, 5] відношень
P
|=IR,
P
|=T,
P
|=F,
P
|=TF
R
|=TF.
Властивості монотонності:
M) та ( |=
|= ).
Властивості декомпозиції формул:
L) , |= , |= .
R) |= , |= , .
L) , |= , |= та , |= .
R) |= , |= , , .
L) (), |= , , |= .
R) |= , ()
|= , та |= , .
Для
Pс
|=IR додатково маємо:
L) ,
Pс
|=IR
Pс
|=IR , .
R)
Pс
|=IR , ,
Pс
|=IR .
Властивості L та R невірні для
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF.
Новими для відношень в LC є спе-
цифічні властивості декомпозиції в яких
фігурує . Зокрема, стосовно
Pc
|=TF та
Rc
|=TF така декомпозиція можлива лише ок-
ремо для |=T та для |=F; для
Pс
|=IR коректно
зробити декомпозицію неможливо.
Теорема 4. Для відношення
Pс
|=IR
неможливо задати коректним способом
умови декомпозиції формул вигляду .
Нехай , , Fr; JPС.
Маємо , J|=IR
( ) ( ) ( )J J JT F
( ) ( ) ( ) ( )J J J JT F T F .
Нехай предикат утворено за допо-
могою та із деяких 1,…, n Тоді T()
та F() подаються через області істинності
й хибності предикатів 1,…, n за допомо-
гою лише та .
Шукаємо теоретико-множинну фу-
нкцію f(X, Y), будовану із та таку, що
за умови XY = маємо X Y L
f(X, Y) L = . Має виконуватись умо-
ва
( ) ( ) ( ) ( )J J J JT F T F
( ( ), ( )) ( ) ( )J J J Jf T F T F .
Проте із X, Y таких, що XY = , за
допомогою та можна отримати лише 4
різних множини: , X, Y, XY. Тому для
( ( ), ( ))J Jf T F маємо лише 4 варіанти: ,
T(J), F(J), T(J)F(J). Жоден з них не
влаштовує зазначену умову.
Декомпозиція формул необхідна
при побудові секвенційного числення, яке
формалізує відповідне відношення логіч-
ного наслідку. Для
Pс
|=IR така декомпозиція
вимагає явного виділення області невизна-
Теоретичні та методологічні основи програмування
18
ченості, адже умова для J|=IR не дає змоги
подати область невизначеності через обла-
сті істинності та хибності за допомогою
лише та . Явне виділення області неви-
значеності означає перехід від
Pс
|=IR до
більш загального відношення |=IR
неспро-
стовнісного логічного наслідку за умов не-
визначеності, що зроблено в [10].
Відношення
Pс
|=IR далі зазвичай роз-
глядати не будемо.
В подальшому використаємо такі
теоретико-множинні співвідношення:
A B L A B L (Set1)
A B L A B L (Set2)
Розглянемо властивості декомпози-
ції формул для
Pс
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F.
та можуть бути в лівій
частині та в правій частині відношення ти-
пу |=T та типу |=F – всього 8 комбінацій.
LT) , |=T |=T , , .
Використаємо Set1 та умову
( ) ( ) ( ) ( ) ( )T P T P F P T P T P .
Маємо , |=T для кожної J
T
(J) ( )JT T
(J) для кожної J
T
(J) ( ) ( )J JT T T
(J) для
кожної J T
(J) T
(J) T(J) T(J)
|=T , , .
RT) |=T ,
, |=T та , |=T .
Беремо до уваги Set2 та умову
( ) ( ) ( )T P T P T P .
Маємо |=T , для кожної J
T
(J) T
(J) ( )JT для кожної J
T
(J) T
(J) ( ) ( )J JT T для
кожної J T
(J) (T(J) T(J)) T
(J)
для кожної J T
(J) T(J) T
(J)
та T
(J) T(J) T
(J) , |=T
та , |=T .
RF) |=F , , , |=F .
Використаємо Set1 та умову
( ) ( ) ( ) ( )F P T P F P F P .
Маємо |=F
, для кож-
ної J F
(J) ( )F F
(J) для ко-
жної J F
(J) ( ) ( )J JF F F
(J)
F
(J) F
(J) F(J) F(J) для
кожної J , , |=F .
LF) , |=F
|=F , та |=F , .
Використаємо Set2 та умову
( ) ( ) ( )F P F P F P .
Маємо , |=F
для кожної
J F
(J) F
(J) ( )JF для ко-
жної J F
(J) F
(J) ( ) ( )J JF F
F
(J) (F(J) F(J)) F
(J) для
кожної J F
(J) F(J) F
(J) та
F
(J) F(J) F
(J) для кожної J
|=F , та |=F , .
Наступні властивості El та El
фактично є властивостями спрощення.
Для El та El беремо до уваги
( ) ( )T P F P .
El) |=T , |=T .
Маємо |=T
, для кожної
J T
(J) T
(J) ( )JT для кож-
ної J T
(J) T
(J) |=T .
El) , |=F |=F .
Маємо , |=F для кожної J
F
(J) F
(J) ( )JF для кожної J
F
(J) F
(J) |=F .
Залишились 2 комбінації, які дають
властивості гарантованої наявності відно-
шення логічного наслідку. Для всіх JRС
маємо ( ) ( )J JF T звідки:
)C | ,F .
)C , |=T .
Теоретичні та методологічні основи програмування
19
Зауважимо, що аналогічна до C
властивість для |=T – це властивість LT,
аналогічна до C властивість для |=F –
це властивість LF.
На відміну від J|=IR, для J|=T та J|=F
області невизначеності можна подати че-
рез області істинності та хибності за допо-
могою лише та , тобто можна еліміну-
вати області невизначеності. Це засвідчу-
ють LT, RT, RF, LF, El, El.
Для відношень
Rc
|=TF та
Pc
|=TF ситуа-
ція дещо інша. Це зумовлено асиметрич-
ною поведінкою композиції щодо обла-
стей істинності й хибності. Для відношень
типу |=T та типу |=F маємо різні властивості
декомпозиції формул вигляду , які не
можна подати як спільну властивість для
відношень типу |=TF. Для них маємо:
, |=TF , |=T та
, |=F |=T , , та |=F .
|=TF , |=T , та
|=F , |=T та , , |=F .
|=TF , |=T , та
|=F , , |=T та , |=T .
, |=TF , |=T та
, |=F |=F , та |=F , .
Тому при побудові секвенційних
числень, які формалізують
Rc
|=TF та
Pc
|=TF,
опираємось на базові визначення:
Rс
|=TF
Rс
|=T та
Rс
|=F ;
Pс
|=TF
Pс
|=T та
Pс
|=F .
Таким чином, секвенційне числення
для відношення |=TF має бути поєднанням
числень для відношень |=T та |=F :
для встановлення |=TF будуємо два ви-
ведення, перше виведення встановлює
|=T , а друге – |=F .
Розглянемо властивості, які гаранту-
ють наявність відношення логічного нас-
лідку. Для усіх розглянутих відношень ло-
гічного наслідку маємо властивість:
С) , |= , .
Для
Pс
|=IR С випливає з того, що
T(J) F(J) = для кожної JPС.
Для інших відношень використовує-
мо співвідношення T(J) L T(J) M
та F(J) L F(J) M.
Додатково гарантують наявність від-
повідного відношення такі властивості.
СL) , ,
Pс
|=T .
Випливає з того, що для кожної
JPС T(J) T(J) = T(J) F(J) = .
СR)
Pс
|=F , , .
Випливає з того, що для кожної
JPС F(J) F(J) = F(J) T(J) = .
СLR) , ,
Pс
|=TF , , .
Справді, для кожної JPС маємо
F(J) F(J) = F(J) F(J) = .
Маємо властивості гарантованої на-
явності відношення логічного наслідку:
– С, СL, C для
Pс
|=T ;
– С, СR, C для
Pс
|=F ;
– С, СLR для
Pс
|=TF ;
– С, C для
Rс
|=T ;
– С, C для
Rс
|=F ;
– С для
Rс
|=TF .
Описані властивості засвідчують іс-
тотну відмінність LC від традиційної логі-
ки квазіарних предикатів. Зокрема,
R
|=T,
R
|=F,
R
|=TF – це єдине відношення, а в LC
маємо різні відношення
Rс
|=T,
Rс
|=F,
R
|=TF. В
LC відношення
Pс
|=IR є некоректним.
Розглянемо пов’язані з реномінаці-
єю властивості еквівалентних перетворень
для відношень логічного наслідку в LC. Їх
доведення базується на теоремі 3. Кожна з
наведених вище властивостей R, RI, RU,
RR, R, R, ,R R, Rs продукує 4 відпо-
відні властивості для відношень
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F, коли виділена формула чи її за-
перечення знаходиться у лівій чи правій
частині цього відношення. Ці властивості
формулюються однотипно.
Наведемо тут властивості, індукова-
ні ,R інші властивості формулюються
Теоретичні та методологічні основи програмування
20
аналогічно відповідним властивостям [5]
для
P
|=T,
P
|=F,
R
|=TF.
Нехай Fr; , Fr; нехай |= –
одне з
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F.
R L) ( ),v
xR |= ( ),v
xR |= .
R R) |= , ( )v
xR |= , ( )v
xR .
R L) ( ),v
xR |=
( ),v
xR |= .
R R) |= , ( )v
xR
|= , ( )v
xR .
Для відношень типу |=TF властивос-
ті еквівалентних перетворень теж вірні,
проте їх задаємо опосередковано, через ві-
дповідні властивості для відношень типу
|=T та типу |=F. При цьому враховуємо:
|=TF |=T та |=F .
Властивості елімінації кванторів, E-
розподілу та первісного означення для від-
ношень
Pс
|=T,
Rс
|=T,
Pс
|=F,
Rс
|=F форму-
люються та доводяться аналогічно відпо-
відним властивостям [5] для відношень
P
|=T,
P
|=F,
R
|=TF .
Теорема 5. Нехай Fr; , Fr;
тоді:
L) за умови zfu(, , х)) маємо
х, |= ,),( EzR x
z |= ;
RL) за умови ))(,,( xRfuz u
v
( ), u
vR x |= ,),(,
, EzR xu
zv |= ;
R) за умови zfu(, , х)) маємо
|= х, , Ez |= ),(x
zR
RR) за умови ))(,,( xRfuz u
v
|=
),( xRu
v , Ez |=
,
, ( ),u x
v zR
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 |= .
Теорема 6. Для , Fr маємо:
Ed) |= |= , Ey та Ey, |= .
Ev) |= Ez, |= , де zfu(, ).
3. Відношення логічного наслідку
за умов невизначеності
Наявність в LC нової композиції
предикатного доповнення мотивує до роз-
гляду нових відношень логічного наслідку,
які враховують особливості цієї компози-
ції. Такими є відношення логічного наслід-
ку за умови невизначеності.
Узагальненням відношення
P
|=IR є
досліджене в [10] відношення |=IR
неспро-
стовнісного логічного наслідку за умов не-
визначеності. Нехай , U, Fr.
є неспростовнісним наслідком
за умов невизначеності U при інтерпрета-
ції J, що позначимо U / J|=IR
, якщо
T
(J)
(UJ) F
(J) = .
є неспростовнісним логічним
наслідком за умов невизначеності U, що
позначимо U / |=IR
, якщо U / J|=IR
для кожної інтерпретації JPС.
Якщо U = , то отримуємо
визначення відношення
Pс
|=IR .
Подібне вироджене відношення
R
|=IR
, яке відповідає виродженому відно-
шенню
Rс
|=IR, тут розглядати не будемо.
Узагальненнями відомих [3, 5] від-
ношень типу |=T, |=F та |=TF для традицій-
них логік квазіарних предикатів є пропо-
новані в цій роботі відношення істиннісно-
го хибнісного та строгого логічного нас-
лідку за умов невизначеності. Ми вводимо:
– відношення
P
|=T
логічного T-нас-
лідку в LPC за умов невизначеності;
– відношення
P
|=F
логічного F-нас-
лідку в LPC за умов невизначеності;
Теоретичні та методологічні основи програмування
21
– відношення
P
|=TF
логічного TF-на-
слідку в LPC за умов невизначеності;
– відношення
R
|=T
логічного T-нас-
лідку в LC за умов невизначеності;
– відношення
R
|=F
логічного F-нас-
лідку в LC за умов невизначеності;
– відношення
R
|=TF
логічного FT-на-
слідку в LC за умов невизначеності.
Неформально те, що є T-наслід-
ком за умови невизначеності U при ін-
терпретації J, має означати: “для кожного
d
V
A якщо d
(UJ), то (dT
(J)
dT
(J))”. Це рівносильне наступному:
“для кожного d
V
A якщо d
(UJ)
та dT
(J) то dT
(J)”.
Te, що є F-наслідком за умови
невизначеності U при інтерпретації J, має
означати: “для кожного d
V
A якщо
d
(UJ), то (dF
(J) dF
(J))”.
Це рівносильне: “для кожного
d
V
A якщо d
(UJ) та dF
(J) то
dF
(J)”.
Te, що є TF-наслідком за умов
невизначеності U при інтерпретації J, має
означати: “для кожного d
V
A якщо
d (UJ), то (dT
(J) dT
(J)) та
(dF
J) dF
(J))”.
Це рівносильне: “для кожного d
V
A
якщо d
(UJ) та dT
(J) то dT
(J) та
якщо d
(UJ) та dF
(J) то dF
(J))”.
Приходимо до наступних визна-
чень.
є T-наслідком за умови невизна-
ченості U при інтерпретації J, якщо
T
(J)
(UJ) T
(J).
Це позначимо U / J|=T
.
є F-наслідком за умови невизна-
ченості U при інтерпретації J, якщо
F
(J)
(UJ) F
(J).
Це позначимо U / J|=F
.
є TF-наслідком за умови неви-
значеності U при інтерпретації J, якщо
U / J|=T
та U / J|=F
.
Це позначимо U / J|=TF
.
Якщо U = , то маємо визначення
відношень J|=T , J|=F , J|=TF в LC.
Далі визначаємо традиційно.
є логічним T-наслідком за
умови невизначеності U в семантиці PС,
що позначимо U /
P
|=T
, якщо
U / J|=T
для кожної JPС.
є логічним F-наслідком за
умови невизначеності U в семантиці PС,
що позначимо U /
P
|=F
, якщо
U / J|=F
для кожної JPС.
є логічним TF-наслідком за
умови невизначеності U в семантиці PС,
що позначимо U /
P
|=TF
, якщо
U / J|=TF
для кожної JPС.
є логічним T-наслідком за
умови невизначеності U в семантиці RС,
що позначимо U /
R
|=T
, якщо
U / J|=T
для кожної JRС.
є логічним F-наслідком за
умови невизначеності U в семантиці RС,
що позначимо
R
|=F
, якщо U / J|=F
для кожної JRС.
є логічним TF-наслідком за
умови невизначеності U в семантиці RС,
що позначимо U /
R
|=TF
, якщо
U / J|=TF
для кожної JRС.
Якщо U = , то маємо визначення
Pс
|=T,
Pс
|=F,
Pс
|=TF,
Rс
|=T,
Rс
|=F,
Rс
|=TF.
Твердження 7. U /
P
|=TF
U /
P
|=T
та U /
P
|=F
;
U /
R
|=TF
U /
R
|=T
та
U /
R
|=F
.
Твердження 8. Для S Fr та JPС
T
(SJ) F
(SJ) = та F
(SJ) T
(SJ) = .
Звідси як наслідок отримуємо
Твердження 9. Для довільних
, U, Fr та JPС маємо:
U / J|=T
U / J|=IR
;
U / J|=F
U / J|=IR
.
Справді, згідно твердження 8:
Теоретичні та методологічні основи програмування
22
T
(J)
(UJ) T
(J)
T
(J)
(UJ) F
(J) = ;
F
(J)
(UJ) F
(J)
T
(J)
(UJ) F
(J) = .
Твердження 10. Беручи до уваги
приклади 4–7, маємо наступні властивості:
1) U / |=IR
, та U / , |=IR
;
2)
Pс
|T , та ,
Pс
|F , тому
U /
P
|T
, та U / ,
P
|F
;
3) U / ,
P
|=T
, та
U / ,
P
|=F
, , тому
U / ,
P
|=TF
, ;
4) U / ,
R
|T , ;
U / ,
R
|F
, ;
U / ,
R
|TF
, .
Теорема 7. Маємо співвідношення:
R
|=TF
R
|=T
P
|=T
;
R
|=TF
R
|=F
P
|=F
;
R
|=TF
P
|=TF
P
|=F
;
R
|=TF
P
|=TF
P
|=T
;
P
|=T
|=IR
;
P
|=F
|=IR
;
R
|=T
P
|=F
та
P
|=F
R
|=T
;
R
|=F
P
|=T
та
P
|=T
R
|=F
.
Графічно це можна подати так (тут
замість вживаємо стрілку ):
R
|=T
P
|=T
R
|=TF
P
|=TF
|=IR
R
|=F
P
|=F
Таким чином, співвідношення між
відношеннями |=IR
,
P
|=T
,
P
|=F
,
P
|=TF
,
R
|=T
,
R
|=F
,
R
|=TF
ідентичні співвідношен-
ням між відношеннями
Pс
|=IR,
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF.
Сформулюємо теорему заміни екві-
валентних для відношень |=T
, |=F
, |=TF
.
Теорема 8. 1) Нехай
P
TF , тоді
маємо (
P
|= – це
P
|=T
,
P
|=F
чи
P
|=TF
):
U / ,
P
|= U / ,
P
|= ;
U /
P
|= , U /
P
|= , ;
U, /
P
|= U, /
P
|= .
2) Нехай
R
TF , тоді маємо (
R
|= –
це
R
|=T
,
R
|=F
чи
R
|=TF
):
U / ,
R
|= U / ,
R
|= ;
U /
R
|= , U /
R
|= , ;
U, /
R
|= U, /
R
|= .
Дослідимо властивості відношень
P
|=T
,
P
|=F
,
P
|=TF
,
R
|=T
,
R
|=F
,
R
|=TF
.
Особливості цих відношень прояв-
ляються вже на пропозиційному рівні, то-
му в першу чергу розглядаємо властивості
пропозиційного рівня.
Для множини формул Fr вико-
ристаємо позначення
= { | }.
Позначимо
)( JT як T
(
J),
)( JF як F
(
J),
)( J як
(
J), ( )JT
як T
(
J),
)( JF
як F
(
J),
)( J як
(
J).
Маємо )()()( SFSTS . Звідси
UU
))()(()()U(
JJJJ FT
.)()()()(
UUUU
JJJJ FTFT
Таким чином, для R-предикатів:
UU
)()()U(
JJJ TT
UU
)()(
JJ FF .
Звідси визначальне твердження:
Теоретичні та методологічні основи програмування
23
Теорема 9. Відношення J|=T
можна
звести до J|=T ; відношення J|=F
можна
звести до J|=F .
Для довільних , U, Fr та J має-
мо (тут s означає “ згідно Set1”):
U / J|=T
T
(J)
(UJ) T
(J)
T
(J)
UU
)()(
JJ TT T
(J) s
T
(J) T
(J)
UU
)()(
JJ TT
T
(J) T
(J) T
(UJ) T
(
UJ)
J|=T , U,
U;
U / J|=F
F
(J)
(UJ) F
(J)
F
(J)
UU
)()(
JJ FF F
(J)s
F
(J) F
(J)
UU
)()(
JJ FF
F
(J) F
(J) F
(UJ) F
(
UJ)
, U,
U J|=F .
Подібним способом отримуємо за-
гальніші твердження:
W, U / J|=T
W / J|=T
, U,
U;
W, U / J|=F
W / , U,
U J|=F
.
Ми отримали фундаментальну тео-
рему про елімінацію умов невизначеності:
Теорема 10.
W, U /
P
|=T
W /
P
|=T
, U,
U;
W, U /
R
|=T
W /
R
|=T
, U,
U;
W, U /
P
|=F
W / , U,
U
P
|=F
;
W, U /
R
|=F
W / , U,
U
R
|=F
.
Як наслідок отримуємо: відношення
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
можна цілком звес-
ти до відношень
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F.
Наслідок 1.
U /
P
|=T
Pc
|=T , U,
U;
U /
R
|=T
Rc
|=T , U,
U;
U /
P
|=F
, U,
U
Pc
|=F ;
U /
R
|=F
, U,
U
Rc
|=F .
Теорема 10 дає змогу сформулюва-
ти властивості елімінації умов невизначе-
ності у відношеннях
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
:
ElUT) W,U /
P
|=T
W /
P
|=T
, U,
U;
W, U /
R
|=T
W /
R
|=T
, U,
U;
ElUF) W,U /
P
|=F
W / , U,
U
P
|=F
;
W, U /
R
|=F
W / , U,
U
R
|=F
.
Таким чином, від відношень
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
можна перейти до відно-
шень
Pс
|=T,
Pс
|=F,
Rс
|=T,
Rс
|=F.
Дещо складніша ситуація із відно-
шеннями
P
|=TF
та
R
|=TF
. Маємо:
U / |=TF
U / |=T
та |=F
|=T , U,
U та , U,
U |=F
.
Звідси:
Наслідок 2. U /
P
|=TF
Pс
|=T , U,
U та , U,
U
Pс
|=F
.
U /
R
|=TF
Rс
|=T , U,
U та , U,
U
Rс
|=F
.
Отже, відношення типу |=TF
можна
звести лише до сукупності відношень типу
|=T та типу |=F, а не до єдиного відношення
типу |=TF. Те ж саме було для
Pc
|=TF та
Rc
|=TF: проведення декомпозиції формул
вимагає подання
Rc
|=TF через
Rc
|=T та
Rc
|=F, а
Pc
|=TF – через
Pc
|=T та
Pc
|=F.
Підсумовуючи, отримуємо:
Теорема 11. Відношення
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
та
P
|=TF
,
R
|=TF
можна
промоделювати за допомогою
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F, усунувши умови невизначенос-
ті.
Водночас для відношення |=IR
не-
можливо таким способом усунути умови
невизначеності і тим самим промоделюва-
ти |=IR
за допомогою
Pс
|=IR. Це фактично
вже випливає з теореми 4: для відношення
Pс
|=IR неможливо задати коректним спосо-
бом умови декомпозиції формул вигляду
. Доведення неможливості моделюван-
ня |=IR
за допомогою
Pс
|=IR подібне до до-
ведення теореми 4:
Теоретичні та методологічні основи програмування
24
Нехай , , Fr; JPС. Маємо
/ J|=IR
T(J) F(J) (J) =
T(J) F(J) ( ) ( )J JT F
Нехай предикат утворено за до-
помогою та із деяких 1,…, n Тоді
T() та F() подаються через області іс-
тинності й хибності предикатів 1,…, n за
допомогою лише та . Проте із множин
X, Y таких, що XY = , за допомогою
та можна отримати лише 4 різних мно-
жини: , X, Y, XY. Нехай f(X, Y) – будо-
вана із та така теоретико-множинна
функція, що за умови XY = маємо
L X Y L f(X, Y) = . Має ви-
конуватись наступна умова: / J|=IR
T(J) F(J) ( ) ( )J JT F
T(J) F(J) ( ( ), ( ))J Jf T F = . Проте
для f(T(J), F(J)) маємо лише 4 варіанти:
, T(J), F(J), T(J)F(J). Жоден з них
не влаштовує нашу умову. Таким чином:
Теорема 12. В LC відношення |=IR
не можна звести до відношення
Pс
|=IR.
Укажемо основні властивості відно-
шень
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
,
P
|=TF
,
R
|=TF
.
Надалі, якщо інше не зазначене окремо:
|=
– одне з
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
;
|=T
– одне з
P
|=T
,
R
|=T
;
|=F
– одне з
P
|=F
,
R
|=F
;
|=TF
– одне з
P
|=TF
,
R
|=TF
.
Із визначень отримуємо властивості
монотонності M:
M) Нехай , U W, та ;
тоді U / |=
W / |=
.
Маємо такі властивості гарантова-
ної наявності логічного наслідку.
С) U / , |=
, .
)C U / , |=T
.
)C U / |=F
, .
Властивість С випливає з того що
T(J)L T(J)M, F(J)L F(J)M.
В силу T( J) = F( J) =
умова T( J) T
(J)
(UJ) T
(J)
гарантована, звідки випливає C .
Властивість C випливає з того,
що ( )JF , звідки маємо гарантова-
не F
(J)
(UJ) ( )JF F
(J).
Додатково гарантують наявність ві-
дповідного відношення такі властивості.
СL) U / , ,
P
|=T
; це рівно-
сильне такому: , ,
Pс
|=T , U,
U;
СR) U /
P
|=F
, , ; це рівно-
сильне такому: , U,
U
Pс
|=F , , .
Властивості С, ,C ,C СL, СR
вже були сформульовані для відношень
логічного наслідку в LC, тут вони узагаль-
нені для відношень логічного наслідку за
умов невизначеності.
Властивості декомпозиції логічних
зв'язок аналогічні відповідним властивос-
тям для відношень
P
|=T,
P
|=F,
P
|=TF,
R
|=TF
традиційної логіки квазіарних предикатів
та наведеним вище відповідним властиво-
стям для
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF ; вони виконуються для усіх відно-
шень
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
,
P
|=TF
,
R
|=TF
.
L) U / , |=
U / , |=
.
R) U / |=
, U / |=
, .
L) U / , |=
U / , |=
та U / , |=
.
R) U / |=
, U / |=
, , .
L) U / (), |=
U / , , |=
.
R) U / |=
, ()
U / |=
, та U / |=
, .
Для |=IR
додатково маємо [10] вла-
стивості L та R. Ці властивості невірні
Теоретичні та методологічні основи програмування
25
для
Pс
|=T,
Pc
|=F,
Pc
|=TF,
Rc
|=T,
Rc
|=F,
Rc
|=TF та
для
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
,
P
|=TF
,
R
|=TF
.
Для
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
власти-
вості декомпозиції, в яких фігурує ,
аналогічні наведеним вище відповідним
властивостям для
Pс
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F.
LT) U / , |=T
U / |=T
, , ;
RT) U / |=T
,
U / , |=T
та U / , |=T
;
RF) U / |=F
,
U / , , |=F
;
LF) U / , |=F
U / |=F
, та U / |=F
, ;
El) U / |=T
, U / |=T
;
El) U / , |=F
U / |=F
.
Властивості El та El – це влас-
тивості спрощення, елімінації .
Доведення цих властивостей зво-
диться до елімінації умов невизначеності
згідно теореми 10, застосування одно-
йменних властивостей для відношень логі-
чного наслідку в LC та застосування теоре-
ми 10 в зворотному порядку. Наведемо для
прикладу доведення LT та LF.
Маємо U / , |=T
(теоре-
ма 10) , |=T , U,
U ( LT в LC)
|=T , U,
U, , (теорема 10)
U / |=T
, , .
Маємо U / , |=F
(теоре-
ма 10) , , U,
U |=F ( LF в LC)
, U,
U |=F , та , U,
U |=F ,
(теорема 10) U / |=F
, та
U / |=F
, .
Для всіх відношень
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
можна сформулювати:
*C ) U, / |=
, ;
*C ) U, / , |=
.
Для |=F
властивість *C – окремий
випадок C ; для |=T
*C є похідною від
ElUT, RT, С. Для |=T
властивість *C –
окремий випадок C ; для |=F
ця влас-
тивість є похідною від ElUF, LF, С.
Властивості декомпозиції формул
вигляду різні для відношень типу |=T
та типу |=F
, тому для відношень типу |=TF
властивості декомпозиції не можна
подати як спільну властивість для відно-
шень типу |=TF.
Проте |=TF
|=T
та |=F
,
тому властивості декомпозиції та гаранто-
ваної наявності логічного наслідку для від-
ношень типу |=TF
можна задати опосеред-
ковано, через відповідні властивості для
відношень типу |=T
та типу |=F
.
Властивості, в яких фігурує ,
істотно різні для |=IR
,
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
,
P
|=TF
,
R
|=TF
. Це ще раз засвідчує
відмінність усіх зазначених відношень.
Пов’язані з реномінацією властиво-
сті еквівалентних перетворень для відно-
шень
P
|=T
,
R
|=T
,
P
|=F
,
R
|=F
подібні до від-
повідних властивостей еквівалентних пе-
ретворень для відношень
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F . Їх доведення базується на теоремі 8.
Кожна з властивостей R, RI, RU, RR, R,
R, R , R, Rs дає 6 відповідних власти-
востей для
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
, коли
виділена формула чи її заперечення знахо-
диться у лівій чи правій частині цього від-
ношення або входить до умови невизначе-
ності. Враховуючи властивості ElUT та
ElUF елімінації умови невизначеності, явно
виписувати 2 випадки, коли виділена фор-
мула чи її заперечення входить до умови
невизначеності, немає потреби, тому за-
лишаються 4 випадки. Наведемо для прик-
ладу властивості, індуковані, R .
Нехай , Fr; , U, Fr; |=
–
одне з
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
.
R L) U / ( ),v
xR |=
Теоретичні та методологічні основи програмування
26
U / ( ),v
xR |=
;
R R) U / |=
, ( )v
xR
U / |=
, ( )v
xR ;
R L) U / ( ),v
xR |=
U / ( ),v
xR |=
;
R R) U / |=
, ( )v
xR
U / |=
, ( )v
xR .
Для відношень типу |=TF
властиво-
сті еквівалентних перетворень можна зада-
ти опосередковано, через відповідні влас-
тивості для відношень типу |=T
та |=F
.
Властивості елімінації кванторів,
E-розподілу та первісного означення для
відношень
P
|=T
,
R
|=T
,
P
|=F
,
R
|=F
подібні
до відповідних властивостей для відно-
шень
Pс
|=T,
Rс
|=T,
Pс
|=F,
Rс
|=F, сформульова-
них в теоремах 5 та 6.
Наведемо для прикладу властивості
L та RvR.
L) за умови zfu(U, , , х))
U / х, |=
U / ( ), , x
zR Ez |=
;
RvR) U / , Ey |=
, ( ) u
vR x
U / , Ey |=
,
,, ( ), ( ) u u x
v v yR x R .
Доведення властивостей елімінації
кванторів та побудова для LC першо-
порядкових числень секвенційного типу
будуть проведені в наступних статтях.
Висновки
В роботі досліджено першопоряд-
кові LC – логіки часткових предикатів з
композицією (операцією) предикатного до-
повнення Подібні операції використо-
вуються в різних варіантах логік Флойда-
Хоара з частковими перед- та після-умо-
вами. Описано композиційні алгебри і мо-
ви LC. Запропоновано низку відношень
логічного наслідку в LC (типів |=T, |=F, |=TF,
а також відношення
Pс
|=IR) та відношень
логічного наслідку за умови невизначенос-
ті (типів |=T
, |=F
, |=TF
). Досліджено влас-
тивості цих відношень, встановлено спів-
відношення між ними. Для запропонова-
них відношень описано умови їх гаранто-
ваної наявності, наведено властивості де-
композиції формул та елімінації кванторів.
Для відношень типів |=T та |=F дове-
дено теорему про елімінацію умов неви-
значеності, що дає змогу звести відношен-
ня
P
|=T
,
P
|=F
,
R
|=T
,
R
|=F
до відношень
Pc
|=T,
Pc
|=F,
Rc
|=T,
Rc
|=F. Водночас |=IR
не-
можливо звести до відношення
Pс
|=IR. По-
над те, для
Pс
|=IR неможливо коректно зада-
ти умови декомпозиції формул .
Встановлені властивості LC засвід-
чують істотну її відмінність від традицій-
ної логіки квазіарних предикатів.
Для пропонованих відношень логіч-
ного наслідку в LC та відношень логічного
наслідку за умов невизначеності в наступ-
них статтях планується побудова першопо-
рядкових числень секвенційного типу.
Література
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. S.C. Kleene. Mathematical Logic. New York,
1967.
3. Нікітченко М.С., Шкільняк С.С. Приклад-
на логіка. К.: ВПЦ Київський університет,
2013. 278 с.
4. Нікітченко М.С., Шкільняк С.С. Матема-
тична логіка та теорія алгоритмів. К.: ВПЦ
Київський університет, 2008. 528 с.
5. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С. Чисті першопорядкові логіки квазіар-
них предикатів. Проблеми програмування.
2016. № 2–3. C. 73–86.
6. Мykola S. Nikitchenko and Stepan S.
Shkilniak. Algebras and logics of partial
quasiary predicates. Algebra and
Discrete Mathematics, Vol. 23 (2017). N 2.
P. 263–278.
7. Hoare C. An axiomatic basis for computer
programming, Comm. 1969. ACM. 12(10).
P. 576–580.
8. 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.
Теоретичні та методологічні основи програмування
27
Vol. 2104 of CEUR Workshop Proc. 2018.
P. 716–724.
9. 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.
10. Нікітченко М.С., Шкільняк О.С., Шкільняк
С.С., Мамедов Т.А. Пропозиційні логіки
часткових предикатів з композицією пре-
дикатного доповнення. Проблеми програ-
мування. 2019. № 1. C. 3–13.
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. KLEENE, S. (1967) Mathematical Logic.
New York.
3. NIKITCHENKO, M. and SHKILNIAK, S.
(2013). Applied logic. Кyiv: VPC Кyivskyi
Universytet (in ukr).
4. NIKITCHENKO, M. and SHKILNIAK, S.
(2008). Mathematical logic and theory of
algorithms. Кyiv: VPC Кyivskyi Universytet
(in ukr).
5. 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).
6. NIKITCHENKO, M. and SHKILNIAK, S.
(2017). Algebras and logics of partial
quasiary predicates. In Algebra and Discrete
Mathematics. Vol. 23. No 2. P. 263–278.
7. HOARE, C. (1969). An axiomatic basis for
computer programming, Comm. ACM
12(10), 576–580, 1969.
8. 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., P. 716–724.
9. 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, P. 71–88.
10. 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).
Одержано 21.05.2019
Про автора:
Шкільняк Оксана Степанівна,
кандидат фізико-математичних наук,
доцент, доцент кафедри
інформаційних систем.
Кількість наукових публікацій в
українських виданнях – понад 95,
у тому числі у фахових виданнях – 36.
Кількість наукових публікацій в
зарубіжних виданнях – 13.
Scopus Author ID: 57190873266
h-індекс (Google Scholar): 5 (4 з 2014)
http://orcid.org/0000-0003-4139-2525.
Місце роботи автора:
Київський національний університет
імені Тараса Шевченка,
01601, Київ, вул. Володимирська, 60.
Тел.: (044) 259 05 19.
E-mail: me.oksana@gmail.com
|