Konard Apr 1 at 23:35

Глубокая Теория Связей 0.0.1

Hard

24 min

6.8K

Deep.Foundation corporate blogOpen source*Programming*Mathematics*Data Engineering*

Translation

Original author: Иван Глазунов

В прошлое первое апреля, как вы могли догадаться, мы пошутили. Пора это исправить, и теперь $100\%$ всё серьёзно.

TL;DR (too long; didn't read)

В этой статье много букв, но её можно записать всего 4-мя символами теории множеств:

$L \to L^2$

Всё остальное следствие из них.

Сравнение теорий

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

Реляционная алгебра

Реляционная алгебра и реляционная модель основаны на понятиях отношения и n-кортежей.

Отношение определяется как множество n-кортежей:

$\mathbf{R \subseteq S_1 \times S_2 \times \dots \times S_n.}$ [1]

Рис. 1. Таблица описывается отношением , которое представляется множеством строк , принадлежащих декартову произведению . — Рис. 1. Таблица описывается отношением $\mathbf{R}$ , которое представляется множеством строк $\mathbf{r}$ , принадлежащих декартову произведению $\mathbf{S_1 \times S_2 \times \dots \times S_n}$ .

Где:

$\mathbf{R}$ обозначает отношение (таблицу);
$\subseteq$ обозначает, что левая часть выражения является подмножеством правой части выражения;
$\times$ обозначает декартово произведение множеств;
$\mathbf{S_n}$ обозначает множество возможных значений (домен) которые может содержать каждая ячейка в столбце $\mathbf{n}$ ;
Строки или элементы множества $\mathbf{R}$ представлены в виде n-кортежей.

Данные в реляционной модели группируются в отношения. Используя n-кортежи в реляционной модели, можно точно представить любую возможную структуру данных. Но нужны ли вообще n-кортежи? Например, каждый n-кортеж можно представить в виде вложенных упорядоченных пар. Вероятно из этого следует, что достаточно упорядоченных пар для представления любых данных. Также не часто встретишь, что значения столбцов в таблицах представляются n-кортежами (хотя, например, число можно разложить на n-кортеж битов). В некоторых SQL базах данных даже запрещено использовать более $\mathbf{32}$ столбцов в таблице и ее строке (n-кортеже). Так что $\mathbf{N}$ обычно меньше $\mathbf{32}$ . Поэтому, в этом случае, нет реальных n-кортежей, даже в современных реляционных базах данных.

Рис. 2. Сравнение реляционной модели и ассоциативной модели данных (изначальная модель Саймона Вильямса была упрощена дважды). Иными словами для представления всех данных в реляционной модели требуется множество таблиц под каждый тип данных, в ассоциативной модели как оказалось было достаточно сначала двух таблиц, а потом и вовсе одной таблицы триплетов или дуплетов.

Ориентированный граф

Направленный граф и графы в целом основаны на понятиях вершины и ребра (2-кортежа).

Направленный граф $\mathbf{G}$ определяется так:

$\mathbf{G = (V, E), \quad E \subseteq V \times V.}$ [2]

Где:

$\mathbf{V}$ - это множество, элементы которого называются вершинами, узлами или точками;
$\mathbf{E}$ - это множество упорядоченных пар (2-кортежей) вершин, называемых дугами, направленными ребрами (иногда просто ребрами), стрелками или направленными линиями.

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

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

Теория связей

Теория связей основана на понятии связи.

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

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

Дуплеты

Связь-дуплет представлена дуплетом (2-кортежем или упорядоченная парой) ссылок на связи. У связи-дуплета есть собственная ссылка.

L = { 1 , 2 }

L × L = {
  (1, 1),
  (1, 2),
  (2, 1),
  (2, 2),
}

Где: — это множество ссылок (от английского Links — ссылки).

В этом примере в множестве всего ссылки на связи, то есть и . Иными словами в сети связей построенной на таком множестве ссылок может быть только связи.

Чтобы получить все возможные значения связи используется декартово произведение на само себя, то есть $L \times L$ .

alt text — Рис. 4. Матрица представляющая декартово произведение множества { 1, 2 } на само себя. Здесь мы видим что у связей с двумя ссылками на связи может быть всего 4 возможных значения.

Сеть связей-дуплетов определяется как:

$\mathbf{\lambda: L \to L \times L}$

Где:

$\to$ обозначает отображение (функцию);
$\mathbf{\lambda}$ обозначает функцию, которая определяет сеть дуплетов;
$\mathbf{L}$ обозначает множество ссылок на связи.

Пример:

$1 \to (1, 1)$
$2 \to (2, 2)$
$\mathbf{3 \to (1, 2)}$

Сеть связей-дуплетов может представлять любую структуру данных.

Например, связи-дуплеты могут:

связывать объект со своими свойствами;
связывать два дуплета вместе, чего не позволяет теория графов;
представлять любую последовательность (n-кортеж) в виде дерева, построенного из вложенных упорядоченных пар;
описать предложение на естественном языке, например по модели subject-predicate.

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

Триплеты

Связь-триплет представлена триплетом (3-кортежем) ссылок на связи.

L = { 1 , 2 }

L × L = {
  (1, 1),
  (1, 2),
  (2, 1),
  (2, 2),
}

L × L × L = {
  (1, 1, 1),
  (1, 1, 2),
  (1, 2, 1),
  (1, 2, 2),
  (2, 1, 1),
  (2, 1, 2),
  (2, 2, 1),
  (2, 2, 2),
}

Сеть связей-триплетов определяется как:

$\mathbf{\lambda : L \to L \times L \times L}$

Где:

$\mathbf{\lambda}$ обозначает функцию, определяющую сеть триплетов;
$\mathbf{L}$ обозначает множество ссылок на связи.

Пример функции задающей конкретную сеть триплетов:

$1 \to (1, 1, 1)$
$2 \to (2, 2, 2)$
$3 \to (3, 3, 3)$
$\mathbf{4 \to (1, 2, 3)}$

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

Например, связи-триплеты могут:

связывать объект, его свойство и значение;
связывать две связи вместе определённым отношением;
описать предложение на естественном языке, например по модели subject-verb-object.

Вектора

Вектор (последовательность) ссылок на связи также известный как n-кортеж, является общим случаем.

Сеть связей в общем виде определяется так:

$\mathbf{\lambda : L \rightarrow \underbrace{ L \times L \times \ldots \times L}_{n}}$

Где:

$\mathbf{\lambda}$ обозначает функцию, определяющую сеть связей;
$\mathbf{L}$ обозначает множество ссылок на связи.

Пример:

$1 \to (1)$
$2 \to (2, 2)$
$3 \to (3, 3, 3)$
$\mathbf{4 \to (1, 2, 3, 2, 1)}$

В этом примере используются n-кортежи переменной длины в качестве значений связей.

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

Итоги сравнения

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

Ассоциативная модель может легко представить n-кортеж неограниченной длины с использованием кортежей с $\mathbf{n \geq 2}$ , она столь же хороша, как теория графов, в своей способности представлять ассоциации, и она также мощна, как реляционная модель, и может полностью представить любую таблицу SQL. Также ассоциативная модель может представлять строгие последовательности, причём так что любая последовательность может быть представлена всего одной связью, что полезно для дедупликации.

В реляционной модели нет необходимости в более чем одном отношении, чтобы заставить ее вести себя как ассоциативная модель. И в этом отношении нет необходимости в более чем 2-3 столбцах, кроме явного ID или встроенного ID строки.

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

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

На этом перевод с исправлениями прошлой статьи закончен.

Математическое введение в теорию связей

Введение

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

Теория связей разрабатывается как более фундаментальная теория по сравнению с теорией множеств и теорий типов и на замену реляционной алгебре и теории графов. В то время, как в теории типов основными понятиями являются «тип» и «терм», а в теории множеств — «множество», «элемент», в теории связей все сводится к единому понятию «связь».

В этом разделе мы разберём основные понятия и термины, используемые в теории связей.

Затем перейдем к определениям теории связей в рамках теории множеств, которое мы отразим на теорию типов используя интерактивное программное средство доказательства теорем «Coq».

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

Теория связей

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

Связь

Связь имеет ассиметричную рекурсивную структуру, которая может быть выражена просто: связь связывает связи. Под ассиметричностью имеется ввиду то, что каждая связь имеет направление от источника (начала) к приёмнику (концу).

Определения теории связей в рамках теории множеств

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

Множество ссылок на вектора:

$\mathbf{L ⊆ ℕ_0}$

Вектор ссылок — это вектор, состоящий из нуля или нескольких ссылок на вектора, где количество ссылок соответствует количеству элементов вектора.

Множество всех векторов ссылок длины :

$\mathbf{V_n = L^n}$

Декартова степень всегда даст вектор длины , так как все его компоненты будут одного и того же типа .
Другими словами, представляет собой множество всех возможных n‑элементных векторов, где каждый элемент вектора принадлежит последовательности . Это эквивалентно по сути n‑кортежу.

Ассоциация — это упорядоченная пара, состоящая из ссылки на вектор и вектора ссылок.
Эта структура служит для отображения между ссылками и векторами.
Множество всех ассоциаций:

$\mathbf{A = L \times V_n}$

Ассоциативная сеть векторов длины n (или n‑мерная ассоциативная сеть) из семейства функций $\{anetv^n\}$ , отображает ссылку из множества в вектор ссылок длины , который принадлежит множеству , фактически идентифицирует точки в n‑мерном пространстве.
в указывает на то, что функция возвращает вектора, содержащие ссылок.
Каждая n‑мерная ассоциативная сеть таким образом представляет последовательность точек в n‑мерном пространстве.

Семейство функций:

$\mathbf{∪_f \{anetv^n | n ∈ ℕ_0\} ⊆ A}$

Здесь обозначает объединение всех функций в семействе $\{anetv^n\}$ , обозначает «это подмножество», а — множество всех ассоциаций.
Это говорит о том, что все упорядоченные пары, функций , представленных в виде функционального бинарного отношения, являются подмножеством .

Множество дуплетов (упорядоченных пар или двумерных векторов) ссылок:

$\mathbf{D = L^2}$

Это множество всех дуплетов , или вторая декартова степень .

Ассоциативная сеть дуплетов (или двумерная ассоциативная сеть):

$\mathbf{anetd: L → L^2}$

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

Пустой вектор представлен пустым кортежем: представляемый как .

Ассоциативная сеть вложенных упорядоченных пар:

$\mathbf{anetl: L → NP}\textbf{, где }\mathbf{NP = \{(∅, ∅) | (l, np), l ∈ L, np ∈ NP\} }$

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

Проекция теории cвязей в теории типов (Coq) через теорию множеств

Про Coq

Coq — это интерактивное средство для создания доказательств, реализующее теорию типов высшего порядка, которая известна также как Язык Калькуляции Индуктивных Построений (Calculus of Inductive Constructions, CIC). Это среда обладает возможностями формализации сложных математических теорем, проверки доказательств на корректность, а также извлечения работающего программного кода из формально проверенных спецификаций. Coq широко используется в академических кругах для формализации математики, а также в IT-индустрии для верификации программного обеспечения и оборудования.

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

В преддверии обширной работы по доказательству эквивалентности реляционной модели и ассоциативной сети дуплетов, мы представляем в этом разделе начальные шаги выполненные с использованием системы доказательств языка Coq. На первом этапе стоит задача формализации структур ассоциативных сетей через определения базовых типов функций и структур внутри Coq.

Определения ассоциативных сетей

Ссылка на исходник


Require Import PeanoNat.
Require Import Coq.Init.Nat.
Require Import Vector.
Require Import List.
Require Import Coq.Init.Datatypes.
Import ListNotations.
Import VectorNotations.

(* Последовательность ссылок на вектора: L ⊆ ℕ₀ *)
Definition L := nat.

(* Дефолтное значение L: ноль *)
Definition LDefault : L := 0.

(* Множество векторов ссылок длины n ∈ ℕ₀: Vn ⊆ Lⁿ *)
Definition Vn (n : nat) := t L n.

(* Дефолтное значение Vn *)
Definition VnDefault (n : nat) : Vn n := Vector.const LDefault n.

(* Множество всех ассоциаций: A = L × Vn *)
Definition A (n : nat) := prod L (Vn n).

(* Ассоциативная сеть векторов длины n (или n-мерная ассоциативная сеть) из семейства функций {anetvⁿ : L → Vn} *)
Definition ANetVf (n : nat) := L -> Vn n.

(* Ассоциативная сеть векторов длины n (или n-мерная ассоциативная сеть) в виде последовательности *)
Definition ANetVl (n : nat) := list (Vn n).

(* Вложенные упорядоченные пары *)
Definition NP := list L.

(* Ассоциативная сеть вложенных упорядоченных пар: anetl : L → NP *)
Definition ANetLf := L -> NP.

(* Ассоциативная сеть вложенных упорядоченных пар в виде последовательности вложенных упорядоченных пар *)
Definition ANetLl := list NP.

(* Дуплет ссылок *)
Definition D := prod L L.

(* Дефолтное значение D: пара из двух LDefault, используется для обозначения пустого дуплета *)
Definition DDefault : D := (LDefault, LDefault).

(* Ассоциативная сеть дуплетов (или двумерная ассоциативная сеть): anetd : L → L² *)
Definition ANetDf := L -> D.

(* Ассоциативная сеть дуплетов (или двумерная ассоциативная сеть) в виде последовательности дуплетов *)
Definition ANetDl := list D.

Функции преобразования ассоциативных сетей

(* Функция преобразования Vn в NP *)
Fixpoint VnToNP {n : nat} (v : Vn n) : NP :=
  match v with
  | Vector.nil _ => List.nil
  | Vector.cons _ h _ t => List.cons h (VnToNP t)
  end.

(* Функция преобразования ANetVf в ANetLf *)
Definition ANetVfToANetLf {n : nat} (a: ANetVf n) : ANetLf:=
  fun id => VnToNP (a id).

(* Функция преобразования ANetVl в ANetLl *)
Definition ANetVlToANetLl {n: nat} (net: ANetVl n) : ANetLl :=
  map VnToNP net.

(* Функция преобразования NP в Vn *)
Fixpoint NPToVnOption (n: nat) (p: NP) : option (Vn n) :=
  match n, p with
  | 0, List.nil => Some (Vector.nil nat)
  | S n', List.cons f p' => 
      match NPToVnOption n' p' with
      | None => None
      | Some t => Some (Vector.cons nat f n' t)
      end
  | _, _ => None
  end.

(* Функция преобразования NP в Vn с VnDefault *)
Definition NPToVn (n: nat) (p: NP) : Vn n :=
  match NPToVnOption n p with
  | None => VnDefault n
  | Some t => t
  end.

(* Функция преобразования ANetLf в ANetVf *)
Definition ANetLfToANetVf { n: nat } (net: ANetLf) : ANetVf n :=
  fun id => match NPToVnOption n (net id) with
            | Some t => t
            | None => VnDefault n
            end.

(* Функция преобразования ANetLl в ANetVl *)
Definition ANetLlToANetVl {n: nat} (net : ANetLl) : ANetVl n :=
  map (NPToVn n) net.

(* Функция преобразования NP в ANetDl со смещением индексации *)
Fixpoint NPToANetDl_ (offset: nat) (np: NP) : ANetDl :=
  match np with
  | nil => nil
  | cons h nil => cons (h, offset) nil
  | cons h t => cons (h, S offset) (NPToANetDl_ (S offset) t)
  end.

(* Функция преобразования NP в ANetDl*)
Definition NPToANetDl (np: NP) : ANetDl := NPToANetDl_ 0 np.

(* Функция добавления NP в хвост ANetDl *)
Definition AddNPToANetDl (anet: ANetDl) (np: NP) : ANetDl :=
  app anet (NPToANetDl_ (length anet) np).

(* Функция отрезает голову anetd и возвращает хвост начиная с offset  *)
Fixpoint ANetDl_behead (anet: ANetDl) (offset : nat) : ANetDl :=
  match offset with
  | 0 => anet
  | S n' =>
    match anet with
    | nil => nil
    | cons h t => ANetDl_behead t n'
    end
  end.

(* Функция преобразования ANetDl в NP с индексации в начале ANetDl начиная с offset*)
Fixpoint ANetDlToNP_ (anet: ANetDl) (offset: nat) (index: nat): NP :=
  match anet with
  | nil => nil
  | cons (x, next_index) tail_anet =>
    if offset =? index then
      cons x (ANetDlToNP_ tail_anet (S offset) next_index)
    else
      ANetDlToNP_ tail_anet (S offset) index
  end.

(* Функция чтения NP из ANetDl по индексу дуплета*)
Definition ANetDl_readNP (anet: ANetDl) (index: nat) : NP :=
  ANetDlToNP_ anet 0 index.

(* Функция преобразования ANetDl в NP начиная с головы списка асети *)  
Definition ANetDlToNP (anet: ANetDl) : NP := ANetDl_readNP anet 0.


(*
  Теперь всё готово для преобразования асети вложенных упорядоченных пар anetl : L → NP
в асеть дуплетов anetd : L → L².

Данное преобразование можно делать по разному: с сохранением исходных ссылок на вектора
либо с переиндексацией. Переиндексацию можно не делать если написать дополнительную функцию для
асети дуплетов которая возвращает вложенную упорядоченную пару по её ссылке.
*)

(* Функция добавления ANetLl в ANetDl *)
Fixpoint AddANetLlToANetDl (anetd: ANetDl) (anetl: ANetLl) : ANetDl :=
  match anetl with
  | nil => anetd
  | cons h t => AddANetLlToANetDl (AddNPToANetDl anetd h) t
  end.

(* Функция преобразования ANetLl в ANetDl *)
Definition ANetLlToANetDl (anetl: ANetLl) : ANetDl :=
  match anetl with
  | nil => nil
  | cons h t => AddANetLlToANetDl (NPToANetDl h) t
  end.

(* Функция поиска NP в хвосте ANetDl начинающемуся с offset по её порядковому номеру. Возвращает offset NP *)
Fixpoint ANetDl_offsetNP_ (anet: ANetDl) (offset: nat) (index: nat) : nat :=
  match anet with
  | nil => offset + (length anet)
  | cons (_, next_index) tail_anet =>
    match index with
    | O => offset
    | S index' => 
      if offset =? next_index then
        ANetDl_offsetNP_ tail_anet (S offset) index'
      else
        ANetDl_offsetNP_ tail_anet (S offset) index
    end
  end.

(* Функция поиска NP в ANetDl по её порядковому номеру. Возвращает offset NP *)
Definition ANetDl_offsetNP (anet: ANetDl) (index: nat) : nat :=
  ANetDl_offsetNP_ anet 0 index.

(* Функция преобразования ANetVl в ANetDl *)
Definition ANetVlToANetDl {n : nat} (anetv: ANetVl n) : ANetDl :=
  ANetLlToANetDl (ANetVlToANetLl anetv).


(*
  Теперь всё готово для преобразования асети дуплетов anetd : L → L²
 в асеть вложенных упорядоченных пар anetl : L → NP

Данное преобразование будем делать с сохранением исходных ссылоке на вектора.
Переиндексацию можно не делать, потому что есть функция ANetDl_offsetNP для
асети дуплетов которая возвращает смещение вложенной УП по ссылке на её.
*)

(* Функция отрезает первую NP из ANetDl и возвращает хвост *)
Fixpoint ANetDl_beheadNP (anet: ANetDl) (offset: nat) : ANetDl :=
  match anet with
  | nil => nil
  | cons (_, next_index) tail_anet =>
    if offset =? next_index then (* конец NP *)
      tail_anet
    else  (* ещё не конец NP *)
      ANetDl_beheadNP tail_anet (S offset)
  end.

(* Функция преобразования NP и ANetDl со смещения offset в ANetLl *)
Fixpoint ANetDlToANetLl_ (anetd: ANetDl) (np: NP) (offset: nat) : ANetLl :=
  match anetd with
  | nil => nil (* отбрасываем NP даже если она недостроена *)
  | cons (x, next_index) tail_anet =>
    if offset =? next_index then (* конец NP, переходим к следующей NP *)
      cons (app np (cons x nil)) (ANetDlToANetLl_ tail_anet nil (S offset))
    else  (* ещё не конец NP, парсим асеть дуплетов дальше *)
      ANetDlToANetLl_ tail_anet (app np (cons x nil)) (S offset)
  end.

(* Функция преобразования ANetDl в ANetLl *)
Definition ANetDlToANetLl (anetd: ANetDl) : ANetLl :=
  ANetDlToANetLl_ anetd nil LDefault.

Предикаты эквивалентности ассоциативных сетей

(* Определение anets_equiv вводит предикат эквивалентности двух ассоциативных сетей векторов длины n,
 anet1 и anet2 типа ANetVf. 

  Данный предикат описывает свойство "эквивалентности" для таких сетей.
 Он утверждает, что anet1 и anet2 считаются "эквивалентными", если для каждой ссылки id вектор,
 связанный с id в anet1, точно совпадает с вектором, связанным с тем же id в anet2.
*)
Definition ANetVf_equiv {n: nat} (anet1: ANetVf n) (anet2: ANetVf n) : Prop :=
  forall id, anet1 id = anet2 id.

(* Определение anets_equiv вводит предикат эквивалентности двух ассоциативных сетей векторов длины n,
 anet1 и anet2 типа ANetVl.
*)
Definition ANetVl_equiv_Vl {n: nat} (anet1: ANetVl n) (anet2: ANetVl n) : Prop :=
  anet1 = anet2.

(* Предикат эквивалентности для ассоциативных сетей дуплетов ANetDf *)
Definition ANetDf_equiv (anet1: ANetDf) (anet2: ANetDf) : Prop := forall id, anet1 id = anet2 id.

(* Предикат эквивалентности для ассоциативных сетей дуплетов ANetDl *)
Definition ANetDl_equiv (anet1: ANetDl) (anet2: ANetDl) : Prop := anet1 = anet2.

Леммы эквивалентности ассоциативных сетей

(* Лемма о сохранении длины векторов ассоциативной сети *)
Lemma Vn_dim_preserved : forall {l: nat} (t: Vn l), List.length (VnToNP t) = l.
Proof.
  intros l t.
  induction t.
  - simpl. reflexivity.
  - simpl. rewrite IHt. reflexivity.
Qed.


(* Лемма о взаимном обращении функций NPToVnOption и VnToNP

  H_inverse доказывает, что каждый вектор Vn без потери данных может быть преобразован в NP
 с помощью VnToNP и обратно в Vn с помощью NPToVnOption.

  В формальном виде forall n: nat, forall t: Vn n, NPToVnOption n (VnToNP t) = Some t говорит о том,
 что для всякого натурального числа n и каждого вектора Vn длины n,
 мы можем преобразовать Vn в NP с помощью VnToNP,
 затем обратно преобразовать результат в Vn с помощью NPToVnOption n,
 и в итоге получать тот же вектор Vn, что и в начале.

  Это свойство очень важно, потому что оно гарантирует,
 что эти две функции образуют обратные друг к другу пары функций на преобразуемом круге векторов Vn и NP.
 Когда вы применяете обе функции к значениям в преобразуемом круге, вы в итоге получаете исходное значение.
 Это означает, что никакая информация не теряется при преобразованиях,
 так что можно свободно конвертировать между Vn и NP,
 если это требуется в реализации или доказательствах.
 *)
Lemma H_inverse: forall n: nat, forall t: Vn n, NPToVnOption n (VnToNP t) = Some t.
Proof.
  intros n.
  induction t as [| h n' t' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.


(*
  Теорема обертывания и восстановления ассоциативной сети векторов:

Пусть дана ассоциативная сеть векторов длины n, обозначенная как anetvⁿ : L → Vⁿ.
Определим операцию отображения этой сети в ассоциативную сеть вложенных упорядоченных пар anetl : L → NP,
  где NP = {(∅,∅) | (l,np), l ∈ L, np ∈ NP}.
Затем определим обратное отображение из ассоциативной сети вложенных упорядоченных пар обратно в ассоциативную сеть векторов длины n.

  Теорема утверждает:

Для любой ассоциативной сети векторов длины n, anetvⁿ, применение операции преобразования в ассоциативную сеть вложенных упорядоченных пар
 и обратное преобразование обратно в ассоциативную сеть векторов длины n обеспечивает восстановление исходной сети anetvⁿ.
То есть, если мы преобразуем anetvⁿ в anetl и потом обратно в anetvⁿ, то мы получим исходную ассоциативную сеть векторов anetvⁿ.
 Иначе говоря:

    ∀ anetvⁿ : L → Vⁿ, преобразование обратно(преобразование вперед(anetvⁿ)) = anetvⁿ.
*)
Theorem anetf_equiv_after_transforms : forall {n: nat} (anet: ANetVf n),
  ANetVf_equiv anet (fun id => match NPToVnOption n ((ANetVfToANetLf anet) id) with
                            | Some t => t
                            | None   => anet idhttps://github.com/deep-foundation
                            end).
Proof.
  intros n net id.
  unfold ANetVfToANetLf.
  simpl.
  rewrite H_inverse.
  reflexivity.
Qed.


(* Лемма о сохранении длины списков NP в ассоциативной сети дуплетов *)
Lemma NP_dim_preserved : forall (offset: nat) (np: NP), 
    length np = length (NPToANetDl_ offset np).
Proof.
  intros offset np.
  generalize dependent offset. 
  induction np as [| n np' IHnp']; intros offset.
  - simpl. reflexivity.
  - destruct np' as [| m np'']; simpl; simpl in IHnp'.
    + reflexivity.
    + rewrite IHnp' with (offset := S offset). reflexivity.
Qed.

Примеры преобразования ассоциативных сетей друг в друга

(*  Нотация записи списков  *)
Notation "{ }" := (nil) (at level 0).
Notation "{ x , .. , y }" := (cons x .. (cons y nil) ..) (at level 0).

(*  Трёхмерная ассоциативная сеть  *)
Definition complexExampleNet : ANetVf 3 :=
  fun id => match id with
  | 0 => [0; 0; 0]
  | 1 => [1; 1; 2]
  | 2 => [2; 4; 0]
  | 3 => [3; 0; 5]
  | 4 => [4; 1; 1]
  | S _ => [0; 0; 0]
  end.

(*  Вектора ссылок  *)
Definition exampleTuple0 : Vn 0 := [].
Definition exampleTuple1 : Vn 1 := [0].
Definition exampleTuple4 : Vn 4 := [3; 2; 1; 0].

(*  Преобразование векторов ссылок во вложенные упорядоченные пары (списки)  *)
Definition nestedPair0 := VnToNP exampleTuple0.
Definition nestedPair1 := VnToNP exampleTuple1.
Definition nestedPair4 := VnToNP exampleTuple4.

Compute nestedPair0.  (* Ожидается результат: { } *)
Compute nestedPair1.  (* Ожидается результат: {0} *)
Compute nestedPair4.  (* Ожидается результат: {3, 2, 1, 0} *)

(*  Вычисление значений преобразованной функции трёхмерной ассоциативной сети   *)
Compute (ANetVfToANetLf complexExampleNet) 0. (* Ожидается результат: {0, 0, 0} *)
Compute (ANetVfToANetLf complexExampleNet) 1. (* Ожидается результат: {1, 1, 2} *)
Compute (ANetVfToANetLf complexExampleNet) 2. (* Ожидается результат: {2, 4, 0} *)
Compute (ANetVfToANetLf complexExampleNet) 3. (* Ожидается результат: {3, 0, 5} *)
Compute (ANetVfToANetLf complexExampleNet) 4. (* Ожидается результат: {4, 1, 1} *)
Compute (ANetVfToANetLf complexExampleNet) 5. (* Ожидается результат: {0, 0, 0} *)

(*  Ассоциативная сеть вложенных УП (упорядоченных пар)  *)
Definition testPairsNet : ANetLf :=
  fun id => match id with
  | 0 => {5, 0, 8}
  | 1 => {7, 1, 2}
  | 2 => {2, 4, 5}
  | 3 => {3, 1, 5}
  | 4 => {4, 2, 1}
  | S _ => {0, 0, 0}
  end.

(*  Преоразованная ассоциативная сеть вложенных УП в трёхмерную ассоциативную сеть (размерность должна совпадать) *)
Definition testTuplesNet : ANetVf 3 :=
  ANetLfToANetVf testPairsNet.

(*  Вычисление значений преобразованной функции ассоциативной сети вложенных УП   *)
Compute testTuplesNet 0.   (* Ожидается результат: [5; 0; 8] *)
Compute testTuplesNet 1.   (* Ожидается результат: [7; 1; 2] *)
Compute testTuplesNet 2.   (* Ожидается результат: [2; 4; 5] *)
Compute testTuplesNet 3.   (* Ожидается результат: [3; 1; 5] *)
Compute testTuplesNet 4.   (* Ожидается результат: [4; 2; 1] *)
Compute testTuplesNet 5.   (* Ожидается результат: [0; 0; 0] *)

(*  Преобразование вложенных УП в ассоциативную сеть дуплетов  *)
Compute NPToANetDl { 121, 21, 1343 }.
(* Должно вернуть: {(121, 1), (21, 2), (1343, 2)} *)

(*  Добавление вложенных УП в ассоциативную сеть дуплетов  *)
Compute AddNPToANetDl {(121, 1), (21, 2), (1343, 2)} {12, 23, 34}. 
(* Ожидается результат: {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} *)

(*  Преобразование ассоциативной сети дуплетов во вложенные УП  *)
Compute ANetDlToNP {(121, 1), (21, 2), (1343, 2)}. 
(* Ожидается результат: {121, 21, 1343} *)
  
Compute ANetDlToNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)}. 
(* Ожидается результат: {121, 21, 1343} *)

(*  Чтение вложенных УП из ассоциативной сети дуплетов по индексу дуплета - начала вложенных УП  *)
Compute ANetDl_readNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} 0.
(* Ожидается результат: {121, 21, 1343} *)

Compute ANetDl_readNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} 3.
(* Ожидается результат: {12, 23, 34} *)


(*  Определяем ассоциативная сеть вложенных УП *)
Definition test_anetl := { {121, 21, 1343}, {12, 23}, {34}, {121, 21, 1343}, {12, 23}, {34} }.

(*  Преобразованная ассоциативная сеть вложенных УП в ассоциативную сеть дуплетов  *)
Definition test_anetd := ANetLlToANetDl test_anetl.

(*  Вычисление преобразованной ассоциативной сети вложенных УП в ассоциативную сеть дуплетов  *)
Compute test_anetd.
(* Ожидается результат:
 {(121, 1), (21, 2), (1343, 2),
  (12, 4), (23, 4),
  (34, 5),
  (121, 7), (21, 8), (1343, 8),
  (12, 10), (23, 10),
  (34, 11)} *)


(*  Вычисления преобразования ассоциативной сети вложенных УП в ассоциативную сеть дуплетов и обратно в test_anetl *) 
Compute ANetDlToANetLl test_anetd.
(* Ожидается результат:
  {{121, 21, 1343}, {12, 23}, {34}, {121, 21, 1343}, {12, 23}, {34}}  *)

(*  Вычисления смещения вложенных УП в ассоциативной сети дуплетов по их порядковому номеру  *)
Compute ANetDl_offsetNP test_anetd 0.   (* Ожидается результат: 0 *)
Compute ANetDl_offsetNP test_anetd 1.   (* Ожидается результат: 3 *)
Compute ANetDl_offsetNP test_anetd 2.   (* Ожидается результат: 5 *)
Compute ANetDl_offsetNP test_anetd 3.   (* Ожидается результат: 6 *)
Compute ANetDl_offsetNP test_anetd 4.   (* Ожидается результат: 9 *)
Compute ANetDl_offsetNP test_anetd 5.   (* Ожидается результат: 11 *)
Compute ANetDl_offsetNP test_anetd 6.   (* Ожидается результат: 12 *)
Compute ANetDl_offsetNP test_anetd 7.   (* Ожидается результат: 12 *)


(*  Определяем трёхмерную ассоциативную сеть как последователность векторов длины 3  *)
Definition test_anetv : ANetVl 3 :=
  { [0; 0; 0], [1; 1; 2], [2; 4; 0], [3; 0; 5], [4; 1; 1], [0; 0; 0] }.

(*  Преобразованная трёхмерная ассоциативная сеть в ассоциативную сеть дуплетов через ассоциативную сеть вложенных УП  *)
Definition test_anetdl : ANetDl := ANetVlToANetDl test_anetv.

(*  Вычисление трёхмерной ассоциативной сети преобразованной в ассоциативную сеть дуплетов через ассоциативную сеть вложенных УП  *)
Compute test_anetdl.
(* Ожидается результат:
{ (0, 1), (0, 2), (0, 2),
  (1, 4), (1, 5), (2, 5),
  (2, 7), (4, 8), (0, 8),
  (3, 10), (0, 11), (5, 11),
  (4, 13), (1, 14), (1, 14),
  (0, 16), (0, 17), (0, 17)}  *)

(*  Преобразованная трёхмерная ассоциативная сеть в ассоциативную сеть дуплетов через ассоциативную сеть вложенных УП и наоборот в трёхмерную ассоциативную сеть  *)
Definition result_TuplesNet : ANetVl 3 :=
  ANetLlToANetVl (ANetDlToANetLl test_anetdl).

(*  Итоговая проверка эквивалентности ассоциативных сетей   *)
Compute result_TuplesNet.
(* Ожидается результат:
  { [0; 0; 0], [1; 1; 2], [2; 4; 0], [3; 0; 5], [4; 1; 1], [0; 0; 0] }  *)

Практическая реализация

Существует несколько практических реализаций: Deep, LinksPlatform и Модель Отношений.

Deep

Deep — это система, основанная на теории связей. В теории связей с помощью связей можно представлять любые данные или знания, а также использовать их для программирования. На это ориентирован Deep. В Deep всё — связи. Однако если разделить их на две категории, то у нас будут собственно данные и поведение. Поведение, представленное код в Deep хранится в ассоциативном хранилище в виде связей, а для исполнения передаётся в docker соответствующего языка программирования и изолированно и безопасно выполняется. Вся коммуникация между различными частями кода осуществляется через связи в хранилище (базы данных), что делает базу данных универсальным API основанном на данных (в отличии от традиционной практике вызова функций и методов). В данный момент в качестве ассоциативного хранилища в Deep используется PostgreSQL, который позднее будет заменён на движок данных основанный на дуплетах и триплетах из LinksPlatform.

Deep позволяет делать весь софт на планете совместимым, представляя все его части в виде связей. Также возможно хранить любые данные и код вместе, связывать события действий над различными типами ассоциаций с соответствующим кодом, который выполняется для обработки этих событий. Каждый обработчик может получать необходимые связи из ассоциативного хранилища и вставлять/обновлять/удалять связи в него, что может инициировать дальнейшее каскадное выполнение обработчиков.

Таблица links в базе данных (PostgreSQL) Deep содержит записи, которые можно интерпретировать как связи. Они имеют такие колонки как id, type_id, from_id, и to_id. Типы связей помогают разработчику ассоциативных пакетов предопределить семантику отношений между различными элементами. Что гарантирует однозначное понимание связей как людьми так и кодом в ассоциативных пакетах. Кроме таблицы links, в системе также присутствуют таблицы numbers, strings и objects для хранения числовых, строковых и JSON значений соответственно. К каждой связи можно привязать только одно значение.

LinksPlatfrom

LinksPlatfrom — это кроссплатформенный мультиязычный фреймворк который направлен на то, чтобы осуществить низкоуровневую реализацию ассоциативности в виде конструктора движков баз данных. К примеру, на текущий момент у нас существует бенчмарк, который сравнивает реализацию дуплетов в PostgreSQL и аналогичную реализацию на чистом Rust/C++, лидирующая реализация на Rust обгоняет PostgreSQL на операциях записи в 200+ раз, а на операциях чтения в 1000+ раз.

Модель отношений

Модель отношений — это язык метапрограммирования основанный на представлении программы в виде трёхмерной ассоциативной сети.
Модель отношений относится к сущностно‑ориентированному программированию, где сущность используется в качестве единственной фундаментальной концепции, т. е. предполагается, что всё есть сущность и нет ничего кроме сущностей.
В модели отношений, сущность в зависимости от своего внутреннего конститутивного принципа может быть либо структурой (объектом) либо функцией (методом).
В отличии от известной ER — модели, где для представления схемы базы данных используются два базовых понятия — сущность и связь, в модели отношений и сущность и связь есть суть одно и тоже.
Такое представление позволяет описывать не только внешние отношения сущности, но и внутреннюю её модель — модель отношений.
Сущность в своём внутреннем принципе триедина (троична, трёхэлементна), потому что она есть объединение (синтез) трёх аспектов (качеств) других (или себя) сущностей.

jsonRVM — многопоточная виртуальная машина для исполнения json проекции модели отношений.
Модель отношений представленная в виде json позволяет писать программы непосредственно на json. Такое представление представляет собой гибрид сегмента данных и кода и позволяет легко десериализовать/исполнять/сериализовать проекцию модели отношений, а так же использовать редакторы json для программирования. В процессе исполнения модели отношений, метапрограмма может не только обрабатывать данные но и генерировать многопоточные программы и метапрограммы и сразу исполнять их или выгружать в виде json.

Заключение

В этой статье мы рассмотрели математический базис реляционной алгебры, теории графов, а так же изложили определения теории связей в терминах теории множеств и отразили это на теорию типов. А так же определили набор функций и лемм необходимых для доказательства возможности эквивалентного преобразования из любого вектора/последовательности в вложенные связи-дуплеты и обратно. А значит достаточно только одной формулы:

$L \to L^2$

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

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

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

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

Планы на будущее

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

Чтобы не пропустить обновления, рекомендуем подписаться на блог Deep.Foundation здесь или уже сейчас посмотреть наши наработки на GitHub или напрямую написать нам на нашем сервере в Discord (особенно подойдёт, если вы боитесь что вас заминусуют в комментариях).

Будем рады любой вашей обратной связи что здесь на хабре, что на GitHub и Discord. Вы так же можете поучаствовать в разработке теории, или ускорить эту разработку любым взаимодействием с нами.

P.S.

Статья будет обновляться по мере развития и дополнения теории связи в течение следующего месяца.

P.S.S.

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

Символами юникода:

L ↦ L²

Используя LaTeX:

L \to L^2

Который преобразуется в SVG (нажимается):

$L \to L^2$

Ссылки

Edgar F. Codd, IBM Research Laboratory, San Jose, California, June 1970, “Relational Model of Data for Large Shared Data Banks.”, paragraph 1.3., page 379
Bender, Edward A.; Williamson, S. Gill (2010). “Lists, Decisions and Graphs. With an Introduction to Probability.”, section 2, definition 6, page 161

Tags:

Hubs:

Глубокая Теория Связей 0.0.1

TL;DR (too long; didn't read)

Сравнение теорий

Реляционная алгебра

Ориентированный граф

Теория связей

Дуплеты

Триплеты

Вектора

Итоги сравнения

Математическое введение в теорию связей

Введение

Теория связей

Связь

Определения теории связей в рамках теории множеств

Проекция теории cвязей в теории типов (Coq) через теорию множеств

Про Coq

Определения ассоциативных сетей

Функции преобразования ассоциативных сетей

Предикаты эквивалентности ассоциативных сетей

Леммы эквивалентности ассоциативных сетей

Примеры преобразования ассоциативных сетей друг в друга

Практическая реализация

Deep

LinksPlatfrom

Модель отношений

Заключение

Планы на будущее

P.S.

P.S.S.

Ссылки

Articles

Information