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

Язык родов структур

Выпуск 7

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

Введение

Формальная система Бурбаки [1, 2] разрабатывалась с 40-х гг. XX в. с целью дать универсальный метод описания математических объектов исследования с помощью математической логики и теории множеств. В качестве такого метода Бурбаками был предложен аппарат родов структур. Критерием корректности математической теории, таким образом, можно считать возможность трансляции её определений, утверждений и доказательств в формально корректные родоструктурные тексты.

Область применения родов структур, однако, не ограничивается внутриматематическими задачами. С 70-х гг. XX в. в нашей стране развивается «концептуальное направление», основной идеей которого является использование аппарата родов структур Бурбаки для построения концептуальных моделей различных предметных областей [3]. В частности, разрабатывались методы создания автоматизированных систем управления предприятиями на основании синтаксически корректной концептуальной модели того, что на современном языке называется «бизнес-сущностями» и «бизнес-процессами».

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

Двумя ключевыми требованиями, предъявляемыми к выражениям термов и логических соотношений, которые могут быть использованы в тексте рода структуры, являются 1) их синтаксическая корректность и 2) их биективная переносимость. Данная статья концентрируется в основном на втором из этих требований. В статье показано, что условия биективной переносимости, выявленные ещё Бурбаки, могут быть выражены в виде семантических правил языка (термин «семантическое правило» употребляется в смысле, принятом в теории формальных языков, см. [5]), и алгоритмы проверки обоих условий могут быть эффективно построены с помощью стандартных методов, применяемых при создании компиляторов языков программирования.

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

 

1 Теории

Напомним, что в математической логике термин «теория» определяется как совокупность замкнутых формул (аксиом) некоторой сигнатуры. В сигнатуре с единственным предикатным символом «∈ » можно построить теорию множеств — например, ZFC. Как известно, ZFC не является единственной возможной теорией множеств: независимость аксиом выбора и континуум-гипотезы от остальных аксиом ZF, возможность их формулировки в различных «сильных» и «слабых» формах порождает большое количество вариантов того, что можно считать «теорией множеств».

Для дальнейших построений нам будет несущественно, какой из вариантов теории множеств выбрать. Для большей части построений этой главы существенной будет только выполнимость первых четырёх аксиом ZF (экстенсиональности, множества-степени, множества-суммы и схемы подстановки), которых, как мы знаем, достаточно для того, чтобы ввести операции построения множества частей 𝔓 (x)  и декартова произведения x × y  . Для того, чтобы наши рассуждения обрели максимальную общность, мы введём специальные соглашения.

Будем обозначать теории каллиграфической буквой T со штрихами и индексами. Говорят, что теория T ′ сильнее теории T , если все без исключения теоремы T являются теоремами T ′ . В частности, любая теория сильнее себя самой, противоречивая теория сильнее любой теории, и если T ′ получена добавлением новых аксиом к T , то T ′ сильнее T .

 

2 Шкалы и ступени

Схема конструкции ступени (по Павловскому [2]) есть выражение, определяемое следующим образом:

  1. индекс

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

    есть схема конструкции ступени;
  2. если S  — схема конструкции ступени, то 𝔓 (S)  — схема конструкции ступени;
  3. если S  и S′ — схемы конструкции ступени, то (S ×  S′)  — схема конструкции ступени;
  4. других схем конструкции ступени не существует.

Иногда вместо «схема конструкции ступени» мы будем говорить просто «схема», если из контекста ясно, что речь идёт о схеме конструкции ступени. Если S  — схема, а n  — максимальный индекс, использованный при её построении, то S  называется схемой конструкции ступени над n  множествами.

Примеры: 1  — схема над одним множеством; 2  , (1 × 2)  , 𝔓 (𝔓 (2))  и 𝔓 (1 × 𝔓 (2))  — схемы над двумя множествами; 𝔓 (3 × 5 )  — схема над пятью множествами.

Внешние скобки на каждом шаге построения схемы нужны для того, чтобы однозначным образом определять последовательность вычислений. Для удобства будем экономить скобки в тех случаях, когда последовательность очевидна: прежде всего, откажемся от внешних скобок на последнем шаге построения схемы (например, схему (1 × 2)  будем записывать как 1 × 2  ). Во-вторых, будем считать, что операция × выполняется последовательно слева направо, т. е. схемы вида (1 × 2) × 3  (но не 1 × (2 × 3)  ) будем записывать как 1 × 2 × 3  .

Пусть дана схема S  над n  множествами и не менее чем n  переменных ξ1,...ξn′ ,   ′
n  ≥ n  . Тогда терм, полученный заменой индексов в схеме S  на буквы ξ1,...ξn  с соответствующими индексами, мы будем называть ступенью, построенной по схеме S  над множествами ξ1,...ξn′ и обозначать как S[ξ1,...ξn′]  . Пример: если S  — схема 𝔓 (1 × 𝔓 (2))  , то S[x1,x2] = 𝔓 (x1 × 𝔓 (x2))  и S[y1,y2] = 𝔓 (y1 × 𝔓 (y2))  .

Шкалой над множествами x1,...xn  называется совокупность всех ступеней, которые можно построить по какой-л. схеме над множествами x1,...xn  . Иначе говоря, шкала над x1,...xn  — это совокупность всех множеств, которые можно построить из исходных множеств при помощи операций декартова произведения и множества-степени. Шкала сама является множеством (причём счётным), т. к. все её элементы можно перечислить при помощи рекурсии.

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

Построим граф по следующему алгоритму: изобразим множества x1,...xk  в виде вершин; если A  — вершина, соответствующая ступени m  , то для ступени 𝔓 (m )  достроим новую вершину M-графа, соединяя её дугой с вершиной A  ; если A1   , A2   — вершины, соответствующие ступеням m1   , m2   (возможно, какие-то из них — совпадающие), то для ступени m  ×  m
  1     2   достроим новую вершину M-графа, соединяя её нумерованными дугами с вершинами A1   , A2   , причём номер каждой дуги соответствует позиции mi  в декартовом произведении. Пример M-графа см. на рис. 1: в нём вершина A  соответствует ступени 𝔓 (x1)  , вершина B  — ступени x1 × x2   и т. д.

 


           PWPWQVQVRURUSSTT
        F

                 2

                   PWPWPWQVQVQVRRRUUUSTSTST E


         1               1

                 2         PWPWQVQVRRUUSSTTD
                              |
                              |
                              |

A  PWQVPWQVRRUUSSTT   PWQVRUST B         PWPWPWQVQVQVRRRUUUSSSTTTC
     |                     --  --
     |   1       2         1    2
     |                     --  --
   PWQVxRUST           PWxQVRUST   PWQVxRUST
     1                2       3


Рис. 1: Пример M-графа

 


3 Соотношение типизации

Формула вида ξ ∈ S[x1,...xn]  , где ξ  — произвольная переменная или терм, называется соотношением типизации для переменной (терма) ξ  . Если для ξ  выполняется соотношение типизации, то говорят также, что множество (переменная, терм) ξ  типизировано ступенью S [x1, ...xn]  , или имеет тип S [x1,...xn]  .

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

  • элементы множеств x1,...xn  (если соотношение типизации имеет вид ξ ∈ xi  ), в этом случае говорят, что ξ  имеет характер элемента;
  • кортежи, каждый компонент которых типизирован (если соотношение типизации имеет вид ξ ∈ S [x ,...x ] × ...× S  [x ,...x  ]
     1  1     n           k 1      n  ), в этом случае говорят, что ξ  имеет характер кортежа;
  • множества, каждый элемент которых типизирован (если соотношение типизации имеет вид ξ ∈ 𝔓 (S[x1,...xn])  ), в этом случае говорят, что ξ  имеет характер множества.

Например, если d ∈ x1 × x2   , то d — это пара элементов: (...,...)  . Если d ∈ 𝔓 (x1 × x2)  , то d — это некоторое множество пар: {(...,...)  , (...,...),...} . Если d ∈ 𝔓𝔓 (x1 × x2)  , то d — это множество множеств пар: {{(...,...)  , (...,...) ...} , {(...,...)  , (...,...)...}, ...} . Если d ∈ 𝔓 (x ) × 𝔓 (x )
        1        2  , то d — это пара множеств: ({...},{...})  . Если d ∈ 𝔓 (𝔓 (x ) × x )
           1     2  , то d — это множество пар вида «множество, элемент»: {({...},...)  , ({...},...),...} и т. д.

Таким образом, типизированное множество не допускает, например, существования среди своих элементов «вперемешку» множеств и кортежей, или кортежей с разным количеством компонент. Условие ξ ∈ S [x  ,...x ]
        1     n  кажется существенным ограничением для ξ  , но, как показывает практика, одних только типизированных множеств вполне достаточно для описания средствами теории множеств математических объектов и построения прикладных моделей.

 

4 Канонические распространения отображений

Другой важной особенностью типизированного множества является тот факт, что в ситуации, когда множества x1,...xn  подвергаются преобразованиям, типизированное множество ξ ∈ S [x1,...xn ]  может быть преобразовано вместе с x1,...xn  некоторым согласованным образом.

Пусть даны множества x  и x ′ , а также функция f : x → x′ . Функция fˆ: 𝔓 (x) → 𝔓 (x′)  , определённая по формуле 𝔓ˆ(f) = {(u,v ) ∈ 𝔓 (x) × 𝔓 (x′) | f [u ] = v} , называется каноническим распространением f  на множество частей.

Пусть даны множества x1   , x2   , x′
 1   , x ′
  2   , а также функции f1 : x1 → x ′
           1   и f : x →  x ′
 2   2     2   . Функция f ׈f   : x × x  →  x′×  x′
 1   2   1    2     1    2   , определённая по формуле                    ′  ′                  ′    ′            ′           ′
f1׈f2  = {((u,v),(u ,v )) ∈ (x1 × x2) × (x1 × x2) | f1(u) = u & f2(v) = v } , называется каноническим распространением f1   , f2   на декартово произведение.

Пусть имеются множества x1,...xn  , x ′1,...x′n  и функции f1,...fn  такие, что fi : xi → x ′
           i  , как показано на диаграмме:

x1      x2      ...     xn
 |       |               |
 f1      f2               fn
x′      x′      ...     x′
 1       2               n

Пусть также дана схема S  над не более чем n  множествами.

Функция, получаемая из схемы S  заменой индексов 1, 2,3...  на буквы fi  с соответствующими индексами, знаков 𝔓  на 𝔓ˆ  и знаков × на ˆ× , называется каноническим распространением f1,...fn   по схеме S  , обозначается           S
⟨f1,...fn⟩  и обладает свойством

          S                    ′     ′
⟨f1,...fn⟩ : S[x1,...xn] →  S[x1,...xn].

Например, если даны f1 : x1 → x′1   и f2 : x2 → x ′2   , а также схема 𝔓 (1 × 2)  , то можно построить по этой схеме функцию ˆ𝔓 (f1ˆ×f2) : 𝔓 (x1 × x2) → 𝔓 (x′1 × x′2)  .

Применение функции ⟨f1,...fn ⟩S  к типизированному множеству d ∈ S[x1,...xn]  называется переносом множества d  с помощью функций f1,...fn  . В соответствии с данными нами определениями, результат переноса будет являться типизированным множеством, причём

          S         ′      ′
⟨f1,...fn⟩ (d) ∈ S [x1,...x n].

Например, если d ∈ 𝔓 (x1 × x2)  и даны f1 : x1 → x ′1   и f2 : x2 → x′2   , то мы можем получить d′ = 𝔓ˆ(f1ˆ×f2 )(d)  , такую, что d ∈ 𝔓 (x′×  x′)
        1    2  , при этом каждой паре (u,v ) ∈ d  соответствует пара (u ′,v′) ∈ d′ такая, что u′ = f (u )
      1  и v′ = f (v)
      2  .

 

5 Перенос типизированных множеств

Пусть фиксированы

  • теория множеств T ,
  • переменные x1,...xn  , называемые основными базисными множествами;
  • термы теории T θ1,...θm  , называемые вспомогательными базисными множествами;
  • схема S  не более чем над n + m  множествами и соотношение типизации T  вида d ∈ S[x1,...xn,θ1,...θm ]  (здесь и далее предполагается, что при построении ступени по схеме S  индексы n +  i  в выражении схемы заменяются на множества θi  , т. е. d  есть элемент некоторой ступени, построенной на множествах x1,...xn,θ1,...θm  ), буква d  будет называться родовой константой;
  • переменные  ′     ′
x1,...xn  , переменные f1,...fn  и соотношение переноса F  вида            ′                   ′
f1 : x1 ↔ x1 & ...& fn : xn ↔ xn

    (каждая fi  есть биекция между xi  и x ′
  i  ).

Если значения переменных x ,...x
 1     n  , x′,...x′
 1     n  , f ,...f
 1     n  заданы (т. е. приравнены некоторым термам теории   ′
T , совпадающей с T или более сильной), причём  ′
T  ⊢ T & F  , то мы можем построить множество  ′     ′      ′
d ∈ S [x1,...x n,θ1,...θm]  следующим образом:

 ′                         S
d = ⟨f1,...fn,idθ1,...idθn⟩ (d),

где idθi   — тождественное отображение θi  в θi  .

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

Формула R  , возможно, содержащая в качестве параметров переменные x1,...xn  и переменную d  , называется биективно переносимой (в теории T при типизации T  ), если

T ⊢ T &  F ⇒  (R ⇔  (x1 | x′)...(xn | x ′)(d | d′)R ).
                          1           n

Терм ξ  , возможно, зависящий от переменных x1,...xn  и d  , называется биективно переносимым (в теории T при типизации T  ), если имеется такая схема S ξ  , что выполняются следующие два условия:

 

  1. T ⊢ T  ⇒  ξ ∈ S [x ,...x  ,θ ,...θ ]
               ξ  1     n  1     n  ,
  2.                     ′           ′      ′                           Sξ
T ⊢ T &  F ⇒  (x1 | x1)...(xn | xn)(d | d)ξ = ⟨f1,...fn,idθ1,...idθn⟩ (ξ)  .

Примеры:

  • если T  есть d ∈ x ×  x
     1    1   , то соотношение pr (d) = pr (d)
  1        2  биективно переносимо (в самом деле: пусть d = (u,v)  , тогда  ′
d =  (f1(u ),f1(v ))  и                        ′         ′
pr1(d) = pr2(d) ⇔ pr1(d ) = pr2(d )  );
  • соотношение x1 = x2   не является биективно переносимым (в самом деле: пусть x1 = x2   , x′1 = x1   , f1 = idx1   , в качестве x′2   возьмём любое равномощное x′
 2   , но не равное x2   множество и получим x ′⁄= x ′
  1    2   );
  • если T  есть d ∈ 𝔓 (x1)  , то соотношение d =  x1   биективно переносимо, а соотношение d = x2   не является биективно переносимым;
  • терм x1 ∪ x2   не является биективно переносимым (нарушается первое условие биективной переносимости термов);
  • если T  есть d ∈ 𝔓 (x1) × 𝔓(x1)  , то терм pr1(d) ∪ pr2 (d )  является биективно переносимым (с типом 𝔓 (x1)  ).
  • терм {t ∈ Sξ[x1,...] | x1 = x2 } не является биективно переносимым (выполняется первое условие: терм имеет типизацию 𝔓 (Sξ[x1,...])  , но нарушается второе условие биективной переносимости термов).

 

6 Условия биективной переносимости

Выявим некоторые достаточные условия биективной переносимости термов и соотношений.

Теорема 1. Справедливы следующие утверждения:

  • если ни одна из букв x1, ...xn   , d  не встречается в соотношении R  , то R  биективно переносимо;
  • терм ∅  есть биективно переносимый терм типа 𝔓S  ′[x1,...]  , какова бы ни была схема S′ ;
  • при типизации d ∈ S[x1,...]  xi   — биективно переносимые термы типа 𝔓 (xi)  , θi   — биективно переносимые термы типа 𝔓 (θi)  , d  — биективно переносимый терм типа S [x1,...]  ;
  • если R  и R′ — биективно переносимые соотношения, то же верно и для соотношений R  , R ∨ R ′ , R &  R′ , R ⇒  R ′ , R  ⇔  R′ .

◃ Эти условия вытекают непосредственно из определений.▹

Теорема 2. Справедливы следующие утверждения:

  • если ξ  — биективно переносимый терм типа Sξ[x1,...]  и ξ′ — биективно переносимый терм типа 𝔓 (S ξ[x1, ...])  , то соотношение ξ ∈ ξ ′ биективно переносимо;
  • если ξ  и  ′
ξ — биективно переносимые термы одного и того же типа S ξ[x1,...]  , то соотношение ξ = ξ ′ биективно переносимо.

◃ Пусть, для краткости, f Sξ = ⟨f1,...fn, id θ1,...idθn⟩Sξ   . Докажем первое утверждение. По условию,

                    ′         ′      Sξ
T ⊢ T & F  ⇒  (x1 | x1)...(d | d )ξ = f (ξ)&
         &(x1 | x′1) ...(d | d′)ξ′ = ˆ𝔓f Sξ(ξ′).

В силу свойств равенства,

T  ⊢ T & F  ⇒ (x1 | x ′1)...(d | d′)(ξ ∈ ξ′) ⇔ (fSξ(ξ) ∈ ˆ𝔓f Sξ(ξ′)).

Но  ˆ Sξ  ′     Sξ  ′
𝔓f   (ξ ) = f  [ξ]  , откуда  Sξ      ˆ  Sξ  ′     Sξ       Sξ ′
f  (ξ) ∈ 𝔓f   (ξ ) ~ f  (ξ) ∈ f  [ξ ]  .

Индукцией по построению S ξ  можно показать, что, когда все f1,...fn  — биекции,  S
f ξ   — также биекция, откуда следует fSξ(ξ) ∈ fSξ[ξ′] ~ ξ ∈ ξ′ и биективная переносимость соотношения ξ ∈ ξ′ .

Второе утверждение теоремы доказывается аналогичным образом.▹

Теорема 3. Если термы ξ  и η  переносимые термы типов, соответственно 𝔓 (S  [x ,...])
    ξ  1  и 𝔓 (S [x ,...])
    η  1  , то ξ × η  есть переносимый терм типа 𝔓 (Sξ[x1,...] × Sη[x1,...])  и 𝔓 (ξ)  есть переносимый терм типа 𝔓 𝔓 (S ξ[x1,...])  .

Обратим внимание: существенно, чтобы ξ  и η  имели характер множеств.

◃ Докажем, что (x1 | x′1)...(d | d′)(ξ × η ) = 𝔓ˆ(f Sξ× ˆf Sη)(ξ × η)  , для чего, в силу биективной переносимости и характера ξ  и η  , достаточно доказать, что fSξ[ξ] × f Sη[η] = fSξ׈f Sη[ξ × η]  .

В самом деле: t ∈ fSξ[ξ] × fSη[η]  ~ ∃u ∃v(u ∈ f Sξ[ξ] & v ∈ fSη[η] & t = (u,v))
~ ~
~      S    Sη
t ∈ f ξ× ˆf  [ξ × η]  .

(Последний шаг выкладки выполнен с учётом (f Sξ(z),f Sη(w)) = fSξ ˆ×f Sη((z,w ))  .)

Докажем биективную переносимость терма .


.                                                        ▹

Теорема 4. Для всякой схемы конструкции ступени S′ терм S ′[x1,...xn,θ1,...θn ]  есть биективно переносимый терм типа 𝔓S ′[x ,...x  ,θ ,...θ ]
     1      n  1     n  .

◃ Доказывается с помощью теоремы 3 индукцией по построению S ′ .▹

Теорема 5. Пусть формула R  (зависящая, возможно, от t  ) удовлетворяет условию

T  & F & (t ∈ St[x1,...]) ⇒ (R  ⇔  (x1 | x ′1)...(d | d′)(f St(t) | t)R ).

Тогда терм {t ∈ St[x1, ...] | R } биективно переносим.

(Заметим, что условие, налагаемое теоремой на R  , по сути ничего нового не добавляет к условию биективной переносимости: в частности, ему удовлетворяют не зависящие от t  биективно переносимые соотношения и соотношения, биективно переносимые при соотношении типизации t ∈ St[x1,...]  .)

◃ Воспользовавшись теоремой о дедукции, перейдём, для удобства, в теорию TT  , полученную добавлением к T соотношений T  , F  и t ∈ St[x1,...]  . Нам нужно доказать, что

T  ⊢ 𝔓ˆf  St({t ∈ S [x ,...] | R }) = (x | x′)...(d | d′){t ∈ S [x ,...] | R }.
 T               t  1               1   1                 t 1

Действительно:
.

К только что выведенному соотношению f St[{t ∈ St[x1,...] | R}] = {t ∈ fSt[S[x1,...]] | ((f St)- 1(t) | t)R} можно прийти и таким неформальным рассуждением: чтобы найти «образ» терма {t ∈ St[x1,...] | R } , мы должны среди элементов множества fSt[St[x1, ...]]  выбрать такие, чей «прообраз» удовлетворяет R  .

В силу установленной в теореме 4 биективной переносимости терма St[x1,...xn,θ1,...θn]  , в TT  имеет место fSt[St[x1, ...]] = 𝔓ˆf St(St[x1,...]) = (x1 | x′1) ...(d | d′)S  , и для доказательства 𝔓ˆf St({t ∈ St[x1,...] | R }) = (x1 | x′1)...(d | d′){t ∈ St[x1,...] | R } осталось установить, что

TT ⊢ ((fSt(u))-1 | t)R ⇔ (x1 | x′1)...(d | d′)R.

В силу свойства R  , заданного условием, T  ⊢ ((f St)- 1(t) | t)R
 T  ⇔ (x | x′)...
  1   1       ′   St   St- 1       St -1      St -1
(d | d )(f ((f   )  (t)) | (f )  (t))((f  )  (t) | t)R  , но результат подстановок в правой части — и есть формула (x1 | x ′1)...(d | d′)R  .▹

Теорема 6. Пусть формула R  (зависящая, возможно, от t  ) удовлетворяет условию

T  & F & (t ∈ St[x1,...]) ⇒ (R  ⇔  (x1 | x ′)...(d | d′)(f St(t) | t)R ).
                                        1

Тогда соотношения

∃t(t ∈ St[x1,...xn, θ1,...θn] & R ),
∀t(t ∈ St[x1,...xn, θ1,...θn] ⇒ R )

биективно переносимы.

◃ В самом деле: терм ξ = {t ∈ St[x1 ...] | R } — биективно переносимый типа 𝔓S [x1,...]  (теорема 5). Первое соотношение эквивалентно (ξ = ∅ )  , а второе — ξ = St[x1 ...]  . Из уже установленных условий биективной переносимости (теоремы 1, 2) следует, что оба этих соотношения биективно переносимы.▹

Соотношения рассматриваемого в теореме 6 вида (называемые соотношениями с ограниченными кванторами) часто записывают в сокращённом виде:

∃t ∈ St[x1,...]R ⇌  ∃t(t ∈ St[x1,...] & R ),
∀t ∈ S [x ,...]R ⇌  ∀t(t ∈ S [x ,...] ⇒ R ).
      t  1                 t 1

При таком определении ограниченных кванторов сохраняются законы де Моргана:

 ∃t ∈ S [x ,...]R ~  ∀t ∈ S [x ,...]R,
        t  1               t  1
 ∀t ∈ St[x1,...]R ~  ∃t ∈ St[x1,...]R.

Действительно: используя эквивалентность A ⇒  B  ~ A  ∨ B  и законы де Моргана, имеем  ∀x(x ∈ S [...] ⇒ R )  ~ ∃x  (x  ∈ S[...] ∨ R )  ~ ∃x (x ∈ S[...] & R )  ~ ∃x ∈ S[...]R  . Обратно,  ∃x(x ∈ S [...] & R )  ~ ∀x(x  ∈ S[...] ∨ R )  ~ ∀v(x ∈ S [...] ⇒ R )  ~ ∀x ∈  S[...]R  .

Теорема 7. Пусть ξ  — биективно переносимый терм типа 𝔓 (S ξ[x1,...])  такой, что в T выводимо, что ξ  — одноэлементный терм, т. е. T  ⊢ ∀x∀y (x ∈ ξ & y ∈ ξ ⇒ x =  y)  . Тогда ⋃ ξ  (равный единственному элементу множества ξ  ) есть биективно переносимый терм типа S ξ[x1, ...]  .

◃ В самом деле:                   ⋃
(x1 | x′1)...(d | d′) ξ = {u | ∃t(t ∈ f Sξ[ξ] & u ∈ t)} = {u | ∃t(∃v(v ∈ ξ & t = fSξ(v)) & u = t)} . Но, в силу того, что ξ  — одноэлементное множество,              ⋃
v ∈ ξ ⇔  v =   ξ  и цепочка равенств продолжается следующим образом: (x1 | x ′) ...(d | d′) ⋃ ξ = {u | ∃t(t = fSξ(⋃ ξ) & u ∈ t)} = {u | u ∈ f Sξ(⋃ ξ)} = fSξ(⋃ ξ)
       1  , что и требовалось доказать.▹

Итак, если биективно переносимый терм ξ  имеет тип 𝔓(S ξ)  , то ⋃
   ξ  биективно переносим, если ξ  необходимо состоит из одного элемента. Если ξ  может состоять более чем из одного элемента, то ⋃
   ξ  может быть и не переносим биективно (так обстоит, например, с термом ⋃ x
   1   ). Как мы увидим далее, если биективно переносимый терм ξ  имеет тип 𝔓 𝔓 (Sξ)  , то для биективной переносимости терма ⋃
  ξ  не требуется дополнительных условий.

Теорема 8. Пусть ξ  — биективно переносимый терм типа S1[x1,...] × S2[x1,...]  . Тогда pr (ξ)
  1  есть биективно переносимый терм типа S1[x1,...]  , pr (ξ)
  2  — биективно переносимый терм типа S2[x1,...]  .

◃ Пусть t = (u,v)  . Тогда

(x1 | x′)...(d | d′)pr (t) = pr (fS1 ˆ×f S2((u,v))) =
      1    S1     S21        1S1       S1
  =  pr1((f   (u ),f  (v))) = f  (u) = f  (pr1(t)),

что и требовалось.▹

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

  • Если ξ  — биективно переносимый терм с типом Sξ[x1, ...]  , то соотношения ∃t ∈ ξR  , ∀t ∈ ξR  биективно переносимы (здесь ∃t ∈ ξR ⇌  ∃t ∈ S [x ,...](t ∈ ξ ⇒ R ),
                 ξ  1                  )
∀t ∈ ξR ⇌  ∀t ∈ Sξ[x1,...](t ∈ ξ ⇒ R ).

     

  • Если ξ  , ξ′ — биективно переносимые термы одного и того же типа 𝔓(S ξ)  , то соотношения ξ ⊆ ξ′ , ξ ⊂ ξ′ биективно переносимы.

 

7 Формальный язык, удовлетворяющий условиям переносимости

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

Для удобства введём следующие обозначения [6, 7]:

  • τ(ξ)  обозначает ступень, которой типизирован терм ξ  , т. е. выражение τ(ξ) = Sξ[x1,...]  означает, что T ⊢ T ⇒  ξ ∈ Sξ[x1,...]  .
  • DS  обозначает схему конструкции ступени такую, что 𝔓 (DS )  совпадает с S  . Разумеется, это определение имеет смысл только в случае, когда S  имеет вид 𝔓 (S ′)  (и тогда DS  есть S ′ ). Ситуация, в которой DS  не определена, означает нарушение какого-либо из условий биективной переносимости.
  • P1S  и P2S  обозначают схемы конструкции ступеней такие, что P1S × P2S  = S  . Разумеется, это определение имеет смысл только в случае, когда S  имеет вид S1 × S2   (и тогда P1S  и P2S  есть S1   и S2   , соответственно). Ситуация, в которой ступень P  S
  1  или P  S
  2  не определена, означает нарушение какого-либо из условий биективной переносимости.

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

  1. ∅  есть биективно переносимый терм типа 𝔓 (S′[x1,...])  , какова бы ни была схема S′ ;
  2. базисные множества x1,...xn  есть биективно переносимые термы, τ(xi) = 𝔓 (xi)  ;
  3. вспомогательные множества θ1,...θn  есть биективно переносимые термы, τ(θi) = 𝔓(θi)  ;
  4. родовая константа d  , для которой вводится соотношение типизации d ∈ S [x1,...]  , есть биективно переносимый терм, τ (d ) = S[x1,...]  ;
  5. если R  , возможно, зависящее от t  , биективно переносимо в случае, когда τ(t) = St[x1,...]  , то {t ∈ St[x1,...] | R } — биективно переносимый терм, τ({t ∈ St[x1,...] | R }) = 𝔓 (St[x1,...])  .
  6. если ξ  — биективно переносимый терм, причём T  ⊢ ∀x∀y (x ∈ ξ & y ∈ ξ ⇒ x = y)  , то ⋃
   ξ  (равный единственному элементу множества ξ  ) есть биективно переносимый терм и τ (⋃  ξ) = D τ(ξ)  ;
  7. если ξ  — биективно переносимый терм, то pr1(ξ)  и pr2(ξ)  — биективно переносимые термы, τ(pr1(ξ)) = P1τ(ξ)  , τ(pr2(ξ)) = P2 τ(ξ)  ;
  8. если ξ  и η  — биективно переносимые термы и 𝔓 (τ(ξ)) = τ(η)  , то ξ ∈ η  — биективно переносимое соотношение;
  9. если ξ  и η  — биективно переносимые термы и τ(ξ) = τ(η)  , то ξ = η  — биективно переносимое соотношение;
  10. если R  и R ′ — биективно переносимые соотношения, то R  , R ∨ R ′ , R & R ′ , R ⇒  R ′ , R ⇔  R ′ — биективно переносимые соотношения;
  11. если ξ  — биективно переносимый терм, а R  , возможно, зависящее от t  , биективно переносимо в случае, когда τ(t) = St[x1,...]  , то ∀t ∈ St[x1,...]R  и ∃t ∈ St[x1,...]R  — биективно переносимые соотношения.

Примеры биективно переносимых термов и соотношений рассматриваемого вида:

 

  1. для случая d ∈ 𝔓 (x ×  x )
        1    2  соотношения
    1. ∀v ∈ x2,∃u ∈  x1 × x2 (u ∈ d & pr2(u ) = v)  ;
    2. ∀t ∈  x ×  x ,∀t ∈ x  × x  (t  ∈ d & t ∈ d & pr (t ) = pr (t ) ⇒ t =  t)
  1    1    2   2    1    2 1        2         1 1      1  2     1    2

    термы

    1. {t ∈ x1 | ∃u ∈ x1 × x2(u ∈ d & pr1(u) = t)} ;
    2. {t ∈ 𝔓(x1) | ∃u ∈ x2 t = {a ∈ x1 | ∃v ∈ x1 × x2(v ∈ d & pr1(v) = a & pr2(v) = u)}} ;
  2. для случая d ∈ 𝔓 𝔓 (x1)  соотношения
    1. ∀a ∈ 𝔓 (x1),∀b ∈ 𝔓 (x1)(a ∈ d & b ∈ d ⇒ {t ∈ x1 | t ∈ a & t ∈ b} ∈ d)  ;
    2. ∀a ∈ 𝔓 (x1),∀b ∈ 𝔓 (x1)(∀t ∈ x1 (t ∈ a ⇒ t ∈ b) ⇒ b ∈ d )  ;

    термы

    1. {t ∈ x | ∃v ∈ 𝔓 (x )(v ∈ d & t ∈ v)}
      1           1 ;
    2. {t ∈ x1 × x1 | ∃v ∈ 𝔓 (x1)(v ∈ d & pr (t) ∈ v & pr (t) ∈ v)}
                                    1           2

и так далее.

Для ясности выделим подтермы в выражениях некоторых из примеров, приведённых выше, и укажем их тип. В примере 1a τ(v) = x
        2   , τ(u) = x  × x
        1    2   , τ(d) = 𝔓 (x ×  x )
           1    2  , τ(pr2(u )) = x2   ; в примере 1d τ(t) = 𝔓(x1 )  , τ(u) = x2   , τ(a) = x1   , τ(v) = x1 × x2   , τ(d ) = 𝔓 (x1 × x2)  , τ(pr1(v)) = x1   , τ pr2(v) = x2   , τ({a ∈ x1 | ...}) = 𝔓 (x1)  , τ({t ∈ 𝔓 (x1) | ...} ) = 𝔓 𝔓 (x1)  .

Как видим, в отличие от термов и соотношений теории множеств общего вида, термы и соотношения рассматриваемого вида удовлетворяют двум основным принципам. Во-первых, любой терм — сам по себе или в составе подформулы — имеет свой тип (что неудивительно, т. к. наличие типа является необходимым условием биективной переносимости терма), тип связанных переменных декларируется (т. е. недопустимы выражения вида ∀xR  , {x | R } , а только ∀x ∈  S[x1,...]R  , {x  ∈ S[x1,...] | R } ). Во-вторых, действуют ограничивающие правила, предписывающие определённую типизацию термам, участвующим в выражениях вида ξ ∈ η  , ξ = η  , ⋃
  ξ  , pri(ξ)  . Если эти принципы выполняются на каждом шаге при построении выражения, то выражение оказывается биективно переносимой формулой или термом.

 

8 Расширение формального языка операциями над множествами

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

ξ ⊆ η ⇌  ∀t ∈ D τ(ξ)((t ∈ ξ) ⇒ (t ∈ η)).

Так определённое отношение ⊆ является биективно переносимым по построению. Конструкция t ∈ D τ(ξ)  в ограничивающем выражении квантора обеспечивает совпадение типа связанной переменной t  с типом каждого элемента ξ  и правомерность (с точки зрения условий биективной переносимости) записи t ∈ ξ  в логическом выражении. Какие ограничения на ξ  и η  накладывает эта формула? Прежде всего, отношение ξ ⊆ η  допустимо не на всех термах, а только на тех, у которых совпадает типизация. Это следует из того, что отношение «∈ » применяется в двух случаях: (t ∈ ξ  ) и (t ∈ η  ), но переменная t  имеет одну типизацию. Далее, применение D τ(ξ)  предполагает, что оба терма должны иметь характер множеств. Последнее условие интуитивно можно трактовать следующим образом: использование знака «⊆ » бессмысленно между элементами или кортежами, а имеет смысл только между множествами. Если указанные условия выполняются, «биективно переносимый вариант» отношения «⊆ » имеет тот же смысл, что и обычное отношение «⊆ » в теории множеств.

Обобщение ограниченных кванторов:

Для знаков «⊂ » определения аналогичные.

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

  • Синглетон: {ξ} ⇌  {x ∈ τ (ξ)|(x = ξ)},  τ ({ξ}) = 𝔓 (τ(ξ)).

     

Для биективной переносимости {ξ} достаточно биективной переносимости ξ  , на вид типизирующей терм ξ  ступени не накладывается никаких ограничений.

  • Множество-сумма: ⋃
   ξ ⇌ {x ∈  DD τ (ξ)|∃u ∈ ξ (x ∈  u)},

     

      ⋃
τ (  ξ) = 𝔓 (DD  τ(ξ))

     

На диаграмме показана «верхушка» М-графа для ступеней, типизирующих термы ξ  , ⋃ ξ  и связанную переменную x  , фигурирующую в определении ⋃
  ξ  .

Таким образом, множество-сумма, образованное от биективно переносимого терма с типом 𝔓 𝔓 (S [x1,...])  биективно переносимо (для случая типизации 𝔓 (S [x1,...])  см. теорему 7).

Выражение 𝔓 (DD  τ(ξ))  не сокращается до D τ(ξ)  , поскольку иначе потеряется ограничение на типизацию аргумента (D τ(ξ)  определена и для типов 𝔓 (S [x1,...])  , не только 𝔓 𝔓 (S[x1,...])  ). Общее правило таково: допустимо сокращать конфигурацию D 𝔓  (т. к. она всюду применима и тождественна), но недопустимо сокращать конфигурацию 𝔓D  (т. к. она, хотя и является тождественной, применима только для ступеней вида 𝔓 (S [x1, ...])  ). На M-графе видно, что при построении выражения необходимо «спускаться» на два шага вниз.

Нетрудно проверить, что

  ⋃     ⋃             n+1
τ(   ...   (ξ)) = 𝔓 (D   τ (ξ )).
  ◟-n-◝р◜аз-◞

 

  • Объединение, пересечение, дополнение и симметрическая разность: ξ ∪ η ⇌ {x ∈  Dτ (ξ)|(x ∈ ξ) ∨ (x ∈  η)},

     

    ξ ∩ η ⇌ {x ∈ D τ (ξ )|(x ∈ ξ) & (x ∈ η)},

     

    ξ \ η ⇌ {x ∈ D τ(ξ)|(x ∈ ξ) & (x ∈∕η )},

     

    ξ △ η ⇌ {x ∈  D τ(ξ)|(x ∈ ξ) ⊕ (x ∈ η)},

     

    τ(ξ ∪ η ) = τ (ξ ∩ η) =
= τ(ξ \ η ) = τ (ξ △ η) =
  = 𝔓 (D (τ(ξ))) = 𝔓(D (τ(η))).

     

Для биективной переносимости этих термов требуется, чтобы биективно переносимые аргументы имели характер множеств и были одинаково типизированы. Совпадения типов требуют логические условия в выражениях: например, в выражении для ξ ∪ η  связанная переменная имеет тип D τ(ξ)  и, чтобы подформула x ∈ η  также была биективно переносимой, требуется τ(ξ) = τ (η )  .

  • Дополнение множества относительно собственного типа: ∁ξ ⇌  {x ∈ D τ(ξ)|(x ∈ ξ)},

     

    τ(∁ξ) = 𝔓 (D τ(ξ)).

     

  • Неупорядоченная пара:

     

    τ({ξ,η }) = 𝔓 (D 𝔓 (ξ)) = 𝔓 (ξ) = 𝔓 (η ).

     

Здесь вновь требуется совпадение типов ξ  и η  .

  • Упорядоченная пара:

     

     

  • Декартово произведение: ξ × η ⇌ {x ∈  D τ(ξ) × D τ (η ) | (pr1(x) ∈ ξ) & (pr2(x) ∈ η)},

     

    τ(ξ × η) = 𝔓 (D τ(ξ) × D τ(η)).

     

Заметим, что, в отличие от упорядоченной пары, биективно переносимого при как угодно типизированных ξ  и η  , декартово произведение биективно переносимо для термов, имеющих характер множеств.

  • Множество-степень:

     

     

Сравните определение биективно переносимого множества-степени с определением биективно переносимого синглетона, а также выражения для их типов. Использование в выражении множества-степени знака «⊆ » неявно задействует определение (ξ ⊆ η) ⇌  ∀t ∈ D τ(ξ)((t ∈ ξ) ⇒  (t ∈ η))  , предполагающее «спуск на ступень вниз» по M-графу, что и приводит к другому выражению для типа 𝔓 (ξ)  и другим требованиям к типизации аргумента. В отличие от операции образования синглетона, которую можно применять к как угодно типизированному терму, операция 𝔓  допустима только для термов, имеющих характер множества.

  • Большая проекция: P ri(ξ) ⇌ {x ∈ PiD τ (ξ )|∃y ∈ ξ(x =  pri(y))},

     

    τ(P r(ξ)) = 𝔓 (P D τ(ξ)).
     i          i

     

Для биективной переносимости терма P ri(ξ)  достаточно, чтобы терм ξ  был биективно переносимым термом и выражение PiD τ (ξ)  было определено, т. е. чтобы ξ  был типизирован ступенью 𝔓(S  [x ,...] × S [x  ,...])
    1  1        2  1  .

В самом деле: для того, чтобы «добраться» до типизации элемента P ri(ξ)  , необходимо сначала получить D τ(ξ)  — типизацию элемента ξ  (а каждый элемент ξ  есть кортеж), затем — PiD τ(ξ)  , т. е. типизацию i  -го компонента элемента ξ  . Наконец, множество элементов, типизированных PiD τ(ξ)  , будет иметь тип 𝔓 (PiD τ(ξ))  , как показано на M-графе:

              ξ-----PWQVR∙UST
                      |
                      |
                      |

  P r1(ξ)----PWQVR∙UST   PWQVRUS∙T---y ∈ ξ
              |
              |
              |
x ∈ P r (ξ)---∙
       1    PWQVRUST           PWQVRUST

 

  • Операция ξη  представляет собой множество всевозможных отображений из η  в ξ  . Нетрудно проверить, что если x  и y  имеют характер множеств, τ(ξη) = 𝔓 𝔓 (Dτ (η) × D τ (ξ ))  .

 

9 Определение рода структуры и языка родоструктурной экспликации

Пусть T — теория, более сильная чем теория множеств. Род структуры (esp`ece de structure) Σ  представляет собой текст из следующих составляющих (конституэнт):

 

  1. переменных x1,...xn  , называемых основными базисными множествами;
  2. термов θ1,...θm  теории T , называемых вспомогательными базисными множествами;
  3. формулы T  вида d ∈ S [x  ,...x ,θ ,...θ  ]
        1     n  1     m  (где S[x ,...x ,θ ,...θ  ]
   1     n  1     m  — ступень над n + m  множествами), являющейся соотношением типизации и называемой тґиповой характеристикой рода структуры, буква d  при этом называется родовой константой;
  4. формулы R  , биективно переносимой при типизации T  , называемой аксиомой рода структуры.

Если тґиповая характеристика имеет вид d ∈ S1 [...] × ...× Sk[...]  , то мы можем эквивалентным образом говорить не об одной, а о k  родовых константах d1, ...dk  таких, что d1 ∈ S1[...]  ,…dk ∈ Sk[...]  , полагая d =  (d1, ...dk)  и используя буквы dk  в аксиоме R  вместо соответствующих проекций d  , что бывает удобнее в плане экономии места.

Если аксиома R  рода структуры имеет вид R1 & ...& Rl  , где каждая Ri  — биективно переносимая формула, то мы можем эквивалентным образом говорить не об одной, а об l  аксиомах R1   ,…Rl  .

Пусть даны некоторый род структуры Σ  (в теории T , с типовой характеристикой T  и аксиомой R  ) и теория   ′
T , более сильная чем T . Тогда терм теории   ′
T вида (ξ1,...ξn,δ)  называется Σ  -объектом

Термин Ю. Н. Павловского.

(или теоретико-множественной интерпретацией Σ  ), если   ′
T  ⊢ (ξ1 | x1)...(ξn | xn )(δ | d)(T & R).

Иначе говоря, упорядоченный набор термов теории T ′ называется Σ  -объектом, если подстановка этих термов на место соответствующих базисных множеств и родовой константы в типизирующую формулу и аксиому рода структуры приводит к выводимости этих формул в теории   ′
T . При этом про каждое из множеств ξi  , δ  , входящих в Σ  -объект, мы будем говорить, что они интерпретируют соответствующие буквы xi  , d  рода структуры Σ  . Разумеется, вспомогательные базисные множества в интерпретации не нуждаются: являясь по определению термами T , они останутся таковыми и в T ′ .

Иногда бывает удобно говорить о классе всех Σ  -объектов в теории   ′
T :

K  =  {(x ,...x ,d ) | T & R}.
  Σ      1     n

Т. к. соотношение T &  R  не обязательно является коллективизирующим в   ′
T по x1,...xn,d  (а чаще всего именно так и есть), то класс KΣ   может и не являться множеством. Если σ = (ξ1,...ξn,δ)  , то условия σ ∈ K Σ   , «σ  есть Σ  -объект», «σ  есть теоретико-множественная интерпретация Σ  » эквивалентны.

Исчисление рода структуры T Σ   есть формальная система, получающаяся добавлением к аксиомам T в качестве явной аксиомы соотношения T &  R  . Таким образом, род структуры можно считать описанием схемы образования математического (или концептуально моделируемого) объекта определенного типа, а исчисление TΣ   специально предназначено для его изучения. При этом создание термов и теорем в T
 Σ   есть развитие теории объекта, заданного родом структуры Σ  .

Язык родоструктурной экспликации (сокращенно ЯРЭ) есть язык, на котором может быть записан род структуры.

10 Техническая реализация парсера языка родоструктурной экспликации

Рассматривая критерии биективной переносимости, мы приходим к мысли, что язык родоструктурной экспликации можно представить в виде атрибутной грамматики [4, 5], атрибутом в которой будет являться схема конструкции ступени, типизирующая каждый подтерм каждого терма. По явно заданной атрибутной грамматики с помощью автоматизированных средств (например, утилиты Yacc [8]) можно сгенерировать программный код процедуры парсера (верификатора, проверяющей процедуры), которая, имея на входе текст на языке родоструктурной экспликации, способна выверить его синтаксическую корректность и биективную переносимость всех входящих в него выражений, и в случае обнаружения несоответствий, выдать предупреждения.

В реализации парсера программы «Бурбакизатор» [9] была выбрана утилита Yacc и язык программирования Pascal. Опишем основные шаги, требуемые для реализации.

Как и в компиляторе обычного языка программирования, в программном коде парсера должна быть доступна таблица символов [5, с. 124], в которую помещается информация о именах и типизации глобальных термов, а также информация о именах и типизациях связанных переменных кванторных формул и сверток вида {x ∈ S [...] | R} .

В качестве особого типа данных в коде парсера необходимо ввести тип данных «ступень», для которого должны быть доступны операции D,P, ×, 𝔓  , определённые в разделе 7.

Кроме того, должны быть доступны следующие процедуры:

 

  1. D, P,×, 𝔓  — преобразуют типизации, как описано выше (из определений непосредственно ясны необходимые структуры данных и алгоритмы).
  2. НачалоБлока() — увеличивает счетчик вложенных блоков на единицу.
  3. Добавить(имя, типизация) — добавляет запись о терме с именем имя, типизацией типизация и уровнем видимости, равным текущему счётчику вложенных блоков, в таблицу символов. Генерирует ошибку «Переменная с именем уже определена», если производится попытка дважды использовать одно и то же имя для разных термов.
  4. Найти(имя) — находит в таблице символов терм с именем имя, помечает его как использованный и возвращает сохранённую типизацию этого терма. Генерирует ошибку «Переменная не определена», если производится попытка найти типизацию неопределенного терма.
  5. КонецБлока() — уменьшает счетчик вложенных блоков на единицу и удаляет из локальной таблицы символов все термы с уровнем видимости, равным предыдущему значению счетчика вложенных блоков. Если при этом приходится удалять записи о термах, не помеченных как использованные, генерируется ошибка «Локальная переменная определена, но не используется».
  6. Сравнить(типизация1, типизация2) — если аргумент типизация1 не равен аргументу типизация2, генерирует ошибку «Несоответствие типизаций: ожидается , имеется …».
  7. Преобразовать(имяФункции, парам1, парам2, типизация) — преобразовывает типизацию для унарных теоретико-множественных операций, как описано выше.
  8. Принять() — завершает разбор конституэнты и возвращает управление вызывающей программе.

C учетом сказанного выше, спецификация языка родоструктурной экспликации, записанная в форме синтаксических и семантических правил Yacc, выглядит следующим образом:
<конституэнта>

: <имяБМ><конецCтроки> {Добавить($1, 𝔓  $1);

| <имяРС>∈<ступень><конецCтроки> {Добавить($1, $3);

  Принять();}

| <имяТерма>=<терм><конецCтроки> {Добавить($1, $3);

  Принять();}

| <имяАксиомы>:<соотношение><конецCтроки> {Принять();}

| <имяТеоремы>:<соотношение><конецCтроки> {Принять();}

;

<ступень> : <ИмяБМ> {$$ := D(Найти($1));}

| <ступень>×<ступень> {$$ := $1×$3;}

| 𝔓  (<ступень>) {$$ := 𝔓  $2;}

;

<терм> : <ИмяБМ> {$$ := Найти($1);}

| <буква> {$$ := Найти($1);}

| <ИмяРС> {$$ := Найти($1);}

| <ИмяТерма> {$$ := Найти($1);}

| <терм><терм> {Сравнить($1, $3); $$ := 𝔓D  $1;}

| <терм><терм> {Сравнить($1, $3); $$ := 𝔓D  $1;}

| <терм>\<терм> {Сравнить($1, $3); $$ := 𝔓D  $1;}

| <терм>ч <терм> {Сравнить($1, $3); $$ := 𝔓D  $1;}

| <терм>×<терм> {$$ := 𝔓 (D$1  ×  D  $3);}

|  <терм> {$$ := 𝔓D  $2;}

| <функция>

| {<перечисление>} {$$ := 𝔓  $2;}

| {<декларация>|<соотношение>}{НачалоБлока();

  $$ := 𝔓  $2;

  КонецБлока();}

| (<кортеж>)

;

<функция> : <ИмяФункции>(<терм>) {$$ := Преобразовать($1, "", "", $3);}

| <ИмяФункции><число>(<терм>) {$$ := Преобразовать($1, $2, "", $4);}

| <ИмяФункции><число><число>(<терм>)

 {$$ := Преобразовать($1, $2, $3, $5);}

;

<кортеж> : <терм>

| <кортеж>,<терм> {$$ := $1×$3);}

;

<перечисление>

: <терм>

| <перечисление>,<перечисление>{Сравнить($1, $3); $$ := $1;}

;

<декларация>

: <буква>∈<ступень> {Добавить($1, $3); $$ := $3;}

;

<соотношение>

: <квантор><алгформ> {}

| <алгформ> {}

| <предикат> {}

;

<квантор> : <декларация> {}

| <декларация> {}

| <квантор>,<квантор> {}

;

<алгформ> : (<предикат>) {}

| (<алгформ>) {}

|  <алгформ> {}

| <алгформ>&<алгформ> {}

| <алгформ><алгформ> {}

| <алгформ><алгформ> {}

| <алгформ><алгформ> {}

;

<предикат>: <терм>∈<терм> {Сравнить($1,D$3);}

| <терм>∕∈<терм> {Сравнить($1,D$3);}

| <терм><терм> {D$3; Сравнить($1, $3);}

| <терм><терм> {D$3; Сравнить($1, $3);}

| <терм>⁄⊂ <терм> {D$3; Сравнить($1, $3);}

| <терм>=<терм> {Сравнить($1, $3);}

| <терм>⁄=<терм> {Сравнить($1, $3);}

| <терм>=  ∅  {D$1;}

| <терм>⁄=  ∅  {D$1;}

;

На основании приведённой спецификации языка был построен семантико-синтаксический анализатор родоструктурных текстов «Бурбакизатор» [9], применяемый в настоящее время автором при преподавании студентам элементов математической логики, теории множеств и аппарата концептуальных методов.

 

Литература

 

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

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

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

[4] Ахо А., Сети Р., Ульман Дж. Компиляторы: принципы, технологии, инструменты: Пер. с англ. — М.: Издательский дом «Вильямс», 2003. — 768 с.

[5] Серебряков В. А. и др. Теория и реализация языков программирования: Учебное пособие. — М.: МЗ-Пресс, 2003. — 345 с.

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

[7] Пономарев И. Н. Язык родоструктурной экспликации как атрибутная грамматика // Труды XLVII научной конференции МФТИ. — 2004.

[8] Levine J. R., Mason T., Brown D. Lex & Yacc. — 2nd, updated edition. — Sebastopol: O’Reilly & Associates, 1992. — 366 pp.

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

[10] Пономарев И. Н. Применение LALR-парсинга к языкам математической логики и теории множеств // Труды XLVIII научной конференции МФТИ. — 2005.

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

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

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

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