diff --git "a/docs/theory/\320\220\320\275\320\260\320\273\320\270\320\267 \320\277\321\200\320\270\321\200\320\276\320\264\321\213 \321\201\320\272\320\276\320\261\320\276\320\272 \320\262 \320\234\320\242\320\241.md" "b/docs/theory/\320\220\320\275\320\260\320\273\320\270\320\267 \320\277\321\200\320\270\321\200\320\276\320\264\321\213 \321\201\320\272\320\276\320\261\320\276\320\272 \320\262 \320\234\320\242\320\241.md" new file mode 100644 index 0000000..34deb23 --- /dev/null +++ "b/docs/theory/\320\220\320\275\320\260\320\273\320\270\320\267 \320\277\321\200\320\270\321\200\320\276\320\264\321\213 \321\201\320\272\320\276\320\261\320\276\320\272 \320\262 \320\234\320\242\320\241.md" @@ -0,0 +1,288 @@ +# Анализ природы скобок в МТС + +## Постановка вопроса + +В системе аксиом МТС квадратные скобки `[...]` используются в нескольких аксиомах (А5, А6, А8–А13), но не имеют собственного аксиоматического определения. Данный анализ исследует глубинную природу скобок в МТС: что они делают, какова их роль, и как они соотносятся с минимальным ядром системы. + +## 1. Текущее использование скобок в МТС + +### 1.1 Квадратные скобки `[...]` в аксиомах + +| Аксиома | Формула | Роль `[...]` | +|---------|---------|-------------| +| А5 | `∞♀ : [⟼]♀` | Связь взята целиком — применяется оператор начала | +| А6 | `♂∞ : ♂[⟼]` | Связь взята целиком — применяется оператор конца | +| А8 | `1 : [⟼]` | Связь как объект домена сериализации (абит 1) | +| А9 | `↛ : ¬[⟼]` | Инверсия связи, взятой целиком | +| А10 | `0 : [↛]` | Несвязь как объект домена сериализации (абит 0) | +| А11 | `[⟼]♀ : [⟼] ⟼ [⟼]♀` | Начало связи как объекта | +| А12 | `♂[⟼] : ♂[⟼] ⟼ [⟼]` | Конец связи как объекта | +| А13 | `¬[⟼] : ♂[⟼] ⟼ [⟼]♀` | Инверсия связи через начало и конец | +| А15 | `[ : ∞♀`, `] : ♂∞` | Абиты начала и конца смысла | + +### 1.2 Круглые скобки `(...)` в нотации + +Круглые скобки используются для группировки, переопределяя левоассоциативный порядок: +- `a(bc) = a ⟼ (b ⟼ c)` — переопределение порядка связывания +- `(a ⟼ b) ⟼ c` — явная группировка по умолчанию (левоассоциативность) + +### 1.3 Фигурные скобки `{...}` в нотации + +Фигурные скобки обозначают множество (пакет) выражений: +- `{A, B} = {B, A}` — неупорядоченный контейнер + +### 1.4 Три типа скобок — три уровня конструирования + +| Тип скобок | Функция | Уровень | +|------------|---------|---------| +| Круглые `(...)` | Группировка: приоритет операций | Одна связь, порядок конструирования | +| Квадратные `[...]` | Создание объекта: связь берётся целиком | Одна связь как целое | +| Фигурные `{...}` | Множество: набор связей | Множество связей | + +## 2. Что делают скобки? + +### 2.1 Группировка и приоритет операций + +Скобки задают **группировку и приоритет операций** — они указывают интерпретатору, в каком порядке конструировать связи из последовательности символов. + +Рассмотрим две формулы: +``` +(a ⟼ b) ⟼ c и a ⟼ (b ⟼ c) +``` + +Без скобок по А16 (левоассоциативность): `abc = (a ⟼ b) ⟼ c`. Скобки переопределяют этот порядок. + +### 2.2 Создание объекта из частей + +Скобки **создают конструкцию, на которую можно ссылаться как на целое или манипулировать как целым**. + +Пример с универсальным конструктором (А3: `rv : r ⟼ v`): + +``` +be = b ⟼ e — связь от b к e + +(b⟼)e = (b ⟼ ?) ⟼ e — связь от b с опущенным концом берётся + как целое, и от неё ведётся связь к e + +b(⟼e) = b ⟼ (? ⟼ e) — связь к e с опущенным началом берётся + как целое, и от b ведётся связь к ней + +b(⟼)e = b ⟼ (⟼) ⟼ e — связь (⟼) берётся целиком как объект, + создаётся последовательность связей +``` + +Ключевое наблюдение: **скобки берут смысл символа как связь в натуре** — берут связь целиком, позволяя манипулировать ею как объектом. + +### 2.3 Скобки как синтаксический сахар + +В обсуждении (Alex Bur) отмечено, что скобки — это **синтаксический сахар**. Минимальное ядро системы не обязано работать со скобками — их можно добавить позже, подобно тому, как макросы добавляются поверх ассемблера. + +Это важное наблюдение: скобки не являются фундаментальными операторами системы. Они — инструмент нотации, который упрощает запись и чтение формул, но всё, что выражается скобками, в принципе может быть выражено без них (через явное именование промежуточных конструкций). + +### 2.4 Квадратные скобки в ачислах + +При этом квадратные скобки в ачислах — это не просто синтаксический сахар. По А15 (`[ : ∞♀`, `] : ♂∞`) они являются **абитами** — элементами домена сериализации. В формулах аксиом квадратные скобки читаются посимвольно, и их смысл совпадает с их значением: + +- А5: `∞♀ : [⟼]♀` — посимвольное прочтение: начало смысла определяется началом связи +- А6: `♂∞ : ♂[⟼]` — посимвольное прочтение: конец смысла определяется концом связи + +Это глубинное совпадение — формулы МТС являются одновременно и математическими выражениями, и посимвольными описаниями смысла. + +## 3. Двойственная природа `[⟼]` + +### 3.1 `[⟼]` как формула и как ачисло + +Запись `[⟼]` обладает двойственной природой: + +1. **Как формула** (в домене форм связей): `[⟼]` — это связь `⟼`, взятая как целое. По А7: `⟼ : ∞♀ ⟼ ♂∞`, поэтому `[⟼] = ∞♀ ⟼ ♂∞`. + +2. **Как ачисло** (в домене сериализации): `[⟼]` — это последовательность абитов `[`, `⟼`, `]`. По А15: `[ = ∞♀`, `] = ♂∞`. Связь `⟼` между ними — единица смысла. Получаем ачисло: `∞♀ ⟼ ♂∞ = 1`. + +Таким образом, `[⟼]` = `1` — **совпадение формулы и ачисла не случайно**. Это проявление глубинной связи между доменом форм и доменом сериализации. Формальная нотация МТС и ачисла пересекаются более плотно, чем кажется на первый взгляд. + +### 3.2 Природа `[]` — ссылка на акорень + +По А15: `[ = ∞♀`, `] = ♂∞`. Если читать `[]` как последовательность абитов: +``` +[] = ∞♀ ⟼ ♂∞ = 1 +``` + +Но в контексте ачисел `[]` имеет другой, более глубокий смысл. Как отмечает @netkeep80: + +> `[]` в ачисле неявно порождают ссылку на акорень, а акорень — это целый смысл. Т.е. получается, что `[]` — это **любая связь, но обязательно конкретно одна** в натуре любая. + +Таким образом, `[]` в ачисле — это не «пустой объект», а **ссылка на акорень `∞`** (недифференцированный смысл). Поскольку акорень `∞` — это полностью самозамкнутая связь (А4: `∞ : ∞ ⟼ ∞`), ссылка на него означает **любую конкретную связь** — одну, но произвольную. + +Это согласуется с двойственностью: как абитовая последовательность `[]` даёт `1` (одну связь), а как конструкция в ачисле — ссылку на акорень, т.е. одну произвольную связь в натуре. + +## 4. Иерархия скобок и уровни конструирования + +### 4.1 `[]` — ровно одна связь + +Квадратные скобки обозначают **ровно одну связь**, взятую как объект: +``` +[⟼] = связь, взятая целиком = абит 1 +[↛] = несвязь, взятая целиком = абит 0 +[] = ссылка на акорень = любая конкретно одна связь +``` + +Ключевое свойство `[]`: это **обязательно одна** связь. `[]` порождает ссылку на акорень `∞`, а акорень — это целый смысл. Поэтому `[]` — это любая связь, но именно одна конкретная. + +### 4.2 `{}` — множество связей (включая пустое) + +Фигурные скобки обозначают **множество связей**, причём это может быть и **ни одной** связи: +``` +{A, B} = неупорядоченный набор связей A и B +{A} = одна связь (частный случай) +{} = пустое множество связей (ни одной) +``` + +Принципиальное отличие от `[]`: фигурные скобки допускают **ноль или более** связей, тогда как квадратные — всегда **ровно одну**. + +### 4.3 Сравнение `[]` и `{}` + +| Свойство | `[]` | `{}` | +|----------|------|------| +| Количество связей | Ровно одна | Ноль или более | +| Пустой случай | `[]` = ссылка на акорень (одна произвольная связь) | `{}` = пустое множество (ни одной связи) | +| Тип | Конкретная одна связь как целое | Множество (набор) связей | +| Аналогия | Переменная (один объект) | Коллекция (множество объектов) | + +Это согласуется с общей идеей МТС: скобки — инструменты конструирования, позволяющие собирать части в целое на разных уровнях. + +## 5. Связь с процессом конструирования + +### 5.1 Конструирование связи из последовательности символов + +Когда мы читаем последовательность символов, мы конструируем связи. Квадратные скобки обозначают границы конструирования: + +- `[` — **начало конструирования**: начало сборки новой связи. По А15: `[ = ∞♀` — начало смысла. +- `]` — **завершение конструирования**: связь собрана, можно использовать как целое. По А15: `] = ♂∞` — конец смысла. + +### 5.2 Аксиомы А8 и А10 как примеры конструирования + +- А8: `1 : [⟼]` — конструирование связи как объекта даёт абит `1` +- А10: `0 : [↛]` — конструирование несвязи как объекта даёт абит `0` + +Квадратные скобки здесь обозначают процесс «упаковки» формы связи в объект домена сериализации. + +## 6. Три аспекта определения каждого символа + +Каждый знак формальной нотации МТС — это аксиома. Поэтому каждый знак (включая скобки) должен быть определён явно в трёх аспектах: + +1. **Остенсивно** (графически) — стрелками или метками с верёвками +2. **Формально** — формула МТС +3. **Содержательно** — текст на естественном языке + +Скобки определяют процедуру для интерпретатора: +- Создание объекта из нескольких частей +- Возможность присвоить ему имя, чтобы манипулировать им (вычислять, копировать и т.п.) + +Эту процедуру можно описать двумя способами: +- **Декларативно** — на языке логики первого порядка в виде аксиом, задающих свойства (через инварианты) +- **Операционно** (остенсивно) — как преобразование строки: «строка со скобками на входе ⇒ строка на выходе» + +## 7. Шаблоны, конкретные связи и два режима конструирования + +### 7.1 Ачисла — конструкторы конкретных связей + +Ачисла всегда конструируют **конкретные связи**. Каждый элемент ачисла — метка-константа, и результат — конкретная структура-константа (где сами метки не важны, важна структура). + +Особый случай: в ачислах `[]` неявно порождает **ссылку на акорень** `∞`. Акорень — это целый смысл, поэтому `[]` обозначает любую конкретно одну связь. Это — **дырка для шаблона**, место, куда может быть подставлена любая конкретная связь. + +### 7.2 Формальная нотация — шаблоны связей + +Формальная нотация МТС описывает **шаблоны связей** (шаблоны смыслов, шаблонные смыслы). Формулы аксиом — это не конкретные связи, а **виды форм связей**, т.е. паттерны, под которые подпадает множество связей. + +Задавая связь в общей форме как тройку меток `(м1 м2 м3)`, мы: +- Определяем **шаблон** (синтаксис, обозначение, которое умеет дешифровывать интерпретатор) +- Определяем **очень общий смысл** + +Где `*` — абстрактная метка, не обязательно совпадающая с другой `*`. + +### 7.3 Два режима конструирования + +Из различия между ачислами и формальной нотацией вытекают два режима конструирования: + +1. **Конкретный конструктор** — конструирование одной конкретной связи (ачисла) +2. **Конструктор шаблона** — конструирование шаблона связи, в котором начало и конец рекурсивно задаются шаблонами начала и конца (формальная нотация) + +В формальной нотации необходимо различать, когда мы указываем **конкретную связь в натуре**, а когда мы **используем связь для передачи её смысла** (как шаблон). + +### 7.4 Константы и переменные + +Различие конкретных связей и шаблонов сводится к различию: +- **Метки-константы** — конкретные, фиксированные (как в ачислах) +- **Метки-переменные** — абстрактные, подставляемые (как в шаблонах формальной нотации) + +### 7.5 Частичное задание смысла + +Смысл связи определяется смыслом её начала и конца. Мы можем **частично наделить связь смыслом**, задав только часть формы: + +- Шаблон с самозамкнутым началом и неуточнённым концом +- Шаблон с неуточнённым началом и самозамкнутым концом +- И другие комбинации + +Это позволяет создавать **шаблонный смысл** — частично определённый, покрывающий множество конкретных связей. + +### 7.6 Именование — не только декларация + +Именование связи (через аксиому определения) — это не только сокращение длинной строки (синоним, макрос). Именование может быть дополнено **преобразованиями** — подобно тому, как класс объединяет данные (запись) и функции/процедуры работы с записью. + +Смысл именованной связи однозначно определяется её полной записью — полным отношением к акорню. + +## 8. Сравнение текущей и предложенной системы аксиом + +### 8.1 Структура предложенной системы (из issue #42) + +Предложенная в issue #42 формулировка сохраняет все формулы аксиом А4–А13, но: + +1. **Переставляет приоритет**: начинает с аксиомы смысла (А4) как первой и фундаментальной +2. **Фокусирует** на ядре (А4–А13), подчёркивая его самозамкнутость +3. **Добавляет**: теорему конца начала `♂♀ = ∞` как завершение ядра системы +4. **Указывает**: «Осталось аксиомы для абитов `[]` скобок добавить...» — система не завершена + +### 8.2 Принцип самозамкнутой системы + +В текущей документации принцип самозамкнутой системы уже присутствует (в `Шаблон аксиом МТС.md` и в `Метатеория связей.md`). Issue #42 подчёркивает этот принцип как центральный: + +> Система аксиом МТС это самозамкнутая система, в которой каждая аксиома вводит одно понятие — один символ, и определяет для него формулу, т.е. форму связи. При этом формула аксиомы может рекурсивно использовать и себя и другие аксиомы, это похоже на систему логических уравнений, которая решается только вместе. + +## 9. Открытые вопросы + +1. **Скобки как сахар vs. скобки как абиты.** Если скобки — синтаксический сахар (группировка, приоритет), то они вне минимального ядра. Но аксиома А15 определяет `[` и `]` как абиты — элементы самого языка. Как совместить эти два взгляда? + +2. **Нужны ли отдельные аксиомы для скобок?** Issue #42 заканчивается словами: «Осталось аксиомы для абитов `[]` скобок добавить...». Вопрос: определить скобки через существующие аксиомы (А15 уже достаточно?) или ввести новые? + +3. **Фигурные скобки.** В текущей системе `{}` используются в формальной нотации (А1, А2). Если `[]` = одна связь, а `{}` = множество связей, это можно формализовать аксиоматически. + +4. **Посимвольное чтение формул.** Формулы МТС в аксиомах А5, А6 читаются посимвольно и при этом передают свой смысл. Это глубинное свойство нотации. Как формализовать это наблюдение? + +5. **Как формализовать частичное конструирование?** Примеры из обсуждения: + - `(b⟼)e` — связь от b с опущенным концом, взятая как целое + - `b(⟼e)` — связь к e с опущенным началом, взятая как целое + - `b(⟼)e` — связь как объект между b и e + +6. **Как формализовать два режима конструирования?** Конкретный конструктор (ачисла) vs. конструктор шаблона (формальная нотация) — как это различие отразить в системе аксиом? Нужны ли разные нотационные средства для конкретных связей и шаблонов? + +7. **`[]` как дырка для шаблона.** В ачислах `[]` неявно обозначает акорень — место подстановки. Как формализовать этот механизм? Является ли это первым шагом к полноценной системе шаблонов? + +8. **Три аспекта определения скобок.** Для полного определения скобок в МТС необходимо дать их описание остенсивно, формально и содержательно. Какой должна быть остенсивная (графическая) интерпретация скобок? + +## 10. Выводы + +1. **Скобки — это группировка, приоритет и создание объектов из частей.** Они позволяют создавать конструкции, которыми можно манипулировать как целым. Скобки — **не** «операторы контекста». + +2. **Квадратные скобки — синтаксический сахар** для минимального ядра, но одновременно абиты (А15) для домена сериализации. Эта двойственность требует осмысления. + +3. **Двойственность `[⟼]`** (одновременно формула и ачисло `1`) указывает на глубинную связь между доменом форм и доменом сериализации, которая пока не полностью формализована. + +4. **Иерархия скобок**: `[]` — ровно одна связь (ссылка на акорень), `{}` — множество связей (включая пустое). `[]` — обязательно одна конкретная связь, `{}` — ноль или более. Эта иерархия может быть формализована аксиоматически. + +5. **Формальная нотация МТС и ачисла пересекаются плотнее**, чем описано в текущей документации. Возможна такая формульная нотация, которая описывает смысл с максимальной глубиной и точностью. + +6. **Ачисла — конкретные связи, формальная нотация — шаблоны связей.** Это фундаментальное различие двух режимов конструирования, которое должно быть отражено в системе аксиом. + +7. **Частичное задание смысла** позволяет создавать шаблонные смыслы — виды форм связей, покрывающие множество конкретных связей. Это путь к формализации шаблонов и контекстов в МТС. + +8. **Вопрос остаётся открытым**: какую именно форму должны принять аксиомы для скобок, и нужны ли они вообще для минимального ядра.