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

ISSN 2079-3316 ПРОГРАММНЫЕ СИСТЕМЫ: ТЕОРИЯ И ПРИЛОЖЕНИЯ т. 9, № 1(36), с. 53-83 УДК 519.682

М. В. Кучуганов

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

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

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

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

Ключевые слова и фразы: языки описания действий, STRIPS, ADL, ситуационное исчисление, реляционные преобразования.

Введение

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

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

© М. В. Кучуглнов, 2018

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

© Программные системы: теория и приложения (дизайн), 2018

ГО! 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 | соответственно.

Формулы языка логики первого порядка сигнатуры £ строятся обычным образом из термов (констант ci G C и переменных), предикатных символов pi € P, предиката равенства =, логических констант (true, false), связок (Л, v, —) и кванторов (V, 3).

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

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

a, b, c — кортежи констант; x, y, z —кортежи переменных; t —кортежи произвольных термов.

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

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

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

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

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

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

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

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

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

Определение 5. Суперпозиция £ -спецификаций а, в G Spec(£) — это операция

а * в : Spec(£) х Spec(£) ^ Spec(£) = (а \ -в) U в-

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

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

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

а * в * а = в * а.

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

Единица: для любого а G Spec

а * 0 =(а \ -0) U0 = а;

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

Идемпотентность: для любых а € Брес(Е) а * а = (а \ -а) и а = а.

Ассоциативность: для любых а, в, 7 € Брес

(а * в) * 7 =а \-в и в) \-7 и 7

=(а \-в) \-7 и в \-7 и 7 =а \ -(в и 7) и в * 7 =а \-(в * 7 и в П-7) и в * 7 =(а \-(в * 7)) \-(в П-7) и в * 7.

Так как -(в П -7) = -в П 7 С в * то имеем (а * в) * 7 = а \-(в * 7) и в * 7 = а * (в * 7).

Сокращение: для любых а, в € Брес

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

=(а \-в) \-а и в \-а и а = в * а.

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

Определение 6. Е-спецификация а € Брес(Е) совместна если

а П -а = 0.

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

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

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

сша(а) = Neg(Е) * а.

Каждому предикатному символу р € Р в каждой модели ц € М(Е) соответствует отношение такой же арности.

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

Rel(p,M) = {c | p(c) G ц}.

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

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

Если ц G M(S), a G CSpec(S), то (ц * a) G M(X).

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

Определение 9. Реляционное преобразование сигнатуры X арности к есть отображение

r : Cк ^ (M(S) ^ Spec(S)).

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

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

Appr(x, ц) = if r(x, ц) G CSpec(S) then ц * r(x, ц).

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

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

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

ц = ФИ ^ ц = ^(c).

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

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

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

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

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

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

(3) если р G R(E) и £ G R(E), то (р U £) G R(E) (объединение);

(4) если р G R(E) и £ G R(E), то (р П £) G R(E) (пересечение);

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

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

(7) если р G R(E), х —переменная, то (Uхр) G R(E) (универсальное объединение);

(8) если р G R(E), х — переменная, то (р|хр) G R(E) (универсальное пересечение);

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

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

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

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

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

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

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

(2) sp(J,if ф then р else £ fi) = if p = ф then sp(J,p) else sp(J,£);

(3) sp(J, р U £) = sp(J, р) U sp(J, £);

(4) sp(J, р П £) = sp(J, р) П sp(J, £);

(5) sp( J ~ р) =~ sp( J р);

(6) sp(J, -р) =

(7) sp( J, ^J хр(х)) = U{sp( J, р(с)) | c G C};

(8) sp(J,Г\xр(x)) = f| {sp( J, р(с)) | с G C};

(9) sp(J,F(t)) = J(F)(t)(p).

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

р(J): RT(£)A ^ RT(£) = sp(J^).

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

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

{L1,...,Lk } = Uiei..k рь>, где

Li G F(£) - литеры, рLi = {p(t)}, если Li = p(t) и

PLi = -{p(t)}, если Li = —p(t) — множество литер; т = Upep(Т+ UT-), где

т+ = U y{p(y)},

T- = У y{—p(y)} — top-оператор, t(p) = CF(£) для всех p G M(£);

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

±(p) = 0 для всех p G M(£); ф? = if ф then T else ± fi — оператор проверки условия, тест; if ф then р fi = ф? П р — сокращенный условный оператор; I = UpePU+ U Ip-), где

I+ = U y(if p(y) then {p(y)}), I- = Uy(if —p(y) then {—p(y)}),

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

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

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

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

(3) конъюнктом, если р является пересечением (конечного числа) простых операторов и операторов вида Г(1), ~ Г(Ь), -Г(Ь), где

Г € А.

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

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

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

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

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

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

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

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

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

(3) если р € Р — предикатный символ арности п > 1, ¿1, . . . , ¿п-1 — квазитермы, то р(Ь1,. .., ¿п-1) — квазитерм;

(4) если р € Р — бинарный предикатный символ, Ь — квазитерм, то р-1(Ь) — квазитерм.

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

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

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

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

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

(1) если Ь € Т(Е), то БС(у = Ь) = (у = Ь);

(2) если Ь = р, где р € Р — унарный предикатный символ, то

БС(у = р) = р(у);

(3) если Ь = р(Ь1, .. ., Ьп-1), где р € Р — предикатный символ арности п > 1, Ь1, .. . ,Ьп-1 — квазитермы, то

БС(у = р(*1,. .., Ьп-1)) = 3у1 ... у„-1 (БС(у1 = *1) А ...

Л БС(у„-1 = Ьп-1) А р(у 1, .. . ,у„-1,у)), где переменные у1,..., уп-1 не входят в Ь;

(4) если Ь = р-1(Ь'), где р € Р — бинарный предикатный символ, Ь' — квазитерм, то

БСДу = р-1(Ь')) = 3у1 (БС4(у1 = Ь') Ар(у,у1)), где переменная у1 не входит в Ь.

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

ВО

= ЗУ1У2

Лрз

ЛРз

= Зу1У2(Зуз(Р1(Уз) Л Р2 (уз, У1)) Л (У2 = х) Л Рз(у1 ,У2,У)). Упрощая формальную расшифровку, получаем

ВО(у = Рз(Р2(Р1),х)) = Зу1уз(Р1(уз) Л Р2(уз, У1) Л Рз(у1, х, у)).

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

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

(1) если формула имеет вид в = Ь, где в,Ь — квазитермы, то ВС(в = Ь)) = Зуву4(БО(ув = в) Л ВОг(уг = Ь) Л (у, = у)),

где переменные у8,уг не входят в квазитермы в и Ь;

(2) если формула имеет вид р(Ь1, . .., Ьп), где Р € Р — это п-арный предикатный символ, а ¿1, . . . ,Ьп — квазитермы, то

ВО

ЛР(У1,.. .,Уn)),

где переменные У1,. .. ,уп не входят в р(Ь1,. .., Ьп);

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

Г(¿1,. ..,Ьп), где р € Р, Г € А — символы арности п, ¿1, .. . ,Ьп —

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

БС(р(^,...^п))= J ((DCt(yi = ti))? П ... П(БС4(у„ = tn))?

yi-yn пр(у1,...,уп)),

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

Расшифровка DC(ф) произвольной расширенной формулы ф G Lр(Е) определяется как результат замены всех ее атомарных формул ф1,... ,фп на соответствующие расшифровки DC^i),..., DC(фn).

Расшифровка DC^) произвольного расширенного оператора р G Rp(X) определяется как результат замены всех его атомарных формул ф1,... ,фп и операторов р1,..., р^ на соответствующие расшифровки DC^i),..., DC^J и DC^i),..., DC^).

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

DC

= U(DCt(yi = At-i(Next(At(v))))? П RShift(yi)),

где yi

DCt

= 3y2

= 3y2

= 3y2(3уз(3у4((у4 = v) Л At(y4,y3)) Л Next(y3,y2)) Л At(yi,y2)).

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

DC

= У yi

= U yiy2y3(((At(v,y3) Л Next(y3,y2) Л At(yi,y2))? П RShift(yi)).

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

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

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

DC(^) ^ ф и DC(p) = р.

(2) Для всех ф(х) € Lp(Е),р(х) € Rp(Е) и t € Tp(E)|x| выполняется

DC(DC(ф)(t)) ^ DC^(t)) и DC(DC(p)(t)) = DC(p(t)).

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

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

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

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

(1) p+p(t)} = (yi = ti) А ... Л (yn = tn),

P+q(t)} = false, если p = q,

„+ -

pif ф then p else £ fi Pif ф then p else £ fi

p-q(t)} = false;

(ф Л p+) V (-Ф Л p+), (ф Л p-) V (-Ф Л p-);

(3) p+u£ = p+ V p+ p-u£ = p- V p-

(4) p+n£ = p+ Л p+; p-n£ = p- Л p-

(5) ptp = -p+ pZp- = -p-;

(6) p-p = p-, p-p = p+;

(7) pU xp = 3xp+, pu xp = 3xp-;

(8) pn xp = Vxp+, pn xp = Vxp-.

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

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

Для любого оператора р(х) € К0(Е), для любой модели ^ € М(е), для каждого предикатного символа р € Р, для всех а € С|х|, Ь € С|р|

выполняется

P

и

-P(b) е р(а)(м) ^ М = P-(a)(b).

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

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

Утверждение 5 (Пустота спецификации оператора). Для любого оператора р(х) е R(£), для любой модели м е M(£), для всех с е C|x| выполняется

р(с)(м) = 0 ^^ М = emptyp(c),

где

emptyp

peP

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

Утверждение 6 (Совместность спецификации оператора). Для любого оператора р(х) € К(Е), для любой модели ц € М(Е), для всех с € С|х| выполняется

р(с)(^) € СБрее(Е) ^^ ^ = сопвр(с),

где

соп5р

рер

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

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

Теорема 1

т (x) = U (т+ и Tp-),

peP

где для каждого предикатного символа p G P

т+ = Uy(if p+(x)(y)then lp(y)i fi),

TP = Uy(if p-(x)(y) then {-Р(У)} fi).

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

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

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

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

Пусть для любых реляционных преобразований r,r' G RT

r Ert(s) r' ^ Vc G C VM G M(E) r(c)(M) С r'(c)(M) и для любых интерпретаций J, J' G RT(E)A

J С J' ^ vF G A J(F) Crt(s) J'(F)).

Очевидно, что отношения CRT(S) и С являются полными частичными порядками на множествах RT(£) и RT(S)A соответственно.

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

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

68 М. В. Кучуганов

(1) монотонным, т.е. для любых J, J' G RT(X)A если J С J', то

P(J) Ert(e) p(j');

(2) непрерывным, 'т.е. для любого направленного S С RT(X)A множество p(S) = {p(J)}jes также направленное и выполняется P(supE(S)) = supERT(E) (p(S)).

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

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

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

J< = {J<i(F)(x)= —(i > x)?}ieN

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

с с

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

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

Ert

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

Пусть каждому символу преобразования F G A сигнатуры X сопоставлен оператор рр(x) G R(X). Результат замены в операторе р G R(X) каждого вхождения применения преобразования вида F(t),F G A на вхождение соответствующего оператора рр(t) будем обозначать р[Урe^(F ^ рр)], а простые операторы р[Урe^(F ^ и р[УрeA(F ^ T)] — как р[^] и р[Т] соответственно.

Определение 21. Система (позитивных) определений реляционных преобразований сигнатуры £ есть отображение Э : А ^ К + (£) такое, что для всех Г € А количество свободных переменных оператора Э(Г) не превышает арности символа преобразования Г.

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

{Г(х) = рР(х) | Г € А,рр = Э(Г)}.

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

Определение 22. Преобразование интерпретаций по системе определений Э € Def + (£) это такое отображение Л : КТ(£)А ^ КТ(£)А, для которого Л (Л)(Г) = вр(Л, Э(Г)) выполняется при всех

Г € А.

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

Определение 23. Неподвижная точка преобразования интерпретаций Л по системе определений Э € Def +(£) есть такая интерпретация Л € КТ(£)А, что Л (Л) = Л.

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

Теорема 2 (Существование наименьшей неподвижной точки преобразования Л). Пусть задана система позитивных определений Э € Def +(£) и для всех Г € А для соответствующей последовательности операторов выполняется

Т^ = ±, тру = Э(Г){УреА(Г ^ т^)].

Тогда для всех Г € А, г € N, для любой модели ц € М(£), для всех с € С выполняется

т^(с)(М) С т]+1(с)(М) и реляционное преобразование /гх(Лд) € КТ(£)А такое, 'что

/гх(Л)(Г)(с)(М)= У {т^(с)(М)},

ieN

является наименьшей (относительно С) неподвижной точкой преобразования .

Для каждого Г € А реляционное преобразование /гх(^)(Г) € КТ(Е) по системе определений Э € Def + (£) будем обозначать через

Гд.

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

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

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

Определение 24. Вычислительная последовательность оператора р € С[?+(£) по системе определений Э € Def +(£) есть последовательность операторов (рг)геы такая, что

р0 = Р, Рт = (/)', где р' = р[УРеА(Г ^ Э(Г))].

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

Утверждение 8 (Свойства вычислительной последовательности). Пусть (р1)гем — вычислительная последовательность оператора р € С[?+(£) по системе определений Э € Def + (£). Тогда для любой модели р € М(£), для всех г € N выполняется:

1) р*[±](р) С р4+1[±](р), рт[Т](р) С р4[Т](р),;

(2) и{р'[^](р)1«е^ = р(^э)(р), где — ННТ системы Э € Def + (£);

(3) если р1 [Т](р) С р*Щ(р), то р4 [±](р) = р(.1д)(р).

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

Например, не вычисляется оператор Г, определенный системой Э = {Г = Г}, хотя очевидно, что Гд =

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

Пусть для любой системы позитивных определений Э € Def +

е Евир р ^ U{ei[±](м)}ieN с у{рч±](м)}^,

с ~8ир р ^^ е Евир р и р Евир е. Пусть для любых операторов р

С Ем р ^ VЛ € КТ(£)А У zе(z)(Л)(м) С У ур(у)(Л)(м),

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

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

Пусть для любых операторов р,е € К

С Ек р ^^ существуют тр,т£ € К0(£) и ар,а£ € К(£) такие, что

р = Тр

и

М = VyЗz вшрЬу(т£(у, z) \ Тр(z)).

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

(1) если С ек р, то е Ем р;

(2) если р' Ем С и а и а ем р, то р' Евир С и а[±]. Доказательство.

(1) По утверждению 5, если м 1= VyЗz етрЬу(т^(у, z) \ тр^)), то VyЗz(т5(у, z) Ем Тр^)).

Тогда, если £ ek р, то £ р.

(2) Здесь р,£,а € CR+(E), так как отношение Esup определено только для таких операторов. Докажем, что для всех i € N выполняется рг+1 EM £г U а.

Базис индукции: р1 £0 U а по условию.

Шаг индукции. Если рг £г-1 U а, то рг+1 £г U а'. Так как а Р, то и а' р', а значит £г U а' £г U р' £г U (£ U а). Так как £ См £', то (£г U £) U а EM £г U а, а значит рг+1 EM £г U а.

Таким образом, для всех i € N имеем рг+1[±] См £г [±] U а[±], а значит р' Esup £ U а[±].

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

(Г Rel А) Ур € Г3£ € А (р Rel £).

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

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

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

р(у)ег

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

Утверждение 9 (Дизъюнктивная нормальная форма). Существует вычислимая функция йЫР(р) : CR+(E) ^ т<ш(KR+(E)) сопоставляющая каждому замкнутому оператору р € CR+ (Е) непустое конечное множество его конъюнктов йЫР(р) С KR+(E) такое, что р = У йЫР(р).

Очевидно, что ограничение отношения Ek на множество (позитивных) конъюнктов KR+ (E) разрешимо, а значит

Утверждение 10 (Минимизация). Если отношение р = ф разрешимо, то существует вычислимая функция Min (Г) : т<ш (KR+(E)) ^ p<u (KR+(E)) сопоставляющая каждому конечному множеству конъюнктов г С KR+(E) его минимальное (по отношению с) подмножество Min (Г) С Г такое, что Г Ek Min (Г).

Для вычисления определенных рекурсивно реляционных преобразований определим функцию RT-Calc: Т<ш(KR+(E)) х Т<ш(R+(E)) ^ CR0(£) Пусть

RT-Calc (Г, Д) =

if j = empty^j Д[Т] \ (J(Д U Г)Щ) then IJ(Д U Г)[±] else RT-Calc (Г U Д, Calc (Г, Д)),

где

Calc (Г, Д) = Cut (Г U Д, Min(New (Д))), Ывш(Д) = (J|DNF(p')}peA, Cut (Г, Д) = {£ е Д | -Эр е Г £ ок р}, DNF и Min — функции, определенные в утверждениях 9 и 10 соответственно.

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

Лемма 2 (Свойства функций в RT-Calc). Для любой системы, позитивных определений D е Def +(£), для любых г, д е Т<ш(KR+(£)) и j е M(E) выполняется:

(1) New (Г) = Г', где Г' = {р' | р е Г};

(2) Min(T) Г;

(3) Calc (Г, Д) Cut(^ Д');

(4) Cut(Г, Д) С Д, Д \ Cut(Г, Д) Г. Доказательство.

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

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

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

Cut(T U Д, Min(New^))) = Min(Cut^ U Д, New^)),

Min(Cut(^ New (Д)) Cut (Г, Д');

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

Итак,

Теорема 3

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

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

RT-Calc ({}, {р})Ы = p( Jd)(p). Доказательство.

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

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

Го = {}, До = {р}, Гт = Г U Д>, Дт = Calc (Г;, Д<),

где г;, д; — это аргументы функции RT-Calc перед выполнением i + 1 шага вычисления.

Для всех i € N имеем (Г;+1 U Д;+1) Esup (Г U Д;)', так как ri+i = Г; U Д (Г; U Д>)' и Дт С Д;.

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

д; EM Cut (г u д>, д;) U г U д>,

а значит, по пункту 2 леммы 1

Д; Esup Cut (Г; U Д;, Д;) U Г; U Д; [±] .

Тогда для всех i € N имеем (Г; U Д;)' Esup Г;+1 U Д;+1, так как

(Г; U Д;)' =( U Д; U Д;)' = ( Ц Д;)' = Ц Д$ j<i j<i j<i

Esup U

j<i

U

j<i

= ( U Д; U Д; U Д;+1) U Г; U U Д; Ш 0<j<i j<i

=Г;+1 U Д;+1 U U Д; U U Д; [^]=Г;+1 U Д;+1. 0<j<i j<i

Таким образом, для всех г € N имеем (г и дг)' ^нир гг+1 и дг+1, а значит Г и Дг ^Нир Г4+1 и Дг+1.

Тогда для любых € N имеем гг и Дг ^нир г и д^- и гг и Дг ^нир Го и До = {р}.

Если на шаге г + 1 выполняется условие завершения р = ешрЬу(и Дг[Т] \ У(Дг и Г<)[±]),

то для любого ^ > г будет выполнятся

и(Д3- и Г)[±])(м) с У(Дг и Гг)[±])(М),

а значит

и(Дг и Г<) ^Нир и Г<)[±]). Тогда вычисление можно закончить, так как

р ~Нир У

р№)Ы = У(Дг и Гг)Ш(ц) = У(Дг и Г4)[±])(м).

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

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

Э = {Л = Л1Л1 и Б1Л2 и С1, Л2 = Л2Л1 и Б2Л2 и С2},

где Л1,Б1,С1,Л2,Б2,С2 € СК0(Е).

В записи конъюнктов в уравнениях и далее опущены очевидные, в данном примере, применения операции П. Вычислим Итак, Го = {}, До = {Л\}.

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

Г1 =Го и До = №}; иДо[Т] = Л[Т] = Т; и(До и Го)[±] = и Г1 [±] = Л [±] = ±.

и

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

New^o) = {A^, B1F2, C1};

Д1 =Cut

=Cut({F1}, {A1F1, B1F2, C1}) = {B1F2, C1}.

Здесь функцией Cut сокращен конъюнкт A1F1 из New (До), который уже можно не вычислять, так как A1F1 Ek F1 - он поглощается уже вычисляемым конъюнктом F1 из Г1.

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

Г2 =Г1 и Д1 = {F1, B1F2, C1}; иД1[Т] = U{B1,C1}; и(Д1 и Г1)[±] = и Г2Ш = C1.

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

New

={B1A2F1, B1B2F2, B1C2} U {C1}; Д2 =Cut

=Cut({F1, B1F2, C1}, {B1A2F1, B1B2F2, B1C2, C1}) = {B1C2}

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

B1A2F1 EkF1, B1B2F2 Ek B1F2, C1 Ek C1.

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

Гз =Г2 U Д2 = {F1, B1F2, C1, B1C2}. иД2[Т] =B1C2; и(Д2 U Г2)[±] = U Гз[±] = U{C1, B1C2}.

Так как иД2[Т](^) С и(Д2 U Г2)[Х](^), заканчиваем вычисление с результатом C1 U B1C2.

Более содержательный пример рассматривается далее. §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) в модели

Р =cwa(pAt U ^Linked U PMext ),

где

PAt ={At(1,1), At(2, 2), At(3, 3), At(4, 4)}, pLinked ={Linked(1, 2), Linked(2, 1), Linked(2, 3), Linked(3, 2)}, PNext = {Next(x,x + 1) | x € Z}.

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

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

Г1 =Го U До = {RShift(3)}; иДо[Т] =RShift(3)[T] = Т; и(До U Го)[±] = U Г1[±] = RShift(3)[±] =

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

Ывш

={ 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(ri, Min (New (До))) = New (До).

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

Г2 = Г1 U Д1 =K3 U {RShift(2), RShift(3), RShift(4)};

UДl[T] =Т; U(Дl U Г1)[±] = U Г2[±] = K3.

Так как UДl[T](^,) ^ U(Дl 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-1(Next(At(4))))} U {RShift(Linked(4))}

u к4

={} 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. Вычисляем

г3 = г2 и д2 =к2 и к3 и к4

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

иД2[Т] =T; и(Д2 U Г2)[±] = U Гэ[±] = K2 U K3 U K4.

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

New(Д2) =K2 U K4 U New({RShift(1)}),

где

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

и k1

={RShift(2)} U {} U K1,

где

K1 ={—At(1, At (1)), At(1, Next (At (1)))} ={—At(1,1), At(1, 2)};

Итак,

New(Д2) =K1 U K2 U K4 U {RShift(2)}. Д3 =Cut(Г3, Min(New(Д2))) = K1.

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

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

г4 =г3 и Д3 = к1 и к2 и к3 и к4

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

иД3 [T] =K1;

и(Д3 и г3)[±] = и г4[±] = к1 и к2 и к3 и к4.

Так как ид3[Т](р) С и(д3 U г3)[±](р), заканчиваем вычисление с результатом K1 U K2 U K3 U K4.

Итак, RShift(3)(p) = {—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)(p) к модели р являются суперпозиция модели и множества вычисленных эффектов действия

AppRShift (3, P) = P * RShift(3)(p) = Cwa (pAt U PLi nked U pNext ) ,

где pAt = {At(1, 2), At(2, 3), At(3,4), At(4, 5)}, а pLinked ,pNext такие же, как до применения действия.

Заключение

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

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

Список литературы

[1] F. Harmelen, V. Lifschitz, B. Porter (eds.), Handbook of Knowledge

Representation, Foundations of Artificial Intelligence, 1st edition, Elsevier,

2008, 1034 p. tss

[2] R. Fikes, N. Nilsson. "STRIPS: A new Approach to the Application of

Theorem Proving to Problem Solving", Artificial Intelligence, 2:3-4 (1971),

pp. 189-208, d ' 53

[3] E.P.D. Pednault. "ADL: Exploring the middle ground between STRIPS and the Situation Calculus", Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, KR'89 (Royal York Hotel, Toronto, Ontario, Canada, May 15-19, 1989), Morgan Kaufmann Publishers Inc., San Francisco, 1989, pp. 324-332, ||5з

[4] E. P. D. Pednault. "ADL and the State-Transition Model of Action", J. Log. Compute 4:5 (1994), pp. 467-512, d f53

[5] М. В. Кучуганов. «Системы реляционных преобразований: правила и критерий реализуемости», Вестник Удмуртского университета. Математика. Механика. Компьютерные науки, 25:1 (2015), с. 117-125,

[6] J. Claßen, G. Lakemeyer. "A Semantics for ADL as Progression in the Situation Calculus", Proceedings of the 11th International Workshop on Non-Monotonic Reasoning, NMR'06 (Lake District, UK, 30 May-1 June, 2006), Institut für Informatik, Technische Universität Clausthal, pp. 334-341,

[7] V. Stoltenberg-Hansen, I. Lindstrom, E. R. Griffor, Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science, vol. 22, 1st edition, Cambridge University Press, 2008, 364 p., © d t69

Пример ссылки на эту публикацию:

М. В. Кучуганов. «Рекурсивные определения реляционных преобразований». Программные системы: теория и приложения, 2018, 9:1(36), с. 53-83. d 10.25209/2079-3316-2018-9-1-53-83

url http://psta.psiras.ru//read/psta2018_l_53-83.pdf

Об авторе:

Рекомендовал к публикации

д.ф.-м.н. Н.Н . Непейвода

Преподавал на математическом факультете Удмуртского государственного университета. Автор нескольких статей по конструктивным логикам, синтезу схем программ и баз данных, планированию действий.

Михаил Валерьевич Кучуганов

[Da 0000-0002-9550-2753 e-mail: qmikle1@yandex.ru

UDC 519.682

Mikhail Kuchuganov. A recursive definitions of relational transformations.

Abstract. In the paper we describe and investigate a basic constructions and semantics of a new action description language KSL (Knowledge Specification Language) which is based on the notion of relational transformation.

The main difference the described language from traditional ones (STRIPS, ADL, etc.) is in extension traditional (STRIPS-like) rules by means of its set-theoretic compositions and recursion - this greatly increases the expressiveness of the language.

Also we define a function to calculate a recursively defined relational transformations and prove its partial correctness. (in Russian).

Key words and phrases: action description languages, STRIPS, ADL, situation calculus, relational transformations.

References

[1] F. Harmelen, V. Lifschitz, B. Porter (eds.), Handbook of Knowledge Representation, Foundations of Artificial Intelligence, 1st edition, Elsevier, 2008, 1034 p., ISBN : 0444522115/9780444522115

[2] R.~Fikes, N.~Nilsson. "STRIPS: A new Approach to the Application of Theorem Proving to Problem Solving", Artificial Intelligence, 2:3-4 (1971), pp. 189-208,

[3] E. P. D.~Pednault. "ADL: Exploring the middle ground between STRIPS and the Situation Calculus", Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, KR'89 (Royal York Hotel, Toronto, Ontario, Canada, May 15-19, 1989), Morgan Kaufmann Publishers Inc., San Francisco, 1989, pp. 324-332,

[4] E. P. D.~Pednault. "ADL and the State-Transition Model of Action", J. Log. Comput., 4:5 (1994), pp. 467-512,

[5] M. V.~Kuchuganov. "Systems of Relational Transformations: Rules and Realiz-ability Criterion", Vestnik Udmurtskogo universiteta. Matematika. Mekhanika. Komp'yuternyye nauki, 25:1 (2015), pp. 117—125,

[6] J.~Claßen, G.~Lakemeyer. "A Semantics for ADL as Progression in the Situation Calculus", Proceedings of the 11th International Workshop on Non-Monotonic Reasoning, NMR'06 (Lake District, UK, 30~May-l~June, 2006), Institut für Informatik, Technische Universität Clausthal, pp. 334—341, url

[7] V.~Stoltenberg-Hansen, I.~Lindstrom, E. R.~Griffor, Mathematical Theory of Domains, Cambridge T'acts in Theoretical Computer Science, vol. 22, 1st edition, Cambridge University Press, 2008, 364 p.,

© M. V. Kuchuganov, 2018

© Independent Researcher, 2018

© Program Systems: Theory and Applications (design), 2018

DOI 10.25209/2079-3316-2018-9-1-53-83 (SSjBS1

Sample citation of this publication:

Mikhail Kuchuganov. "A recursive definitions of relational transformations". Program Systems: Theory and Applications, 2018, 9:1(36), pp. 53-83. (In Russian). 10.25209/2079-3316-2018-9-1-53-83

URL http://psta.psiras.ru//read/psta2018_l_53-83.pdf