The Links Theory 0.0.2

Note: The article was published at the 1st of April, but the translation is in the progress (some parts are still in Russian). I hope for your understanding. This note will be removed once it is ready. Save it to bookmarks to read later, please.

Last April 1st, as you might have guessed, we were joking. It’s time to fix that, and now everything is $100\%$ serious.

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

This article contains many letters, but it can be represented using just 4 symbols from set theory:

$L \to L^2$

Everything else follows from them.

Overview

This article is primarily aimed at programmers and mathematicians, yet we’ve designed it to be accessible to anyone interested in the ideas it presents. We believe that the concepts discussed here can serve as inspiration across a wide range of scientific disciplines.

Our goal was to create a self-contained text that guides you through each topic in a clear, logical order. Throughout the article, you’ll find links to Wikipedia for those who wish to explore specific terms or concepts in more depth — but these are entirely optional. The text is intended to be easily understood when read from start to finish.

Every symbol and formula is explained individually, with concise definitions provided where needed. We’ve also included images to help illustrate key ideas. If you come across anything that isn’t clear, please let us know so we can improve it.

Comparison of theories

To quickly dive in, we begin by comparing the mathematical foundations of the two most popular data models with that of the associative model of data.

In the course of our research, we discovered that traditional theories were sometimes overly complex or redundant, while at other times they imposed too many artificial constraints.

This overall lack of flexibility, adaptability, and universality motivated us to search for a simpler yet all-encompassing informational theory and a data storage model that future artificial intelligence could easily understand and effectively utilize. Along the way, we drew inspiration from the workings of our own associative memory and associative thought processes.

Relational Algebra

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

A relation is defined as a set of n-tuples:

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

Рис. 1. Таблица описывается отношением , которое представляется множеством строк , принадлежащих декартову произведению . — **Figure 1.** A table is described by a relation $\mathbf{R}$ , which is represented as a set of rows $\mathbf{r}$ , belonging to a Cartesian product $\mathbf{S_1 \times S_2 \times \dots \times S_n}$ .

Where:

The symbol $\mathbf{R}$ denotes a relation (table);
The symbol $\subseteq$ indicates that the left side of the expression is a subset of the right side;
The symbol $\times$ denotes the Cartesian product of sets;
The expression $\mathbf{S_n}$ represents the domain, i.e., the set of all possible values that each cell in a column can contain.

Rows, or elements of the relation $\mathbf{R}$ , are represented as n-tuples.

Data in the relational model is grouped into relations. By using n-tuples in this model, one can precisely represent any conceivable data structure. But are n-tuples really necessary? For example, every n-tuple can be represented as nested ordered pairs, which suggests that ordered pairs alone might be sufficient to represent any data. Moreover, it’s uncommon for column values in tables to be represented as n-tuples (although, for instance, a number can be decomposed into an n-tuple of bits). In some SQL databases, it is even forbidden to use more than $\mathbf{32}$ columns in a table (and, by extension, in its corresponding n-tuple). Thus, the actual value of $\mathbf{N}$ is usually lower than $\mathbf{32}$ . Therefore, in these cases, there are no true n-tuples — even in modern relational databases.

Рис. 2. Сравнение реляционной модели и ассоциативной модели данных (изначальная модель Саймона Вильямса была упрощена дважды). Иными словами для представления всех данных в реляционной модели требуется множество таблиц под каждый тип данных, в ассоциативной модели как оказалось было достаточно сначала двух таблиц, а потом и вовсе одной таблицы триплетов или дуплетов. — **Figure 2.** Comparison of the relational model and the associative model of data (the original model proposed by Simon Williams was simplified by us twice) [3]. In other words, representing all data in the relational model requires a multitude of tables — one for each data type — whereas in the associative model, it turned out that initially two tables were sufficient (`items` and `links`), and eventually just a single table (`links`) of triplets or doublets was enough.

Directed Graph

Directed graphs — and graphs in general — are based on the concepts of vertices and edges (2-tuples).

A directed graph $\mathbf{G}$ is defined as follows:

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

Where:

$\mathbf{V}$ — это множество, элементы которого называются вершинами, узлами или точками;
$\mathbf{V}$ is a set whose elements are called vertices, nodes, or points;
$\mathbf{E}$ — это множество упорядоченных пар (2-кортежей) вершин, называемых дугами, направленными ребрами (иногда просто ребрами), стрелками или направленными линиями.
$\mathbf{E}$ is a set of ordered pairs (2-tuples) of vertices, referred to as arcs, directed edges (sometimes simply edges), arrows, or directed lines segments.

In the directed graph model, data is represented by two separate sets: nodes and edges. This model can be used to represent almost all data structures, except perhaps sequences (n-tuples). Sometimes, chains of vertices are used to represent sequences. Although this method works, it invariably leads to data duplication, and deduplication in such cases is either complicated or unfeasible. Furthermore, sequences in graphs might be represented by decomposing the sequence into nested sets, but in our view, this is not a practical approach. It appears that we are not alone in this belief, which may explain why we have not encountered examples of others employing such methods.

Рис. 3. Сравнение теории графов и теории связей. Вершина эквивалентна замкнутой на себя связи, то есть связи которая в себе начинается и в себе заканчивается. Направленное ребро отображается в направленную связь-дуплет. А ненаправленное ребро отображается в пару направленных связей-дуплетов в обоих направлениях. То есть если в теории графов требуется два типа сущностей - вершины и рёбра, то в теории связей достаточно только связей (больше всего похожих на рёбра). — **Figure 3.** Comparison of the graph theory and the links theory. A vertex is equivalent to a self-referential link — a link that begins and ends on itself. A directed edge is represented as a directed doublet-links, while an undirected edge is represented as a pair of directed doublet-links in both directions. In other words, while graph theory requires two types of entities — vertices and edges — in the links theory only links (which most closely resemble edges) are necessary.

The links theory

The links theory is based on the concept of a link.

In the projection of the links theory into set theory, a link is defined as an n-tuple of references to links, which has its own reference that other links can use to refer to it.

It is worth noting that the separate notion of a reference is required here solely because circular definitions are not available in set theory. In fact, the links theory can describe itself without needing a distinct term for a reference — in other words, a reference is simply a special case of a link.

Duplets

A doublet-link is represented by a duplet (2-tuple or ordered pair) of references to links. A doublet-link also has its own reference.

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

Where:

is the set of references (from the English word “Links” as in “References”).

In this example, the set contains only references to links, namely and . In other words, in a network of links built on such a set of references, there can be only links.

To obtain all possible values of a link, the Cartesian product of with itself is used, i.e., $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)}$

Triplet-links can perform the same functions as doublet-links. Since triplet-links include an additional reference, that extra element can, for example, be used to indicate the type of link.

For instance, triplet-links can:

Link an object, its property, and its value;
Link two links together using a defined relation;
Describe a natural language sentence, for example, using a subject-verb-object model.

Vectors

A vector (i.e., a sequence) of link references — also known as an n-tuple — is the general case.

In general, a links network is defined as:

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

Where:

The $\mathbf{\lambda}$ symbol denotes the function that defines the links network;
The $\mathbf{L}$ symbol denotes the set of link references.

Example:

$1 \to (1)$

$2 \to (2, 2)$

$3 \to (3, 3, 3)$

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

In this example, n-tuples of variable lengths are used as link’s values.

Sequences (vectors) are, in essence, equivalent in expressive power to the relational model — a fact that remains to be proven within the developing theory. However, once we observed that doublet-links and triplet-links are sufficient for representing sequences of any size, we hypothesized that there is no need to use sequences directly as they representable by double-links.

Comparison summary

The relational data model can represent everything — even the associative model. In contrast, the graph model excels at representing relationships, but is less effective at representing unique deduplicated sequences.

The associative model can easily represent n-tuples of unlimited length using tuples with $\mathbf{n \geq 2}$ . It is as capable as graph theory in representing associations and as powerful as the relational model, being able to fully represent any SQL table. Additionally, the associative model can represent strict sequences, allowing any sequence to be encapsulated in a unique single link, which is beneficial for deduplication.

In the relational model, only one relation is needed to mimic the behavior of the associative model, and typically no more than 2–3 columns are required aside from an explicit ID or built-in row ID. The ID itself is required in relational model because it is built up on concept of set, for the contrast the links theory builds up on concept of sequence thus explicit ID is not required (and can optionally added if user really needs it).

By definition, the graph model cannot directly create an edge between edges. Thus, it would need either a redefinition or an extension with an unambiguous method for storing unique deduplicated sequences. While sequences might be stored as nested sets within the graph model, this approach is not popular. Although the graph model is closest to doublet-links, it still differs by definition.

Using the associative model means there is no longer a need to choose between SQL and NoSQL databases; instead, an associative data store can represent everything in the simplest possible way, with data always kept in its form closest to the original (usually this the normalized form, but denormalization also possible if needed).

Mathematical introduction to the links theory

Introduction

Now that we have briefly introduced the origins of our work, it is time to delve deeper into the theory.

The links theory is being developed as a more fundamental framework compared to set theory or type theory, and as a replacement for relational algebra and graph theory as unifying theory. While type theory is built upon the basic notions of “type” and “term”, and set theory on “set” and “element”, the links theory reduces everything to the single concept of a “link”.

In this section, we will explain the core concepts and terminology used in the links theory.

We will then present the definitions of the links theory within the framework of set theory, and subsequently project these definitions into type theory using the interactive theorem prover Coq.

Finally, we will summarize our findings and outline directions for further research and development of the links theory.

The links theory

At the heart of the links theory lies the unified concept of a link. The additional notion of a reference to a link is introduced only for theories that do not support circular definitions — such as set theory and type theory.

LinkA link possesses an asymmetrical recursive (fractal) structure, which can be simply expressed as: a link links links. The term “asymmetrical” refers to the fact that every link has a direction — from its source (beginning) to its destination (end).

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

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

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

$\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\} }$

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

Projection of the links theory into type theory (coq) via set theory

About Coq

Coq is an interactive theorem prover based on higher-order type theory, also known as the Calculus of Inductive Constructions (CIC). It is a powerful environment for formalizing complex mathematical theorems, checking proofs for correctness, and extracting executable code from formally verified specifications. Coq is widely used both in academia for the formalization of mathematics and in the IT industry for the verification of software and hardware.

The decision to use Coq to describe the links theory within type theory was driven by the need for rigorous formalization of proofs and assurance of logical correctness during the development of the links theory. Coq enables the precise expression of properties and operations on links through its robust type system and advanced proof mechanisms.

In anticipation of extensive work aimed at proving the equivalence of the relational model and the associative network of doublets, this section presents the initial steps undertaken using the Coq proof system. In the first phase, our goal is to formalize the structures of associative networks by defining the basic types, functions, and structures within Coq.

Definitions of associative networks

[Link to source code]

Require Import PeanoNat. Require Import Coq.Init.Nat. Require Import Vector. Require Import List. Require Import Coq.Init.Datatypes. Import ListNotations. Import VectorNotations.  (* Set of vector references: L ⊆ ℕ₀ *) Definition L := nat.  (* Default value for L: zero *) Definition LDefault : L := 0.  (* Set of vectors of references of length n ∈ ℕ₀: Vn ⊆ Lⁿ *) Definition Vn (n : nat) := t L n.  (* Default value for Vn *) Definition VnDefault (n : nat) : Vn n := Vector.const LDefault n.  (* Set of all associations: A = L × Vn *) Definition A (n : nat) := prod L (Vn n).  (* Associative network of vectors of length n (or n-dimensional associative network) from the family of functions {anetvⁿ : L → Vn} *) Definition ANetVf (n : nat) := L -> Vn n.  (* Associative network of vectors of length n (or n-dimensional associative network) as a sequence *) Definition ANetVl (n : nat) := list (Vn n).  (* Nested ordered pairs *) Definition NP := list L.  (* Associative network of nested ordered pairs: anetl : L → NP *) Definition ANetLf := L -> NP.  (* Associative network of nested ordered pairs as a sequence of nested ordered pairs *) Definition ANetLl := list NP.  (* Duplet of references *) Definition D := prod L L.  (* Default value for D: a pair of two LDefault values, used to denote an empty duplet *) Definition DDefault : D := (LDefault, LDefault).  (* Associative network of duplets (or two-dimensional associative network): anetd : L → L² *) Definition ANetDf := L -> D.  (* Associative network of duplets (or two-dimensional associative network) as a sequence of duplets *) Definition ANetDl := list D.

Functions for converting associative network

(* Function to convert Vn to 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.  (* Function to convert ANetVf to ANetLf *) Definition ANetVfToANetLf {n : nat} (a: ANetVf n) : ANetLf :=   fun id => VnToNP (a id).  (* Function to convert ANetVl to ANetLl *) Definition ANetVlToANetLl {n: nat} (net: ANetVl n) : ANetLl :=   map VnToNP net.  (* Function to convert NP to Vn, returning an option *) 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.  (* Function to convert NP to Vn using VnDefault *) Definition NPToVn (n: nat) (p: NP) : Vn n :=   match NPToVnOption n p with   | None => VnDefault n   | Some t => t   end.  (* Function to convert ANetLf to ANetVf *) Definition ANetLfToANetVf { n: nat } (net: ANetLf) : ANetVf n :=   fun id => match NPToVnOption n (net id) with             | Some t => t             | None => VnDefault n             end.  (* Function to convert ANetLl to ANetVl *) Definition ANetLlToANetVl {n: nat} (net : ANetLl) : ANetVl n :=   map (NPToVn n) net.  (* Function to convert NP to ANetDl with an index offset *) 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.  (* Function to convert NP to ANetDl *) Definition NPToANetDl (np: NP) : ANetDl := NPToANetDl_ 0 np.  (* Function to append NP to the tail of ANetDl *) Definition AddNPToANetDl (anet: ANetDl) (np: NP) : ANetDl :=   app anet (NPToANetDl_ (length anet) np).  (* Function that removes the head of anetd and returns the tail starting at 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.  (* Function to convert ANetDl to NP with indexing starting at the beginning of ANetDl from 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.  (* Function to read NP from ANetDl by the duplet index *) Definition ANetDl_readNP (anet: ANetDl) (index: nat) : NP :=   ANetDlToNP_ anet 0 index.  (* Function to convert ANetDl to NP starting from the head of the anet list *) Definition ANetDlToNP (anet: ANetDl) : NP := ANetDl_readNP anet 0.  (*   Now everything is ready for converting the associative network of nested ordered pairs anetl : L → NP   into the associative network of duplets anetd : L → L².      This conversion can be done in different ways: either preserving the original references to vectors   or with reindexing. Reindexing can be omitted if one writes an additional function for the duplet associative network   that returns the nested ordered pair by its reference. *)  (* Function to add ANetLl to ANetDl *) Fixpoint AddANetLlToANetDl (anetd: ANetDl) (anetl: ANetLl) : ANetDl :=   match anetl with   | nil => anetd   | cons h t => AddANetLlToANetDl (AddNPToANetDl anetd h) t   end.  (* Function to convert ANetLl to ANetDl *) Definition ANetLlToANetDl (anetl: ANetLl) : ANetDl :=   match anetl with   | nil => nil   | cons h t => AddANetLlToANetDl (NPToANetDl h) t   end.  (* Function to find NP in the tail of ANetDl starting at offset by its ordinal number.    Returns the NP offset. *) 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.  (* Function to find NP in ANetDl by its ordinal number.    Returns the NP offset. *) Definition ANetDl_offsetNP (anet: ANetDl) (index: nat) : nat :=   ANetDl_offsetNP_ anet 0 index.  (* Function to convert ANetVl to ANetDl *) Definition ANetVlToANetDl {n : nat} (anetv: ANetVl n) : ANetDl :=   ANetLlToANetDl (ANetVlToANetLl anetv).  (*   Now everything is ready for converting the duplet associative network anetd : L → L²   into the associative network of nested ordered pairs anetl : L → NP.      We will perform this conversion while preserving the original references to vectors.   Reindexing can be omitted because there is the function ANetDl_offsetNP for the duplet associative network   that returns the offset of the nested ordered pair by its reference. *)  (* Function that removes the first NP from ANetDl and returns the tail *) Fixpoint ANetDl_beheadNP (anet: ANetDl) (offset: nat) : ANetDl :=   match anet with   | nil => nil   | cons (_, next_index) tail_anet =>     if offset =? next_index then (* end of NP *)       tail_anet     else  (* NP not ended yet *)       ANetDl_beheadNP tail_anet (S offset)   end.  (* Function to convert NP and ANetDl with an offset into ANetLl *) Fixpoint ANetDlToANetLl_ (anetd: ANetDl) (np: NP) (offset: nat) : ANetLl :=   match anetd with   | nil => nil (* discard NP even if incomplete *)   | cons (x, next_index) tail_anet =>     if offset =? next_index then (* end of NP, move to the next NP *)       cons (app np (cons x nil)) (ANetDlToANetLl_ tail_anet nil (S offset))     else  (* NP not finished yet, continue parsing the duplet network *)       ANetDlToANetLl_ tail_anet (app np (cons x nil)) (S offset)   end.  (* Function to convert ANetDl to ANetLl *) Definition ANetDlToANetLl (anetd: ANetDl) : ANetLl :=   ANetDlToANetLl_ anetd nil LDefault.

Predicates of equivalence for associative networks

(* The definition ANetVf_equiv introduces a predicate for the equivalence of two associative networks of vectors of length n,    anet1 and anet2 of type ANetVf.     This predicate describes the property of "equivalence" for such networks.    It asserts that anet1 and anet2 are considered "equivalent" if, for every reference id, the vector associated with id in anet1    exactly matches the vector associated with the same id in anet2. *) Definition ANetVf_equiv {n: nat} (anet1: ANetVf n) (anet2: ANetVf n) : Prop :=   forall id, anet1 id = anet2 id.  (* The definition ANetVl_equiv_Vl introduces a predicate for the equivalence of two associative networks of vectors of length n,    anet1 and anet2 of type ANetVl. *) Definition ANetVl_equiv_Vl {n: nat} (anet1: ANetVl n) (anet2: ANetVl n) : Prop :=   anet1 = anet2.  (* Equivalence predicate for associative networks of duplets ANetDf *) Definition ANetDf_equiv (anet1: ANetDf) (anet2: ANetDf) : Prop := forall id, anet1 id = anet2 id.  (* Equivalence predicate for associative networks of duplets ANetDl *) Definition ANetDl_equiv (anet1: ANetDl) (anet2: ANetDl) : Prop := anet1 = anet2.

Lemmas of equivalence of associative networks

(* Lemma on preservation of vector length in the associative network *) 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.   (* Lemma on the mutual inversion of the functions NPToVnOption and VnToNP     H_inverse proves that every Vn vector can be converted losslessly to an NP    using VnToNP and then back to Vn using NPToVnOption.     Formally, forall n: nat, forall t: Vn n, NPToVnOption n (VnToNP t) = Some t states that    for every natural number n and each Vn vector of length n,    we can convert Vn to NP using VnToNP,    then convert the result back to Vn using NPToVnOption n,    and ultimately obtain the same Vn vector we started with.     This property is very important because it guarantees that these two functions    form an inverse pair on the set of convertible vectors Vn and NP.    When you apply both functions to values in this set, you end up with the original value.    This means that no information is lost during the transformations,    so you can freely convert between Vn and NP as required in implementations or proofs. *) 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.   (*    The Wrapping and Recovery Theorem for the Associative Network of Vectors:     Let an associative network of vectors of length n be given, denoted as anetvⁿ : L → Vⁿ.    Define an operation that maps this network to the associative network of nested ordered pairs anetl : L → NP,    where NP = {(∅,∅) | (l, np), l ∈ L, np ∈ NP}.    Then define the inverse mapping from the associative network of nested ordered pairs back to the associative network of vectors of length n.     The theorem states:     For any associative network of vectors of length n, anetvⁿ, applying the transformation to the associative network    of nested ordered pairs and then the inverse transformation back to the associative network of vectors of length n    recovers the original network anetvⁿ.    In other words:         ∀ anetvⁿ : L → Vⁿ, inverse(forward(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.   (* Lemma on preservation of the length of NP lists in the duplet associative network *) 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.

Examples of conversions between associative networks

(* Notation for list notation *) Notation "{ }" := (nil) (at level 0). Notation "{ x , .. , y }" := (cons x .. (cons y nil) ..) (at level 0).  (* Three-dimensional associative network *) 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.  (* Vectors of references *) Definition exampleTuple0 : Vn 0 := []. Definition exampleTuple1 : Vn 1 := [0]. Definition exampleTuple4 : Vn 4 := [3; 2; 1; 0].  (* Conversion of vectors of references into nested ordered pairs (lists) *) Definition nestedPair0 := VnToNP exampleTuple0. Definition nestedPair1 := VnToNP exampleTuple1. Definition nestedPair4 := VnToNP exampleTuple4.  Compute nestedPair0.  (* Expected result: { } *) Compute nestedPair1.  (* Expected result: {0} *) Compute nestedPair4.  (* Expected result: {3, 2, 1, 0} *)  (* Computing the values of the converted function of the three-dimensional associative network *) Compute (ANetVfToANetLf complexExampleNet) 0. (* Expected result: {0, 0, 0} *) Compute (ANetVfToANetLf complexExampleNet) 1. (* Expected result: {1, 1, 2} *) Compute (ANetVfToANetLf complexExampleNet) 2. (* Expected result: {2, 4, 0} *) Compute (ANetVfToANetLf complexExampleNet) 3. (* Expected result: {3, 0, 5} *) Compute (ANetVfToANetLf complexExampleNet) 4. (* Expected result: {4, 1, 1} *) Compute (ANetVfToANetLf complexExampleNet) 5. (* Expected result: {0, 0, 0} *)  (* Associative network of nested ordered pairs *) 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.  (* Converted associative network of nested ordered pairs into a three-dimensional associative network (dimensions must match) *) Definition testTuplesNet : ANetVf 3 :=   ANetLfToANetVf testPairsNet.  (* Computing the values of the converted function of the associative network of nested ordered pairs *) Compute testTuplesNet 0.   (* Expected result: [5; 0; 8] *) Compute testTuplesNet 1.   (* Expected result: [7; 1; 2] *) Compute testTuplesNet 2.   (* Expected result: [2; 4; 5] *) Compute testTuplesNet 3.   (* Expected result: [3; 1; 5] *) Compute testTuplesNet 4.   (* Expected result: [4; 2; 1] *) Compute testTuplesNet 5.   (* Expected result: [0; 0; 0] *)  (* Conversion of nested ordered pairs into the associative network of duplets *) Compute NPToANetDl { 121, 21, 1343 }. (* Should return: {(121, 1), (21, 2), (1343, 2)} *)  (* Adding nested ordered pairs to the associative network of duplets *) Compute AddNPToANetDl {(121, 1), (21, 2), (1343, 2)} {12, 23, 34}.  (* Expected result: {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} *)  (* Conversion of the associative network of duplets into nested ordered pairs *) Compute ANetDlToNP {(121, 1), (21, 2), (1343, 2)}.  (* Expected result: {121, 21, 1343} *)    Compute ANetDlToNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)}.  (* Expected result: {121, 21, 1343} *)  (* Reading nested ordered pairs from the associative network of duplets by the duplet index (start of the nested ordered pair) *) Compute ANetDl_readNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} 0. (* Expected result: {121, 21, 1343} *)  Compute ANetDl_readNP {(121, 1), (21, 2), (1343, 2), (12, 4), (23, 5), (34, 5)} 3. (* Expected result: {12, 23, 34} *)  (* Defining an associative network of nested ordered pairs *) Definition test_anetl := { {121, 21, 1343}, {12, 23}, {34}, {121, 21, 1343}, {12, 23}, {34} }.  (* Converted associative network of nested ordered pairs into the associative network of duplets *) Definition test_anetd := ANetLlToANetDl test_anetl.  (* Computing the converted associative network of nested ordered pairs into the associative network of duplets *) Compute test_anetd. (* Expected result:  {(121, 1), (21, 2), (1343, 2),   (12, 4), (23, 4),   (34, 5),   (121, 7), (21, 8), (1343, 8),   (12, 10), (23, 10),   (34, 11)} *)  (* Converting the associative network of nested ordered pairs into the associative network of duplets and back into test_anetl *)  Compute ANetDlToANetLl test_anetd. (* Expected result:   {{121, 21, 1343}, {12, 23}, {34}, {121, 21, 1343}, {12, 23}, {34}}  *)  (* Computing the offset of nested ordered pairs in the associative network of duplets by their ordinal number *) Compute ANetDl_offsetNP test_anetd 0.   (* Expected result: 0 *) Compute ANetDl_offsetNP test_anetd 1.   (* Expected result: 3 *) Compute ANetDl_offsetNP test_anetd 2.   (* Expected result: 5 *) Compute ANetDl_offsetNP test_anetd 3.   (* Expected result: 6 *) Compute ANetDl_offsetNP test_anetd 4.   (* Expected result: 9 *) Compute ANetDl_offsetNP test_anetd 5.   (* Expected result: 11 *) Compute ANetDl_offsetNP test_anetd 6.   (* Expected result: 12 *) Compute ANetDl_offsetNP test_anetd 7.   (* Expected result: 12 *)  (* Defining a three-dimensional associative network as a sequence of vectors of length 3 *) Definition test_anetv : ANetVl 3 :=   { [0; 0; 0], [1; 1; 2], [2; 4; 0], [3; 0; 5], [4; 1; 1], [0; 0; 0] }.  (* Converted three-dimensional associative network into the associative network of duplets via the associative network of nested ordered pairs *) Definition test_anetdl : ANetDl := ANetVlToANetDl test_anetv.  (* Computing the three-dimensional associative network converted into the associative network of duplets via the associative network of nested ordered pairs *) Compute test_anetdl. (* Expected result: { (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)}  *)  (* Converted three-dimensional associative network into the associative network of duplets via the associative network of nested ordered pairs and then back into a three-dimensional associative network *) Definition result_TuplesNet : ANetVl 3 :=   ANetLlToANetVl (ANetDlToANetLl test_anetdl).  (* Final check of the equivalence of associative networks *) Compute result_TuplesNet. (* Expected result:   { [0; 0; 0], [1; 1; 2], [2; 4; 0], [3; 0; 5], [4; 1; 1], [0; 0; 0] } *)

Practical implementation

There are several practical implementations: Deep, LinksPlatform and the model of relations.

Deep

Deep is a system based on the links theory. In links theory, links can be used to represent any data or knowledge, as well as to perform programming. Deep is built around this philosophy: in Deep, everything is a link. However, if we divide these links into two categories, we have data itself and behavior. Behavior — represented by code in Deep — is stored in the associative store as links, and for execution it is passed to a Docker container of the corresponding programming language, where it runs in isolation and safely. All communication between different parts of the code is carried out through links in the store (database), making the database a universal data-based API (in contrast to the traditional practice of calling functions and methods). At present, PostgreSQL is used as the associative store in Deep, which will later be replaced by a data engine based on doublets and triplets from LinksPlatform.

Deep makes all software on the planet interoperable by representing all its parts as links. It is also possible to store any data and code together, linking events or actions on various types of associations with the corresponding code that is executed to handle those events. Each handler can retrieve the necessary links from the associative store and insert/update/delete links in it, which may trigger further cascade execution of handlers.

The links table in Deep’s PostgreSQL database contains records that can be interpreted as links. They have columns such as id, type_id, from_id, and to_id. The links types help the developer of associative packages predefine the semantics of the relationships between various elements, ensuring an unambiguous understanding of links by both people and code in the associative packages. In addition to the links table, the system also includes tables named numbers, strings, and objects for storing numeric, string, and JSON values, respectively. Each link can be associated with only one value. This is temporary solution, that is used until Deep will not migrate to use of LinksPlatform as a database engine. Once migration is complete all these seemingly basic types will be built from the ground up using only links. It will allow to use deduplication (that arises as a consequence of the links theory) and deep understanding of values inner structure. Also it is planned to add indexing of such complex values represented by links, to improve performance to make it as fast or faster than current PostgreSQL implementation.

LinksPlatfrom

LinksPlatfrom is a cross-platform, multi-language framework aimed at providing a low-level implementation of associativity in the form of a database engine constructor. For example, at present we have a benchmark that compares the implementation of doublets in PostgreSQL with a similar implementation in pure Rust/C++; the leading implementation in Rust outperforms PostgreSQL by over 200 times in write operations and over 1000 times in read operations.

The model of relations

The model of relations is a meta-programming language based on representing a program as a three-dimensional associative network. The model of relations adheres to entity-oriented programming, where the entity is used as the single fundamental concept — that is, it assumes that everything is an entity and there is nothing besides entities.

In the model of relations, an entity, depending on its internal constitutive principle, can be either a structure (object) or a function (method). Unlike the well-known ER model, which uses two basic concepts — entity and relation — to represent the database schema, in the model of relations the entity and the relation are essentially the same. This representation allows one to describe not only the external relationships of an entity, but also its internal model — the model of relationships.

An entity, in its internal principle, is triune (threefold, consisting of three elements) because it is a synthesis of three aspects (qualities) of other entities (or of itself).

jsonRVM is a multithreaded virtual machine for executing the JSON projection of the model of relations. The model of relations, when represented as JSON, allows programs to be written directly in JSON. This representation is a hybrid of data and code segments and makes it easy to deserialize/execute/serialize the projection of the model of relations, as well as to use JSON editors for programming. In the execution process of the model of relations, the meta-program can not only process data but also generate multithreaded programs and meta-programs, and either execute them immediately or export them as JSON.

Conclusion

In this article, we examined the mathematical foundations of relational algebra and graph theory, and presented the definitions of the links theory in terms of set theory and its projection into type theory. We also defined a set of functions and lemmas necessary for proving the possibility of an equivalent conversion from any vector/sequence into nested doublet-links and back. This means that only one formula is sufficient to represent any possible type of information:

$L \to L^2$

Thus, this forms the basis for testing the hypothesis that any other data structure can be represented by doublet-links. In other words, doublet-links are sufficient to represent any tables, graphs, strings, arrays, lists, numbers, sound, images, videos, and much more.

We continue to make progress in synchronizing meaning between our three projects and among the people in our associative community. These projects are designed to bring associativity into the world and make it useful for humanity. This article is another iteration of our discussion, allowing us to agree on a unified meaning of words and terms within the general associative theory. We believe this theory can become a meta-language on which is already used by people and machines to communicate.

With each further refinement, we will be one step closer to speaking a common language and making this idea more understandable to everyone. This theory will also be useful for various optimizations in the associative implementations under development, and in the future, for the design of associative chips (or coprocessors) to accelerate operations on data represented as links.

Plans for the future

This article has demonstrated only a small part of all the developments in the links theory that have accumulated over several years of work and research. In subsequent articles, other projections of the links theory will gradually be revealed, in terms of other theories such as relational algebra, graph theory, and also in terms of type theory without using set theory directly, as well as an analysis of the differences from Simon Williams’ associative model of data [3].

We also plan to project the links theory to into itself, showing that it can be used as meta-theory. That will also open a door for projecting set theory and type theory into the links theory, meaning we now complete the cycle of definition (the links theory is defined in the set theory which itself can be defined in the links theory). We also be able to compare set theory, type theory, graph theory, relational algebra and links theory, that will help us to test the equivalence of these theory or at least get the precise bijective function to convert between them.

There are also plans to present a clear and unified terminology of the links theory, its basic postulates, aspects and so on. The current progress in developing the theory can be observed in the deep-theory repository.

To get updates, we recommend subscribing to the Deep.Foundation blog here or checking out our work on GitHub now, or directly contacting us at our Telegram public chat (especially if you’re afraid of getting downvoted in the comments).

We welcome any feedback you may have, whether on Habr, GitHub, or Telegram. You can also participate in the development of the theory or help accelerate its progress by engaging with us in any way.

P.S.

This and previous articles will be updated as the links theory develops and expands over the next 6 months.

P.S.S.

If you have become a fan of the links theory, we invite you to spread this formula as a meme-virus on social media.

Using Unicode symbols:

L ↦ L²

Using LaTeX:

L \to L^2

Which is rendered as SVG (clickable):

$L \to L^2$

References

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
Simon Williams, Great Britain (1988), The Associative Model Of Data

ссылка на оригинал статьи https://habr.com/ru/articles/895896/

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

Overview

Comparison of theories

Relational Algebra

Directed Graph

The links theory

Duplets

Триплеты

Vectors

Comparison summary

Mathematical introduction to the links theory

Introduction

The links theory

LinkA link possesses an asymmetrical recursive (fractal) structure, which can be simply expressed as: a link links links. The term “asymmetrical” refers to the fact that every link has a direction — from its source (beginning) to its destination (end).

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

Projection of the links theory into type theory (coq) via set theory

About Coq

Definitions of associative networks

Functions for converting associative network

Predicates of equivalence for associative networks

Lemmas of equivalence of associative networks

Examples of conversions between associative networks

Practical implementation

Deep

LinksPlatfrom

The model of relations

Conclusion

Plans for the future

P.S.

P.S.S.

References

Комментарии

Добавить комментарий Отменить ответ