# Эрик Демейн о математике алгоритмов: «Инварианты гарантируют корректность»

Источник: https://www.youtube.com/watch?v=gVdrFsnOo_s
Канал: MIT OpenCourseWare
Опубликовано: 24.07.2025

---

## Анализ конечных автоматов: от инвариантов до завершения алгоритмов
[[JUMP:0:12]]

Конечные автоматы представляют собой мощный инструмент для анализа алгоритмов, позволяющий отслеживать изменение состояния системы во времени. Профессор Эрик Демейн в рамках курса MIT OpenCourseWare демонстрирует, как с помощью формальных методов математической индукции можно доказывать корректность и завершаемость программ, используя понятия инвариантов, предикатов и производных переменных.

### ⚙️ Основы теории конечных автоматов
[[JUMP:1:05]]

Конечный автомат состоит из набора возможных состояний $Q$, начального состояния $q_0$ и множества допустимых переходов $T$. Простейшим примером является счетчик, который начинает работу с 0 и последовательно переходит в 1, 2, 3 и так далее.

Исполнение автомата — это последовательность состояний $q_0, q_1, \dots, q_n$, где каждый переход $q_i \to q_{i+1}$ принадлежит множеству допустимых переходов. Состояние $r$ считается достижимым, если существует последовательность переходов, начинающаяся в $q_0$ и оканчивающаяся в $r$. Ключевой задачей при анализе алгоритмов является определение того, будет ли выполнение конечным (завершится ли программа) и является ли результат корректным.

### 🧩 Анализ игры «Восьмерка»
[[JUMP:8:59]]

Игра «Восьмерка» (3x3 поле с одной пустой клеткой) служит наглядным примером для доказательства недостижимости определенных состояний. Смысл игры заключается в перемещении плиток, чтобы достичь целевой конфигурации (упорядоченного состояния).

Для анализа Демейн вводит понятие **инвертированной пары**: это пара чисел $(i, j)$, где $i < j$, но при этом $j$ предшествует $i$ в «порядке чтения» поля. 

*   **Предикат состояния** $P(q)$ — это логическая функция, принимающая значение «истина» или «ложь» для состояния $q$.
*   Предикат **сохраняется** (preserved), если переход из «истинного» состояния всегда ведет в «истинное».
*   Предикат является **инвариантом**, если он верен для всех достижимых состояний.

Доказано, что если $P(q_0)$ истинно и предикат сохраняется, то $P$ является инвариантом (принцип инвариантности). Используя этот принцип, профессор доказывает, что в «Восьмерке» невозможно перейти из состояния с нечетным количеством инверсий в состояние с четным количеством (или нулевым, как в решенной головоломке).

### 🔄 Завершаемость алгоритмов: «простой сортировщик»
[[JUMP:57:36]]

Для проверки того, не будет ли алгоритм работать вечно, используется понятие **производной переменной** (derived variable).

1.  Производная переменная $x(q)$ — это функция, отображающая состояния в натуральные числа.
2.  Переменная является **строго убывающей**, если каждый допустимый переход уменьшает ее значение.
3.  **Теорема завершаемости**: если существует строго убывающая производная переменная, ограниченная снизу натуральными числами, то автомат обязан достичь финишного состояния и остановиться.

При анализе алгоритма простой сортировки (который меняет соседние элементы, если они стоят в неправильном порядке) в качестве такой переменной выступает общее количество инвертированных пар. Каждая перестановка соседних элементов уменьшает количество таких пар ровно на единицу, гарантируя, что алгоритм достигнет отсортированного состояния за конечное время.