Электронный Научно - Информационный Журнал Системное Управление. Проблемы и Решения
 

Операции над родами структур

Выпуск 8

Пономарев И.Н.

Введение

Операциями над родами структур [1, 6] называются формальные преобразования, позволяющие из существующих текстов родов структур получать новые. В практике концептуального анализа и проектирования [2] наибольшее значение имеют операция порождения множества структур данного рода и операция синтеза, впервые описанные, по-видимому, в [3]. Хотя обе операции давно применяются, автору не известно опубликованных теоретических работ, содержащих строго формальные определения для этих операций и обосновывающих свойства родов структур, получаемых в результате. Данная статья призвана в некоторой степени восполнить этот пробел. Кроме того, в статье впервые исследуется вопрос непротиворечивости родов структур, получаемых при помощи операции синтеза.

1 Операция порождения множества структур данного рода

Пусть дан род структуры Σ  , имеющий типовую характеристику d ∈ S [x1,...xn]  и класс Σ  -объектов (теоретико-множественных интерпретаций) K    Σ   . Операция порождения множества структур данного рода позволяет в этом случае построить из Σ  такой род структуры ˜Σ  , что класс ˜Σ  -объектов будет удовлетворять условию

                  ˜           ˜  K ˜Σ = { (x1, ...xn,d) | ∀d(d ∈ d ⇒ (x1,...xn,d) ∈ K Σ)}.

Например, если Σ  есть род структуры функции из x1   в x2   , то ˜Σ  , получаемый из него операцией порождения множества структур данного рода, есть род структуры множества функций из x1   в x2   . В ˜Σ  -объекте элементами множества, соответствующего родовой константе, являются множества, которые могут интерпретировать родовую константу Σ  при фиксированной интерпретации базисных множеств.

Построить ˜Σ  можно по следующим правилам:

  1. базисные множества не изменяются;
  2. типовая характеристика T  вида d ∈ S [x1, ...xn]  заменяется на ˜T  вида ˜d ∈ 𝔓S [x1,...xn]  ;
  3. аксиома R  заменяется на аксиому R˜  вида ∀u ∈ d˜((u | d)R ).

Как видим, родовая константа в этом процессе превращается во множество, каждый элемент которого типизирован как исходная родовая константа. Заметим, что прежние выражения для внутренних термов Σ  теряют смысл в ˜Σ  в силу изменения типизации родовой константы.

Рассмотрим пример. Пусть x1   и x2   — базисные множества, тогда

  • род структуры функции Σ  :

    d ∈ 𝔓 (x1 × x2)  ;

    R1 : ∀u ∈ x1,∃v ∈ x2((u,v) ∈ d)  ;

    R2 : ∀t1 ∈ d,∀t2 ∈ d(pr1(t1) = pr1(t2) ⇒ t1 = t2)  ;

  • род структуры множества функций ˜Σ  :

    ˜d ∈ 𝔓 𝔓 (x1 × x2 )  ;

              ˜  R1 : ∀z ∈ d,∀u ∈ x1,∃v ∈ x2 ((u, v) ∈ z )  ;

    R2 : ∀z ∈ ˜d,∀t1 ∈ z, ∀t2 ∈ z (pr (t1) = pr (t2) ⇒ t1 = t2)                                1        1  .

Теорема 1. Если ˜Σ  построена из Σ  при помощи операции порождения структур данного рода, то класс ˜Σ  -объектов удовлетворяет условию

K ˜Σ = { (x1, ...xn, ˜d) | ∀d(d ∈ d˜⇒ (x1,...xn,d) ∈ K Σ)}.

◃ В самом деле: в силу определения 𝔓  , ˜T  ~ d˜∈ 𝔓S  [e1,...en]  ~ ∀d (d ∈ ˜d ⇒ d ∈ S [e ,...e ])                     1     n  , откуда T˜~  ∀d(d ∈ d˜⇒  T)  . По определению, R˜ ~ ∀d (d ∈ ˜d ⇒ R )  , из чего следует

T˜&  ˜R ~ ∀d (d ∈ ˜d ⇒ T &  R),

откуда и вытекает требуемое.▹

Род структуры ˜  Σ  , полученный операцией порождения множества структур данного рода заведомо непротиворечив, т. к. (ξ1,...ξn,∅ )  есть, как легко видеть, ˜Σ  -объект при любых множествах ξ1,...ξn  .

Можно доказать, что среди ˜Σ  -объектов (ξ1,...ξn,˜δ)  существуют объекты с непустым δ˜  тогда и только тогда, когда Σ  непротиворечив.

Теорема 2. Если F  — теорема Σ  , то формула F˜  вида       ˜  ∀u ∈ d(u | d )F  есть теорема ˜Σ  .

◃ При доказательстве теоремы 1 было установлено, что

⊢ ˜T & R˜ ⇒  ∀u(u ∈ ˜d ⇒  (u | d)(T & R )).

Но если T ′ ⊢ T & R ⇒  F  , то T ′ ⊢ (u | d)(T & R ) ⇒ (u | d )F  , и

T ′ ⊢ T˜ & ˜R ⇒ ∀u (u ∈ ˜d ⇒ (u | d )F ),

т. е. F˜  — теорема ˜Σ  .▹

2 Синтез родов структур

Потребность в синтезе родов структур возникает, когда имеется набор родов структур, описывающих различные аспекты изучаемой области, и требуется построить обобщающий, комплексный род структуры. Пусть даны род структуры Σ  с типовой характеристикой TΣ   и аксиомой R Σ   и род структуры Θ  с типовой характеристикой TΘ   и аксиомой RΘ   . Теоретико-множественные интерпретации Σ  и Θ  будут рассматриваться в некоторой единой теории T ′ .

Везде в дальнейшем мы будем предполагать, что имена всех конституэнт выбраны таким образом, что ни одно имя конституэнты (за исключением, может быть, имён вспомогательных базисных множеств) из Σ  не встречается среди имён конституэнт Θ  : простой перенумерацией конституэнт одной из родовых структур этого всегда можно добиться. Таким образом, текст, полученный простым объединением текстов Σ  и Θ  , является родом структуры с типовой характеристикой TΣ & T Θ   и аксиомой R Σ & R Θ   . Класс теоретико-множественных интерпретаций такого рода структуры будет, в некотором смысле, равен K   × K    Σ     Θ   и не будет пустым, если одновременно не пусты KΣ   и K Θ   .

Обычного слияния текстов родов структур бывает недостаточно: часто к получившемуся роду структуры необходимо добавлять утверждения о тождестве некоторых множеств Σ  некоторым множествам Θ  .

Рассмотрим пример. Предположим, что имеется род структуры Σ  линейного векторного пространства над полем действительных чисел ℝ  , с базисным множеством векторов x1   и родовой константой d1 ∈ 𝔓 (x1 × x1 × x1) × 𝔓 (ℝ × x1 × x1)  . Пусть, далее, имеется род структуры Θ  множества функций из x2   в x3   , с родовой константой d2 ∈ 𝔓 𝔓(x2 × x3)  . Объединив тексты этих родов структур и отождествив множество функций с базисным множеством векторов, т. е. добавив условие d  = x   2    1   , мы получим систему, некоторым образом описывающую линейные пространства над множеством функций. Эта система, однако, не будет являться родом структуры, т. к. соотношение d2 = x1   не является биективно переносимым. Но мы можем обойти эту ситуацию следующим образом: отбросить базисное множество x1   , родовую константу d1   заменить на ˜d ∈ 𝔓 (𝔓(x2 × x3) × 𝔓 (x2 × x3) × 𝔓 (x2 × x3 )) × 𝔓 (ℝ × 𝔓 (x2 × x3) × 𝔓 (x2 × x3))  , добавить аксиому  ˜  d ∈ 𝔓 (d2 × d2 × d2) × 𝔓(ℝ ×  d2 × d2)  и по всему тексту заменить x1   на d2   . Получившаяся система уже будет родом структуры, с вполне корректной типовой характеристикой и биективно переносимой аксиомой, класс его теоретико-множественных интерпретаций представляет собой класс линейных пространств функций над полем действительных чисел.

Подобную процедуру мы можем проделать в любом случае, когда базисное множество Σ  отождествляется с термом рода структуры Θ  типа 𝔓 (S)  (т. е. с термом, имеющим характер множества, но не элемента или кортежа). Разумеется, чтобы привести типизацию этого терма к нужному виду, можно воспользоваться операцией порождения множества структур данного рода над Θ  .

Рассмотрим ещё один, прикладной, пример: пусть имеется род структуры, описывающий «теорию субординации» в организации, в котором задано множество сотрудников x1   и на этом множестве введено отношение «подчинения» d1 ∈ 𝔓 (x1 × x1)  . Пусть, кроме этого имеется род структуры, описывающий «теорию родства», в котором задано множество людей x2   и на этом множестве введено отношение «быть родителем» d ∈  𝔓(x  × x )   2       2    2  . Если теперь отождествить множество сотрудников в первой теории и людей во второй (что в рассматриваемом случае можно сделать простой заменой x1   на x2   по всему тексту рода структуры), то в синтезированной теории будет выразимо и отношение «подчинения», и отношение «быть родителем». Также можно будет образовать принципиально новые термы, в которых используются оба эти отношения. Например, терм «множество подчинённых, которые являются детьми своего начальника».

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

Теперь перейдём к формальному определению. Пусть даны

  1. род структуры Σ  (который будем называть конкретизируемым родом структуры) с выделенными в нём p  базисными множествами. Без ограничения общности можно считать, что Σ  построен на n  базисных множествах x1,...xn  , из которых выделены p  первых x1,  xp  , p ≤ n  , и имеет родовую константу dΣ   , типовую характеристику T Σ   вида d Σ ∈ SΣ[x1,...xn]  и аксиому R Σ   ;
  2. род структуры Θ  (который будем называть конкретизирующим родом структуры) с выделенными в нём p  внутренними термами

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

    с типами 𝔓 (S1),...𝔓 (Sn)  , причём не исключается случай, когда любой из ψi  совпадает либо с базисным множеством Θ  , либо с родовой константой Θ  . Без ограничения общности можно считать, что Θ  построен на m  базисных множествах xn+1,...xn+m  и имеет родовую константу dΘ   , типовую характеристику TΘ   вида dΘ ∈  SΘ[xn+1,...xn+m ]  и аксиому R    Θ   .

В этом случае мы будем говорить, что Σ  и Θ  удовлетворяют условиям синтеза.

Рассмотрим класс

˜K =  {(x1,...xn,d Σ,xn+1,...xn+m, dΘ ) |       (T Σ & RΣ & T Θ & R Θ & (ψ1 = x1) & ...& (ψp = xp ))}.

Это есть интересующий нас класс пар вида «Σ  -объект, Θ  -объект» таких, что базисные множества x1,...xp  рода структуры Σ  тождественны термам ψ1,...ψp  рода структуры Θ  . Но коль скоро термы ψ1,...ψp  могут быть вычислены при данных xn+1,...xn+m, dΘ   , то каждому элементу ˜K можно поставить во взаимно однозначное соответствие элемент класса

K ˜Σ = {(xp+1,...xn, dΣ,xn+1,...xn+m, d Θ) |      (ψ1 | x1)...(ψp | xp)(TΣ & R Σ & TΘ & R Θ )}.

В самом деле: если (ξ1,...ξn,δΣ,ξn+1,...ξn+m, δΘ) ∈ K˜ , то отбрасывание из этого кортежа компонентов ξ1,...ξp  даёт, в силу свойств равенства, элемент класса K ˜    Σ   ; если же дан элемент (ξ   ,...ξ ,δ  ,ξ   ,...ξ    ,δ ) ∈ K   p+1     n  Σ   n+1     n+m   Θ      ˜Σ   , то добавление компонентов (ξn+1 | xn+1 )...(ξn+m | xn+m )(δΘ | d Θ)ψi  , i = 1,...p  в качестве первых p  множеств ξi  даёт, опять же в силу свойств равенства, элемент класса ˜K .

В определении класса K ˜Σ   отсутствуют не переносимые биективно условия (ψ1 = x1 ) & ...& (ψp = xp)  , и этот класс, как мы сейчас убедимся, является классом теоретико-множественных интерпретаций некоторого рода структуры  ˜  Σ  , который формально строится из родов структур Σ  и Θ  и который мы будем называть синтезированным родом структуры.

Правила построения синтезированного рода структуры ˜Σ  :

  1. конкретизируемые множества x ,   1  x   p  удаляются из текста конкретизируемого рода структуры (их место в синтезированном роде структуры займут термы ψ1,  ψp  );
  2. тексты обоих родов структур объединяются в один текст (предполагается, что имена всех конституэнт выбраны таким образом, что ни одно имя конституэнты из Σ  не встречается среди имён конституэнт Θ  ); если в текстах Σ  и Θ  имеются совпадающие вспомогательные базисные множества, то в тексте  ˜  Σ  оставляется одна копия;
  3. типовая характеристика TΣ   вида dΣ ∈ SΣ[x1,...xp,xp+1, xn]  заменяется на типовую характеристику T˜  вида ˜  d ∈ SΣ [S1[xn+1,...xn+m ],...Sp[xn+1,...xn+m  ],xp+1,xn ]

    (напомним, что термы ψ1,  ψp  имеют типы 𝔓 (S1),...𝔓 (Sn)  );

  4. во всех прочих выражениях все вхождения букв x1,  xp  заменяются на термы ψ1,  ψp  : мы будем обозначать через R˜  результат этой замены в аксиоме RΣ   ; ясно, что выражения TΘ   и RΘ   , не содержащие x1,  xp  в качестве параметров, в синтезированную схему перейдут без изменений;
  5. добавляется аксиома синтеза R   S  вида (ψ  | x )...(ψ | x )T    1   1       p   p  Σ   .

При этом мы говорим, что множества x  ,    1  x   p  рода структуры Σ  отождествляются с термами ψ1,  ψp  рода структуры Θ  . Вновь заметим, что не исключается случай, когда любой из ψi  совпадает либо с базисным множеством Θ  , либо с родовой константой Θ  (второе, правда, возможно лишь в случае, когда dΘ ∈ 𝔓 (...)  , т. е. dΘ   имеет характер множества).

Рассмотрим, теперь уже более развёрнуто, ещё один пример синтеза: рода структуры функции с родом структуры разбиения множества, где каждый элемент разбиения отождествляется с аргументом функции.

  • Род структуры функции Σ  :

    x1   , x2   ;

    d  ∈ 𝔓 (x  × x )   Σ       1    2  ;

    R1 : ∀u ∈ x1,∃v ∈ x2((u,v) ∈ dΣ )  ;

    R2 : ∀t1 ∈ dΣ, ∀t2 ∈ dΣ (pr1(t1) = pr1(t2) ⇒ t1 = t2)  .

  • Род структуры разбиения множества Θ  :

    x3   ;

    dΘ ∈ 𝔓 𝔓 (x3)  ;

    R3 : ∀u ∈ x3,∃g ∈ dΘ (u ∈  g)  ;

    R  : ∀g ∈ d  ,∀g  ∈ d ((g  = g ) ∨ (g  ∩ g  = ∅ ))    4    1    Θ   2    Θ   1    2      1   2  .

  • Род структуры функции от элементов разбиения ˜  Σ  :

    x2   , x3   ;

    ˜d ∈ 𝔓 (𝔓(x3 ) × x2)  ;

    dΘ ∈ 𝔓 𝔓 (x3)  ;

    ˜R1 : ∀u ∈ dΘ,∃v ∈ x2 ((u, v) ∈ d˜)  ;

               ˜      ˜  ˜R2 : ∀t1 ∈ d,∀t2 ∈ d(pr1(t1) = pr1(t2) ⇒ t1 = t2)  ;

    R  : ∀u ∈ x ,∃g ∈ d  (u ∈  g)    3        3       Θ  ;

    R4 : ∀g1 ∈ d Θ,∀g2 ∈ dΘ((g1 = g2) ∨ (g1 ∩ g2 = ∅ ))  ;

         ˜  RS : d ∈ 𝔓(dΘ ×  x2)  .

Может ли каждый элемент первой большой проекции ˜  d  быть любым подмножеством x3   ? Разумеется, нет: синтезируя Σ  и Θ  , мы предполагаем, что каждый аргумент функции d˜  является элементом разбиения dΘ   . Но легко видеть, что сам по себе этот факт не есть теорема ˜Σ  , поэтому в синтезированный род структуры добавляется аксиома синтеза RS  . Заметим, что в этом случае вкупе с соотношением типизации для ˜  dΣ   аксиома синтеза эквивалентна утверждению      ˜  P r1(d) ⊆ dΘ   .

Произведённые нами действия можно следующим образом проиллюстрировать на M-графах:

                       PWQVRU∙ST---dΣ              PWQVRUS∙T----˜d                            |                       |                            |                       |         d Θ                |             dΘ        |           -                               -         PWQV∙RUST           PWQVRUST           PWQVR∙UST   PWQVRUST           |                                |           |                                |           |           1       2            |   1       2  t ∈ dΘ----         PWQV∙RUST + PWQVxR1UST           PWQVxR2UST=  PWQVRUST           PWxQV2RUST           |       ∙---u ∈ x1               |           |                                |           |                                |                                          PWQVxRUST         PWxQV3RUST                              3

Не обязательно записывать аксиомы синтеза в виде, диктуемом определением операции синтеза. Действительно: пусть базисное множество x1   отождествляется с термом ψ  . Нетрудно проверить, что при типовых характеристиках 1) d ∈ x1   , 2) d ∈ x1 × x2   , 3) d ∈ 𝔓 (x1 × x2 )  , 4) d ∈ 𝔓 𝔓 (x  × x )            1    1  , 5) d ∈ 𝔓 𝔓 𝔓 (x ×  x )              1    2  , 6) d ∈ 𝔓 ((x ×  x ) × x )           1    2     1  , 7) d ∈ 𝔓 (x ) × x × x          1     1    2   аксиомы синтеза вместе с новым соотношением типизации будут эквивалентны, соответственно 1) d ∈ ψ  , 2) pr1(d) ∈ ψ  , 3) Pr1(d) ⊆ ψ  , 4)      ⋃               ⋃  P r1(  d) ⊆ ψ & P r2(  d) ⊆ ψ  , 5)      ⋃ ⋃  P r1(    d) ⊆ ψ  , 6) P r1(P r1(d )) ⊆ ψ &  Pr2(d) ⊆ ψ  , 7) pr1(d) ⊆ ψ &  pr2(d) ∈ ψ  .

Теорема 3. Пусть ˜Σ  — синтезированный из Σ  и Θ  род структуры, K ˜    Σ   — класс ˜Σ  -объектов. В этом случае выполняется соотношение

K ˜Σ = {(xp+1,...xn, dΣ,xn+1,...xn+m, d Θ) |      (ψ1 | x1)...(ψp | xp)(TΣ & R Σ & TΘ & RΘ )}.

(Как мы помним, из этого класса можно построить класс пар вида «Σ  -объект, Θ  -объект» таких, что базисные множества x1,...xp  рода структуры Σ  тождественны термам ψ1,...ψp  рода структуры Θ  .)

◃ В соответствии с определениями операции синтеза и класса теоретико-множественных интерпретаций,

KΣ˜=  {(xp+1,...xn,d Σ,xn+1,...xn+m, dΘ ) |      T˜&  TΘ & R Θ & (ψ1 | x1)...(ψp | xp)(T Σ & RΣ )}.

Здесь знаком T˜  обозначено соотношение типизации, получаемое из T   Σ   заменой всех вхождений букв x1,  xp  на S1[...],...Sp [...]  . Выражение (ψ1 | x1)...(ψp | xp )TΣ   соответствует аксиоме синтеза. Иначе говоря, требуется доказать, что

(ψ  | x )...(ψ  | x )(T & R   & T  & R  ) ~     1 ˜ 1      p   p   Σ     Σ    Θ     Θ    ~  T & T Θ & RΘ & (ψ1 | x1)...(ψp | xp)(TΣ & R Σ).

Формула TΘ & R Θ   , унаследованная из конкретизирующего рода структуры, не содержит в качестве параметров букв x1,  xp  , поэтому (ψ1 | x1)...(ψp | xp)(TΘ & R Θ ) ~ T Θ & R Θ   и эту формулу вообще можно исключить из рассмотрения, доказывая лишь, что

(ψ1 | x1)...(ψp | xp)(T Σ & RΣ ) ~    ~ T˜ & (ψ  | x )...(ψ | x )(T   & R  ).             1   1       p   p   Σ     Σ

Но для этого достаточно доказать, что

                             ˜  ⊢ (ψ1 | x1)...(ψp | xp)T Σ ⇒ T .

Напомним, что формула T Σ   имеет вид dΣ ∈ SΣ [x1,...xn ]  , а T˜  — вид

dΣ ∈ SΣ [S1 [xn+1, ...xn+m ],...Sp [xn+1, ...xn+m ],xp+1, ...xn],

где 𝔓Si [xn+1, ...xn+m ]  — типизация терма ψi  , i = 1,...p  . Докажем (ψ1 | x1 )...(ψp | xp)TΣ ⇒ T˜  индукцией по построению схемы SΣ   .

  1. Если SΣ =  i  , то возможны два варианта. Случай i > p  тривиален: замены нет и TΣ   и ˜  T  есть одна и та же формула. Если i ≤ p  , то u ∈ ψi & ψi ∈ 𝔓Si [xn+1, ...xn+m ] ⇒ u ∈ Si[xn+1,...xn+m ]  .
  2. Если SΣ = 𝔓 (S *)  , причём, по предположению индукции,                           *  (ψ1 | x1)...*(ψp | xp)(u ∈ S ) ⇒    ⇒  u ∈ S [S1[xn+1,...xn+m ],...Sp[xn+1,...xn+m ],xp+1,...xn],

    то, с учётом

             *                    *  u ∈ 𝔓 (S  ) ~ ∀t(t ∈ u ⇒ t ∈ S )

    имеем

    (ψ1 | x1)...(ψp | xp )(u ∈ 𝔓 (S *)) ⇒    ⇒  u ∈ 𝔓 (S*[S [x   ,...x    ],...S [x   ,...x    ],x   ,...x ]).                  1  n+1     n+m       p  n+1     n+m    p+1     n
  3. Если SΣ = S *1 × S *2   , то u ∈ S*[...] × S*[...] ⇒  ∃v∃w (v ∈ S*[...] & w ∈ S *[...] & (v,w ) = u),       1        2                   1             2

    откуда, с использованием предположения индукции, уже легко получить требуемое.▹

Можно доказать, что если F  — теорема Σ  , то (ψ1 | x1)...(ψp | xp )F  — теорема ˜Σ  .

3 Критерий непротиворечивости синтезированного рода структуры

Будет ли построенный при помощи синтеза род структуры ˜Σ  непротиворечивым? Легко видеть, что необходимым условием непротиворечивости синтезированного рода структуры является непротиворечивость синтезируемых родов структур.

Однако даже при синтезе непротиворечивых родов структур может образоваться противоречивый род структуры. Например, характер аксиом Σ  может влечь бесконечность множества, соответствующего x1   , в любой теоретико-множественной интерпретации Σ  , а терм ψ1   рода структуры Θ  может быть конечным в любой теоретико-множественной интерпретации Θ  . Ясно, что если попытаться отождествить x   1   с ψ   1   , то для синтезированного рода структуры не найдётся теоретико-множественных интерпретаций, т. е. он будет противоречивым.

Теорема 4. Пусть Σ  — конкретизируемый, Θ  — конкретизирующий род структуры, причём множества x ,    1  x    p   рода структуры Σ  отождествляются с термами ψ1,  ψp   рода структуры Θ  . Синтезированный род структуры Σ˜  непротиворечив тогда и только тогда, когда одновременно выполнены следующие условия:

  1. существует Σ  -объект υ =  (ξ ,...ξ ,δ )         1     n  Σ  ;
  2. существует Θ  -объект ω = (ξn+1,...ξn+m, δΘ)  ;
  3. каждое из множеств ξ1,...ξp   равномощно соответствующему множеству Їψi = (ξn+1 | xn+1)...(ξn+m | xn+m )(δΘ | dΘ)ψi,

    где i = 1 ...p  , p ≤ n  .

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

◃ В одну сторону: пусть указанная пара объектов υ  , ω  существует. По условию, должны существовать биекции φ1 : ξ1 ↔ Їψ1   , φ2 : ξ2 ↔ ψЇ2   φp : ξp ↔ Їψp  и возможен перенос ξ1,...ξp  на Їψ1,...ψЇp  при типовой характеристике рода структуры Σ  с построением терма ˜δ  из терма δ   Σ   при помощи канонического распространения. Покажем, что ˜Σ  -объектом является объект, построенный следующим образом:

  1. базисные множества, унаследованные из Σ  , интерпретируются термами ξp+1,...ξn  ;
  2. базисные множества, унаследованные из Θ  , интерпретируются термами ξn+1,...ξn+m  ;
  3. множество, интерпретирующее родовую константу ˜  d  , получается из δΣ   переносом ξ1,...ξp  на ψЇ1, ...Їψp  при типовой характеристике рода структуры Σ  ;
  4. родовая константа, унаследованная из Θ  , интерпретируется термом δΘ   .

В самом деле: поскольку ξn+1   ,…ξn+m  и δΘ   , составляющие Θ  -объект ω  , используются без изменений, то переходящие без текстуальных изменений в синтезированный род структуры соотношения TΘ & R Θ   продолжают выполняться. Аксиома RΣ   выполняется в силу своей биективной переносимости, аксиома синтеза выполняется по построению, типовая характеристика ˜T  синтезированного рода структуры выполняется в силу

⊢ (ψ1 | x1)...(ψp | xp)TΣ ⇒ ˜T

(см. доказательство теоремы 3).

В обратную сторону: пусть имеется ˜Σ  -объект ζ  . Тогда терм ω  , полученный отбрасыванием из ζ  множеств, соответствующих базисным множествам и родовой константе, унаследованным из Σ  , является Θ  -объектом ( ˜  T & T Θ & R Θ & (ψ1 | x1)...(ψp | xp )(T Σ & RΣ ) ⇒ TΘ & R Θ   ).

Пусть полученный таким образом объект ω  равен (ξn+1,...ξn+m, δΘ)  , а Їψi = (ξn+1 | xn+1)...(ξn+m | xn+m )(δΘ | dΘ)ψi  , i = 1...p  . Терм υ  , полученный из ζ  использованием

  1. Ї      Ї  ψ1,...ψp  для интерпретации первых p  базисных множеств;
  2. множеств, интерпретирующих унаследованные из Σ  , для интерпретации базисных множеств с номерами p + 1 ...n  ;
  3. множества, интерпретирующего синтезированную родовую константу, для интерпретации родовой константы dΣ

есть Σ  -объект. Первые p  множеств этого Σ  -объекта совпадают по построению с термами ψЇ1, ...Їψp  — следовательно, они равномощны этим термам.▹

Литература

[1] Бурбаки Н. Теория множеств: Пер. с фр. / Под ред. Успенского В. А. — М.: Мир, 1965. — 455 с.

[2] Кучкаров З. А. Методы концептуального анализа и синтеза в теоретическом исследовании и проектировании социально-экономических систем: Курс лекций. В 2 т. — М.: «Концепт», 2005. — 252, 260 с.

[3] Никитина Н. К. Разработка и исследование методов и средств автоматизированного синтеза баз данных на концептуальном уровне: Автореф. дис. канд. техн. наук: 05.13.06. — МФТИ, 1984. — 24 с.

[4] Пономарев И. Н. Семантико-синтаксический анализатор текстов родов структур Бурбакизатор // Технология концептуального проектирования / Под ред. Никанорова С. П. — М.: «Концепт», 2004.

[5] Пономарев И. Н., Гараева Ю. Р. Базисные преобразования на множестве ступеней и операции над термами в аспекте этих преобразований // Труды XLVI научной конференции МФТИ. — 2003.

[6] Павловский Ю. Н., Смирнова Т. Г. Проблема декомпозиции в математическом моделировании. — М.: ФАЗИС, 1998. — 266 с.

 
© МФТИ
© МЭРТ
© НП Аналитический центр "Концепт"
Сайт разработан:
"Golden CMF" ™ - 2energies ©

Издательство «Концепт» Москва 2004
Дата последней редакции: 16.10.2009

ГЛАВНАЯ   |   ПУБЛИКАЦИИ   |   РУБРИКАТОР   |    АВТОРСКИЙ УКАЗАТЕЛЬ   |   О ЖУРНАЛЕ   |   УЧРЕДИТЕЛИ