Scientific journal
Modern problems of science and education
ISSN 2070-7428
"Перечень" ВАК
ИФ РИНЦ = 1,006

INTENSIONAL OPERATORS FOR SPECIALIZATION MODELS OF IMITATING SIMULATORS

Kosikov S.V. 1 Ismailova L. Y. 2
1 Institute «Jurinfor-MGU»
2 НИЯУ MEPhI
The paper presents means of specialization conceptual models aimed at building simulation systems. Specialization is necessary to introduce a model-specific tools to reflect the specificities of the problem domain. Formalized means of specialization are offered through the construction and study of intensional entities. The primary means of specialization include propositional concepts of the intensional view. Concepts are included in the syntactic-semantic system, providing a selection of individuals and their classification into the possible, the real and the virtual individuals. To clarify the status of the actual individuals the system uses the formalism of assignment points, between which, in turn, can set of a higher order. A research on the various structures used in the simulation includes the extensional and intensional predicates. We introduce and study different types of intensional operators.
interpretations
intensional and eхtensional predicates
semantic domains
intensional operators
specialization of conceptual models
information systems for supporting law-enforcement activity

Построение информационных систем в целом и систем, относящихся к классу имитационных симуляторов в частности предполагает построение модели предметной области (ПО). Настоящая работа рассматривает модели, построенные методом концептуального моделирования (КМ) [1]. В большинстве нетривиальных ПО такие модели требуют включения дополнительных выразительных средств, зависящих от специфики ПО. Процесс такого включения будем кратко называть специализацией модели (СМ), хотя точнее было бы использовать термин «специализация выразительных средств модели».

В случае построения систем из класса имитационных симуляторов (ИС) [2] в ходе специализации необходимо ввести в модель, как минимум, средства описания следующих особенностей ПО: (1) наличие в ПО активно действующих объектов (активность которых позволяет трактовать их как субъектов ПО); (2) взаимодействие субъектов, в том числе с точки зрения требуемой временной и пространственной синхронизации; (3) моделирование действий субъектов в условиях неполной и/или неточной информации, предполагающее поддержку «локальной» модели ПО с точки зрения конкретного субъекта. Далее будем называть их особенностями моделей для ИС (ОМИС).

Указанные задачи интенсивно исследовались как с теоретических, так и с практических позиций. В частности, в теоретической области были разработаны различные системы эпистемической и динамической логики [3]. Практические требования разработки ИС привели как к созданию языков моделирования (GPSS, СИМУЛА, IDEF), так и к включению в языки общего назначения (Pascal, Ada, Java, Concurent PROLOG) моделирующих возможностей [4].

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

Настоящая работа нацелена на построение формализованных средств СМ ИС на основе определения и исследования интенсиональных сущностей. В качестве основного средства специализации предлагаются пропозициональные концепты интенсионального вида. Предполагается, что подобное решение позволит повысить уровень средств СМ, используемых при разработке ИС.

1. Базовые языковые средства специализации модели

Алфавит используемого языка включает следующие символы:

(1) предметные константы a1, a2, …, an, … Константы также будут обозначаться буквами b, c, …, возможно, с индексами;

(2) предметные переменные x1, x2, …, xn, … Переменные также будут обозначаться буквами y, z, …, возможно, с индексами;

(3) предикатные константы P1, P2, …, Pn, … Предикатные константы также будут обозначаться буквами Q, R, …, возможно, с индексами;

(4) логические символы Ø, Ù, Ú, Þ, Û, ", $, =.

(5) скобки `(´, `)´ и запятая `,´;

(6) операторы: операторы необходимости □ и возможности ◊; пропозициональные операторы N1, N2, …, Nk, …, и операторы, связывающие переменные S1, S2, …, Sn, ….

Термы и формулы языка определяются в виде индуктивных классов. Поскольку возможны случаи как включения терма в формулу, так и обратного включения, классы термов и формул должны определяться одновременно. С учётом этого замечания классы термов и формул строятся обычным образом.

Далее будем рассматривать интерпретации различных языковых конструкций и вводить семантические домены, необходимые для построения интерпретаций. В качестве одного из основных доменов вводится множество индивидов D. Предполагаем, что индивид – исходное, неопределяемое понятие. При рассмотрении индивидов будем различать действительные, возможные и виртуальные индивиды, причём область D будем считать областью возможных индивидов. Будем также рассматривать область виртуальных индивидов V, которые будем понимать как некоторые идеальные объекты, вводимые для того, чтобы увеличить закономерность в рассматриваемом языке.

Ещё один семантический домен – множество точек соотнесения, понимаемых как различные собрания индивидов с дополнительной структурой или без неё. Любая система структур может быть индексирована элементами подходящего множества, причём различными способами. Возьмём фиксированное множество индексов, которые будем далее называть точками соотнесения (ТС) [3], так как для определения значения выражения необходимо «соотнести» его с точкой. Множество ТС будем обозначать Asg, отдельные ТС будем обозначать k Î Asg.

Прежде всего, отметим индексами систему действительных индивидов, положив возможно различные, Ak Í D для каждого k Î Asg. Не предполагается одно однозначное соответствие между Ak и k, так как элементы множества Asg могут обладать структурой, не полностью отражающейся в отличиях одного Ak от другого. Таким образом, в модели различаются действительные, возможные и виртуальные индивиды.

2. Цель исследования (постановка задачи)

В работе ставится задача построения формальной основы для СМ ИС, в том числе в области правоприменительной деятельности. Рассматривается класс КМ, содержащих средства, которые могут быть использованы для описания активных субъектов ПО и их точек зрения на ПО. Основой средств специализации является построение СМ на основе интерпретации языковых конструкций на (возможно, структурированном) множестве ТС.

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

3. Средства специализации моделей на основе интенсиональных концептов

В разделе задаются средства определения и вычисления значений интенсиональных концептов, используемые для специализации модели. В качестве основного средства специализации предлагаются пропозициональные концепты (ПК) интенсионального вида. Выполняется исследование различных конструкций, используемых при моделировании, в том числе экстенсиональных и интенсиональных предикатов. Фактически все рассматриваемые конструкции представляют собой функции, параметризованные посредством введения управления точками соотнесения, что обеспечивает согласованный учёт ОМИС. Основным средством согласования различных ОМИС являются интенсиональные операторы (ИО) различных видов.

Анализ средств, необходимых для учёта ОМИС позволяет сформулировать требования к средствам специализации КМ, ориентированных на построение ИС. Такие средства должны обеспечивать: 1) построение синтаксических средств задания ПК и ИО, включающих средства их параметризации посредством Asg; 2) построение средств интерпретации ПК и ИО с учётом набора приписанных способов параметризации; 3) задание ИО, предоставляющих формальные средства описания моделей субъектов ПО и их действий; 4) определение способов настройки интерпретации с учётом вложенности ИО различных видов.

Значением (индивидного) терма τ, используемого для описания индивида модели, будем считать частично определённую функцию с областью определения Asg. При этом считаем, что значения дескрипций должны принадлежать только D, а значения термов в общем случае должны лежать в V. Используем Asg → V+ для обозначения множества частичных функций, в то время как Asg → V есть множество всюду определённых функций. Тогда ||τ|| Î Asg → V+.

Примем обозначения истинностных значений: будем писать 1 для обозначения истины и 0 для обозначения лжи. Далее, утверждению Φ сопоставим функцию ||Φ||, определённую на Asg, со значениями из множества 2. Иначе говоря, будем писать ||Φ|| k = 1, когда Φ истинно относительно k. Тогда || Φ|| Î Asg → 2, если ||Φ|| k Î 2,  где k Î Asg, где A → B – множество функций, определённых на A со значениями из B.

Введём далее в язык константы a* для всех a Î V. Предполагаем, что соответствие между a и a* является взаимно однозначным.

При интерпретации кванторов вводим два квантора с разными свойствами.

(")  ||" x Φ (x)|| k = 1  т. и т.т., к. ||Φ (a*)|| k = 1 для всех a Î D

(".) ||". x Φ (x)|| k = 1 т. и т.т., к. ||Φ (a*)|| k = 1 для всех a Î Ak

и аналогично для ($) и ($.).

Рассмотрим предикаты, представляющие бинарные отношения. Будем допускать в языке выражения вида τ R σ, где τ, σ – термы. Это позволяет поставить вопрос, как интерпретировать R. Интерпретацию R по общим правилам обозначим через ||R||. Принимаем, что она является отношением между индивидными концептами. Таким образом,

||R|| Î ((Asg → V+) × (Asg → V+)) → (Asg → 2),  так что ||τ R σ|| = ||R|| (||τ||, ||σ||).

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

Принятый способ интерпретации R позволяет гарантировать, что если формула логически общезначима (то есть истинна во всех интерпретациях и относительно всех точек соотнесения в интерпретации), то она остаётся общезначимой и тогда, когда в неё вместо предикатных букв подставлены формулы.

Рассмотрим некоторые частные виды предикатов. Одним из практически наиболее интересных видов являются экстенсиональные предикаты. Лучшим примером экстенсиональных предикатов могут служить обыкновенные отношения R Í V × V. По аналогии с индивидами ту константу языка, которая соответствует отношению R, будем обозначать R*. Тогда: (R) ||τ R* σ|| k = 1 т. и т.т., к. (||τ|| k, ||σ|| k) Î R.

Для того, чтобы эта элементарная формула была истинной, должны быть определены как ||τ|| k, так и ||σ|| k. Однако для равенства принимается другое соглашение, потому что особая роль равенства обуславливает различные соглашения, принимаемые для большего единообразия среди общезначимых формул.

Принцип экстенсиональности для R* формулируется следующим образом:

τ = τ' Ù σ = σ' Ù τ R* σ Þ τ' R* σ'.

Рассмотрим теперь общий случай экстенсионального предиката. Предположим, что каждому k Î Asg сопоставлено отношение Rk Í V × V с возможно различными Rk для различных k. Можно рассматривать R как функцию, значениями которой служат отношения. Затем можно ввести в язык константу R~ (звёздочка (*) обозначает textit{константное} отношения, а тильда (~) – переменное отношение), значение которой задаётся так:

(R~) ||τ R~ σ|| k = 1 т. и т.т., к. (||τ|| k, ||σ|| k) Î Rk.

Введённый выше предикат Ak Í D как раз является предикатом отмеченного выше вида. Поэтому можно ввести в язык константу A~, описывающую существование в данной точке соотнесения: (A~) ||A~ τ|| k = 1 т. и т.т., к.  ||τ|| k Î Ak.

Для объяснения значения пропозициональных связок дадим обычные семантические определения: (Ø) ||Ø Φ|| k = 1 т. и т.т., к. ||Φ|| k = 0

(Ù) ||Φ Ù Ψ|| k = 1 т. и т.т., к. ||Φ|| k = 1 и ||Ψ|| k = 1

(Ú) ||Φ Ú Ψ|| k = 1 т. и т.т., к. ||Φ|| k = 1 или ||Ψ|| k = 1

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

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

(=) ||σ = τ|| k = 1 т. и т.т., к. ||σ|| k и ||τ|| k оба либо определены и равны, либо неопределённы.

4. Операторные средства специализации модели

Для установления и учета отношений более высокого порядка на ТС предлагается использовать операторы. Простейшим пропозициональным интенсиональным оператором является оператор необходимости □. (□) ||□ Φ|| k = 1 т. и т.т., к. ||Φ|| j = 1 для всех j Î Asg. Возможность ◊ определяется двойственным образом.

При желании можно сказать, что □ имеет в качестве интерпретации ||□||. В самом деле, ||□|| имеет тот же логический тип, что и ||Ø||: ||□||, ||Ø|| Î (Asg → 2) → (Asg → 2).

Они являются отображениями из множества пропозициональных концептов на множество пропозициональных концептов. Разница в том, что один из них экстенсионален, а другой нет. Можно написать ||□ Φ|| = ||□|| (||Φ||), что позволяет, в частности, представить интерпретацию операторов в аппликативной форме [1]. Введение оператора необходимости даёт возможность рассмотреть некоторые сложные фразы, например, □ (τ = σ). По определению: ||□ (τ = σ)|| k = 1 т. и т.т., к. ||τ|| j = ||σ|| j для всех j Î Asg.

Правое равенство выполняется и в случае, когда оба его терма неопределённы. Это означает, что ||□ (τ = σ)|| является концептом истинного выражения тогда и только тогда, когда выполняется ||τ|| = ||σ||, т.е. если ||τ|| и ||σ|| есть один и тот же индивидный концепт. Введём для этого понятия особый символ: τ º σ тогда и только тогда, когда □ (τ = σ).

Так различается экстенсиональное равенство (τ = σ) и интенсиональное (τ º σ). Назовём это более строгое понятие тождеством.

Легко показать, что предлагаемая система допускает подстановочность в следующем смысле. На основе принятых определений интенсионалов может быть выведено, что если τ и σ не имеют свободных переменных, то τ º σ Ù Φ (τ) Þ Φ (σ)

верно для тождества, тогда как аналогичный принцип для равенства не выполняется.

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

В системе могут рассматриваться отношения альтернативности. Пусть ρ Í Asg × Asg будет бинарным отношением на Asg, тогда соответствующий ρ оператор Nρ определяется так:

(Nρ) ||Nρ Φ|| k = 1 т. и т.т., к. ||Φ|| j = 1 для всех j Î Asg, где k ρ j.

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

Теперь оказывается достаточно легко перейти к самому общему монадическому пропозициональному оператору. Сопоставим каждому k Î Asg семейство Gk подмножеств Asg. Тогда можно определить следующий оператор:

(NG) || NG Φ|| k = 1 т. и т.т., к. { j Î Asg: ||Φ|| j = 1 } Î G_k,

что является просто тривиальной переформулировкой утверждения

||NG|| : (Asg → 2) → (Asg → 2).

До сих пор говорилось только об интенсиональных отношениях или интенсиональных операторах, действующих на предложения. Однако для дальнейшей специализации КМ требуются интенсиональные двойники экстенсиональных операторов типа кванторов и операторов дескрипции. Рассмотрим теперь, прежде всего, оператор S, который связывает одну переменную и навешивается на один терм и одну формулу; можно использовать его в языке в следующих выражениях: S x [τ (x), Φ (x)].  Будем считать S термообразующим оператором. Принимается, что  ||S x [τ (x), Φ (x)]|| Î Asg → V+.

Для определения зависимости от τ (x) и Φ (x) отметим, что эти выражения являются функциями от x, а все связанные переменные пробегают по D. Поэтому можно утверждать, что ||S|| Î U → (Asg → V+), где U = (D → ((Asg) → V)) × (D → (Asg → 2)), причём D → (Asg → V+) есть множество всех функций, значениями которых являются концепты, а областью определения – D; D → (Asg → 2) есть множество заданных на D функций, значениями которых служат пропозициональные концепты. Таким образом,

(S) ||S x [τ (x), Φ (x)]|| k = ||S|| (f, F) k, где f Î D → (Asg → V+) и F Î D → (Asg → 2) определяются так:  f(a)k = ||τ (a*)|| k, F (a) k = ||Φ (a*)|| k для всех a Î D.

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

Заключение

В работе предложены формализованные средства специализации КМ, в том числе используемых при разработке ИС в правоприменительной деятельности. Средства специализации построены на основе использования ПК различной степени интенсиональности. Выполнено исследование различных конструкций, используемых при КМ: (1) введён интенсиональный язык описания ПО, включающий интенсиональные описания, как основа для последующей специализации, определены его синтаксис и семантика; (2) определение экстенсиональных и интенсиональных предикатов обеспечивает возможность комбинирования различных способов оперирования объектами, включающих как чисто экстенсиональные способы, соответствующие пропозициональным связкам, так и специализированные кванторные операции, для которых формулируются условия применения; (3) введены специализированные операторы, позволяющие согласовывать результаты вычисления операций в различных точках соотнесения; (4) введены связывающие операторы, обеспечивающие возможность построения интенсиональных двойников рассматриваемых экстенсиональных понятий, в том числе кванторных операций. Операции включают возможности традиционных средств работы с данными (репликация и т. д.), но не ограничиваются ими.

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

Работа поддержана грантом РФФИ 11-07-00080-a.

Рецензенты:

Загребаев Андрей Маркоянович, д-р физ.-мат. наук, профессор, зав. кафедрой кибернетики, НИЯУ МИФИ, г. Москва.

Лебедев Георгий Станиславович, д-р техн. наук, заместитель директора, ЦНИИ ОИЗ, г. Москва.

Лубенцов Валерий Федорович, д-р техн. наук, профессор кафедры "Информационные системы, электропривод и информатика" Невинномысского технологического института ФГАОУ ВПО "Северо-Кавказский федеральный университет" Минобрнауки РФ, г. Невинномысск.