Автоматное программирование это морфизм

1. Что такое "зависимая сумма" и "произведение" пространств

Произведение A × B — это множество пар (a, b), где a ∈ A, b ∈ B. Обе компоненты присутствуют одновременно.

Зависимая сумма (она же Σ-тип, tagged union, sum type) Σ_{i∈I} A_i — это множество пар (i, a), где i ∈ I — тег (вариант), а a ∈ A_i — значение, тип которого зависит от тега. В каждый момент активен ровно один вариант.

Разница принципиальна:

произведение — «и то, и другое»;
сумма — «или то, или другое, но мы знаем, что именно».

2. Пространство состояний автомата

Классический автомат Мили:

S — конечное множество состояний
X — входной алфавит
Y — выходной алфавит
δ: S × X → S   — функция переходов
λ: S × X → Y   — функция выходов

Ключевое: в каждый момент автомат находится ровно в одном состоянии. Множество S — это размеченное объединение (дискретная сумма) вариантов поведения. Каждое состояние s — это тег, за которым стоит своя логика.

3. Управляющее и вычислительное пространства

В автоматном программировании (Шалыто, Harel, statecharts) принято разделять:

Управляющее пространство C — состояния автомата (конечное, обозримое, верифицируемое). Это «скелет» логики.
Вычислительное пространство D — данные (переменные, память, контекст). Это «мясо».

Автомат с данными — это расширенный автомат (extended state machine): состояние = (c, d), где c ∈ C, d ∈ D(c).

4. Собственно гомоморфизм

Утверждение: пространство состояний автомата гомоморфно вложено в зависимую сумму (в вырожденном случае — произведение) управляющего и вычислительного пространств.

Формально:

S  ≅  Σ_{c ∈ C} D(c)

если D(c) = D для всех c (данные не зависят от управляющего состояния) — получаем произведение C × D;
в общем случае — зависимую сумму: для каждого управляющего состояния c свой тип данных D(c).

Гомоморфизм здесь означает: переходы автомата согласованы со структурой суммы. Переход s → s' — это отображение, которое:

1. меняет тег c → c' (управляющий переход),

2. преобразует данные d ∈ D(c) в d' ∈ D(c') (вычислительное действие).

То есть логика = (управление, вычисление), и это не произвольная пара, а именно расслоенное пространство: вычисление живёт «над» управлением.

5. Почему это полезно — что следует

5.1. Локальность и композициональность

Зависимая сумма даёт локализацию: код, работающий с D(c), не может случайно обратиться к данным другого состояния — типобезопасность гарантирует, что вы в правильном «слое». Это ровно то, что дают sum types в Rust (enum), Haskell (ADT), TypeScript (discriminated unions).

5.2. Исчерпывающая проверка (exhaustiveness)

Компилятор может проверить, что обработаны все состояния. Забыли вариант — ошибка компиляции. Это прямое следствие того, что S — сумма, а не произведение.

5.3. Тестируемость

Покрытие = покрытие переходов и состояний. Метрики автоматного тестирования (all-states, all-transitions, all-paths, pair-wise) становятся формально определёнными. Спека — это граф переходов, тест — обход графа.

5.4. Формальная верификация

Модель-чекинг (SPIN, NuSMV), LTL/CTL-спецификации работают именно с конечным управляющим пространством. Вычислительное пространство можно абстрагировать. Гомоморфизм гарантирует, что абстракция корректна.

5.5. Устойчивость к изменениям

Новое требование = новое состояние или новый переход. Локальное изменение в сумме не ломает произведение (в отличие от «спагетти» с флагами).

5.6. Документируемость

Диаграмма состояний — это буквально визуализация зависимой суммы. Код и документация совпадают.

6. Почему «почти везде»

Потому что любая система с режимами работы — это автомат:

парсеры (состояния лексера),
сетевые протоколы (TCP state machine),
UI (экраны, диалоги),
бизнес-процессы (заказы, документооборот),
встроенные системы (Шалыто — про них),
компиляторы, драйверы, игры.

Даже если явно не выделять состояния, они неявно есть — в виде булевых флагов, вложенных if, «режимных» переменных. Явное выделение = переход от произведения флагов (bool × bool × bool…) к сумме состояний. Это сжатие пространства состояний и устранение недопустимых комбинаций.

7. Связь с идеями Шалыто

Шалыто (совместно с Туккелем) формализовал это как «автоматное программирование»:

управляющий автомат — конечный, явный;
вычислительная часть — в «содержательных» операциях;
switch-технология: один switch по состоянию, внутри — вызовы действий.

Это ровно реализация зависимой суммы: switch (state) — это pattern matching по тегу, а тело case — работа с D(c).

8. Практический вывод

> Везде, где есть режимность, реализуйте логику как автомат.

Потому что:

1. Формализуется — граф переходов = спека.

2. Тестируется — покрытие графа = покрытие кода.

3. Верифицируется — model checking применим.

4. Типобезопасно — sum types ловят ошибки на компиляции.

5. Документируется — диаграмма = код.

6. Масштабируется — композиция автоматов (statecharts, иерархия, параллельность).

И всё это — прямое следствие того, что пространство состояний есть зависимая сумма управляющего и вычислительного пространств. Это не метафора, а структурный факт, из которого растут и типобезопасность, и тестируемость, и верифицируемость.

---

Если хочется глубже — смотрите:

Harel, Statecharts: A Visual Formalism for Complex Systems (1987) — иерархические автоматы;
Шалыто, Туккель, SWITCH-технология — автоматное программирование;
Pierce, Types and Programming Languages — зависимые суммы;
статья «Automata-based programming» в русской Википедии — обзор.

Программирование