Метатеория связей (МТС) исследует системы, в которых единственным первичным видом сущности является связь.
Главный постулат:
всё есть связь
МТС начинается не с программного типа и не с графической стрелки. Её исходная наглядность — остенсивная форма связи: сама запись показывает, какие полюса различены, а какие самозамкнуты.
Акорень обозначается знаком:
∞
и является полностью самозамкнутой связью:
∞ = ∞ ⟼ ∞
Акорень — различённая неподвижная точка, в которой смысл связывает смысл с самим смыслом. Отдельная сущность «смысл» для этого не требуется: смысл остаётся связью.
Из акорня видны четыре основные формы различённости бинарной связи:
∞ оба полюса самозамкнуты
♂e начало самозамкнуто, конец e различён
b♀ начало b различено, конец самозамкнут
b ⟼ e оба полюса различены
Структурно:
R = R ⟼ R # ∞
S = S ⟼ e # ♂e
E = b ⟼ E # b♀
X = b ⟼ e # b ⟼ e
Знаки ♂ и ♀ не являются командами взять начало или конец. Они остенсивно показывают самозамыкание соответствующего полюса:
♂e = S = S ⟼ e
b♀ = E = b ⟼ E
В конкретном акте интерпретации такая форма может участвовать в поиске, построении, проверке или разрешении недостающего полюса. Операция определяется актом и связями контекста, а не скрытым вторым значением знака.
Важно:
самозамкнутая форма ≠ автоматически акорень
самозамкнутая форма ≠ автоматически незавершённая связь
Текущий кандидат основания МТС использует пятисвязное корневое ядро:
R = ∞
R = R ⟼ R
O = O ⟼ R
C = R ⟼ C
L = O ⟼ C
U = C ⟼ O
Корневой словарь:
∞ → R
[ → O
] → C
1 → L
0 → U
Первые различения вокруг акорня можно видеть непосредственно:
[ → O = O ⟼ R ≡ ♂∞
] → C = R ⟼ C ≡ ∞♀
1 → L = O ⟼ C
0 → U = C ⟼ O
Поэтому [ ] 1 0 — корневые абиты ачисел. Знаки ♂ и ♀ относятся уже к формальной записи форм самозамыкания. Эти уровни нельзя отождествлять.
После остенсивного определения связь можно представить нейтральной машинной структурой:
Link(start, end)
Это представление для реализации, а не замена языка МТС.
В самой связи нет обязательных полей «контекст», «теория», «правило», «смысл» или «тип». Если роль существенна, она выражается другими связями сети.
Одинаковые полюса не означают тождество связей:
P1 = A ⟼ B
P2 = A ⟼ B
P1 ≠ P2
То же относится к самозамкнутым формам:
R = R ⟼ R
Q = Q ⟼ Q
R ≠ Q
Поэтому форма, положение в снимке памяти или физический адрес не заменяют тождество конкретного вхождения связи.
В эталонной реализации для этого используется OccurrenceRef; имя класса является технической деталью, а не понятием МТС.
Контекст не обязан существовать как скрытый стек среды исполнения:
P = parent ⟼ current
K = K ⟼ P
K — конкретное вхождение состояния контекста.
Запись
↑ = current(K)
означает получение текущей связи из явно указанного K, а не обращение к глобальной переменной.
Новое состояние создаётся новой связью; старое состояние не переписывается задним числом.
Одна и та же последовательность байтов может встретиться несколько раз и получить разные значения в разных словарях. Поэтому различаются:
содержимое исходной записи
конкретное вхождение исходной записи
выбранное разбиение
словарь D
форма F
допуск формы теорией T
Словарь также представляется сетью:
D = D ⟼ (parentScope ⟼ localHistory)
Определение добавляет новое состояние словаря явно и сохраняет предыдущее состояние.
Критическая граница апамяти:
читать / искать / разрешать / проверять
≠
создавать / удалять / изменять
Поиск отсутствующей связи не создаёт её.
Материализация одной и той же пары может создать два разных вхождения:
P1 = materialize(A,B)
P2 = materialize(A,B)
P1 ≠ P2
Индекс по паре полюсов служит поиску, но не определяет тождество связи.
Текущий кандидат локального равенства использует явного представителя в контексте:
Pair = member ⟼ representative
Binding = K ⟼ Pair
Два элемента равны в K, когда их явно выбранные одношаговые представители являются одним и тем же точным вхождением.
Из этого не следуют автоматически глобальная подстановка, транзитивное замыкание, сравнение по форме всей сети или переписывание всех связанных выражений.
Дополнительное правило вывода должно быть отдельно допущено теорией:
T ⟼ Rule
Поиск доказательства может быть сложным и эвристическим; доверенная часть только воспроизводит предъявленные точные связи и принимает либо отвергает результат.
Ачисла используют четыре корневых абита:
[ ] 1 0
Акорень ∞ не является абитом: последовательность начинается относительно него.
Общая лестница получается такой:
связь
→ акорень ∞
→ корневые различения [ ] 1 0
→ ачисла
→ строки
→ формальные знаки
→ словари и теории
→ интерпретация и вывод
При материализации последовательности:
∞ A B C
создаются новые точные вхождения:
A ⟼ B
B ⟼ C
Вложенная группа сначала строит внутреннюю связь и возвращает её как один элемент внешней последовательности.
Подробнее: Ачисла и сериализация.
Апамять — контроллер сети связей. Она должна сохранять:
- множественность одинаковых пар полюсов;
- циклы;
- совместно используемые связи;
- различие чтения и изменения;
- тождество вхождений между сохранениями состояния.
Физический адрес записи в конкретном хранилище не является смыслом связи.
Подробнее: Апамять и управление сетью связей.
Текущая понятийная поверхность:
- Основания МТС — акорень, остенсивность и тождество связей.
- Система аксиом МТС — текущие аксиоматические обязательства.
- Формальная нотация МТС — связь записи с разрешением смысла.
- Ачисла и сериализация — корневые абиты и структурное описание.
- Апамять и управление сетью связей — память, исполнение и проверка.
История принятых ранее версий и исследований сохраняется Git, задачами и запросами на слияние. main должен стремиться хранить текущее состояние МТС, а не журнал пути к нему.
остенсивная форма
→ точное вхождение связи
→ явный контекст и свидетельства
→ ассоциативный поиск
→ детерминированная проверка
→ явное изменение памяти
∞, ♂, ♀ и ⟼ — не украшение поверх машинной модели. Они делают фундаментальную структуру связи видимой в самой записи.