doc/METAMODEL/PROCESS/EPC/epc2_set-theory.md

### EPC2 set-theory
см. https://github.com/bpmbpm/doc/blob/main/METAMODEL/PROCESS/EPC/epc_set-theory.md

## I Описание бизнес-процесса в формализме теории множеств

### 1. Базовые множества

**Универсум объектов процесса:**
```
U = {Событие1, Операция1, Событие2, Событие3, Документ1, Документ2, Документ3}
```

**Множество типов объектов:**
```
T = {Event, Function, Document}
```

### 2. Множества объектов по типам

**Множество событий:**
```
E = {x ∈ U | тип(x) = Event} = {Событие1, Событие2, Событие3}
```

**Множество функций:**
```
F = {x ∈ U | тип(x) = Function} = {Операция1}
```

**Множество документов:**
```
D = {x ∈ U | тип(x) = Document} = {Документ1, Документ2, Документ3}
```

### 3. Функция типизации

**Функция, сопоставляющая объекту его тип:**
```
тип: U → T
тип(Событие1) = Event
тип(Операция1) = Function
тип(Событие2) = Event
тип(Событие3) = Event
тип(Документ1) = Document
тип(Документ2) = Document
тип(Документ3) = Document
```

### 4. Отношения между объектами

**Отношение "вызывается":**
```
R_trigger = {(e, f) ∈ E × F | e вызывает f} = {(Событие1, Операция1)}
```

**Отношение "приводит к событию":**
```
R_produces_event = {(f, e) ∈ F × E | f приводит к e} 
                 = {(Операция1, Событие2), (Операция1, Событие3)}
```

**Отношение "использует как вход":**
```
R_input = {(d, f) ∈ D × F | d является входом для f} = {(Документ1, Операция1)}
```

**Отношение "создает документ":**
```
R_creates = {(f, d) ∈ F × D | f создает d} 
          = {(Операция1, Документ2), (Операция1, Документ3)}
```

**Отношение "подтверждает":**
```
R_validates = {(e, d) ∈ E × D | e подтверждает d} = {(Событие2, Документ2)}
```

**Отношение "отклоняет":**
```
R_invalidates = {(e, d) ∈ E × D | e отклоняет d} = {(Событие3, Документ3)}
```

### 5. Множество статусов документов

**Множество возможных статусов:**
```
S = {НОВЫЙ, УТВЕРЖДЁН, ОТКЛОНЁН}
```

**Функция статусов документов:**
```
статус: D → S
статус(Документ1) = НОВЫЙ
статус(Документ2) = УТВЕРЖДЁН
статус(Документ3) = ОТКЛОНЁН
```

### 6. Отношения принадлежности к процессам

**Множество процессов:**
```
P = {Workflow, Docflow}
```

**Отношение принадлежности к Workflow:**
```
R_workflow = {(x, Workflow) | x ∈ {Событие1, Операция1, Событие2, Событие3}}
           = {(Событие1, Workflow), (Операция1, Workflow), 
              (Событие2, Workflow), (Событие3, Workflow)}
```

**Отношение принадлежности к Docflow:**
```
R_docflow = {(x, Docflow) | x ∈ {Документ1, Операция1, Документ2, Документ3}}
          = {(Документ1, Docflow), (Операция1, Docflow),
             (Документ2, Docflow), (Документ3, Docflow)}
```

### 7. Отношение альтернативных исходов

**Отношение взаимоисключения документов:**
```
R_mutually_exclusive = {(Документ2, Документ3)}
```

**Отношение взаимоисключения событий:**
```
R_mutually_exclusive_events = {(Событие2, Событие3)}
```

### 8. Функция условий выполнения

**Функция условий для событий:**
```
условие: E → C (где C - множество условий)
условие(Событие2) = "заявление соответствует требованиям"
условие(Событие3) = "заявление не соответствует требованиям"
```

### 9. Полная модель процесса

**Процесс как алгебраическая структура:**
```
Process_Algebra = ⟨U, T, E, F, D, P, S, C, 
                  R_trigger, R_produces_event, R_input, R_creates,
                  R_validates, R_invalidates, R_workflow, R_docflow,
                  R_mutually_exclusive, R_mutually_exclusive_events,
                  тип, статус, условие⟩
```

### 10. Свойства модели

**Свойство целостности:**
```
∀f ∈ F, ∃e ∈ E: (e, f) ∈ R_trigger  (каждая функция имеет триггер)
∀d ∈ D \ {Документ1}, ∃f ∈ F: (f, d) ∈ R_creates  (все документы кроме входного создаются функциями)
```

**Свойство непротиворечивости статусов:**
```
∀d ∈ D: (статус(d) = УТВЕРЖДЁН) ⇒ ∃e ∈ E: (e, d) ∈ R_validates
∀d ∈ D: (статус(d) = ОТКЛОНЁН) ⇒ ∃e ∈ E: (e, d) ∈ R_invalidates
```

**Свойство взаимоисключения:**
```
∀(d1, d2) ∈ R_mutually_exclusive: статус(d1) ≠ статус(d2)
∀(e1, e2) ∈ R_mutually_exclusive_events: ¬(∃f ∈ F: (f, e1) ∈ R_produces_event ∧ (f, e2) ∈ R_produces_event)
```

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

## II Часть 
## Формальное выражение связи между множествами событий и документов

### 1. Базовая структура множеств

**Множество событий:**
```
E = {e | e - событие}
```

**Множество документов:**
```
D = {d | d - документ}
```

**Множество типов событий:**
```
T_E = {t | t - тип события}
```

**Множество типов документов:**
```
T_D = {t | t - тип документа}
```

### 2. Функции типизации

**Функция типа события:**
```
тип_E: E → T_E
```

**Функция типа документа:**
```
тип_D: D → T_D
```

### 3. Отношение связи событий и документов

**Общее отношение связи:**
```
R ⊆ E × D × A
```
где A - множество типов связей (подтверждает, отклоняет, создает, и т.д.)

### 4. Конкретизация для случая "отказ - заявление отклоненное"

**Определим конкретные типы:**
```
t_отказ ∈ T_E  (тип события "отказ")
t_отклоненное ∈ T_D  (тип документа "заявление отклоненное")
a_отклоняет ∈ A  (тип связи "отклоняет")
```

**Формальное выражение связи:**
```
∀e ∈ E: (тип_E(e) = t_отказ) ⇒ ∃d ∈ D: (тип_D(d) = t_отклоненное) ∧ (e, d, a_отклоняет) ∈ R
```

### 5. Более общая форма для произвольных пар "событие-документ"

**Пусть задано отображение типов:**
```
Φ: T_E → T_D × A
```

Тогда общее условие связности:
```
∀e ∈ E: ∃d ∈ D: (тип_D(d) = π₁(Φ(тип_E(e))) ∧ (e, d, π₂(Φ(тип_E(e)))) ∈ R
```
где π₁ и π₂ - проекции на первую и вторую компоненты пары.

### 6. Пример для нашего бизнес-процесса

**Конкретные типы в нашем процессе:**
```
T_E = {t_подача, t_согласование, t_отказ}
T_D = {t_составленное, t_согласованное, t_отклоненное}
A = {a_инициирует, a_подтверждает, a_отклоняет, a_создает}
```

**Отображение Φ:**
```
Φ(t_подача) = (t_составленное, a_инициирует)
Φ(t_согласование) = (t_согласованное, a_подтверждает)
Φ(t_отказ) = (t_отклоненное, a_отклоняет)
```

**Проверка условия связности:**
```
∀e ∈ E: ∃d ∈ D: (тип_D(d) = π₁(Φ(тип_E(e))) ∧ (e, d, π₂(Φ(тип_E(e)))) ∈ R
```

### 7. Альтернативное представление через множества

**Множество пар "тип события - тип документа":**
```
P = {(t_e, t_d) ∈ T_E × T_D | события типа t_e связаны с документами типа t_d}
```

**Множество допустимых связей для каждой пары:**
```
A(t_e, t_d) ⊆ A  // допустимые типы связей для пары (t_e, t_d)
```

**Общее условие:**
```
∀e ∈ E: ∃d ∈ D: (тип_E(e), тип_D(d)) ∈ P ∧ ∃a ∈ A(тип_E(e), тип_D(d)): (e, d, a) ∈ R
```

### 8. Условие функциональности (однозначности)

**Если требуется однозначное соответствие:**
```
∀e ∈ E: ∃!d ∈ D: (тип_E(e), тип_D(d)) ∈ P ∧ ∃a ∈ A(тип_E(e), тип_D(d)): (e, d, a) ∈ R
```
где ∃! означает "существует и единственный".

### 9. Применение к нашему примеру

**Для события "отказ":**
```
∃e ∈ E: тип_E(e) = t_отказ ⇒ ∃d ∈ D: тип_D(d) = t_отклоненное ∧ (e, d, a_отклоняет) ∈ R
```

**Конкретная реализация в нашем процессе:**
```
тип_E(Событие3) = t_отказ
тип_D(Документ3) = t_отклоненное
(Событие3, Документ3, a_отклоняет) ∈ R
```

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

### Пояснение
Мы хотим выразить в общем виде связь между множеством событий и множеством документов, в частности, что событие "отказ" связано с документом "заявление отклоненное".

В нашей модели у нас есть:

Множество событий E

Множество документов D

Отношение R_validates ⊆ E × D (подтверждает)

Отношение R_invalidates ⊆ E × D (отклоняет)

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

Однако, в нашей модели типы событий и документов не формализованы как отдельные множества. Мы можем ввести:

Множество типов событий: T_E

Множество типов документов: T_D

И функции:

тип_события: E → T_E

тип_документа: D → T_D

Тогда мы можем определить:

Пусть T_E содержит тип "отказ" (обозначим его как "отказ")

Пусть T_D содержит тип "заявление отклоненное" (обозначим его как "отклоненное")

Тогда мы можем записать:

∀ e ∈ E: (тип_события(e) = "отказ") ⇒ ∃ d ∈ D: (тип_документа(d) = "отклоненное") ∧ (e, d) ∈ R_invalidates

Но в нашем конкретном примере у нас только одно событие отказа (Событие3) и один документ отклонения (Документ3), и они связаны.

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

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

R_типов: T_E × T_D

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

Но в нашей модели мы не вводили такое отношение.

Давайте формализуем это в рамках теории множеств, расширив нашу модель.

Расширенная модель:

T_E = { "подача", "согласование", "отказ" } (типы событий)
T_D = { "составленное", "согласованное", "отклоненное" } (типы документов)

тип_события: E → T_E
тип_документа: D → T_D

Для нашего примера:
тип_события(Событие1) = "подача"
тип_события(Событие2) = "согласование"
тип_события(Событие3) = "отказ"

text
 тип_документа(Документ1) = "составленное"
 тип_документа(Документ2) = "согласованное"
 тип_документа(Документ3) = "отклоненное"
Тогда мы можем определить отношение R_типов_отклонения ⊆ T_E × T_D, такое что:
("отказ", "отклоненное") ∈ R_типов_отклонения

И затем потребовать, чтобы для каждого события e типа "отказ" существовал документ d типа "отклоненное", связанный отношением R_invalidates.

Аналогично для подтверждения:
("согласование", "согласованное") ∈ R_типов_подтверждения

И для каждого события e типа "согласование" существует документ d типа "согласованное", связанный отношением R_validates.

Но note: в нашей модели одно событие согласования связано с одним документом (согласованным) и одно событие отказа связано с одним документом (отклоненным).

Однако, в общем случае, связь может быть не один-к-одному.

Мы можем сформулировать общее утверждение:

Пусть R_T ⊆ T_E × T_D — отношение между типами событий и типами документов, которое указывает, что событие типа t_E должно быть связано с документом типа t_D отношением R (которое может быть R_validates или R_invalidates).

Тогда:

text
 ∀ e ∈ E, ∀ t_E ∈ T_E, ∀ t_D ∈ T_D: 
    (тип_события(e) = t_E) ∧ (t_E, t_D) ∈ R_T ⇒ ∃ d ∈ D: (тип_документа(d) = t_D) ∧ (e, d) ∈ R
где R — это соответствующее отношение (например, R_validates для положительных исходов и R_invalidates для отрицательных).

В нашем случае:

text
 R_T_validates = { ("согласование", "согласованное") }
 R_T_invalidates = { ("отказ", "отклоненное") }
Тогда:

text
 Для R_T_validates: 
    ∀ e ∈ E: (тип_события(e) = "согласование") ⇒ ∃ d ∈ D: (тип_документа(d) = "согласованное") ∧ (e, d) ∈ R_validates

 Для R_T_invalidates:
    ∀ e ∈ E: (тип_события(e) = "отказ") ⇒ ∃ d ∈ D: (тип_документа(d) = "отклоненное") ∧ (e, d) ∈ R_invalidates
Это и есть общее выражение, связывающее множество событий с множеством документов по типам.

Однако, note: в нашем примере также есть событие "подача", которое не связано с документом через R_validates или R_invalidates, но связано с документом через отношение R_input (которое мы не рассматриваем в данном контексте).

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

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