Рекурсивные определения реляционных преобразований

В статье определяются и исследуются основные конструкции и семантика языка описания действий (action description language), предназначенного для описания и вычисления преобразований отношений моделей ситуаций (реляционных преобразований).

Традиционные формализмы описания ситуаций и действий подробно, с примерами, описаны в книге [1] . Основное отличие описываемого языка KSL (Knowledge Specification Language) от традиционных, таких как STRIPS [2] , ADL [3, 4] и им подобных языков описания действий заключается в том, что операторы преобразования не определяют преобразование модели явно, а являются правилами вычисления спецификации (множества эффектов) преобразования.

(О М. В. Кучуганов, 2018

(О Независимый исследователь, 2018

DO| 10.25209/2079-3316-2018-9-1-53-83

Применение оператора преобразования разделено на 2 стадии (фазы):

• ( 1 )    метавычисления — чтение информации, анализ исходной модели (ситуации) и вычисление (с помощью несложных функций) множества эффектов действия — спецификации преобразования модели. Спецификация преобразования — это множество основных литер (не обязательно непротиворечивое) определяющее, что удаляется или добавляется в модель при преобразовании;

• ( 2 )    изменение модели — применение спецификации преобразования к модели, запись информации.

Это позволяет существенно увеличить выразительность языка описания действий, так как появляется возможность определять (и вычислять) множество эффектов действия с помощью теоретико-множественных операций и рекурсии.

В статье [5] описываются синтаксис и семантика простых (не рекурсивных) определений реляционных преобразований и их логические свойства.

В данной статье описываются синтаксис и семантика рекурсивных определений реляционных преобразований и их вычисление.

В §1 определяются основные семантические понятия — спецификация отношений объектов (knowledge specification) — это формальное описание информации о состоянии мира, об эффектах действий и т.п. и операция суперпозиции (updating) спецификаций.

В §2 определяются синтаксис и семантика операторов реляционных преобразований.

В §3 описывается соглашение о функциональной нотации, позволяющее существенно упростить запись формул и операторов.

В §4 рассматриваются основные свойства простых операторов реляционных преобразований - они формулируются в терминах логики предикатов первого порядка (FOL). Доказывается теорема о нормальной форме простого оператора — простые операторы общего вида преобразуются, посредством нормализации (трансляции), к операторам без теоретико-множественных операций, которые можно описать на языке ADL.

В §5 определяются синтаксис и семантика рекурсивных определений реляционных преобразований. Доказывается теорема о существовании наименьшей неподвижной точки системы позитивных определений.

В §6 описывается функция для вычисления операторов, определенных с использованием рекурсии. Доказывается, что она корректно вычисляет значение оператора в наименьшей неподвижной точке системы определений.

В §7 приводится пример системы, действия в которой (с побочными эффектами) удобно описывать с помощью рекурсии и демонстрируется вычисление рекурсивно определенного реляционного преобразования.

• §1. Спецификации отношений и преобразований

Для описания систем отношений и их преобразований используем классическую логику предикатов первого порядка (FOL).

Определим основные понятия.

Определение 1. Сигнатура (алфавит нелогических символов) — это кортеж £ = [C, P, A], где C есть непустое множество констант, P — непустое конечное множество предикатных символов (различной арности), A — непустое конечное множество символов преобразований (различной арности).

Будем обозначать арность символов p ∈ P и F ∈ A через | p | и | F | соответственно.

Формулы языка логики первого порядка сигнатуры £ строятся обычным образом из термов (констант c i ∈ C и переменных), предикатных символов p i ∈ P , предиката равенства =, логических констант (true, f alse), связок ( ∧ , ∨ , ) и кванторов ( ∀ , ∃ ).

Пусть T (£) обозначает множество термов, а L (£) — множество формул (язык) сигнатуры £.

Кортежи (конечные последовательности) термов будем обозначать буквами:

• a , b , c — кортежи констант;

• x , y , z — кортежи переменных;

t — кортежи произвольных термов.

Если арность кортежа t однозначно определяется контекстом, то | t | будет обозначать количество элементов (длину) кортежа.

Определение 2. Литеры сигнатуры £ есть формулы вида p( t ) (позитивные) или — p( t ) (негативные), где p е P, t е T (£) ^|p| .

Далее F (£), CF (£), Neg (£) обозначают множества литер, основных (не содержащих вхождений переменных) литер и множество негативных основных литер сигнатуры £ соответственно.

Символы преобразований используются только при описании преобразований (см. §2) .

Определение 3. Спецификация (преобразования) отношений сигнатуры £ (£-спецификация) есть множество а С CF (£) основных литер языка L (£).

Далее Spec (£) = 2 ^{CF (B)} — множество £-спецификаций.

На спецификациях, как множествах (литер), определены обычные операции ∪ (объединение), ∩ (пересечение), ∼ (дополнение до множества CF (£)), а также операции инверсии и суперпозиции:

Определение 4. Инверсия £-спецификации а е Spec (£) — это операция

• — а : Spec (£) ^ Spec (£) = { p( t ) | — p( t ) е а } U {— p( t ) | p( t ) е а } .

Определение 5. Суперпозиция £ -спецификаций а, в е Spec(£) — это операция а * в : Spec(£) х Spec(£) ^ Spec(£) = (а \ -в) U в.

Операция суперпозиции обладает следующими свойствами.

Утверждение 1 (Алгебраические свойства суперпозиции).

Структура SP(£) = [Spec(£), *, 0] является локально конечной полугруппой идемпотентов с единицей ∅ и законом сокращения: для любых а, в е Spec(£) выполняется а * в * а = в * а.

Доказательство. В записи формул будем опускать некоторые пары скобок. Порядок выполнения операций восстанавливается исходя из того, что операция ∪ имеет самый низкий приоритет.

Единица : для любого а е Spec (£)

а * 0 =(а \ —0 ) U 0 = а;

0 * а =( 0 \ — а) U а = а.

Идемпотентность : для любых а G Spec (E)

а * а = (а \ - а) U а = а.

Ассоциативность : для любых а,в,Y G Spec (E)

(а * в) * Y =а \ — в U в) \ — Y U Y

=^(а \- ^в) \ ^—Y ^{U в} \ ^—Y ^U Y

=а \ - (в U Y) U в * Y

=а \ — (в * Y U в П — y) U в * Y

=(а \- (в * Y)) \- (в П — y ) U в * Y-

Так как — (в П — y) = - в П y С в * Y, то имеем

(а * в) * Y = а \ — (в * Y) U в * Y = а * (в * Y).

Сокращение : для любых а, в G Spec (E)

а * в * а =(а \ - в U в) \ - а U а

=(а \ — в) \ — а U в \ — а U а = в * а.

Локальная конечность: для любого S С Spec (E) мощность его замыкания S ^∗ относительно операции ∗ не превосходит мощности множества конечных последовательностей элементов S без повторений и если множество S конечное, то и S * также конечное.           □

Определение 6. Е-спецификация а G Spec (E) совместна если а П — а = 0 .

Определение 7. Модель сигнатуры Е есть максимальная (по отношению С ) совместная Е-спецификация.

Пусть CSpec (E) обозначает множество совместных спецификаций, а М (Е) — множество моделей сигнатуры Е.

Любую совместную спецификацию а G CSpec (E) можно дополнить до модели. При этом может быть использован оператор построения «замкнутого мира»

cwa (а) = Neg (Е) * а.

Каждому предикатному символу p G P в каждой модели р G M (Е) соответствует отношение такой же арности.

Определение 8. Интерпретация предикатного символа p е P в модели ц е М (Е) есть отношение

^Rel (p,M) = ^{c I P^{(c) е} ц^}.

Очевидно, что

Утверждение 2 (Преобразования моделей).

Если ц е М (Е), а е CSpec (E), то (ц * а) е M (Е).

Используя это свойство, преобразования моделей (действия) определим следующим образом.

Определение 9. Реляционное преобразование сигнатуры Е арности k есть отображение r : Ck ^ (М(Е) ^ Spec(E)).

Далее RT (E) обозначает множество реляционных преобразований сигнатуры Е.

Определение 10. Действие k-арного реляционного преобразования r е RT (E) есть частичная функция App r : C k ^ ( M (Е) ^ M (E)) такая, что для любой модели ц е M (Е), для всех c е C |x| выполняется

App r ( х , ц) = if r( x , ц) е CSpec (E) then ц * r( x , ц).

Таким образом, каждое реляционное преобразование однозначно определяет частичное преобразование моделей.

Отношение истинности ц = ф замкнутой формулы ф языка L (Е) в модели ц сигнатуры Е определяется как обычно.

Определение 11. Формулы ф(х),ф(х) е L(E) эквивалентны (обозначается ф(х) О ^(х)) если для любой модели ц е M (Е), для всех c е C|x| выполняется ц = ф(с)   ^^ ц = ф(с).

Здесь и далее знак ^^ означает «тогда и только тогда, когда».

• §2. Операторы реляционных преобразований

Опишем синтаксис и семантику операторов реляционных преобразований и их основные виды.

Определение 12. Множество R (E) операторов (правил) реляционных преобразований сигнатуры Е определяется индуктивно следующим образом:

• ( 1 )    если p Е P и t Е T (E) | p | , то { p( t ) } Е R (E) ( атомарное преобразование );

• ( 2 )    если р Е R (E),f Е R (E) и ф Е L (E), то (if ф then р else f fi) Е R (E) ( условная композиция операторов с условием ф);

• ( 3 )    если р Е R (E) и f Е R (E), то (р U f) Е R (E) ( объединение);

• ( 4 )    если р Е R (E) и f Е R (E), то (р П f) Е R (E) ( пересечение);

• ( 5 )    если р Е R (E), то (~ р) Е R (E) ( дополнение);

• ( 6 )    если р Е R (E), то ( — р) Е R (E) ( инверсия);

• ( 7 )    если р Е R (E), х — переменная, то (|Jхр) Е R (X) ( универсальное объединение );

• ( 8 )    если р Е R (X), х — переменная, то (Qхр) Е R (X) ( универсальное пересечение );

• ( 9 )    если F Е A, t Е T (S) | F | , то F ( t ) Е R (X) ( применение преобразования ).

Символы преобразований (action names) являются по сути функциональными переменными различной арности.

Определение 13. Интерпретация символов преобразования сигнатуры S есть отображение J : A ^ RT (S), сопоставляющее каждому символу преобразования F ∈ A | F | -арное реляционное преобразование r Е RT (S).

Далее RT (E) A обозначает множество интерпретаций символов преобразования сигнатуры Е.

Каждая интерпретация J Е RT (E) A однозначно определяет интерпретацию операторов р Е R (Е).

Определение 14. Реляционное преобразование sp(J, р) Е RT (E) оператора р Е R (E) при интерпретации J Е RT (E) A определяется индуктивно следующим образом:

• ( 1 )    sp(J, { p( t ) } ) = { p( t ) } ;

• ( 2 )    sp(J,if ф then p else f fi) = if p = ф then sp(J, p~) else sp(J,f);

• ( 3 )    sp(J, p U f) = sp( J, p) U sp( J, f);

• ( 4 )    sp^(J, P П ^f) = sp^(J, p) П sp^(J, ^f);

• ( 5 )    sp^(J, ~ p) =~ sp^(J,p⁾;

• ( 6 )    sp^(J, - p) = -^p^(J,py;

• ( 7 )    sp(j, U xp(x)) = U { sp(J,p(c)) I c g c } ;

• ( 8 )    sp^(J, П xp^(x)) = n { sp^(J,p^(c)) | c ^G C^};

• ( 9 )    sp^(J,F^(t)) = J^{(F)( t )(}p).

Таким образом, каждому реляционному оператору p G R (S) соответствует функционал

p(J) : RT (S) A ^ RT (S) = sp(J,p).

Определение 15. Операторы p,f G R (S) равны (обозначается p = f) если p(J) = f (J), т.е. J G RT (S) A sp( J, p) = sp(J, f).

Будем использовать следующие обозначения для часто используемых операторов:

^{L 1 ,...^,L k ^} = ^U i_G1..k p L i , где

Li G F(X) - литеры, pLi = {p(t)}, если Li = p(t) и pLi = -{p(t)}, если Li = —p(t) — множество литер;

T = UpGp(T+ UT-), где т+ = U y{p(y)}, t- = Uy{p(y)} — top-оператор,

T (p) = CF (S) для всех p G M (S);

± = ~ T — bottom-оператор,

± (p) = 0 для всех p G M (S);

ф? = if ф then T else ± fi — оператор проверки условия, тест ;

if ф then p fi = ф? П p — сокращенный условный оператор ;

I = ^U p G P ^(I + ^U I - ), Где

I _p ⁺ = ^U y ( if p ( y ) then { p ( y ) } ),

I _p ^- = ^U y ( if — p ( y ) then {— p ( y ) } ),

I (p) = p для всех p G M (S) — тождественный оператор.

Определение 16. Оператор р е R (Е) называется

• ( 1    ) простым , если ρ не содержит символов применений преобразований;

• ( 2 )    позитивным , если ρ не содержит символов применений преобразований в области действия операций дополнения и универсального пересечения;

• ( 3 )    конъюнктом , если ρ является пересечением (конечного числа) простых операторов и операторов вида F ( t ), ~ F ( t ), — F ( t ), где F ∈ A.

Будем использовать обозначения:

R ⁰ (Е), C R ⁰ (Е) — для множеств простых и замкнутых (не содержащих свободных вхождений переменных) простых операторов сигнатуры Е;

R + (Е), C R ⁺ (Е) —для множеств позитивных и замкнутых позитивных операторов сигнатуры Е;

K R (Е), K R ⁺ (Е) — для множеств конъюнктов и позитивных конъюнктов сигнатуры Е.

• §3. Функциональная нотация

Для сокращения записи формул и операторов удобно соглашение о функциональной нотации : предикатные символы p ∈ P арности n + 1 будем использовать и как функциональные символы арности n и строить с их помощью термы более сложные, чем константы и переменные.

Определение 17. Множество T f (Е) квазитермов сигнатуры Е определяется индуктивно следующим образом:

• ( 1 )    если t е Т (Е), то t — квазитерм;

• ( 2 )    если p ∈ P — унарный предикатный символ, то p — квазитерм;

• ( 3 )    если p е P — предикатный символ арности n >  1, t i ,..., t _n-1 — квазитермы, то p(t 1 , . .. , t _n-1 ) — квазитерм;

• ( 4    ) если p ∈ P — бинарный предикатный символ, t — квазитерм, то p ^-1 (t) — квазитерм.

Далее L f (S) и R f (S) обозначают, соответственно, множества расширенных (содержащих вхождения квазитермов) формул и операторов сигнатуры S.

Количество аргументов предикатного символа в расширенной формуле (операторе) однозначно определяет, что именно он обозначает в данном вхождении: отношение (см. определение 8) , либо многозначную функцию.

Расширенные формулы и операторы — это сокращенные записи обычных, смысл котрорых задаёт расшифровка. Достаточно определить функцию расшифровки с точностью до имен связанных переменных.

Сначала определим вспомогательную функцию «расшифровки терма».

Определение 18. Расшифровка DC t расширенных формул вида y = t, где t — квазитерм, у — переменная, которая не входит в t, определяется индуктивно следующим образом:

• ( 1 )    если t G T (S), то

DC t (y = t) = (у = t);

• ( 2 )    если t = p, где p G P — унарный предикатный символ, то

DC t ⁽y = p) = p⁽y);

• ( 3 )    если t = p(t _i , ... , t _{n -i} ), где p G P — предикатный символ арности n > 1, t 1 , ... , t _{n -} i — квазитермы, то

DC t (y = p(t i ,..., t n - i )) = 3 y i ... y n - i (DC t (y i = t i ) Л ...

Л DCt(yn-i = tn-1) Л p(yi, . . . ,yn-i,y)), где переменные y1 , . . . , yn-1 не входят в t;

• ( 4 )    если t = p ^-i (t ‘ ), где p G P — бинарный предикатный символ, t ‘ — квазитерм, то

DCt(y = p-i(t’)) = 3yi (DCt(yi = t‘) Лp(y,yi)), где переменная y1 не входит в t.

Пример 1. Пусть p 1 , p 2 , p 3 — унарный, бинарный и тернарный предикатные символы сответственно. Тогда

DC t ⁽y =P 3 ⁽P 2 ⁽P 1 ^),x))

• =    3 y i y 2 ⁽DC t ⁽У 1 = P 2 (p i )) Л DC t ⁽y 2 = ^x) Л P 3 ⁽y i , У 2 , У))

= ^ y i y 2 ⁽ ^ y 3 ⁽DC t ⁽y 3 = P i ) ^Л P 2 (y 3 , y i ))^Л(У 2 = ^x)

^ЛР 3 (У 1 ,У 2 ,у))

= ^ y i y 2 ⁽ ^ y 3 ⁽DC t ⁽y 3 = P i ) ^Л P 2 ⁽У 3 ,У 1 ^))Л(У 2 = ^x)

^ЛР 3 (УьУ 2 ,У))

• =    З у 1 У 2 ⁽ З у з ⁽Р 1 ⁽у з ) ^Л Р 2^yi )) ^{Л (}У 2 = ^{х) Л} Р з ⁽У 1 ^y )).

Упрощая формальную расшифровку, получаем

DC t ⁽y = Р 3 ⁽Р 2 ⁽Р 1 ^),х)) = З у 1 У з ⁽Р 1 ⁽У з ) ^Л Р 2 ⁽У з ,У 1 ) ^Л Р з ⁽У 1 ^,х,у⁾⁾.

Определим функцию расшифровки атомарных формул и операторов.

Определение 19. Расшифровка DC расширенных атомарных формул и операторов определяется следующим образом:

• ( 1 )    если формула имеет вид s = t, где s, t — квазитермы, то

DC(s = t)) = 3ysyt(DCt(ys = s) Л DCt(yt = t) Л (ys = yt)), где переменные ys , yt не входят в квазитермы s и t;

• ( 2 )    если формула имеет вид p(t 1 , . .., t n ), где p E P — это n-арный предикатный символ, а t 1 , . . . , t _n — квазитермы, то

DC(p(t i ,..., t n )) = 3 y i ... y n (DC t (y i = t i ) Л ... Л DC t (y n = t n )

ЛР(У1,. . ./yn)), где переменные y1,. .. ,yn не входят в p(t1,. .. ,tn);

• ( 3 )    если оператор p(t 1 , .. ., t n ) имеет вид { p(t 1 , .. ., t n ) } или

• F (t1,. .. , tn), где p E P, F E A — символы арности n, t1, ... ,tn —

квазитермы, то

DC(p(t i ,...,t n )) = J ((DC t (y i = t i ))? П ... n (DC t (y n = t n ))?

nP(yi, .. .,yn)), где переменные yi,. .. ,yn не входят в p(ti, .. ., tn);

Расшифровка DC(ф) произвольной расширенной формулы ф е L f (Е) определяется как результат замены всех ее атомарных формул ф ₁ ,... ,ф _п на соответствующие расшифровки DC(ф ₁ ),..., DC(ф _n ).

Расшифровка DC(p) произвольного расширенного оператора р е R f (Е) определяется как результат замены всех его атомарных формул ϕ 1 , . . . , ϕ _n и операторов ρ 1 , . . . , ρ k на соответствующие расшифровки DC(ф 1 ),..., DC^J и DC(p i ),..., DC(p k ).

Пример 2. Покажем расшифровку части реляционного оператора RShift из примера 5 . Здесь At , Next — это бинарные предикатные символы, RShift — символ преобразования, v — переменная.

DC( RShift ( At ^-1 ( Next ( At (v)))))

= ^(DCt(yi = At-1 (Next(At(v))))? П RShift(yi)), где

DC t (y i = At ^-1 ( Next ( At (v))))

= 3 y 2 ⁽DC t ⁽y 2 = ^{Next ( At (v)))} Л ^{At (}y i , У 2 ))

= ^ У 2 ⁽ 5 y 3 ^(DC t ⁽У 3 = ^{At (v)) Л} Next ⁽У 3 ^,У 2 ^{)) Л At (}y i ,y 2 ))

= ^ У 2 ( З У 3 ( З У 4 ⁽⁽У 4 = ^{v) Л At (}y 4 ^,y 3 ^{)) Л Next (}y 3 ^,y 2 ^{)) Л At (}y i ^,y 2 ⁾⁾.

Упрощая формальную расшифровку и преобразовывая, получаем

DC( RShift ( At ^-i ( Next ( At (v)))))

= U y i (( ^ y 2 y 3 ( At (v, У з ) Л Next (y 3 ,y 2 ) Л At (y i ,y 2 )))? П RShift (y i ))

= U y i y 2 y 3 ^{((( At (v,}y 3 ) ^{Л Next (}y 3 ^,y 2 ^{) Л At (}y i ,y 2 ))? ^{n RSh}i^{ft (}y i ⁾⁾.

Легко доказать

Утверждение 3 (Корректность функции расшифровки).

• ( 1 )    Для всех ф е L (Е), р е R (E) выполняется

DCW О ф и DC(p) = р.

• ( 2 )    Для всех ф( х ) е L f (Е),р( х ) е R f (е) и t е T f (s) |x| выполняется DC(DC(ф)( t )) О DC(ф( t )) и DC(DC(p)( t )) = DC(p( t )).

Далее расширенные формулы и операторы будут использоваться только в примерах.

• §4 . Свойства простых операторов

Многие свойства простых операторов реляционных преобразований можно охарактеризовать формулами FOL, используя отношение р = ф.

Для этого используем следующие понятия.

Определение 20. Позитивная p + и негативная p ^- характеристические формулы языка L (S) оператора р е R ⁰ (E) относительно предиката p е P сигнатуры Е определяются индуктивно следующим образом:

( 1 )	P { p( t ) } = (У 1 = t 1 ) Л . . . Л (У п = t n ), P { q( t ) } = false, если P = q,            P - q( t ) } = false-'
( 2 )	p +f Ф then p else t fi = (Ф Л P + ) V (-Ф Л Р + f P - f ф then p else S fi = (Ф Л P - ) V (-Ф Л P - ) -
( 3 )	p + u e = p + V P + ,               P -U S = p - v p - ;
( 4 )	p p n e = p p Л p t -              p -o e = p - Л p - -
( 5 )	p f p = -p + ,                   p - p = - p - ;
( 6 )	p - p = p - ,                     p - p = p + ;
( 7 )	P u xp = 3xp + ,                P u xp = 3xp - -
( 8 )	p p xp = ^ xp t ,                P n xp = ^ xp - .

Очевидно, что

Утверждение 4 (Характеризация простых операторов).

Для любого оператора р( х ) Е R ⁰ (£), для любой модели р Е M (3), для каждого предикатного символа p Е P, для всех а Е C |x| , b Е C | p | выполняется

p^{(b) Е} Р(^а)(р)         - Р = p +( a ) ^(b)

и

^-P^{(b) Е} Р(^а)(р)         ' Р = P - ( a ) ^(b)

Это позволяет точно охарактеризовать многие свойства простых реляционных операторов сигнатуры £ формулами FOL языка L (£).

В частности, на языке FOL описываются такие важнейшие свойства, как пустота и совместность спецификации оператора.

Утверждение 5 (Пустота спецификации оператора).

Для любого оператора р( х ) Е R (£), для любой модели р Е M (£), для всех c Е C |x| выполняется

р(с)(р) = 0       ■ р = етрбур(с), где emptyp(x) = Д Vy-(p+(x)(y) Vp-(x)(y))

p∈P означает формулу языка L(£), выражающую условие пустоты спецификации оператора р(х).

Утверждение 6 (Совместность спецификации оператора).

Для любого оператора р( х ) Е R (£), для любой модели р Е M (£), для всех c Е C ^|x| выполняется

р(с)(р) Е CSpec(£)   ^^ р = consp(c), где consp(x) = Д Vy-(p+(x)(y) Л p-(x)(y))

p∈P есть формула языка L(£), выражающая условие совместности спецификации оператора р(х).

С помощью характеристических формул, легко осуществляется преобразование простых реляционных операторов в более простую, «нормальную» форму.

Теорема 1 (Нормальная форма простого оператора). Для любого простого реляционного оператора т ( x ) Е R ° (S)

т (x) = U (т+и т-), p∈P где для каждого предикатного символа p Е P т+ = U y(if p+(x) (y) then {p(y)} fi), т- = U y(if p-(x)(y) then {-P(y)} fi)-

Характеристическая нормальная форма простого реляционного оператора, с точностью до обозначений, совпадает с нормальной формой ADL-правила (см. [6, Theorem 1]).

Это означает, что простые реляционные операторы с теоретико-множественными операциями, которые удобно использовать для описания действий, преобразуются посредством нормализации (трансляции), в ADL-правила и могут быть легко включены в уже существующие системы поиска решений и планирования действий.

• §5 . Определения реляционных преобразований

Для (рекурсивного) определения реляционных преобразований будем использовать только позитивные реляционные операторы.

Пусть для любых реляционных преобразований r, r ‘ Е RT (S)

r E _RT (b) r '    ^^ V c Е C V p Е M (X) r( c )(p) C r ‘ ( c )(^)

и для любых интерпретаций J, J ‘ Е RT (X) A

J E J ‘   ^ VF Е A J(F ) C rt(_B) J ‘ (F )).

Очевидно, что отношения E _RT (b) и E являются полными частичными порядками на множествах RT (X) и RT (X) A соответственно.

Легко доказать, что

Утверждение 7 (Монотонность и непрерывность позитивных операторов). Любой позитивный реляционный оператор р Е R + (X) является:

• ( 1 )    монотонным, т.е. для любых J, J ‘ Е RT (E) A если J С J ‘ , то ^p(J ) ^C RT (B) ^p(J ‘ ^{) ;}

• ( 2 )    непрерывным, т.е. для любого направленного S С RT (£) A множество p(S) = { p(J )} j _e s также направленное и выполняется p⁽sup _c ^(S)) = sup _c _⁽ P^(S)).

^{RI (}^)

Ограничение на использование операции универсального пересечения в определении позитивного оператора необходимо , чтобы гарантировать непрерывность. Например,

Пример 3. Пусть сигнатура £ = [N, { >, Next } , { F } ], где N — множество натуральных чисел, >, Next — бинарные предикатные саимволы, а F — унарный символ преобразования.

Оператор p = P'|x(if x > 0 then F(Next-1(x)) else T)

является монотонным, но не непрерывным, так как в «стандартной» модели p _N , где p _N = x > y ^ ^ N = x > У и ^p N = Next (x,y) ^ z N = x + 1 = y для направленного множества интерпретаций

J< = {Jx)?}ieN имеем sup(J<) = T, ⊑

p(sup(J < )) = T , ⊑

sup (p(J < i )) = ± .

E rt (_E)

но для всех i ∈ N

p(J < i (F )) = ± ,

Опишем синтаксис и семантику определений реляционных преобразований.

Пусть каждому символу преобразования F Е A сигнатуры £ сопоставлен оператор p F ( x ) Е R (£). Результат замены в операторе p Е R (£) каждого вхождения применения преобразования вида F ( t ),F Е A на вхождение соответствующего оператора p F ( t ) будем обозначать p[ V _F e a ( F ^ p F )], а простые операторы p[ V _F e a ( F ^ ^ )] и p\ ^ f e a ( F ^ T )] — как p[ £ ] и p[ T ] соответственно.

Определение 21. Система (позитивных) определений реляционных преобразований сигнатуры £ есть отображение D : A ^ R + (£) такое, что для всех F ∈ A количество свободных переменных оператора D(F ) не превышает арности символа преобразования F .

Как обычно, система определений D сигнатуры £ описывается множеством равенств

{ F ( x ) = p f ( x ) | F Е A,p f = D(F ) } .

Далее Def + (£) обозначает множество (позитивных) определений реляционных преобразований сигнатуры £.

Определение 22. Преобразование интерпретаций по системе определений D Е Def + (£) это такое отображение Jd : RT (£) A ^ RT (£) , для которого Jd ( J )(F ) = sp(J, D(F )) выполняется при всех F ∈ A.

Семантика системы определений D Е Def + (£) определяется через понятие наименьшей неподвижной точки (ННТ) преобразования J D .

Определение 23. Неподвижная точка преобразования интерпретаций Jd по системе определений D Е Def + (£) есть такая интерпретация J Е RT (£) , что Jd ( J ) = J.

Применяя теорему Клини о наименьшей неподвижной точке непрерывного функционала (см. подробное обсуждение в замечательной книге [7] ) получаем, что

Теорема 2 (Существование наименьшей неподвижной точки преобразования JD ). Пусть задана система позитивных определений D Е Def +(£) и для всех F Е A для соответствующей последовательности операторов (TF^)i^N выполняется tFt = ±, TF+1 = D(F)[Vfga(F ^ tFt)].

Тогда для всех F Е A, i Е N, для любой модели p Е M (£), для всех c ∈ C выполняется

TFt(c)(p c TF^1(с)Ы и реляционное преобразование fix(JD) Е RT(£)A такое, что fix(JD)(F)(c)(p)= J {tFt(c)(p)}, i∈N является наименьшей (относительно ⊑) неподвижной точкой преобразования JD .

Для каждого F е A реляционное преобразование fixJ D )(F ) е RT (S) по системе определений D е Def ⁺ (S) будем обозначать через F D .

Хотя для каждого символа преобразования F ∈ A преобразование F D всюду определено, оно не всегда «вычислимо».

• §6. Вычисление рекурсивно определенных реляционных преобразований

Опишем один из возможных способов вычисления реляционных преобразований, определенных рекурсивно.

Определение 24. Вычислительная последовательность оператора р е CR+(E) по системе определений D е Def + (£) есть последовательность операторов (рг)гeN такая, что р° = р, рг+1 = (ргУ, где р = p[Vfga(F ^ D(F))].

Очевидно, что

Утверждение 8 (Свойства вычислительной последовательности). Пусть (p^ i e N — вычислительная последовательность оператора р е C R + (E) по системе определений D е Def + (S). Тогда для любой модели д е M (£), для всех i е N выполняется:

• ( 1 )    Р^гЩ^(Д С р ^{г+1 [} ± ^](д), р ^{г+1 [} Т ^](д) С р ^{г [} Т ^](д),;

• ( 2 )    U { p ^г [ ± ](д) } г_eN = p(JD')(p), где Jd — ННТ системы D е Def ⁺ (Х);

• ( 3 )    если р ^г [ Т ](д) С р ^г [ ± ](д), то р ^г [ ± ](д) = p(J D )(д).

К сожалению, последнего свойства недостаточно для вычисления значения многих, даже очень просто определенных операторов.

Например, не вычисляется оператор F , определенный системой D = { F = F } , хотя очевидно, что Fd = ± .

Для доказательства корректности описываемого ниже алгоритма нам понадобятся следующие отношения.

Пусть для любой системы позитивных определений D е Def + (X), для любых операторов р, € е C R + (X), для любой модели д е M (X)

€ C sup р ^ J { ^ i [ ± ](M) } i_GN С Ц р» }о ,

^€ ^ sup р ^ ^ € E sup р и р E sup €.

Пусть для любых операторов р( y ),€( z ) е R (X), для любой модели д е м (х)

^{€ Е} _м р     ■ v J ^е RT ⁽x^{) A} U ^{z €( z )(J} )(д)^С U y р' y ⁾'^{a )(}д),

€ ~ _д р    ■ € Е _р р и р Е _р €.

Очевидно, что отношения E _sup , E _p являются отношениями частичного порядка (предельный и модельный порядки соответственно), а ^ _sup , ^ _Р — соответстствующие отношения эквивалентности.

Для «вычисления» модельного порядка в алгоритме будем использовать отношение коньюктивного (частичного) порядка, которое определяется следующим образом.

Пусть для любых операторов р,€ е R (X), для любой модели д е м (х)

€ E K р ^ ^ существуют т _р ,т ^ е R 0 (X) и о _р ,о ^ е R (X)

такие, что р = Тр(у) П Ор (у), € = т^ (y, z) П о^ (y, z) П Op (z)

и

Д = ^v y 3 z empty^(т ^ ⁽ у , ^z) \ ^т р ^(z)).

Лемма 1 (Свойства частичных порядков). Для любой системы позитивных определений D е Def + (X), для любых р,€,о е R (X), д е M (X) выполняется:

• ( 1 )    если € E k р, то € Е _Р р;

• ( 2 )    если р E _p € U о и о Е _р р, то р E _sup € U ст[ ± ].

Доказательство.

• (1)    По утверждению 5, если д = V y 3 z етр!у(т ^ ( у , z ) \ T _p ( z )), то V y 3 z (T ₅ ( y , z ) E _p т р ( z )).

Тогда, если e С _к р, то e С _р р.

• (2)    Здесь р, e,ст е C R ⁺ (Е), так как отношение C _sup определено только для таких операторов. Докажем, что для всех i е N выполняется р ⁱ⁺¹ с _р e i и ст.

Базис индукции: р ¹ С _р e ⁰ U ст по условию.

Шаг индукции. Если р ⁱ С _р e i^-1 U ст, то р ⁱ⁺¹ С _р e i U ст ’ . Так как ст С _м р, то и ст ’ С _д р ‘ , а значит e i U ст ’ С _р e i U р ‘ С _р e i U (e U ст). Так как e С д e ‘ , то (e i U e) и ст С _р e i и ст, а значит р ⁱ⁺¹ С _д e i U ст.

Таким образом, для всех i е N имеем р ⁱ⁺¹ [ ± ] С _р e i [ T ] U ст[ ± ], а значит р ‘ C _sup e U ст[ ± ].

□

Любое бинарное отношение Rel С R (Е) х R (Е) однозначно определяет аналогичное отношение между подмножествами Г, А С R (S) Rel С 2 ^r(b) х 2 ^r(b) такое, что

(Г Rel А) ^ ^ У р е r ^ e е А (р Rel e).

Далее Р <_ш (S) обозначает множество всех конечных подмножеств множества (операторов) S.

Пусть для любого Г е Р <_ш ( R (S)) (полное) объединение множества операторов Г есть оператор

U Г = if Г = 0 then ± else U ( U У р( у )).

р( у ) е г

Очевидно, что

Утверждение 9 (Дизъюнктивная нормальная форма). Существует вычислимая функция DNF (р) : C R ⁺ (Е) ^ Р <_ш (K R ⁺ (E)) сопоставляющая каждому замкнутому оператору р е C R ⁺ (Е) непустое конечное множество его конъюнктов DNF (р) С K R ⁺ (Е) такое, что р = U DNF (р).

Очевидно, что ограничение отношения С _к на множество (позитивных) конъюнктов K R ⁺ (Е) разрешимо, а значит

Утверждение 10 (Минимизация). Если отношение ц = ф разрешимо, то существует вычислимая функция Min (Г) : Р <_ш (K R ⁺ (Е)) ^ Р <_ш (K R ⁺ (Е)) сопоставляющая каждому конечному множеству конъюнктов Г С K R ⁺ (Е) его минимальное (по отношению С ) подмножество Min (Г) С Г такое, что Г С к Min (Г).

Для вычисления определенных рекурсивно реляционных преобразований определим функцию RT-Calc : Р <_ш (K R ⁺ (S)) х Р <_ш ( R + (S)) ^ C R ⁰ (S) Пусть

RT-Calc (Г, А) = if ц = empty(U А[Т] \ U(A U Г)[±]) then U(A U Г)[±] else RT-Calc (Г U А, Calc (Г, А)), где

Calc (Г, А) = Cut (Г U А, Min ( New (А))),

New (A) = U { DNF (p ‘ ) } p e A ,

Cut (Г, А) = { f G А |-3 p G Г f C k р } ,

DNF и Min — функции, определенные в утверждениях 9 и

• 10 соответственно.

Интуитивно, Г есть множество (частично) вычисленных операторов, А — множество операторов, которые «еще имеет смысл» вычислять (делать подстановки).

Лемма 2 (Свойства функций в RT-Calc ). Для любой системы позитивных определений D G Def + (£), для любых Г, А G Р <_ш (K R + (S)) и ц G M (X) выполняется:

• ( 1 )    New (Г) = Г ’ , где Г ’ = { р ‘ | р G Г } ;

• ( 2 )    Min (Г) ~ _д Г;

• ( 3 )    Calc (Г, А) ~ _д Cut (Г, А ’ );

• ( 4 )    Cut (Г, А) С А, А \ Cut (Г, А) С _ц Г.

Доказательство.

• (1)    По определению функции New и утверждению 9 ;

• (2)    По определению функции Min и пункту 1 леммы 1;

• (3)    По определению функции Calc и пунктам 1, 2 леммы 2

Cut (Г U А, Min ( New (А))) = Min ( Cut (Г U А, New (А)),

Min ( Cut (Г, New (А)) ^ ^ Cut (Г, А ’ );

• (4)    По определению функции Cut и пункту 1 леммы 1 .        □

Итак,

Теорема 3 (Корректность функции RT-Calc ). Для любой модели ^ € M (S), любой системы позитивных определений D е Def + (£), любого оператора р € C R + (E)

• ( 1 )    если отношение ^ = ф разрешимо, то функция RT-Calc вычислима;

• ( 2 )    если вычисление RT-Calc ( {} , { р } ) заканчивается, то

RT-Calc ^({}, ^{р^})⁽р) = р⁽^⁾⁽^.

Доказательство.

• (1)    По определению функции RT-Calc и утверждениям 9 , 10 ;

• (2)    Вычислению RT-Calc ( {} , { р } ) соответствует последовательность

Го = {}, До = {р}, Pi+i = ri U Ai, Ai+i = Calc (ri, Ai), где Pi, Ai — это аргументы функции RT-Calc перед выполнением i + 1 шага вычисления.

Для всех i е N имеем (P i+i U A i+i ) E s_up (P i U A i ) ’ , так как P i+i = P i U A i . „ (P i U A i ) ’ и A i+i C A i .

По пункту 4 леммы 2, для всех i ∈ N имеем

Ai . „ Cut (Pi U Ai, Ai) U Pi U Ai, а значит, по пункту 2 леммы 1

A i E sup Cut (P i U A i , A i ) U P i U A i [ ± ].

Тогда для всех i е N имеем (P i U A i ) ‘ E sup P i+i U A i+i , так как

(Pi U Ai)’ =(U Aj U Ai)’ = (U Aj)‘ = U Aj j

E sup J ( Cut (P j U A j , A j ) U P j U A j [ ± ])

~ m U (A j+i U P j U A j Щ)

=( J A j U A i U A i+i ) U P i U J A j [ ± ]

0

=^Pi+i ^{U A}i+i ^UU ^Aj^UU ^Aj^[A] = ^Pi+i ^{U A}i+i.

0

Таким образом, для всех i е N имеем (ri U Ai)’ ^sup ri+1 U Ai+1, а значит Pi U Ai ^sup Pi+i U Ai₊i.

Тогда для любых i, j е N имеем ri U Ai ^_suprj U Aj и ri U Ai ^_sup Го U Ao = {p}.

Если на шаге i + 1 выполняется условие завершения

Ц = empty(U Ai[T] \ U(Ai U ri)[±l), то для любого j > i будет выполнятся

U(A,- U rj)[±])(ц) C U(A U Г,)Щ)(д), а значит

U(Ai U ri)   . U(A U №]).

Тогда вычисление можно закончить, так как

P ^SUP U^(Ai ^{U r}i) ^SUP U^(Ai ^{U r}i^)[A])

pW№) = U(Ai U ri)(JD)(_M) = U(Ai U Г,)Щ)(д).

□

Покажем процесс вычисления реляционного оператора на простом примере.

Пример 4. Пусть £ — сигнатура, содержащая 0-арные символы преобразований F1 , F2 и

D = {Fi = A1F1 U B1F2 U Ci,F2 = A2F1 U B2F2 U C2}, где Ai,Bi,Ci,A2,B2,C2 е CRo(£).

В записи конъюнктов в уравнениях и далее опущены очевидные, в данном примере, применения операции ∩.

Вычислим F1. Итак, Го = {}, Ao = {Fi}.

ШАГ 1. Вычисляем ri =Го U Ao = {Fi};

UAo [T] =Fi[T] = T;

U(Ao U ro)[^J = U ri [±] = Fi [±] = ±.

Так как UAo[T](^) ^ U(Ao U Го)[±](^), продолжаем вычисление.

New(Ao) ={AiFi ,BiF2,Ci};

Ai =Cut(Гi, Min(New(Ao)))

=Cut({Fi}, {A1F1, B1F2, Ci}) = {B1F2, Ci}.

Здесь функцией Cut сокращен конъюнкт A_iF_iиз New(A0), который уже можно не вычислять, так как A_iF_i Ск F_i- он поглощается уже вычисляемым конъюнктом Fi из Г₁.

ШАГ 2. Вычисляем

Г =Г1 U Ai = {Fi, BiF2, Ci};

UAi[T] = U{Bi,Ci};

U(Ai U ri)[±] = U Г2[A] = Ci.

Так как UA_i[T](^) ^ U(A_iU ri)[A](^), продолжаем вычисление.

New (Ai) =New({BiF2 }) U New ({Ci})

^BiA^FC ^Bi^B2^F2^{, B}iC2^{} U {}Ci^};

A2 =Cut(r2, Min(New(Ai)))

=Cut({Fi , BiF2 , Ci}, {BiA2Fi, BiB2F2, BiC2, Ci}) ={BiC2}

Здесь функцией Cut сокращены конъюнкты из New(A_i), которые уже можно не вычислять, так как они поглощаются уже вычисляемыми или вычисленными конъюнктами из Г₂:

BiA2Fi СкFi, BiB2F2 Ск BiF2, Ci Ск Ci.

ШАГ 3. Вычисляем

Г3 =Г2 U A2 = {Fi, BiF2, Ci,BiC2}.

UA2[T] =BiC2;

^U(A2 ^{U Г}2^)[А] = ^{U Г}3^[А] = ^U{Ci, ^BiC2^}.

Так как UA2[T](^) C U(A2 U Г₂)[±](^), заканчиваем вычисление с результатом C_iU B_iC₂.

Более содержательный пример рассматривается далее.

• §7. Пример: Wagon World

Рассмотрим пример системы, действия с побочными эффектами в которой удобно описывать с помощью рекурсии.

Пример 5 (Wagon World).

Система: на линейном (без разъездов и стрелок) железнодорожном пути, неограниченном в обе стороны, находятся n вагонов, которые можно двигать, сцеплять и расцеплять.

Объекты:

s,t, • • • € Z [участки железнодорожного пути], v,w, • • • € {1,.. ., n} [вагоны].

Отношения:

Next(s,t)    [участок t следует за участком s],

At(v, s)    [вагон v находится на участке s],

Linked (v,w)    [вагон v сцеплен с вагоном w].

Действия:

Link(v,w) = if Next(v,w) V Next(w,v) then {Linked(v, w), Linked(w,v)} UnLink(v,w) = — Link(v,w) [сцепление и расцепление вагонов];

RShift(v) ={—At(v, At(v)), At(v, Next(At(v)))} [вагон вправо]

U RShift(At^-1(Next(At(v)))) [толкает (рекурсия!)]

U RShift(Linked(v)) [тянет прицепленные (рекурсия!)], LShift(v) ={—At(v, At(v)), At(v, Next^-1(At(v)))} [вагон влево]

U LShift(At^-1(Next^-1(At(v)))) [толкает (рекурсия!)]

U LShift(Linked (v)) [тянет прицепленные (рекурсия!)].

Вычислим RShift(3) в модели

M cwa(^At U ^Linked U ^Next), где

_MAt ={At(1,1), At(2, 2), At(3, 3), At(4,4)},

^Linked ={Linked(1,2), Linked(2, 1), Linked(2, 3), Linked(3, 2)},

MNext ={Next(x, x + 1) | x € Z}.

Итак, Го = {}, До = {RShift(3)}.

ШАГ 1. Вычисляем

Г1 =Го U До = {RShift(3)};

иДо[Т] =RShift(3)[T] = Т;

и(До U Го)[±] = U Г1[±] = RShift(3)[±] = ±.

Так как UДо[Т](^) ^ U(До U Го)[±](^), то продолжаем вычисление.

New(До) =New ({ RShift (3)})

={ RShift (At -1 (Next (At (3))))} U { RShift (Linked (3))} U K3 ={RShift(4)} U {RShift(2)} U K3, где

K3   {— At (3, At (3)), At (3, Next (At (3)))}

={-At(3, 3), At(3,4)};

Д1 =Cut(Г1, Min (New (До))) = New (До).

ШАГ 2. Вычисляем

Г₂= Г1 U Д1 =K₃U {RShift(2), RShift(3), RShift(4)};

UД1[T] =T;

U(Д1 U Г1)[±] = U Г2Щ = K3.

Так как UД₁[T](^) ^ U(Д₁U Г1)[±](^), то продолжаем вычисление.

New(Д1) =K3 U New({RShift(2)}) U New({RShift(4)}), где

New({RShift(2)}) ={RShift(At^-1(Next(At(2))))} U {RShift(Linked (2))} U K2

={RShift(3)} U {RShift(1)} U K2, где

K2 ={-At(2, At(2)),

At (2, Next (At (2)))} ={-At(2, 2), At (2, 3)};

New({RShift(4)}) ={RShift(At ¹(Next(At(4))))} U {RShift(Linked(4))}

U K4

={} U {} U K4 = K4, где

K4 ={—At(4, At(4)),

At(4, Next (At (4)))} ={-At(4, 4), At (4, 5)};

Итак, New(Д1) = K2 U K3 U K4 U {RShift(1), RShift(3)}. Поэтому △2 = Cut(r2, Min (New(Д1))) = K2 U K4 U {RShift (1)}. Здесь функцией Cut сокращены конъюнкт RShift(3) и конъюнкты из K3, так как они уже есть в Г2.

ШАГ 3. Вычисляем

Гз = Г2 U Д2 =K2 U K3 U K4

U {RShift(1), RShift(2), RShift(3), RShift(4)};

U^2[T] =T;

U(^2 U ^)[±] = U Гз[±] = K2 U K3 U K4.

Так как UД₂[T](ц) ^ U(Д₂U Г₂)[±](ц), то продолжаем вычисление.

New(Д₂) =K₂U K4 U New({RShift(1)}), где

New({RShift(1)}) ={RShift(At-¹(Next(At(1))))} U {RShift(Linked(1))}

U K1

={RShift(2)}U{}U Ki, где

Ki ={-At(1, At(1)), At(1, Next (At (1)))} ={-At(1, 1), At(1, 2)};

Итак,

New(Д₂) =K1 U K2 U K₄U {RShift(2)}.

△з =Cut(Г3, Min(New(Д2))) = Ki.

и конъюнкты из

Здесь функцией Cut сокращены конъюнкт RShift(2) K2, K4 , так как они уже есть в Гз .

ШАГ 4. Вычисляем

Г4 =Г3 U A3 = K1 U K2 U K3 U K4

и {RShift(1), RShift(2), RShift(3), RShift(4)};

UA3 [T] =Ki;

U(A₃U Г₃)[±] = U Г₄[±] = K1 U K2 U K3 U K4.

Так как UA₃[T](ц) C U(A₃U Р₃)[±](ц), заканчиваем вычисление с результатом K1 U K2 U K3 U K₄.

Итак, RShift(3)(^) = {-At(3,3), At(3,4)} U {—At(4,4), At(4, 5)}

U{-At(2,2), At(2, 3)} U {—At(1,1), At(1, 2)}.

Результатом применения действия RShift(3)(ц) к модели ц являются суперпозиция модели и множества вычисленных эффектов действия

ApPRShift (3, ц) = Ц * RShift(3)(ц) = CWa(^At U ЦLinked U ^Next), где ЦAt = {At(1, 2), At(2, 3), At(3,4), At(4,5)}, а ЦLinked ,ЦNext такие же, как до применения действия.

Заключение

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

Приведенный пример демонстрирует выразительные возможности рекурсивных определений реляционных преобразований.