diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..d4b0046 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,7 @@ +Issue to solve: https://github.com/netkeep80/jsonRVM/issues/8 +Your prepared branch: issue-8-bab60746bef2 +Your prepared working directory: /tmp/gh-issue-solver-1770331942758 +Your forked repository: konard/netkeep80-jsonRVM +Original repository (upstream): netkeep80/jsonRVM + +Proceed. diff --git a/doc/relations-model-en.md b/doc/relations-model-en.md index 29d5d33..d2bb0ee 100644 --- a/doc/relations-model-en.md +++ b/doc/relations-model-en.md @@ -31,18 +31,28 @@ where Lⁿ is the Cartesian power of set L. **Definition 1.3 (Duplet).** A duplet (ordered pair of references) is an element of the set: ``` -D = L² = L × L = {(a, b) : a ∈ L, b ∈ L} +D = L² = L × L = {(b, e) : b ∈ L, e ∈ L} ``` +where: +- b — begin (start) +- e — end (finish) + **Definition 1.4 (Triplet).** A triplet (tuple of length 3) is an element of the set: ``` -T = L³ = L × L × L = {(s, r, o) : s ∈ L, r ∈ L, o ∈ L} +T = L³ = L × L × L = {(r, s, o) : r ∈ L, s ∈ L, o ∈ L} +``` + +or equivalently: + +``` +T = L × D, where D = L × L ``` where: -- s — reference to subject - r — reference to relation +- s — reference to subject - o — reference to object ### 1.3. Representation of Triplet as Nested Ordered Pairs @@ -50,100 +60,74 @@ where: From the perspective of set theory, a triplet can be represented as nested ordered pairs: ``` -(s, r, o) = ((s, r), o) +(r, s, o) = (r, (s, o)) = (e, d) ``` -This corresponds to the representation of a tuple through a Kuratowski pair. - -## 2. Relations Model as Four Interconnected Sets +where: +- e — reference to entity (in the role of relation) +- d = (s, o) — duplet (subject-object) -### 2.1. Four Aspects of an Entity +This corresponds to the representation of a tuple through a Kuratowski pair. -In the Relations Model, each entity can act in four aspects (roles): +## 2. Internal Structure of Links -1. **E (Entity)** — entity as a whole -2. **R (Relation)** — entity in the role of relation (controller) -3. **S (Subject)** — entity in the role of subject (view) -4. **O (Object)** — entity in the role of object (model) +### 2.1. Two Aspects of an Entity -**Definition 2.1 (Relations Model).** The Relations Model RM is represented as a quadruple of interconnected sets of tuples of length 3: +In the Relations Model, each entity can be defined through links: ``` -RM = {E, O, R, S} +E = ER (entity is defined by entity-relation pair) +R = SO (relation is defined by subject-object pair) +S ⊆ E (subjects are a subset of entities) +O ⊆ E (objects are a subset of entities) ``` -where: +### 2.2. Link Types (Duplets) -``` -R ⊆ (S × O) × E = {((s, o), e) : s ∈ S, o ∈ O, e ∈ E} -O ⊆ (E × R) × S = {((e, r), s) : e ∈ E, r ∈ R, s ∈ S} -S ⊆ (R × E) × O = {((r, e), o) : r ∈ R, e ∈ E, o ∈ O} -E ⊆ (O × S) × R = {((o, s), r) : o ∈ O, s ∈ S, r ∈ R} -``` - -### 2.2. Internal Structure of Links - -The internal aspect (structure) of each entity type is defined through links: +We define two basic link types: ``` -E = SO (entity is defined by subject-object pair) -R = OS (relation is defined by object-subject pair) -O = ER (object is defined by entity-relation pair) -S = RE (subject is defined by relation-entity pair) +SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} +ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} ``` -### 2.3. Link Types (Duplets) - -We define four basic link types: - -``` -OS ⊆ O × S = {(o, s) : o ∈ O, s ∈ S} -SO ⊆ S × O = {(s, o) : s ∈ S, o ∈ O} -RE ⊆ R × E = {(r, e) : r ∈ R, e ∈ E} -ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ R} -``` +where: +- SO — subject-object duplet, defining a relation +- ER — entity-relation duplet, defining an entity ## 3. Reduction of Triplets to Duplets ### 3.1. Theorem on Representation Equivalence -**Theorem 3.1.** The set RM can be equivalently represented by four sets of duplets: +**Theorem 3.1.** The set RM can be equivalently represented by two subsets of duplets: ``` -RM = {ER, OS, RE, SO} +RM = {ER, SO} ``` where: ``` -E = SO ⊆ SO × OS = {(so, os) : so ∈ SO, os ∈ OS} -O = ER ⊆ ER × RE = {(er, re) : er ∈ ER, re ∈ RE} -R = OS ⊆ OS × SO = {(os, so) : os ∈ OS, so ∈ SO} -S = RE ⊆ RE × ER = {(re, er) : re ∈ RE, er ∈ ER} +E = ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} +R = SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} ``` ### 3.2. Proof of Equivalence -Entity tuple is equivalent to subject-object tuple: -``` -e = (s, o, r) = ((s, o), r) = (so, r) ≡ so = (so, re) -``` +A triplet is equivalent to a combination of two duplets: -Object tuple is equivalent to entity-relation tuple: ``` -o = (e, r, s) = ((e, r), s) = (er, s) ≡ er = (er, so) +t = (r, s, o) = (r, (s, o)) = (e, d) ``` -Relation tuple is equivalent to object-subject tuple: -``` -r = (o, s, e) = ((o, s), e) = (os, e) ≡ os = (os, er) -``` +where: +- e ∈ E — entity in the role of relation +- d = (s, o) ∈ SO — subject-object duplet -Subject tuple is equivalent to relation-entity tuple: -``` -s = (r, e, o) = ((r, e), o) = (re, o) ≡ re = (re, os) -``` +Thus, each triplet is uniquely determined by: +1. A reference to the entity-relation (e) +2. A subject-object duplet (d = (s, o)) -## 4. Relations Model as Associative Network +## 4. Relations Model as a Function ### 4.1. Definitions from Links Theory @@ -167,19 +151,26 @@ mapping a reference l from set L to a reference vector of length n. anetd : L → L² ``` -### 4.2. Relations Model as Three-Dimensional Associative Network +### 4.2. Relations Model as a Function -**Theorem 4.1.** The Relations Model can be represented as a three-dimensional associative network: +**Definition 4.4 (Relations Model).** The Relations Model can be represented as a function: ``` -λ : L → L × L × L = L³ +rm : E → E × E × E = E³ ``` -where each entity with identifier l is mapped to a triplet (s, r, o). +where each entity with identifier e is mapped to a triplet (r, s, o). + +Equivalently, considering the nested pair structure: + +``` +rm : E → E × (E × E) +rm(e) = (r, (s, o)) +``` ### 4.3. Reduction to Two-Dimensional Associative Network -**Theorem 4.2.** A three-dimensional associative network can be transformed into a two-dimensional associative network (duplet network) without information loss. +**Theorem 4.1.** A three-dimensional associative network can be transformed into a two-dimensional associative network (duplet network) without information loss. The transformation is performed through nested ordered pairs: @@ -193,10 +184,10 @@ where NP = {∅ | (l, np), l ∈ L, np ∈ NP} — the set of nested ordered pai ### 5.1. Definition of Triune Entity -**Definition 5.1.** A triune entity is an element of the Relations Model defined by a triplet (s, r, o), where: +**Definition 5.1.** A triune entity is an element of the Relations Model defined by a triplet (r, s, o), where: -- **s (subject)** — subject, defining the view (View) - **r (relation)** — relation, defining the controller (Controller) +- **s (subject)** — subject, defining the view (View) - **o (object)** — object, defining the model (Model) ### 5.2. Entity Topologies @@ -239,7 +230,7 @@ The Relations Model supports reflection: a program can analyze and modify its ow ### 6.3. Closure -**Theorem 6.1 (Closure).** The sets E, O, R, S are equivalent. Any entity can act as subject, relation, or object in other entities. +**Theorem 6.1 (Closure).** The sets E, S, O are equivalent. Any entity can act as subject, relation, or object in other entities. ### 6.4. Fractality @@ -264,8 +255,8 @@ An entity in JSON representation is defined by an object with fields: ```json { - "$sub": "", "$rel": "", + "$sub": "", "$obj": "" } ``` @@ -278,8 +269,7 @@ An interesting analogy can be drawn with the complementarity principle of nucleo - Guanine (G) bonds only with cytosine (C) — triple bond Similarly in the Relations Model: -- OS is conjugate with SO -- ER is conjugate with RE +- ER is conjugate with SO (entity-relation ↔ subject-object) This property of preserving relative association type ensures structural integrity. @@ -287,11 +277,11 @@ This property of preserving relative association type ensures structural integri The mathematical formalization of the Relations Model in terms of set theory shows that: -1. Triplets (tuples of length 3) can be equivalently represented as nested ordered pairs (two duplets). +1. Triplets (tuples of length 3) can be equivalently represented as nested ordered pairs: (r, s, o) = (r, (s, o)) = (e, d). -2. The Relations Model is a three-dimensional associative network of the form λ : L → L³. +2. The Relations Model is a function of the form rm : E → E³. -3. The four interconnected sets {E, O, R, S} are equivalent to four sets of duplets {ER, OS, RE, SO}. +3. Two basic duplet types {ER, SO} are sufficient to represent the entire model. 4. The triune entity implements the MVC pattern at the level of the basic language structure. diff --git a/doc/relations-model-ru.md b/doc/relations-model-ru.md index ff3087f..0eeaaad 100644 --- a/doc/relations-model-ru.md +++ b/doc/relations-model-ru.md @@ -31,18 +31,28 @@ Vₙ = Lⁿ **Определение 1.3 (Дуплет).** Дуплет (упорядоченная пара ссылок) — это элемент множества: ``` -D = L² = L × L = {(a, b) : a ∈ L, b ∈ L} +D = L² = L × L = {(b, e) : b ∈ L, e ∈ L} ``` +где: +- b — begin (начало) +- e — end (конец) + **Определение 1.4 (Триплет).** Триплет (кортеж длины 3) — это элемент множества: ``` -T = L³ = L × L × L = {(s, r, o) : s ∈ L, r ∈ L, o ∈ L} +T = L³ = L × L × L = {(r, s, o) : r ∈ L, s ∈ L, o ∈ L} +``` + +или эквивалентно: + +``` +T = L × D, где D = L × L ``` где: -- s — ссылка на субъект - r — ссылка на отношение +- s — ссылка на субъект - o — ссылка на объект ### 1.3. Представление триплета через вложенные упорядоченные пары @@ -50,102 +60,76 @@ T = L³ = L × L × L = {(s, r, o) : s ∈ L, r ∈ L, o ∈ L} С точки зрения теории множеств, триплет можно представить как вложенные упорядоченные пары: ``` -(s, r, o) = ((s, r), o) +(r, s, o) = (r, (s, o)) = (e, d) ``` -Это соответствует представлению кортежа через пару Куратовского. - -## 2. Модель Отношений как четыре взаимосвязанных множества +где: +- e — ссылка на сущность (в роли отношения) +- d = (s, o) — дуплет (субъект-объект) -### 2.1. Четыре аспекта сущности +Это соответствует представлению кортежа через пару Куратовского. -В Модели Отношений каждая сущность может выступать в четырёх аспектах (ролях): +## 2. Внутренняя структура связей -1. **E (Entity)** — сущность как целое -2. **R (Relation)** — сущность в роли отношения (контроллера) -3. **S (Subject)** — сущность в роли субъекта (представления) -4. **O (Object)** — сущность в роли объекта (модели) +### 2.1. Два аспекта сущности -**Определение 2.1 (Модель Отношений).** Модель Отношений RM представляется как четвёрка взаимосвязанных множеств кортежей длины 3: +В Модели Отношений каждая сущность может определяться через связи: ``` -RM = {E, O, R, S} +E = ER (сущность определяется парой сущность-отношение) +R = SO (отношение определяется парой субъект-объект) +S ⊆ E (субъекты — подмножество сущностей) +O ⊆ E (объекты — подмножество сущностей) ``` -где: +### 2.2. Типы связей (дуплетов) -``` -R ⊆ (S × O) × E = {((s, o), e) : s ∈ S, o ∈ O, e ∈ E} -O ⊆ (E × R) × S = {((e, r), s) : e ∈ E, r ∈ R, s ∈ S} -S ⊆ (R × E) × O = {((r, e), o) : r ∈ R, e ∈ E, o ∈ O} -E ⊆ (O × S) × R = {((o, s), r) : o ∈ O, s ∈ S, r ∈ R} -``` - -### 2.2. Внутренняя структура связей - -Внутренний аспект (структура) каждого типа сущности определяется через связи: +Определим два базовых типа связей: ``` -E = SO (сущность определяется парой субъект-объект) -R = OS (отношение определяется парой объект-субъект) -O = ER (объект определяется парой сущность-отношение) -S = RE (субъект определяется парой отношение-сущность) +SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} +ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} ``` -### 2.3. Типы связей (дуплетов) - -Определим четыре базовых типа связей: - -``` -OS ⊆ O × S = {(o, s) : o ∈ O, s ∈ S} -SO ⊆ S × O = {(s, o) : s ∈ S, o ∈ O} -RE ⊆ R × E = {(r, e) : r ∈ R, e ∈ E} -ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ R} -``` +где: +- SO — дуплет субъект-объект, определяющий отношение +- ER — дуплет сущность-отношение, определяющий сущность ## 3. Сведение триплетов к дуплетам ### 3.1. Теорема об эквивалентности представлений -**Теорема 3.1.** Множество RM может быть эквивалентно представлено четырьмя множествами дуплетов: +**Теорема 3.1.** Множество RM может быть эквивалентно представлено двумя подмножествами дуплетов: ``` -RM = {ER, OS, RE, SO} +RM = {ER, SO} ``` где: ``` -E = SO ⊆ SO × OS = {(so, os) : so ∈ SO, os ∈ OS} -O = ER ⊆ ER × RE = {(er, re) : er ∈ ER, re ∈ RE} -R = OS ⊆ OS × SO = {(os, so) : os ∈ OS, so ∈ SO} -S = RE ⊆ RE × ER = {(re, er) : re ∈ RE, er ∈ ER} +E = ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} +R = SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} ``` ### 3.2. Доказательство эквивалентности -Кортеж-сущность эквивалентен кортежу субъект-объекта: -``` -e = (s, o, r) = ((s, o), r) = (so, r) ≡ so = (so, re) -``` +Триплет эквивалентен комбинации двух дуплетов: -Кортеж-объект эквивалентен кортежу сущность-отношения: ``` -o = (e, r, s) = ((e, r), s) = (er, s) ≡ er = (er, so) +t = (r, s, o) = (r, (s, o)) = (e, d) ``` -Кортеж-отношение эквивалентен кортежу объект-субъекта: -``` -r = (o, s, e) = ((o, s), e) = (os, e) ≡ os = (os, er) -``` +где: +- e ∈ E — сущность в роли отношения +- d = (s, o) ∈ SO — дуплет субъект-объект -Кортеж-субъект эквивалентен кортежу отношение-сущности: -``` -s = (r, e, o) = ((r, e), o) = (re, o) ≡ re = (re, os) -``` +Таким образом, каждый триплет однозначно определяется: +1. Ссылкой на сущность-отношение (e) +2. Дуплетом субъект-объект (d = (s, o)) -## 4. Модель Отношений как ассоциативная сеть +## 4. Модель Отношений как функция -### 4.1. Определения из Теории связей +### 4.1. Определение из Теории связей **Определение 4.1 (Ассоциация).** Ассоциация — это упорядоченная пара, состоящая из ссылки и вектора ссылок: @@ -167,19 +151,26 @@ anetⁿ : L → Vₙ anetd : L → L² ``` -### 4.2. Модель Отношений как трёхмерная ассоциативная сеть +### 4.2. Модель Отношений как функция -**Теорема 4.1.** Модель Отношений может быть представлена как трёхмерная ассоциативная сеть: +**Определение 4.4 (Модель Отношений).** Модель Отношений может быть представлена как функция: ``` -λ : L → L × L × L = L³ +rm : E → E × E × E = E³ ``` -где каждая сущность с идентификатором l отображается в триплет (s, r, o). +где каждая сущность с идентификатором e отображается в триплет (r, s, o). + +Эквивалентно, с учётом структуры вложенных пар: + +``` +rm : E → E × (E × E) +rm(e) = (r, (s, o)) +``` ### 4.3. Сведение к двумерной асети -**Теорема 4.2.** Трёхмерная ассоциативная сеть может быть преобразована в двумерную ассоциативную сеть (асеть дуплетов) без потери информации. +**Теорема 4.1.** Трёхмерная ассоциативная сеть может быть преобразована в двумерную ассоциативную сеть (асеть дуплетов) без потери информации. Преобразование выполняется через вложенные упорядоченные пары: @@ -193,10 +184,10 @@ anetl : L → NP ### 5.1. Определение триединой сущности -**Определение 5.1.** Триединая сущность — это элемент Модели Отношений, определяемый триплетом (s, r, o), где: +**Определение 5.1.** Триединая сущность — это элемент Модели Отношений, определяемый триплетом (r, s, o), где: -- **s (subject)** — субъект, определяющий представление (View) - **r (relation)** — отношение, определяющее контроллер (Controller) +- **s (subject)** — субъект, определяющий представление (View) - **o (object)** — объект, определяющий модель (Model) ### 5.2. Топологии сущностей @@ -239,7 +230,7 @@ anetl : L → NP ### 6.3. Замкнутость -**Теорема 6.1 (Замкнутость).** Множества E, O, R, S эквивалентны. Любая сущность может выступать в роли субъекта, отношения или объекта в других сущностях. +**Теорема 6.1 (Замкнутость).** Множества E, S, O эквивалентны. Любая сущность может выступать в роли субъекта, отношения или объекта в других сущностях. ### 6.4. Фрактальность @@ -264,8 +255,8 @@ anetl : L → NP ```json { - "$sub": "<субъект>", "$rel": "<отношение>", + "$sub": "<субъект>", "$obj": "<объект>" } ``` @@ -278,8 +269,7 @@ anetl : L → NP - Гуанин (G) соединяется только с цитозином (C) — тройная связь Аналогично в Модели Отношений: -- OS сопряжено с SO -- ER сопряжено с RE +- ER сопряжено с SO (сущность-отношение ↔ субъект-объект) Это свойство сохранения относительного типа ассоциации обеспечивает целостность структуры. @@ -287,11 +277,11 @@ anetl : L → NP Математическая формализация Модели Отношений в терминах теории множеств показывает, что: -1. Триплеты (кортежи длины 3) могут быть эквивалентно представлены как вложенные упорядоченные пары (два дуплета). +1. Триплеты (кортежи длины 3) могут быть эквивалентно представлены как вложенные упорядоченные пары: (r, s, o) = (r, (s, o)) = (e, d). -2. Модель Отношений является трёхмерной ассоциативной сетью вида λ : L → L³. +2. Модель Отношений является функцией вида rm : E → E³. -3. Четыре взаимосвязанных множества {E, O, R, S} эквивалентны четырём множествам дуплетов {ER, OS, RE, SO}. +3. Два базовых типа дуплетов {ER, SO} достаточны для представления всей модели. 4. Триединая сущность реализует паттерн MVC на уровне базовой структуры языка. diff --git a/proofs/rocq/RelationsModel.v b/proofs/rocq/RelationsModel.v index 95fec36..10f1983 100644 --- a/proofs/rocq/RelationsModel.v +++ b/proofs/rocq/RelationsModel.v @@ -7,7 +7,13 @@ in terms of set theory, following Links Theory (Теория связей). The Relations Model represents a metaprogramming language where everything - is represented as triune entities (subject, relation, object). + is represented as triune entities (relation, subject, object). + + Key changes in this version: + - Duplet notation: (b, e) where b = begin, e = end + - Triplet representation: (r, s, o) = (r, (s, o)) = (e, d) + - Two duplet types: SO (subject-object) and ER (entity-relation) + - Relations Model as function: rm : E → E × E × E References: - Links Theory: https://habr.com/ru/articles/895896/ @@ -40,42 +46,115 @@ Definition L_default : L := 0. (** Section 1.2: Duplets and Triplets *) (** Definition 1.3 (Duplet): An ordered pair of references - D = L² = L × L = {(a, b) : a ∈ L, b ∈ L} + D = L² = L × L = {(b, e) : b ∈ L, e ∈ L} + + where: + - b — begin (start) + - e — end (finish) *) Definition Duplet := prod L L. +(** Duplet accessors *) +Definition duplet_begin (d : Duplet) : L := fst d. +Definition duplet_end (d : Duplet) : L := snd d. + +(** Constructor for Duplet *) +Definition make_duplet (b e : L) : Duplet := (b, e). + (** Default duplet value *) Definition Duplet_default : Duplet := (L_default, L_default). (** Definition 1.4 (Triplet): A tuple of length 3 - T = L³ = {(s, r, o) : s ∈ L, r ∈ L, o ∈ L} + T = L³ = {(r, s, o) : r ∈ L, s ∈ L, o ∈ L} + + Equivalently: T = L × D, where D = L × L + + This uses the representation: + (r, s, o) = (r, (s, o)) = (e, d) where: - - s — reference to subject - r — reference to relation + - s — reference to subject - o — reference to object + - e — entity (in the role of relation) + - d = (s, o) — duplet (subject-object) *) -Definition Triplet := prod (prod L L) L. +Definition Triplet := prod L Duplet. (** Constructor for Triplet from three references *) -Definition make_triplet (s r o : L) : Triplet := ((s, r), o). +Definition make_triplet (r s o : L) : Triplet := (r, (s, o)). + +(** Alternative constructor from entity and duplet *) +Definition make_triplet_ed (e : L) (d : Duplet) : Triplet := (e, d). (** Accessors for Triplet components *) -Definition triplet_subject (t : Triplet) : L := fst (fst t). -Definition triplet_relation (t : Triplet) : L := snd (fst t). -Definition triplet_object (t : Triplet) : L := snd t. +Definition triplet_relation (t : Triplet) : L := fst t. +Definition triplet_subject (t : Triplet) : L := fst (snd t). +Definition triplet_object (t : Triplet) : L := snd (snd t). + +(** Get the subject-object duplet from a triplet *) +Definition triplet_duplet (t : Triplet) : Duplet := snd t. + +(** Get the entity reference from a triplet (same as relation) *) +Definition triplet_entity (t : Triplet) : L := fst t. (** Default triplet value (self-referential entity) *) Definition Triplet_default : Triplet := make_triplet L_default L_default L_default. (* ============================================================ *) -(* 2. Triune Entity (Триединая сущность) *) +(* 2. Triplet as Nested Ordered Pairs (Section 1.3) *) (* ============================================================ *) -(** A triune entity is defined by a triplet (s, r, o) where: - - s (subject) — defines the View +(** Representation of triplet as nested ordered pairs: + (r, s, o) = (r, (s, o)) = (e, d) + + This is the fundamental structure in the new representation. +*) + +(** Convert triplet to (entity, duplet) form *) +Definition triplet_to_ed (t : Triplet) : L * Duplet := + (triplet_entity t, triplet_duplet t). + +(** Convert (entity, duplet) form back to triplet *) +Definition ed_to_triplet (ed : L * Duplet) : Triplet := + let (e, d) := ed in + make_triplet_ed e d. + +(** Theorem: Triplet ↔ (Entity, Duplet) conversion is lossless *) +Theorem triplet_ed_inverse : + forall t : Triplet, + ed_to_triplet (triplet_to_ed t) = t. +Proof. + intros t. + unfold triplet_to_ed, ed_to_triplet. + unfold triplet_entity, triplet_duplet, make_triplet_ed. + destruct t as [r [s o]]. + reflexivity. +Qed. + +(** Theorem: (Entity, Duplet) form preserves components *) +Theorem triplet_components_preserved : + forall r s o : L, + let t := make_triplet r s o in + triplet_relation t = r /\ + triplet_subject t = s /\ + triplet_object t = o. +Proof. + intros r s o. + unfold make_triplet, triplet_relation, triplet_subject, triplet_object. + simpl. + repeat split; reflexivity. +Qed. + + +(* ============================================================ *) +(* 3. Triune Entity (Триединая сущность) *) +(* ============================================================ *) + +(** A triune entity is defined by a triplet (r, s, o) where: - r (relation) — defines the Controller + - s (subject) — defines the View - o (object) — defines the Model This implements the MVC pattern at the language level. @@ -83,29 +162,37 @@ Definition Triplet_default : Triplet := make_triplet L_default L_default L_defau Record TriuneEntity := { entity_id : L; (* Unique identifier *) - entity_subject : L; (* Reference to subject entity *) entity_relation : L; (* Reference to relation entity *) + entity_subject : L; (* Reference to subject entity *) entity_object : L (* Reference to object entity *) }. (** Constructor for TriuneEntity *) -Definition make_entity (id s r o : L) : TriuneEntity := +Definition make_entity (id r s o : L) : TriuneEntity := {| entity_id := id; - entity_subject := s; entity_relation := r; + entity_subject := s; entity_object := o |}. (** Convert TriuneEntity to Triplet *) Definition entity_to_triplet (e : TriuneEntity) : Triplet := - make_triplet (entity_subject e) (entity_relation e) (entity_object e). + make_triplet (entity_relation e) (entity_subject e) (entity_object e). (** Convert Triplet to TriuneEntity (requires id) *) Definition triplet_to_entity (id : L) (t : Triplet) : TriuneEntity := - make_entity id (triplet_subject t) (triplet_relation t) (triplet_object t). + make_entity id (triplet_relation t) (triplet_subject t) (triplet_object t). + +(** Get the subject-object duplet from an entity *) +Definition entity_so_duplet (e : TriuneEntity) : Duplet := + make_duplet (entity_subject e) (entity_object e). + +(** Get the entity-relation duplet from an entity *) +Definition entity_er_duplet (e : TriuneEntity) : Duplet := + make_duplet (entity_id e) (entity_relation e). (* ============================================================ *) -(* 3. Entity Topologies *) +(* 4. Entity Topologies *) (* ============================================================ *) (** Definition 5.2: Entity Topologies @@ -150,11 +237,74 @@ Definition is_projection_source (e : TriuneEntity) : Prop := (* ============================================================ *) -(* 4. Relations Model as Sets *) +(* 5. Two Link Types (Duplets) *) +(* ============================================================ *) + +(** Section 2.2: Two basic link types + + SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} -- defines Relation + ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} -- defines Entity +*) + +Inductive LinkType := + | LinkSO (* Subject-Object pair - defines relation (R = SO) *) + | LinkER. (* Entity-Relation pair - defines entity (E = ER) *) + +(** A typed duplet with its link type *) +Record TypedDuplet := { + typed_duplet_type : LinkType; + typed_duplet_first : L; + typed_duplet_second : L +}. + +(** Create SO duplet (subject-object) - defines a relation *) +Definition make_SO (s o : L) : TypedDuplet := + {| typed_duplet_type := LinkSO; + typed_duplet_first := s; + typed_duplet_second := o |}. + +(** Create ER duplet (entity-relation) - defines an entity *) +Definition make_ER (e r : L) : TypedDuplet := + {| typed_duplet_type := LinkER; + typed_duplet_first := e; + typed_duplet_second := r |}. + +(** Extract SO duplet from a triune entity *) +Definition entity_SO (e : TriuneEntity) : TypedDuplet := + make_SO (entity_subject e) (entity_object e). + +(** Extract ER duplet from a triune entity *) +Definition entity_ER (e : TriuneEntity) : TypedDuplet := + make_ER (entity_id e) (entity_relation e). + +(** Conjugate link types (ER ↔ SO) *) +Definition conjugate_type (lt : LinkType) : LinkType := + match lt with + | LinkSO => LinkER + | LinkER => LinkSO + end. + +(** Theorem: Conjugation is involutive *) +Theorem conjugate_involutive : + forall lt : LinkType, + conjugate_type (conjugate_type lt) = lt. +Proof. + intros lt. + destruct lt; reflexivity. +Qed. + + +(* ============================================================ *) +(* 6. Relations Model as Function (Section 4) *) (* ============================================================ *) -(** The Relations Model RM is represented as a quadruple of - interconnected sets of triplets: RM = {E, O, R, S} +(** Definition 4.4: Relations Model as a function + rm : E → E × E × E = E³ + + Each entity with identifier e is mapped to triplet (r, s, o). + + Equivalently: rm : E → E × (E × E) + rm(e) = (r, (s, o)) *) (** Relations Model: A collection of triune entities *) @@ -176,6 +326,26 @@ Fixpoint RM_find (rm : RelationsModel) (id : L) : option TriuneEntity := else RM_find rest id end. +(** Relations Model as function (functional representation) + rm : E → E³ +*) +Definition RM_as_function (rm : RelationsModel) : L -> option Triplet := + fun id => + match RM_find rm id with + | Some e => Some (entity_to_triplet e) + | None => None + end. + +(** Relations Model as function with nested pairs + rm : E → E × (E × E) +*) +Definition RM_as_nested_function (rm : RelationsModel) : L -> option (L * Duplet) := + fun id => + match RM_find rm id with + | Some e => Some (entity_relation e, entity_so_duplet e) + | None => None + end. + (** Get all entities used as subjects *) Definition RM_subjects (rm : RelationsModel) : list L := map entity_subject rm. @@ -190,96 +360,47 @@ Definition RM_objects (rm : RelationsModel) : list L := (* ============================================================ *) -(* 5. Link Types (Duplet Classification) *) +(* 7. Theorem 3.1: Equivalence of Representations *) (* ============================================================ *) -(** Four basic link types from Section 2.3: - OS ⊆ O × S = {(o, s) : o ∈ O, s ∈ S} - SO ⊆ S × O = {(s, o) : s ∈ S, o ∈ O} - RE ⊆ R × E = {(r, e) : r ∈ R, e ∈ E} - ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ R} -*) - -Inductive LinkType := - | LinkOS (* Object-Subject pair *) - | LinkSO (* Subject-Object pair *) - | LinkRE (* Relation-Entity pair *) - | LinkER. (* Entity-Relation pair *) - -(** A typed duplet with its link type *) -Record TypedDuplet := { - duplet_type : LinkType; - duplet_first : L; - duplet_second : L -}. - -(** Create typed duplets from a triune entity *) - -(** E = SO (entity is defined by subject-object pair) *) -Definition entity_as_SO (e : TriuneEntity) : TypedDuplet := - {| duplet_type := LinkSO; - duplet_first := entity_subject e; - duplet_second := entity_object e |}. +(** Theorem 3.1: RM can be equivalently represented by two subsets of duplets: + RM = {ER, SO} -(** R = OS (relation is defined by object-subject pair) *) -Definition relation_as_OS (e : TriuneEntity) : TypedDuplet := - {| duplet_type := LinkOS; - duplet_first := entity_object e; - duplet_second := entity_subject e |}. - -(** O = ER (object is defined by entity-relation pair) *) -Definition object_as_ER (e : TriuneEntity) : TypedDuplet := - {| duplet_type := LinkER; - duplet_first := entity_id e; - duplet_second := entity_relation e |}. - -(** S = RE (subject is defined by relation-entity pair) *) -Definition subject_as_RE (e : TriuneEntity) : TypedDuplet := - {| duplet_type := LinkRE; - duplet_first := entity_relation e; - duplet_second := entity_id e |}. - - -(* ============================================================ *) -(* 6. Triplet to Duplet Conversion (Theorem 3.1) *) -(* ============================================================ *) - -(** Representation of triplet as nested ordered pairs: - (s, r, o) = ((s, r), o) + where: + E = ER ⊆ E × R = {(e, r) : e ∈ E, r ∈ E} + R = SO ⊆ S × O = {(s, o) : s ∈ E, o ∈ E} *) -(** Convert triplet to nested ordered pairs *) -Definition triplet_to_nested_pair (t : Triplet) : Duplet * L := - let sr := (triplet_subject t, triplet_relation t) in - (sr, triplet_object t). +(** Extract all SO duplets from a Relations Model *) +Definition RM_SO_duplets (rm : RelationsModel) : list TypedDuplet := + map entity_SO rm. -(** Convert nested ordered pairs back to triplet *) -Definition nested_pair_to_triplet (np : Duplet * L) : Triplet := - let (sr, o) := np in - let (s, r) := sr in - make_triplet s r o. +(** Extract all ER duplets from a Relations Model *) +Definition RM_ER_duplets (rm : RelationsModel) : list TypedDuplet := + map entity_ER rm. -(** Theorem: Triplet ↔ Nested Pair conversion is lossless *) -Theorem triplet_nested_pair_inverse : - forall t : Triplet, - nested_pair_to_triplet (triplet_to_nested_pair t) = t. +(** A triplet is equivalent to (e, d) where e ∈ E and d ∈ SO *) +Theorem triplet_as_entity_duplet : + forall r s o : L, + let t := make_triplet r s o in + triplet_entity t = r /\ + triplet_duplet t = make_duplet s o. Proof. - intros t. - unfold triplet_to_nested_pair, nested_pair_to_triplet. - unfold triplet_subject, triplet_relation, triplet_object, make_triplet. - destruct t as [[s r] o]. - reflexivity. + intros r s o. + unfold make_triplet, triplet_entity, triplet_duplet, make_duplet. + simpl. + split; reflexivity. Qed. (* ============================================================ *) -(* 7. Associative Network Representation *) +(* 8. Associative Network Representation *) (* ============================================================ *) (** Definition 4.2: Associative Network of triplets anet³ : L → L³ - Maps a reference to a triplet (subject, relation, object) + Maps a reference to a triplet (relation, subject, object) *) (** Functional representation of 3D associative network *) @@ -292,13 +413,13 @@ Definition ANet3_list := list Triplet. Definition ANet3_list_to_func (net : ANet3_list) : ANet3_func := fun id => nth id net Triplet_default. -(** Theorem 4.1: Relations Model as 3D Associative Network *) +(** Convert Relations Model to 3D associative network *) Definition RM_to_ANet3 (rm : RelationsModel) : ANet3_list := map entity_to_triplet rm. (* ============================================================ *) -(* 8. 2D Associative Network (Duplets) *) +(* 9. 2D Associative Network (Duplets) *) (* ============================================================ *) (** Definition 4.3: Associative Network of Duplets @@ -316,12 +437,12 @@ Definition NestedPairs := list L. (** Convert triplet to nested pairs (list of references) *) Definition triplet_to_NP (t : Triplet) : NestedPairs := - [triplet_subject t; triplet_relation t; triplet_object t]. + [triplet_relation t; triplet_subject t; triplet_object t]. (** Convert nested pairs back to triplet *) Definition NP_to_triplet (np : NestedPairs) : option Triplet := match np with - | [s; r; o] => Some (make_triplet s r o) + | [r; s; o] => Some (make_triplet r s o) | _ => None end. @@ -332,38 +453,18 @@ Theorem triplet_NP_inverse : Proof. intros t. unfold triplet_to_NP, NP_to_triplet. - unfold triplet_subject, triplet_relation, triplet_object, make_triplet. - destruct t as [[s r] o]. + unfold triplet_relation, triplet_subject, triplet_object, make_triplet. + destruct t as [r [s o]]. reflexivity. Qed. -(* ============================================================ *) -(* 9. Conversion between 3D and 2D Associative Networks *) -(* ============================================================ *) - -(** Convert nested pairs to duplet list (with offset indexing) *) -Fixpoint NP_to_duplets_aux (offset : nat) (np : NestedPairs) : ANet2_list := - match np with - | [] => [] - | [h] => [(h, offset)] - | h :: t => (h, S offset) :: NP_to_duplets_aux (S offset) t - end. - -Definition NP_to_duplets (np : NestedPairs) : ANet2_list := - NP_to_duplets_aux 0 np. - -(** Convert ANet3 to ANet2 via nested pairs *) -Definition ANet3_to_ANet2 (net : ANet3_list) : ANet2_list := - flat_map (fun t => NP_to_duplets (triplet_to_NP t)) net. - - (* ============================================================ *) (* 10. Model Properties *) (* ============================================================ *) (** Property 6.1: Closure - Sets E, O, R, S are equivalent - any entity can act as + Sets E, S, O are equivalent - any entity can act as subject, relation, or object in other entities. *) @@ -394,44 +495,18 @@ Definition is_executable (rm : RelationsModel) (e : TriuneEntity) : Prop := (** Get sub-entities of an entity *) Definition get_sub_entities (rm : RelationsModel) (e : TriuneEntity) : option TriuneEntity * option TriuneEntity * option TriuneEntity := - (RM_find rm (entity_subject e), - RM_find rm (entity_relation e), + (RM_find rm (entity_relation e), + RM_find rm (entity_subject e), RM_find rm (entity_object e)). (* ============================================================ *) -(* 11. Conjugate Link Types (Theorem) *) -(* ============================================================ *) - -(** Analogy with DNA complementarity: - - OS is conjugate with SO - - ER is conjugate with RE -*) - -Definition conjugate_type (lt : LinkType) : LinkType := - match lt with - | LinkOS => LinkSO - | LinkSO => LinkOS - | LinkRE => LinkER - | LinkER => LinkRE - end. - -(** Theorem: Conjugation is involutive *) -Theorem conjugate_involutive : - forall lt : LinkType, - conjugate_type (conjugate_type lt) = lt. -Proof. - intros lt. - destruct lt; reflexivity. -Qed. - - -(* ============================================================ *) -(* 12. Example Entities *) +(* 11. Example Entities *) (* ============================================================ *) (** Example 1: Static self-value entity (доменообразующая сущность) Entity10 (Entity10 -Entity10-> Entity10) + Triplet: (10, 10, 10) *) Definition example_static_self : TriuneEntity := make_entity 10 10 10 10. @@ -445,9 +520,10 @@ Qed. (** Example 2: Dynamic self-value entity Entity20 (Entity20 -Entity10-> Entity20) + Triplet: (10, 20, 20) *) Definition example_dynamic_self : TriuneEntity := - make_entity 20 20 10 20. + make_entity 20 10 20 20. (** Verify it's a dynamic self-value *) Example example_dynamic_self_proof : is_dynamic_self_value example_dynamic_self. @@ -458,20 +534,22 @@ Qed. (** Example 3: Reference entity sum (a -add-> b) — sum is the result of adding a and b + Triplet: (2, 1, 3) where 2=add relation, 1=a(subject), 3=b(object) *) Definition example_sum : TriuneEntity := - make_entity 1 1 2 3. (* id=1, subject=a(1), relation=add(2), object=b(3) *) + make_entity 1 2 1 3. (* id=1, relation=add(2), subject=a(1), object=b(3) *) (** Example 4: Simple arithmetic relation result = 1 + 1 { "$rel": "+", "$obj": 1, "$sub": 1 } + Triplet: (102, 101, 101) where 102="+", 101=1 *) Definition example_addition : TriuneEntity := - make_entity 100 101 102 101. (* subject=1, relation="+", object=1 *) + make_entity 100 102 101 101. (* relation="+", subject=1, object=1 *) (* ============================================================ *) -(* 13. Model Construction *) +(* 12. Model Construction *) (* ============================================================ *) (** Build a simple Relations Model *) @@ -482,47 +560,73 @@ Definition example_model : RelationsModel := Definition example_anet3 : ANet3_list := RM_to_ANet3 example_model. -(** Convert to 2D associative network (duplets) *) -Definition example_anet2 : ANet2_list := - ANet3_to_ANet2 example_anet3. +(** Extract SO duplets *) +Definition example_SO_duplets : list TypedDuplet := + RM_SO_duplets example_model. + +(** Extract ER duplets *) +Definition example_ER_duplets : list TypedDuplet := + RM_ER_duplets example_model. (** Compute examples *) Compute example_anet3. -(* Expected: list of triplets *) +(* Expected: list of triplets in form (r, (s, o)) *) + +Compute example_SO_duplets. +(* Expected: list of SO duplets *) -Compute example_anet2. -(* Expected: list of duplets with indexing *) +Compute example_ER_duplets. +(* Expected: list of ER duplets *) (* ============================================================ *) -(* 14. Main Theorems (Summary) *) +(* 13. Main Theorems (Summary) *) (* ============================================================ *) (** Theorem 3.1: Equivalence of Triplet and Duplet Representations - A triplet (s, r, o) can be equivalently represented as - nested ordered pairs ((s, r), o), which reduces to two duplets. + A triplet (r, s, o) can be equivalently represented as + nested ordered pairs (r, (s, o)) = (e, d), which reduces to: + - An entity reference e (in role of relation) + - A subject-object duplet d = (s, o) *) Theorem triplet_duplet_equivalence : - forall s r o : L, - let t := make_triplet s r o in - let np := triplet_to_nested_pair t in - nested_pair_to_triplet np = t. + forall r s o : L, + let t := make_triplet r s o in + let ed := triplet_to_ed t in + ed_to_triplet ed = t. Proof. - intros s r o. - apply triplet_nested_pair_inverse. + intros r s o. + apply triplet_ed_inverse. Qed. -(** Theorem 4.1: Relations Model as 3D Associative Network +(** Theorem 4.1: Relations Model as Function - The Relations Model can be represented as a function λ : L → L³ + The Relations Model can be represented as a function rm : E → E³ + or equivalently rm : E → E × (E × E) *) -Definition RM_as_function (rm : RelationsModel) : L -> option Triplet := - fun id => - match RM_find rm id with - | Some e => Some (entity_to_triplet e) - | None => None - end. +Theorem RM_function_equivalence : + forall (rm : RelationsModel) (id : L) (e : TriuneEntity), + RM_find rm id = Some e -> + RM_as_function rm id = Some (entity_to_triplet e). +Proof. + intros rm id e H. + unfold RM_as_function. + rewrite H. + reflexivity. +Qed. + +(** Theorem: Triplet components are preserved in nested representation *) +Theorem triplet_nested_components : + forall r s o : L, + let t := make_triplet r s o in + fst t = r /\ snd t = (s, o). +Proof. + intros r s o. + unfold make_triplet. + simpl. + split; reflexivity. +Qed. (** Theorem 4.2: 3D to 2D Network Transformation @@ -540,7 +644,7 @@ Qed. (** Theorem 6.1: Closure Property - Sets E, O, R, S are structurally equivalent. + Sets E, S, O are structurally equivalent. Any entity ID can be used in any role (subject, relation, object). *) @@ -558,12 +662,15 @@ Qed. This Rocq/Coq formalization demonstrates that: 1. Triplets (tuples of length 3) can be equivalently represented - as nested ordered pairs (two duplets). + as nested ordered pairs: (r, s, o) = (r, (s, o)) = (e, d). - 2. The Relations Model is a 3D associative network: λ : L → L³ + 2. The Relations Model is a function: rm : E → E³ + or equivalently rm : E → E × (E × E). - 3. Four interconnected sets {E, O, R, S} are equivalent to - four sets of duplets {ER, OS, RE, SO}. + 3. Two basic duplet types {ER, SO} are sufficient to represent + the entire model: + - E = ER (entity defined by entity-relation pair) + - R = SO (relation defined by subject-object pair) 4. The triune entity implements the MVC pattern at the fundamental language structure level.