Известия РАН. Теория и системы управления, 2020, № 6, стр. 120-131

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

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

Традиционные математические формализмы описания ситуаций и действий рассматриваются с примерами и обширной библиографией в [1], а методы планирования – в [2, 3].

Основное отличие языка KSL (knowledge specification language) от традиционных, таких, как STRIPS [4], ADL [5, 6], PDDL [7, 8] и им подобных языков описания действий, заключается в том, что операторы преобразования не определяют преобразование модели явно, а являются правилами вычисления спецификации (множества эффектов) преобразования.

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

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

2. Изменение модели – применение спецификации преобразования к модели, запись информации.

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

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

Характеристическая нормальная форма простого реляционного оператора с точностью до обозначений совпадает с нормальной формой ADL-правила [10]. Это означает, что простые реляционные операторы с теоретико-множественными операциями, которые удобно использовать для описания эффектов действий, преобразуются посредством нормализации (трансляции) в ADL-правила и могут быть легко включены в уже существующие системы поиска решений и планирования действий. В [11] описываются алгебраические свойства операции суперпозиции (updating) спецификаций, синтаксис и семантика рекурсивных определений реляционных преобразований общего вида и их вычисление.

В данной статье рассматривается вариант рекурсивных определений табличных реляционных преобразований, сохраняющих конечность описаний (спецификаций) изменяемых отношений модели. В разд. 1 приводятся основные семантические понятия: спецификация отношений объектов (knowledge specification) – это формальное описание информации о состоянии мира, об эффектах действий и т.п., операция суперпозиции спецификаций, понятия системы, реляционного преобразования и действия. В разд. 2 определяются синтаксис и семантика операторов и рекурсивных определений реляционных преобразований. Приводится пример системы, действия в которой (с побочными эффектами) удобно описывать с помощью рекурсии. В разд. 3 рассматриваются синтаксические ограничения на вид операторов реляционных преобразований, достаточные для элиминации кванторов из определений преобразований и ограничения, гарантирующие сохранение конечности спецификаций изменяемых отношений модели. В разд. 4 описывается функция для вычисления табличных преобразований, определенных с использованием рекурсии. Доказываются ее частичная корректность и достаточное условие, гарантирующее завершение вычисления.

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

Определение 1. Сигнатура (алфавит нелогических символов) Σ – это кортеж $\left\langle {{\text{C,F,}}{{{\text{F}}}_{I}},{\text{P,}}{{{\text{P}}}_{\Delta }},{\text{A}}} \right\rangle $, где C – бесконечное множество констант; F – множество функциональных символов; ${{{\text{F}}}_{I}} \subseteq {\text{F}}$ – множество символов инъективных функций; P – непустое множество предикатных символов; ${{{\text{P}}}_{\Delta }} \subseteq {\text{P}}$ – непустое конечное множество символов изменяемых (fluent) отношений; A – непустое конечное множество символов преобразований.

Количество аргументов (арность) символов $f \in {\text{F}}$, $p \in {\text{P}}$ и $H \in {\text{A}}$ будем обозначать через ${\text{|}}f{\text{|}}$, ${\text{|}}p{\text{|}}$ и ${\text{|}}H{\text{|}}$ соответственно.

Символы преобразований применяются только при описании преобразований (см. разд. 2). Термы и формулы языка логики первого порядка сигнатуры Σ строятся обычным образом с помощью предиката равенства =, связок $ \wedge ,\; \vee ,\;\neg $ и квантора $\exists $. Множества термов и формул сигнатуры Σ будем обозначать через $T(\Sigma )$ и $L(\Sigma )$ соответственно, а количество элементов (длину) кортежа термов t – через ${\text{|}}{\mathbf{t}}{\text{|}}$.

Определение 2. Спецификация (изменяемых) отношений сигнатуры Σ – это множество формул FOL (литер) вида $p({\mathbf{a}})$, $\neg p({\mathbf{a}})$, где $p \in {{{\text{P}}}_{\Delta }}$, ${\mathbf{a}} \in {{{\text{C}}}^{{|p|}}}$.

Множество всех таких литер (фактов) обозначим через ${\text{F}}(\Sigma )$, а множество Σ – спецификаций ${{2}^{{{\text{F}}(\Sigma )}}}$ – через SP(Σ).

На спецификациях как множествах определены обычные операции $ \cap $ (пересечение), $ \cup $ (объединение), \ (разность), а также операции инверсии и суперпозиции.

Определение 3. Инверсия Σ-спецификации – это функция $ - :{\text{SP}}(\Sigma ) \to {\text{SP}}(\Sigma )$, такая, что для всех $\alpha \in {\text{SP}}(\Sigma )$

Определение 4. Суперпозиция Σ-спецификаций – это функция $ * :{\text{SP}}(\Sigma ) \times {\text{SP}}(\Sigma ) \to {\text{SP}}(\Sigma )$, такая, что для всех $\alpha ,\beta \in {\text{SP}}(\Sigma )$

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

Определение 5. Система (структура) $\mathfrak{S}$ сигнатуры Σ – это кортеж $\langle \mathcal{I}_{F}^{\mathfrak{S}},\mathcal{I}_{I}^{\mathfrak{S}},\mathcal{I}_{R}^{\mathfrak{S}}\rangle $, где $\mathcal{I}_{F}^{\mathfrak{S}}$ – отображение (интерпретация функциональных символов), сопоставляющее каждому символу f ∈ F функцию $\mathcal{I}_{F}^{\mathfrak{S}}(f):{\text{SP}}(\Sigma ) \to ({{{\text{C}}}^{{|f|}}} \to {\text{C}})$, такую, что для всех  f ∈ F_I, $\alpha \in {\text{SP}}(\Sigma )$ функция $\mathcal{I}_{F}^{\mu }(f)(\alpha )$ инъективна; $\mathcal{I}_{I}^{\mathfrak{S}}$ – отображение (обратная интерпретация символов инъективных функций), сопоставляющее каждому символу  f ∈ F_I  функцию $\mathcal{I}_{I}^{\mathfrak{S}}(f):{\text{SP}}(\Sigma )$ → $(C \to {{C}^{{|f|}}} \cup \{ \emptyset \} )$, такую, что

для всех  f ∈ F_I, $\alpha \in {\text{SP}}(\Sigma )$, α ∈ C, ${\mathbf{a}} \in {{{\text{C}}}^{{|f|}}}$; $\mathcal{I}_{R}^{\mathfrak{S}}$ – отображение (интерпретация символов нетабличных отношений), сопоставляющее каждому символу функцию $\mathcal{I}_{R}^{{\mathfrak{S}S}}(p):{\text{SP}}(\Sigma ) \to ({{{\text{C}}}^{{|p|}}} \to $ {0, 1}).

Множество систем сигнатуры Σ будем обозначать через $\mathfrak{S}(\Sigma )$, а спецификации $\mu \in {\text{SP}}(\Sigma )$ будем называть (возможными) состояниями системы.

Дополнительный параметр $\alpha \in {\text{SP}}(\Sigma )$ у интерпретаций системы $\mathfrak{S} \in \mathfrak{S}(\Sigma )$ позволяет определять функции и отношения, зависящие не только от явных аргументов, но и от состояния системы (см. ниже пример 1).

Далее, для удобства чтения, опускаем упоминание о рассматриваемой системе $\mathfrak{S} \in \mathfrak{S}(\Sigma )$, поскольку всегда будет ясно, о какой системе идет речь.

Определение 6. Значение ${{\left[\kern-0.15em\left[ t \right]\kern-0.15em\right]}^{\mu }} \in {\text{C}}$ основного (не содержащего переменных) терма $t \in {\text{T}}(\Sigma )$ в состоянии $\mu \in {\text{SP}}(\Sigma )$ определяется индуктивно следующим образом:

1) ${{\left[\kern-0.15em\left[ a \right]\kern-0.15em\right]}^{\mu }} = a$, если $a \in {\text{C}}$;

2) ${{\left[\kern-0.15em\left[ {f({\mathbf{t}})} \right]\kern-0.15em\right]}^{\mu }} = \mathcal{I}_{F}^{\mathfrak{S}}(f)(\mu )({{\left[\kern-0.15em\left[ {\mathbf{t}} \right]\kern-0.15em\right]}^{\mu }})$, если f ∈ F, ${\mathbf{t}} \in T{{(\Sigma )}^{{|f|}}}$.

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

Определение 7. Отношение истинности (выполнимости) $\mu \vDash \phi $ замкнутой (не содержащей свободных переменных) формулы $\varphi \in L(\Sigma )$ в состоянии $\mu \in SP(\Sigma )$ определяется индуктивно следующим образом:

1) $\mu \vDash (t = t{\text{'}})$, если ${{\left[\kern-0.15em\left[ t \right]\kern-0.15em\right]}^{\mu }} = {{\left[\kern-0.15em\left[ {t{\text{'}}} \right]\kern-0.15em\right]}^{\mu }}$;

2) $\mu \vDash p({\mathbf{t}})$, если , ${{\left[\kern-0.15em\left[ {\mathbf{t}} \right]\kern-0.15em\right]}^{\mu }} \in \mathcal{I}_{R}^{\mathfrak{S}}(p)(\mu )$, $\mu {{ \vDash }_{\mathfrak{S}}}p({\mathbf{t}})$, если $p \in {{{\text{P}}}_{\Delta }}$, $p({{\left[\kern-0.15em\left[ {\mathbf{t}} \right]\kern-0.15em\right]}^{\mu }}) \in \mu $;

3) $\mu \vDash (\phi \wedge \psi )$, если $\mu \vDash \phi $ и $\mu \vDash \psi $;

4) $\mu \vDash (\phi \vee \psi )$, если $\mu \vDash \phi $ или $\mu \vDash \psi $;

5) $\mu \vDash (\exists x\phi (x))$, если существует элемент a ∈ C, такой, что $\mu \vDash \phi (a)$;

6) $\mu \vDash (\neg \phi )$, если неверно, что $\mu \vDash \phi $.

Преобразования состояний системы (действия) определим следующим образом.

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

Множество реляционных преобразований сигнатуры Σ будем обозначать через ${\text{RT}}(\Sigma )$.

Реляционные преобразования не определяют действия явно, а “вычисляют” спецификации “эффектов” действий, изменения состояний.

Определение 9. Действие k-арного реляционного преобразования $r \in {\text{RT}}(\Sigma )$ – это k-арное реляционное преобразование $\mathop {{\text{App}}}\nolimits_r \in {\text{RT}}(\Sigma )$, такое, что для всех ${\mathbf{a}} \in {{{\text{C}}}^{k}}$, для всех $\mu \in {\text{SP}}(\Sigma )$

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

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

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

1) если $p \in {{{\text{P}}}_{\Delta }}$, ${\mathbf{t}} \in {\text{T}}{{(\Sigma )}^{{|p|}}}$, то ${\text{\{ }}p({\mathbf{t}}){\text{\} }} \in {\text{R}}(\Sigma )$ – (позитивная) литера оператора;

2) если $\phi \in {\text{L}}(\Sigma )$ – атомарная формула, то $(\phi ?) \in {\text{R}}(\Sigma )$ – проверка условия, тест;

3) если $\rho \in {\text{R}}(\Sigma )$ и $\xi \in {\text{R}}(\Sigma )$, то $(\rho \cap \xi ) \in {\text{R}}(\Sigma )$ – пересечение;

4) если $\rho \in {\text{R}}(\Sigma )$ и $\xi \in {\text{R}}(\Sigma )$, то $(\rho \cup \xi ) \in {\text{R}}(\Sigma )$ – объединение;

5) если $\rho \in {\text{R}}(\Sigma )$, x – переменная, то $( \cup x\rho ) \in {\text{R}}(\Sigma )$ – универсальное объединение, $ \cup $ – квантор объединения;

6) если $\rho \in {\text{R(}}\Sigma )$, то $( \sim {\kern 1pt} \rho ) \in {\text{R}}(\Sigma )$ – дополнение;

7) если $\rho \in {\text{R}}(\Sigma )$, то $( - \rho ) \in {\text{R}}(\Sigma )$ – инверсия;

8) если H ∈ A, ${\mathbf{t}} \in {\text{T}}{{(\Sigma )}^{{|H|}}}$, то $H({\mathbf{t}}) \in {\text{R}}(\Sigma )$ – применение, вызов преобразования.

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

Определение 11. Интерпретация символов преобразования сигнатуры Σ есть отображение $J:{\text{A}} \to {\text{RT}}(\Sigma )$, сопоставляющее каждому символу преобразования H ∈ A |H|-арное реляционное преобразование $r \in {\text{RT}}(\Sigma )$.

Множество интерпретаций $\mathop {{\text{RT}}(\Sigma )}\nolimits^{\text{A}} $ символов преобразования сигнатуры $\Sigma $ будем обозначать через J(Σ). Каждая интерпретация $J \in {\text{J}}(\Sigma )$ однозначно определяет интерпретацию операторов $\rho \in {\text{R}}(\Sigma )$.

Определение 12. Значение $\left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu } \in {\text{SP}}(\Sigma )$ замкнутого (не содержащего свободных переменных) оператора $\rho \in {\text{R}}(\Sigma )$ в состояниии $\mu \in {\text{SP}}(\Sigma )$ при интерпретации $J \in {\text{J}}(\Sigma )$ определяется индуктивно следующим образом:

1) $\left[\kern-0.15em\left[ {\{ p({\mathbf{t}})\} } \right]\kern-0.15em\right]_{J}^{\mu } = \{ p({{\left[\kern-0.15em\left[ {\mathbf{t}} \right]\kern-0.15em\right]}^{\mu }})\} $;

2) $\left[\kern-0.15em\left[ {\phi ?} \right]\kern-0.15em\right]_{J}^{\mu } = \;if\;\mu \vDash \phi \;then\;{\text{F}}(\Sigma )\;else\;\emptyset $;

3) $\left[\kern-0.15em\left[ {\rho \cap \xi } \right]\kern-0.15em\right]_{J}^{\mu } = \left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu } \cap \left[\kern-0.15em\left[ \xi \right]\kern-0.15em\right]_{J}^{\mu }$;

4) $\left[\kern-0.15em\left[ {\rho \cup \xi } \right]\kern-0.15em\right]_{J}^{\mu } = \left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu } \cup \left[\kern-0.15em\left[ \xi \right]\kern-0.15em\right]_{J}^{\mu }$;

5) $\left[\kern-0.15em\left[ {\bigcup {x\rho (x)} } \right]\kern-0.15em\right]_{J}^{\mu } = \bigcup\nolimits_{a \in C} {\left[\kern-0.15em\left[ {\rho (a)} \right]\kern-0.15em\right]} _{J}^{\mu }$;

6) $\left[\kern-0.15em\left[ { \sim {\kern 1pt} \rho } \right]\kern-0.15em\right]_{J}^{\mu } = {\text{F}}(\Sigma ){\backslash }\left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu }$;

7) $\left[\kern-0.15em\left[ { - \rho } \right]\kern-0.15em\right]_{J}^{\mu } = - \left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu }$;

8) $\left. {H({\mathbf{t}})} \right]_{J}^{\mu } = J(H)({{\left[\kern-0.15em\left[ {\mathbf{t}} \right]\kern-0.15em\right]}^{\mu }},\mu )$.

Если значение оператора не зависит от состояния системы или интерпретации, будем опускать соответствующие индексы в обозначении $\left[\kern-0.15em\left[ \rho \right]\kern-0.15em\right]_{J}^{\mu }$.

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

$\emptyset = \{ p({\mathbf{a}})\} \; \cap \sim {\text{\{ }}p({\mathbf{a}}){\text{\} }}$ – пустое множество, bot-оператор, бот;

$ \top \; = \; \sim \emptyset $ – top-оператор, топ;

$(\phi \wedge \psi )? = \phi ? \cap \psi ?$ – проверка конъюнкции;

$(\phi \vee \psi )? = \phi ? \cup \psi ?$ – проверка дизъюнкции;

$(\exists x\phi )? = \bigcup {x(\phi ?)} $ – проверка существования;

$(\neg \phi )? = \sim \phi ?$ – проверка отрицания;

$\bigcap {x\rho } = \; \sim \bigcup {x( \sim \rho )} $ – универсальное пересечение, $ \cap $ – квантор пересечения;

$if\;\phi \;then\;\rho \;fi = \phi ? \cap \rho $ – (сокращенный) условный оператор;

$\{ \neg p({\mathbf{t}})\} = - \{ p({\mathbf{t}})\} $ – негативная литера оператора;

$\{ {{L}_{1}}, \ldots ,{{L}_{k}}\} = \bigcup\nolimits_{i \in 1..k} {\{ {{L}_{i}}\} } $ – множество литер.

Семантические свойства операторов будем описывать с помощью следующих отношений. Пусть для любых замкнутых операторов $\rho ,\xi \in {\text{R}}(\Sigma )$, для любого состояния $\mu \in {\text{SP}}(\Sigma )$

Очевидно, что отношение ${{ \sqsubseteq }_{\mu }}$ является отношением частичного порядка (модельный порядок), а ~_μ – соответствующее отношение эквивалентности.

Определение 13. Операторы $\rho ({\mathbf{x}}),\xi ({\mathbf{x}}) \in {\text{R}}(\Sigma )$ равны (обозначается $\rho ({\mathbf{x}}) = \xi ({\mathbf{x}})$), если для всех ${\mathbf{a}} \in {{{\text{C}}}^{{|{\mathbf{x}}|}}}$, для всех $\mu \in {\text{SP}}(\Sigma )$, $\mathfrak{S} \in \mathfrak{S}(\Sigma )$ $\rho ({\mathbf{a}}){{ \sim }_{\mu }}\xi ({\mathbf{a}})$.

Опишем синтаксис и семантику определений.

Определение 14. Система определений реляционных преобразований сигнатуры Σ – это отображение $\mathfrak{D}:{\text{A}} \to {\text{R}}(\Sigma )$, такое, что для всех H ∈ A количество свободных переменных оператора $\mathfrak{D}(H)$ не превосходит арности символа преобразования H.

Как обычно, система определений $\mathfrak{D}$ сигнатуры Σ описывается множеством равенств

Для определения реляционных преобразований будем использовать только позитивные реляционные операторы, т.е. такие, которые не содержат применения преобразований в области действия операций дополнения. Множество систем определений из таких операторов сигнатуры Σ будем обозначать через ${\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$.

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

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

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

Сигнатура и ее интерпретация:

${\text{C}} = \mathbb{Z}$ – номера участков железнодорожного пути, номера и веса вагонов и грузов;

${\text{P}} = \{ \leqslant ,At,Near,Linked,Loaded\} $, где

$x \leqslant y$ – обычный частичный порядок на множестве целых чисел,

$At(x,y)$ – вагон x находится на участке y,

$Near(x,y)$ – груз x находится на участке y,

$Linked(x,y)$ – вагон x сцеплен с вагоном y,

$Loaded(x,y)$ – груз y находится в вагоне x;

${{{\text{P}}}_{\Delta }} = {\text{\{ }}At,Near,Linked,Loaded{\text{\} }}$;

${\text{F}} = \{ + ,w,{{w}_{{{\text{max}}}}},{{w}_{{cur}}}\} $, где

$x + y$ – сложение целых чисел,

w(x) – вес груза x,

${{w}_{{\max }}}(x)$ – грузоподъемность вагона x,

${{w}_{{cur}}}(x) = \sum\nolimits_{Loaded(x,y) \in \mu } \,w(y)$ – вес грузов в вагоне x, если μ – конечно, иначе –1;

${{{\text{F}}}_{I}} = \{ \} $;

Определения действий:

1) сцепление вагонов:

2) расцепление вагонов:

3) загрузка вагона x:

4) разгрузка вагона x:

5) сдвиг вагона вправо:

6) сдвиг вагона влево:

Семантика системы определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$ определяется через понятие наименьшей неподвижной точки преобразования интерпретаций, соответствующего системе $\mathfrak{D}$.

Определение 15. Преобразование интерпретаций по системе определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$ есть отображение ${\text{J}}{{{\text{T}}}_{\mathfrak{D}}}:{\text{J}}(\Sigma ) \to {\text{J}}(\Sigma )$, такое, что

Неподвижная точка преобразования ${\text{J}}{{{\text{T}}}_{\mathfrak{D}}}$ есть такая интерпретация $J \in {\text{J}}(\Sigma )$, что ${\text{J}}{{{\text{T}}}_{\mathfrak{D}}}(J) = J$.

Пусть для любых интерпретаций $J,J{\text{'}} \in J(\Sigma )$

Если каждому символу преобразования H ∈ A сигнатуры Σ сопоставлен оператор ${{\rho }_{H}}({\mathbf{x}})\, \in \,{\text{R}}(\Sigma )$, то запись $\rho [{{\forall }_{{H \in {\text{A}}}}}(H \leftarrow {{\rho }_{H}})]$ будет обозначать оператор – результат замены в операторе $\rho \in {\text{R}}(\Sigma )$ каждого вхождения применения преобразования вида H(t), H ∈ A на вхождение соответствующего оператора ${{\rho }_{H}}({\mathbf{t}})$, а запись $\rho [\emptyset ]$ – операторы $\rho [{{\forall }_{{H \in {\text{A}}}}}(H \leftarrow \emptyset )]$.

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

Теорема 1 (существование наименьшей неподвижной точки преобразования ${\text{J}}{{{\text{T}}}_{\mathfrak{D}}}$). Пусть задана система позитивных определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$ и для всех $H \in {\text{A}},\;i \in \mathbb{N}$

Тогда для всех $H \in {\text{A}},\;i \in \mathbb{N}$, для всех ${\mathbf{a}} \in {{{\text{C}}}^{{|H|}}}$, для любого состояния $\mu \in {\text{SP}}(\Sigma )$

и реляционное преобразование ${{J}_{\mathfrak{D}}} \in J(\Sigma )$, такое, что является наименьшей (относительно $ \sqsubseteq $) неподвижной точкой преобразования ${\text{J}}{{{\text{T}}}_{\mathfrak{D}}}$.

Реляционное преобразование ${{J}_{\mathfrak{D}}}(H) \in {\text{RT}}(\Sigma )$ по системе определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$ будем обозначать через ${{H}_{\mathfrak{D}}}$. Хотя для каждого символа преобразования H ∈ A преобразование ${{H}_{\mathfrak{D}}}$ всюду определено, оно не всегда вычислимо.

3. Табличные преобразования. Особый интерес представляют преобразования, сохраняющие конечность описаний состояний системы – спецификаций изменяемых отношений модели. Такие преобразования будем называть табличными, так как конечные спецификации отношений могут быть (в принципе) описаны таблицами. Определим класс операторов, в которых значения переменных неявно ограничены табличными отношениями. Множество конечных (табличных) $\Sigma $-спецификаций будем обозначать через ${\text{S}}{{{\text{P}}}_{T}}(\Sigma )$, а множество инъективных (содержащих только инъективные функциональные символы) термов – через ${{{\text{T}}}_{I}}(\Sigma )$.

Определение16. Отношения “переменная x позитивно (негативно) ограничена в операторе $\rho \in {\text{R}}(\Sigma )$” определяются индуктивно следующим образом:

1) любая переменная позитивно ограничена в операторе $\emptyset $;

2) если $p \in {{P}_{\Delta }}$, переменная x имеет вхождение в $t \in {{{\text{T}}}_{I}}(\Sigma )$ и t ∈ t, то переменная x позитивно ограничена в операторе $p({\mathbf{t}})?$;

3) если переменная x имеет вхождение в $t \in {{{\text{T}}}_{I}}(\Sigma )$ и все переменные в $t{\text{'}} \in T(\Sigma )$ позитивно ограничены в операторе ρ, то переменная x позитивно ограничена в операторах $(t = t{\text{'}})? \cap \rho $, $(t{\text{'}} = t)? \cap \rho $, $\rho \cap (t = t{\text{'}})?$, $\rho \cap (t{\text{'}} = t)?$;

4) если переменная x позитивно (негативно) ограничена в операторе ρ, то она негативно (позитивно) ограничена в операторе $ \sim \rho $;

5) если переменная x позитивно (негативно) ограничена в операторах ρ и $\xi $, y – другая переменная и $\chi \in {\text{R}}(\Sigma )$, то переменная x позитивно ограничена в операторах –ρ, $\bigcup {y\rho } $, $\rho \cup \xi $, $\rho \cap \chi $, $\chi \cap \rho $ (негативно ограничена в операторах –ρ, $\bigcup {y\rho } $, $\rho \cap \xi $, $\rho \cup \chi $, $\chi \cup \rho $).

Вхождения переменной в (под)оператор $\rho \in {\text{R}}(\Sigma )$, в котором она (позитивно или негативно) ограничена, будем называть ограниченными.

Очевидно, что эти отношения разрешимы. Для определения и вычисления табличных преобразований важны следующие их свойства.

Пусть для любого оператора $\rho (x,{\mathbf{y}}) \in {\text{R}}(\Sigma )$ для любого состояния $\mu \in {\text{SP}}(\Sigma )$

– μ-диапазон переменной x в операторе $\rho (x,{\mathbf{y}})$.

Утверждение 1 (операторы с ограниченными переменными). Для любого оператора $\rho (x,{\mathbf{y}})\, \in \,{\text{R}}(\Sigma )$, любых ${\mathbf{a}} \in {{{\text{C}}}^{{|{\mathbf{y}}|}}}$, для любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$ выполняется следующее:

1) если переменная x позитивно (негативно) ограничена в операторе $\rho (x,{\mathbf{y}})$, то множество $rang{{e}_{x}}(\rho (x,{\mathbf{y}}),\mu )$ ($rang{{e}_{x}}( \sim \rho (x,{\mathbf{y}}),\mu )$) конечно;

2) если переменная x позитивно ограничена в операторе $\rho (x,{\mathbf{y}})$, то для любого конечного множества $C{\text{'}} \subseteq C$, такого, что $rang{{e}_{x}}(\rho (x,{\mathbf{y}}),\mu ) \subseteq C{\text{'}}$,

3) если переменная x негативно ограничена в операторе $\rho (x,{\mathbf{y}})$, то

Доказательство. 1. Базис и шаги индукции очевидны. Например, если множество $rang{{e}_{x}}( \sim {\kern 1pt} \rho (x$, y), μ) конечно, то и множество $rang{{e}_{x}}( \sim \bigcup {y\rho (x,{\mathbf{y}}),\mu } )$ конечно, так как

2. Следует из п. 1.

3. Следует из п. 1 и того, что множество констант C – бесконечное, а значит, существуют , такие, что $\left[\kern-0.15em\left[ {\bigcup {{\mathbf{y}}\rho (a,{\mathbf{y}})} } \right]\kern-0.15em\right]_{J}^{\mu } = \emptyset .$

Операторы $\rho \in {\text{R}}(\Sigma )$, в которых во всех подоператорах вида $\bigcup {x\xi (x,{\mathbf{y}})} $ переменная x (позитивно или негативно) ограничена в операторе $\xi (x,{\mathbf{a}})$ для произвольного ${\mathbf{a}} \in {{{\text{C}}}^{{|{\mathbf{y}}|}}}$, будем называть операторами с (таблично) ограниченными кванторами, а те из них, в которых все вхождения переменных в применения преобразований оператора ограничены, – операторами с ограниченными применениями преобразований (вызовами).

Используя утверждение 1, легко доказать следующее утверждение.

Утверждение 2 (элиминация кванторов). Пусть $\rho \in {\text{R}}(\Sigma )$ – замкнутый оператор с ограниченными кванторами. Тогда для любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$ существует бескванторный оператор ${\text{ELIM}}(\rho ,\mu ) \in {\text{R}}(\Sigma )$, такой, что $\rho {{ \sim }_{\mu }}\,{\text{ELIM}}(\rho ,\mu )$.

Значение оператора может быть бесконечным из-за наличия в нем операций проверки условия, дополнения, универсального объединения и рекурсии. Для определения табличных преобразований будем использовать операторы, в которых эти операции и рекурсия ограничены следующим образом.

Определение 17. Отношение “оператор $\rho \in {\text{R}}(\Sigma )$ является табличным оператором в (при) системе определений $\mathfrak{D} \in {\text{Def}}_{T}^{ + }(\Sigma )$” определяется индуктивно следующим образом:

1) оператор $\emptyset $ является табличным;

2) операторы $\{ p({\mathbf{t}})\} \in {\text{R}}(\Sigma )$ являются табличными;

3) если операторы $\rho $ и $\xi $ – табличные и $\chi \in {\text{R}}(\Sigma )$, то операторы –ρ, $\rho \cup \xi $, $\rho \cap \chi $, $\chi \cap \rho $ являются табличными;

4) если оператор $\rho $ – табличный и переменная x позитивно ограничена в операторе $\rho $, то оператор $\bigcup {x\rho } $ является табличным;

5) если H ∈ A и оператор $\mathfrak{D}(H)$ – табличный, то операторы $H({\mathbf{t}}) \in {\text{R}}(\Sigma )$ являются табличными.

Очевидно, что это отношение также разрешимо.

Все операторы системы определений, описанной в примере 1, являются табличными операторами с ограниченными вызовами.

Используя утверждение 1 и теорему 1, легко доказать следующее утверждение.

Утверждение 3 (табличные преобразования). Пусть задана система определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$, H ∈ A и оператор $\mathfrak{D}(H)$ является табличным в системе $\mathfrak{D}$. Тогда для любых ${\mathbf{a}} \in {{{\text{C}}}^{{|H|}}}$, для любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$

Итак, синтаксические, легко проверяемые ограничения на вид операторов гарантируют, что преобразования, определяемые табличными операторами, являются табличными.

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

Для вычисления будем использовать (частично вычисленные) конъюнкты – это операторы $\rho \in {\text{R(}}\Sigma )$ вида $\tau $ или $\tau \cap {{\pi }_{1}} \cap \ldots \cap {{\pi }_{k}}$, где

$\tau $ – коэффициент конъюнкта, оператор, построенный из литер вида ${\text{\{ }}P({\mathbf{a}}){\text{\} }}$, где ${\mathbf{a}} \in {{{\text{C}}}^{{|P|}}}$, с помошью операций $ \cap , \cup , \sim , - $;

π_i – варианты применений преобразований конъюнкта, попарно различные операторы вида H(a), $ - H({\mathbf{a}})$, где ${\mathbf{a}} \in {{{\text{C}}}^{{|H|}}}$.

Множество всех таких конъюнктов будем обозначать через ${\text{K}}(\Sigma )$, а коэффициент конъюнкта $\kappa \in {\text{K}}(\Sigma )$ и множество его вариантов применений преобразований – через $\tau (\kappa )$ и $\pi (\kappa )$ соответственно.

Операторы вида ${{\kappa }_{1}} \cup \ldots \cup {{\kappa }_{n}}$, где ${{\kappa }_{i}} \in {\text{K}}(\Sigma )$, будем называть дизъюнктивными.

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

Утверждение 4 (дизъюнктивная нормальная форма). Пусть $\rho \in {\text{R}}(\Sigma )$ – замкнутый позитивный бескванторный оператор. Тогда для любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$ существует дизъюнктивный оператор ${\text{DNF}}(\rho ,\mu ) \in {\text{R}}(\Sigma )$, такой, что $\rho {{ \sim }_{\mu }}\,{\text{DNF}}(\rho ,\mu )$.

Будем говорить, что дизъюнктивный оператор ${{\kappa }_{1}} \cup \ldots \cup {{\kappa }_{n}} \in {\text{R}}(\Sigma )$ является минимальным, если для всех $i,j \in 1..n$ выполняются следующие условия:

1) если $\left[\kern-0.15em\left[ {\tau ({{\kappa }_{i}})} \right]\kern-0.15em\right] = \emptyset $, то $\pi ({{\kappa }_{i}}) = \emptyset $;

2) если $\left[\kern-0.15em\left[ {\tau ({{\kappa }_{i}})} \right]\kern-0.15em\right] \subseteq \left[\kern-0.15em\left[ {\tau ({{\kappa }_{j}})} \right]\kern-0.15em\right]$ и $\pi ({{\kappa }_{j}}) \subseteq \pi ({{\kappa }_{i}})$, то i = j;

3) если $\pi ({{\kappa }_{i}}) = \pi ({{\kappa }_{j}})$, то i = j.

Утверждение 5 (минимизация). Пусть $\rho \in {\text{R}}(\Sigma )$ – дизъюнктивный оператор. Тогда существует минимальный дизъюнктивный оператор ${\text{MIN}}(\rho ) \in {\text{R}}(\Sigma )$, такой, что $\rho = {\text{MIN}}(\rho )$.

Для представления дизъюнктивных операторов и операций с ними удобно использовать множества конъюнктов. Множество всех конечных подмножеств множества K(Σ) будем обозначать через ${{\mathcal{P}}_{{{\text{K}}(\Sigma )}}}$.

Каждому $\Gamma \in {{\mathcal{P}}_{{{\text{K}}(\Sigma )}}}$ соответствует единственный (с точностью до порядка конъюктов, который не влияет на значение) дизъюнктивный оператор

Если $\Gamma ,\Delta \in {{\mathcal{P}}_{{{\text{K}}(\Sigma )}}}$, то вместо $ \cup \Gamma {{ \sqsubseteq }_{\mu }} \cup \Delta $ будем писать $\Gamma {{ \sqsubseteq }_{\mu }}\Delta $ и аналогично для отношений ~_μ и =.

Функция TT–CALC, определяемая ниже, является модификацией функции RT–CALC [11], проще и не требует разрешимости отношения $\mu \vDash \phi $ для вычисления.

Пусть для любой системы определений $\mathfrak{D} \in {\text{Def}}_{T}^{ + }(\Sigma )$, для любых $\Gamma ,\Delta \in {{\mathcal{P}}_{{{\text{K}}(\Sigma )}}}$ и любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$

где

${\text{NEW}}(\Delta ) = \bigcup\nolimits_{\kappa \in \Delta {\text{'}}} {{\text{DNF(ELIM}}(\kappa ))} $ – вычисление новых конъюнктов;

$\Delta = \{ \kappa [{{\forall }_{{H \in {\text{A}}}}}(H \leftarrow \mathfrak{D}(H)]\,{\text{|}}\,\kappa \in \Delta \} $ – подстановка определений в конъюнкты;

${\text{CUT}}(\Gamma ,\Delta ) = \{ \kappa \in \Delta \,{\text{|}}\,\neg \exists \kappa {\text{'}} \in \Gamma \kappa {{ \sqsubseteq }_{\mu }}\kappa {\text{'}}\} $ – сокращение “бесполезных” конъюнктов;

ELIM, DNF, MIN – функции, описанные в утверждениях 2, 4 и 5 соответственно.

Интуитивно, Γ есть множество (частично) вычисленных конъюнктов, а Δ – множество конъюнктов, которые “еще имеет смысл” вычислять (делать подстановки).

При доказательстве корректности функции TT–CALC будем использовать следующие очевидные свойства.

Утверждение 6 (свойства функций в TT–CALC). Для любой системы определений $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$, для любых $\Gamma ,\Delta \in {{\mathcal{P}}_{{{\text{K}}(\Sigma )}}}$ и любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$ выполняется:

1) $\Gamma {\text{'}} = \Gamma \cup \Gamma {\text{'}}$;

2) $\Gamma {\text{'}}{{ \sim }_{\mu }}{\text{NEW}}(\Gamma )$;

3) если $\Gamma {{ \sim }_{\mu }}\Delta $, то $\Gamma {\text{'}}{{ \sim }_{\mu }}\Delta {\text{'}}$;

4) $\Gamma \cup \Delta = \Gamma \cup {\text{CUT}}(\Gamma ,\Delta )$.

Для вычисления функций в TT–CALC достаточно, чтобы система $\mathfrak{S} \in \mathfrak{S}(\Sigma )$ была определена эффективно, т.е. чтобы для всех  f ∈ F, $g \in {{{\text{F}}}_{I}}$, $p \in P{\backslash }{{{\text{P}}}_{\Delta }}$ функции $\mathcal{I}_{F}^{\mathfrak{S}}(f)$, $\mathcal{I}_{I}^{\mathfrak{S}}(g)$, $\mathcal{I}_{R}^{\mathfrak{S}}(p)$ были вычислимы и определены на множестве ${\text{S}}{{{\text{P}}}_{T}}(\Sigma )$.

Теорема 2 (корректность функции TT–CALC). Пусть $\mathfrak{D} \in {\text{De}}{{{\text{f}}}^{ + }}(\Sigma )$ – система определений из операторов с ограниченными кванторами. Тогда для любых H ∈ A, ${\mathbf{a}} \in {{C}^{{|H|}}}$ и любого состояния $\mu \in {\text{S}}{{{\text{P}}}_{T}}(\Sigma )$ выполняется:

1) если вычисление ${\text{TT}} - {\text{CALC}}(\{ \} ,\{ H({\mathbf{a}})\} )$ заканчивается, то

2) если $\mathfrak{D}$ – система из операторов с ограниченными применениями преобразований, то вычисление ${\text{TT}} - {\text{CALC}}(\{ \} ,\{ H({\mathbf{a}})\} )$ заканчивается.

Доказательство. 1. Вычислению ${\text{TT}} - {\text{CALC}}(\{ \} ,\{ H({\mathbf{a}})\} )$ соответствуют последовательности Γ_i, ${{\Delta }_{i}}$, $i \in \mathbb{N}$, такие, что

где ${{\Gamma }_{i}},{{\Delta }_{i}}$ – аргументы функции ${\text{TT}} - {\text{CALC}}$ перед выполнением i + 1 шага вычисления.

Докажем, что для всех i > 0 $\Gamma _{i}^{'}{{ \sim }_{\mu }}{{\Gamma }_{{i + 1}}}$.

Базис индукции:

Шаг индукции:

Из теоремы 1 следует, что

Если ${{\Delta }_{i}} = \emptyset $ для некоторого $i \in \mathbb{N}$, то ${{H}_{\mathfrak{D}}}({\mathbf{a}},\mu ) = \left[\kern-0.15em\left[ { \cup {{\Gamma }_{i}}[\emptyset ]} \right]\kern-0.15em\right]$ и вычисление можно закончить.

2. Допустим, что ${{\Delta }_{i}} \ne \emptyset $ для всех $i \in \mathbb{N}$. Пусть $\Delta = \bigcup\nolimits_{i \in N} \,{{\Delta }_{i}}$, а calls, lits и vals – множества всех применений преобразований, литер и значений коэффициентов в конъюнктах $\kappa \in \Delta $ соответственно.

Эти множества являются конечными, calls – так как все операторы системы являются операторами с ограниченными вызовами, lits – так как для каждого $H({\mathbf{a}}) \in calls$ множество литер в операторе ${\text{ELIM}}(\mathfrak{D}(H)({\mathbf{a}}))$ конечно, vals – так как коэффициенты конъюнктов являются булевой комбинацией литер из lits.

Поскольку у любого конъюнкта $\kappa \in \Delta $ $\left[\kern-0.15em\left[ {\tau (\kappa )} \right]\kern-0.15em\right] \in vals$ и $\pi (\kappa ) \in {{2}^{{calls}}}$, т.е. являются элементами конечных множеств, то найдутся такие $i,j \in \mathbb{N}$, ${{\kappa }_{i}} \in {{\Delta }_{i}}$, ${{\kappa }_{j}} \in {{\Delta }_{j}}$, что i < j и ${{\kappa }_{i}} \sim {{\;}_{\mu }}{{\kappa }_{j}}$.

Это противоречит определению, согласно которому ${{\kappa }_{i}} \sqsubseteq {{\;}_{\mu }}{{\Gamma }_{j}}$ и , а значит, существует наименьшее $i \in \mathbb{N}$, такое, что ${{\Delta }_{i}} = \emptyset $ и вычисление заканчивается на шаге i + 1.

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

Пример 2 (Wagon World, вычисление оператора). Вычислим ${\text{RShift}}(2)(\mu )$ в системе, описаной в примере 1, в состоянии

Итак, ${{\Gamma }_{0}} = \{ \} ,\;{{\Delta }_{0}} = \{ {\text{RShift}}(2)\} $.

Шаг 1. Так как ${{\Delta }_{0}} \ne \emptyset $, вычисляем

Шаг 2. Так как ${{\Delta }_{1}} \ne \emptyset $, вычисляем

Здесь в ${\text{NEW}}({{\Delta }_{1}})$ функцией CUT сокращены конъюнкты ${\text{RShift}}(2)$ и $\{ \neg At(2,0),At(2,1)\} $.

Шаг 3. Так как ${{\Delta }_{2}} \ne \emptyset $, вычисляем

${\text{NEW}}({{\Delta }_{2}}) = {{\Delta }_{2}}$, так как $\Delta _{2}^{'} = {{\Delta }_{2}}$;

Здесь в ${\text{NEW}}({{\Delta }_{2}})$ функцией CUT сокращены все конъюнкты.

Шаг 4. Так как ${{\Delta }_{3}} = \emptyset $, заканчиваем вычисление.

Результатом вычисления является спецификация эффектов действия:

а результатом соответствующего действия $\mathop {{\text{App}}}\nolimits_{{\text{RShift}}} (2,\mu )$ – состояние

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

Применение рекурсии позволяет учитывать причинно-следственные связи, существующие в моделируемой системе, и описывать вместе с самим действием его побочные эффекты – реакцию системы на действие. Это делает язык KSL не менее выразительным, чем логические языки описания действий (см., например, [13, 14]), сохраняя при этом возможности планирования, присущие STRIPS-like языкам.

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

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