Theory of Connections 0.0.1

Last April Fools' Day, as you might have guessed, we joked. It's time to fix it and noweverything is serious.

Comparison of theories

We begin by comparing the mathematical foundations of the two most popular theories and the association theory. This will quickly bring the reader into context.

Relational algebra

Relational algebra and relational model are based on the concepts of relation and n-tuples.

The relation is defined as a bunch of n-tuples:

[1]

Where:

• denotes a relation (table);

• denotes the scope of each column;

• Strings or set elements represented as n-tuples.

Data in the relational model is grouped into relationships. By using n-tuples in the relational model, any possible data structure can be accurately represented. But are n-tuples even necessary? For example, each n-tuple can be represented as nested ordered pairs (2-tuples). It's also not common to see column values ​​in tables represented as n-tuples (although, for example, a number can be decomposed into an n-tuple of bits). Some databases even prohibit using more than columns in the table and its row (n-tuple). So usually less . Therefore, in this case, there are no real n-tuples, even in modern relational databases.

Directed graph

A directed graph and graphs in general are based on the concepts of vertex and edge (2-tuple).

Directed graph defined as an ordered pair :

Where:

• – This a bunch ofwhose elements are called peaksnodes or points;

• – this is a lot ordered pairs (2-tuples) of vertices, called arcs, directed edges (sometimes just edges), arrows, or directed lines.

Data in a graph model is represented as two separate sets of nodes and edges, and one can use this model for almost anything, except perhaps sequences (n-tuples). Well, perhaps they can be imagined sequences as sets, but in our opinion this is not a practical way to represent sequences. We're probably not alone in thinking this, which may explain why we couldn't find examples of other people doing this.

Association theory

Association theory is based on the concept of connection.

The connection is defined as n-tuple links to connections.

Doublets

A doublet is also known as a 2-tuple or ordered pair.

L = { 1 , 2 }

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

A network of doublets is defined as:

Where:

• denotes a function that defines a network of doublets;

• denotes the set of link indices.

Example:

Data in a doublet network is represented using doublets (2-tuples).

Doublets can:

• associate an object with its properties;

• link two doublets together, which graph theory does not allow;

• represent any sequence (n-tuple) as a tree constructed from nested ordered pairs.

Thanks to this, doublets can represent, we believe, any possible data structure.

Triplets

A triplet is also known as a 3-tuple.

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),
}

A triplet network is defined as:

Where:

• denotes the function defining the triplet network;

• denotes a set of link indices.

Example:

Data in a triplet network is represented using triplets (3-tuples).

Triplets can do the same things as doublets, and also allow you to specify types or values ​​directly for each reference.

Vector

Vector (sequence) also known as n-tupleis the general case.

A network of connections is generally defined as follows:

Where:

• denotes a function that defines a network of connections;

• denotes a set of link indices.

Example:

This example uses variable-length n-tuples for link values.

Sequences are essentially equivalent in expressive power to the relational model. And this remains to be proven within the framework of the theory being developed. But when it was noticed that doublets and triplets were sufficient to represent sequences of any size, it was suggested that there was no need to use the sequences themselves directly.

Comparison results

The relational data model can represent everything, including the associative model. The graph model is particularly good at representing relationships and not so good at representing sequences.

The associative model can easily represent an n-tuple of unlimited length using tuples with it is as good as graph theory in its ability to represent associations, and it is as powerful as the relational model and can fully represent any SQL table.

In a relational model, there is no need for more than one relationship to make it behave like an associative model. And for that matter, there is no need for more than 2-3 columns other than the explicit ID or inline ID of the row.

The graph model does not have the ability to directly create an edge between edges by definition. Therefore, the graph model needs to either change its definition or extend it with some additional way of storing sequences. It might actually be possible to store sequences as nested sets inside a graph model, but this method is not popular. The graph model is the closest model to doublets, but it is still different by definition.

Using an associative model means that you no longer have to choose between SQL and NoSQL databases, there is simply an associative data store that can represent everything in the simplest way possible. And the data is always in the form closest to the original.

Mathematical Introduction to Connection Theory

Introduction

And now that we have briefly introduced the reader to how it all began, it is time to dive even deeper into the theory.

Connection theory is being developed as a more fundamental theory compared to set theory and type theories and to replace relational algebra and graph theory. While in the Theory of Types the main concepts are “type” and “value”, and in the Theory of Sets – “set”, “meaning”, in the Theory of Connections everything comes down to a single concept of “connection”.

In this section we will examine the basic concepts and terms used in connection theory.

Then we move on to the definitions of connection theory within the framework of set theory, which we will reflect on type theory using the interactive software theorem prover “Coq”.

In conclusion, the results will be summarized and directions for further research and development of the theory of connections will be presented.

Connection theory

The entire theory of connections is based on a single concept of connection. The additional concept of reference to connection is required to be introduced only for theories that do not support recursive definition, such as set theory and type theory.

Connection

A connection has an asymmetrical recursive structure that can be expressed simply: a connection links connections. By asymmetry we mean that each connection has a direction from the source (beginning) to the receiver (end).

Definitions of Connection Theory within Set Theory

Link to vector – a unique identifier or serial number, each of which is associated with a specific vector representing a sequence of links to other vectors.
Many references to vectors: L ⊆ ℕ₀.

Link vector is a vector consisting of zero or more vector references, where the number of references corresponds to the number of vector elements.
The set of all link vectors of length n ∈ ℕ₀: Vn = Lⁿ.
A Cartesian power Lⁿ will always produce a vector of length n, since all its components will be of the same type L.
In other words, Lⁿ is the set of all possible n-element vectors, where each element of the vector belongs to the sequence L. This is essentially equivalent to an n-tuple.

Association is an ordered pair consisting of a reference to a vector and a vector of references.
This structure serves to map between links and vectors.
The set of all associations: A = L × Vn.

Function family: ∪_f {anetvⁿ | n ∈ ℕ₀} ⊆ A.
Here ∪ denotes the union of all functions in the family {anetvⁿ}, ⊆ denotes 'this is a subset', and A is the set of all associations.
This suggests that all ordered pairs of anetvⁿ functions, represented as a functional binary relation, are a subset of A.

Associative network of vectors of length n (or n-dimensional network) from the family of functions {anetvⁿ}, anetvⁿ : L → Vn maps a link R from a set L to a link vector of length n that belongs to the set Vn, effectively identifying points in an n-dimensional space.
The 'n' in anetvⁿ indicates that the function returns vectors containing n references.
Each n-dimensional association network thus represents a sequence of points in n-dimensional space.

Doublet of links (ordered pair or two-dimensional vector): D = L²
This is the set of all ordered pairs (L, L), or the second Cartesian power of L.

Associative network of doublets (or two-dimensional network): anetd : L → L².
Each associative network of doublets thus represents a sequence of points in two-dimensional space.

An empty vector is represented by an empty set: () represented as ∅.

Associative network of nested ordered pairs: anetl : L → NP, where NP = {(∅,∅) | (l,np), l ∈ L, np ∈ NP} is a set of nested ordered pairs, which consists of empty pairs and pairs containing one or more elements. Thus, lengths n ∈ ℕ₀ can be represented as nested ordered pairs.

Projection of the Theory of Connections into the Theory of Types (Coq) through the Theory of Sets

About Coq

Coq is an interactive proof generation tool that implements higher order type theory, also known as the Calculus of Inductive Constructions (CIC). This environment has the ability to formalize complex mathematical theorems, check proofs for correctness, and extract working program code from formally verified specifications. Coq is widely used in academia to formalize mathematics, as well as in the IT industry for software and hardware verification.

The decision to use Coq to describe the theory of connections within the framework of the theory of types was due to the need to strictly formalize the proofs and guarantee the correctness of logical constructions within the framework of developing the theory of connections. Using Coq allows you to express properties and operations on relationships in precise and reliable terms, thanks to the Coq type system and powerful tools for creating and checking proofs.

In anticipation of the extensive work to prove the equivalence of the relational model and the associative network of doublets, we present in this section the initial steps performed using the proof system of the Coq language. At the first stage, the task is to formalize the structures of associative networks through the definitions of basic types of functions and structures within Coq.

Definitions of associative networks

(* Последовательность ссылок на вектора: 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.

Lemmas of associative networks

(* Функция преобразования 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.

(* Определение 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.

(*  Доказательства *)

(* Лемма о сохранении длины векторов ассоциативной сети *)
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 id
                            end).
Proof.
  intros n net id.
  unfold ANetVfToANetLf.
  simpl.
  rewrite H_inverse.
  reflexivity.
Qed.


(*  Примеры *)

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.
Check nestedPair0.
Check nestedPair1.
Check nestedPair4.
Compute nestedPair0.
Compute nestedPair1.
Compute nestedPair4.

Compute (ANetVfToANetLf complexExampleNet) 0.
Compute (ANetVfToANetLf complexExampleNet) 1.
Compute (ANetVfToANetLf complexExampleNet) 2.
Compute (ANetVfToANetLf complexExampleNet) 3.
Compute (ANetVfToANetLf complexExampleNet) 4.
Compute (ANetVfToANetLf complexExampleNet) 5.

Definition testPairsNet : ANetLf :=
  fun _ => cons 1 (cons 2 (cons 0 nil)).

Definition testTuplesNet : ANetVf 3 :=
  ANetLfToANetVf testPairsNet.

Compute testTuplesNet 0.

(* Предикат эквивалентности для ассоциативных сетей дуплетов 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.

(* Функция преобразования 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.


(*  Доказательства *)

(* Лемма о сохранении длины списков 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.


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

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

  В формальном виде forall (np: NP), ANetDlToNP (NPToANetDl np) = np говорит о том,
 что для всякого список NP, мы можем преобразовать NP в ANetDl с помощью NPToANetDl,
 затем обратно преобразовать результат в NP с помощью ANetDlToNP,
 и в итоге получать тот же список NP, что и в начале.

  Это свойство очень важно, потому что оно гарантирует,
 что эти две функции образуют обратные друг к другу пары функций на преобразуемом круге списоке NP и ANetDl.
 Когда вы применяете обе функции к значениям в преобразуемом круге, вы в итоге получаете исходное значение.
 Это означает, что никакая информация не теряется при преобразованиях,
 так что вы можете свободно конвертировать списком NP и ANetDl,
 если это требуется в вашей реализации или доказательствах.
 
Theorem NP_ANetDl_NP_inverse: forall (np: NP),
  ANetDlToNP_ (NPToANetDl np) (length np) = np.
Proof.
  intros np.
  induction np as [| h t IH].
  - reflexivity.
  - simpl. 
    case_eq t; intros.  
    + reflexivity. 
    + simpl.
      rewrite NP_dim_preserved. 
      rewrite H in IH.
      reflexivity.
Qed.
*)

Notation "{ }" := (nil) (at level 0).
Notation "{ x , .. , y }" := (cons x .. (cons y nil) ..) (at level 0).

Examples of application of lemmas

(*  Примеры *)

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} *)


(*
  Теперь всё готово для преобразования асети вложенных упорядоченных пар 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.


(*  Примеры *)

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)} *)


Compute ANetDl_offsetNP test_anetd 0.
Compute ANetDl_offsetNP test_anetd 1.
Compute ANetDl_offsetNP test_anetd 2.
Compute ANetDl_offsetNP test_anetd 3.
Compute ANetDl_offsetNP test_anetd 4.
Compute ANetDl_offsetNP test_anetd 5.
Compute ANetDl_offsetNP test_anetd 6.
Compute ANetDl_offsetNP test_anetd 7.

Definition test_anetv : ANetVl 3 :=
  { [0; 0; 0], [1; 1; 2], [2; 4; 0], [3; 0; 5], [4; 1; 1], [0; 0; 0] }.

Compute ANetVlToANetDl test_anetv.

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)} *)

Compute ANetDlToANetLl test_anetd.

Definition test_anetdl : ANetDl := ANetVlToANetDl test_anetv.

Definition result_TuplesNet : ANetVl 3 :=
  ANetLlToANetVl (ANetDlToANetLl test_anetdl).

Compute result_TuplesNet.

Practical implementation

There are several practical implementations: Deep, LinksPlatform And Relationship Model.

Deep is a system based on connection theory. In connection theory, connections can be used to represent any data or knowledge, and also use them for programming. This is what Deep is focused on. Deep is all about connections. However, if we divide them into two categories, then we have the actual data and behavior. The behavior represented by the code in Deep is stored in an associative store in the form of connections, and for execution it is transferred to the docker of the corresponding programming language and executed in isolation and safely. All communication between different parts of the code is done through links in the store (database), which makes the database a universal data-driven API (as opposed to the traditional practice of calling functions and methods). At the moment, PostgreSQL is used as an associative storage in Deep, which will later be replaced by a data engine based on doublets and triplets from LinksPlatform.

Deep allows you to make all software on the planet compatible, representing all its parts in the form of connections. It is also possible to store any data and code together, to associate action events on different types of associations with the corresponding code that runs to handle those events. Each handler can retrieve the necessary relationships from the associative store and insert/update/delete relationships into it, which can trigger further cascading execution of handlers.

The links table in the (PostgreSQL) Deep database contains records that can be interpreted as links. They have columns such as id, type_id, from_id, and to_id. Association types help the association package designer to predefine the semantics of relationships between different elements. This guarantees an unambiguous understanding of the connections by both people and code in associative packages. In addition to the links table, the system also contains numbers, strings and objects tables for storing numeric, string and JSON values, respectively. Only one value can be associated with each relationship.

LinksPlatfrom is a cross-platform, multilingual framework that aims to implement a low-level implementation of associativity in the form of a database engine designer. For example, at the moment we have benchmarkwhich compares the implementation of doublets in PostgreSQL and a similar implementation in pure Rust/C++, the leading implementation in Rust outperforms PostgreSQL on write operations by 200+ times, and on read operations by 1000+ times.

Conclusion

Future plans

This article demonstrated only a small part of all the developments in the theory of connections that have accumulated over several years of work and research. In the following articles, other projections of communication theory will be gradually revealed, in terms of other theories, such as: relational algebra, graph theory, as well as consideration in terms of type theory without using set theory based on associative numbers (code name), and an analysis of the differences from Simon Williams' associative data model.
It is also planned to demonstrate a clear and general terminology of the theory of connections, its main postulates, aspects, and associative roots. Current progress in theory development can be seen in the deep-theory repository.

In order not to miss updates, we recommend subscribing to the Deep.Foundation blog here or now look at our work on GitHub or write to us directly at our Discord server (especially suitable if you are afraid that you will be downvoted in the comments).

We will be glad to receive any feedback from you, whether here on Habré or on GitHub and Discord.

PS The article will be updated as the Theory of Communication develops and expands over the next month.

Links

1. “Relational Model of Data for Large Shared Data Banks.”, paragraph 1.3., Edgar F. Codd, IBM Research Laboratory, San Jose, California, June 1970