Анализ конечных автоматов: от инвариантов до завершения алгоритмов 0:12
Конечные автоматы представляют собой мощный инструмент для анализа алгоритмов, позволяющий отслеживать изменение состояния системы во времени. Профессор Эрик Демейн в рамках курса MIT OpenCourseWare демонстрирует, как с помощью формальных методов математической индукции можно доказывать корректность и завершаемость программ, используя понятия инвариантов, предикатов и производных переменных.
⚙️ Основы теории конечных автоматов 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$. Ключевой задачей при анализе алгоритмов является определение того, будет ли выполнение конечным (завершится ли программа) и является ли результат корректным.
🧩 Анализ игры «Восьмерка» 8:59
Игра «Восьмерка» (3x3 поле с одной пустой клеткой) служит наглядным примером для доказательства недостижимости определенных состояний. Смысл игры заключается в перемещении плиток, чтобы достичь целевой конфигурации (упорядоченного состояния).
Для анализа Демейн вводит понятие инвертированной пары: это пара чисел $(i, j)$, где $i < j$, но при этом $j$ предшествует $i$ в «порядке чтения» поля.
- Предикат состояния $P(q)$ — это логическая функция, принимающая значение «истина» или «ложь» для состояния $q$.
- Предикат сохраняется (preserved), если переход из «истинного» состояния всегда ведет в «истинное».
- Предикат является инвариантом, если он верен для всех достижимых состояний.
Доказано, что если $P(q_0)$ истинно и предикат сохраняется, то $P$ является инвариантом (принцип инвариантности). Используя этот принцип, профессор доказывает, что в «Восьмерке» невозможно перейти из состояния с нечетным количеством инверсий в состояние с четным количеством (или нулевым, как в решенной головоломке).
🔄 Завершаемость алгоритмов: «простой сортировщик» 57:36
Для проверки того, не будет ли алгоритм работать вечно, используется понятие производной переменной (derived variable).
- Производная переменная $x(q)$ — это функция, отображающая состояния в натуральные числа.
- Переменная является строго убывающей, если каждый допустимый переход уменьшает ее значение.
- Теорема завершаемости: если существует строго убывающая производная переменная, ограниченная снизу натуральными числами, то автомат обязан достичь финишного состояния и остановиться.
При анализе алгоритма простой сортировки (который меняет соседние элементы, если они стоят в неправильном порядке) в качестве такой переменной выступает общее количество инвертированных пар. Каждая перестановка соседних элементов уменьшает количество таких пар ровно на единицу, гарантируя, что алгоритм достигнет отсортированного состояния за конечное время.
