Теория автоматов состояний: от головоломки «Пятнашки» до верификации алгоритмов

В рамках лекционного курса Корпорации MIT «Математика для компьютерных наук» профессор Эрик Демейн подробно разбирает концепцию автоматов состояний — мощного математического инструмента для моделирования и анализа последовательных процессов во времени. На примере классических головоломок и базовых алгоритмов сортировки демонстрируются методы доказательства корректности и завершаемости программ. Особое внимание уделяется принципу инвариантности и использованию производных переменных для анализа поведения сложных дискретных систем.

🛠️ Что такое автомат состояний 0:12

Автоматы состояний представляют собой абстрактные модели, позволяющие отслеживать и анализировать изменение системы в процессе выполнения последовательных шагов. В контексте компьютерных наук этот инструмент незаменим для верификации алгоритмов, поскольку оперативная память компьютера постоянно меняет свое состояние, и разработчикам необходимо строго доказывать, что программа ведет себя предсказуемо. Центральное место в этой теории занимает понятие инварианта — свойства, которое остается неизменным на протяжении всей работы системы и позволяет математически обосновать ее корректность.

Формально любой автомат состояний состоит из трех ключевых элементов:

Множество состояний ($Q$), которое представляет собой произвольный набор, инкапсулирующий абсолютно всю информацию внутри машины в любой момент времени.
Начальное состояние ($q_0$), являющееся обязательным элементом множества $Q$.
Набор допустимых переходов ($T$), где каждый переход записывается в виде стрелки $q \to r$, указывающей на возможность трансформации одного состояния в другое.

Простейшим примером такой системы является бесконечный счетчик. Визуально его начальное состояние обозначается стрелкой, ведущей «из ниоткуда» в круг с цифрой 0. Множество состояний этого счетчика включает в себя все натуральные числа, а переходы строго регламентированы: из состояния $i$ можно перейти только в состояние $i + 1$. Описать такое множество переходов можно с помощью стандартной нотации задания множества условием, где слева указывается формат элемента, а справа — его критерий. В более сложных автоматах переходы могут образовывать циклы, возвращаться назад или разветвляться, предоставляя системе выбор из нескольких альтернативных путей.

🔄 Исполнение алгоритма и концепция достижимости 4:50

Процесс функционирования автомата описывается через понятие исполнения (execution), которое представляет собой последовательность состояний, связанных валидными переходами. Исполнение всегда берет свое начало в стартовой точке $q_0$, после чего совершаются шаги $q_0 \to q_1 \to q_2$ и так далее. Важнейшим правилом является то, что каждый шаг между соседними элементами последовательности обязан содержаться в предопределенном множестве переходов $T$.

Профессор Демейн классифицирует исполнения на два типа:

Конечные исполнения, которые останавливаются на некотором финальном состоянии $q_n$.
Бесконечные исполнения, продолжающиеся непрерывно и уходящие в бесконечность.

При проектировании программного обеспечения разработчики, как правило, стремятся избегать бесконечных циклов, поэтому умение различать и доказывать конечность исполнения является одной из фундаментальных задач анализа алгоритмов. С этим тесно связано понятие достижимости состояний. Состояние $r$ называется достижимым, если существует хотя бы одно валидное исполнение, которое начинается в $q_0$ и завершается в $r$. Если же в графе автоматов существует изолированное состояние (которое лектор в шутку называет «плохим»), не имеющее входящих стрелок, попасть в него невозможно. В реальном анализе математики фокусируются исключительно на достижимых состояниях, отсекая заведомо невозможные конфигурации системы.

🧩 Головоломка «Пятнашки» и границы возможного 8:40

Для демонстрации прикладного значения теории достижимости Эрик Демейн привлекает знаменитую игру «Пятнашки» в уменьшенном формате 3 на 3, содержащую 8 пронумерованных фишек и одну пустую ячейку. Целевым (или решенным) состоянием в этой игре признается расположение фишек в порядке чтения — слева направо и сверху вниз, где пустая ячейка, обозначаемая как $x$, находится в самом конце. Задача математического анализа состоит не только в поиске алгоритма решения, но и в определении того, разрешима ли конкретная начальная конфигурация в принципе.

Профессор демонстрирует два примера стартовых позиций:

Первая конфигурация (фишки расположены в порядке 1, 3, 4, 2, 5, 7, 8, 6) является полностью разрешимой, и прийти к победе можно довольно быстро, последовательно перемещая фишки в пустую ячейку.
Вторая конфигурация отличается от целевой лишь тем, что фишки 5 и 6 поменялись местами (1, 2, 3, 4, 6, 5, 7, 8). По утверждению лектора, такая задача абсолютно неразрешима, поскольку изолированно поменять местами две фишки, не нарушив общий порядок, физически невозможно по правилам игры.

Чтобы строго доказать это заявление, игра формализуется как автомат состояний. Множество состояний $Q$ включает в себя абсолютно все возможные комбинации размещения восьми фишек и пустой ячейки на поле 3 на 3. Общее число таких комбинаций составляет девять факториал, однако точная цифра на текущем этапе не имеет значения. Переходом $q \to r$ считается перемещение, при котором пустая ячейка меняется местами с одним из своих непосредственных соседей. Таким образом, из любого состояния доступно не более четырех вариантов хода, а если пустая ячейка находится на границе поля, то легальных ходов становится еще меньше.

📜 Принцип инвариантности как расширение индукции 14:45

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

Теория выделяет два важнейших типа предикатов:

Сохраняющийся предикат (preserved), для которого истинность условия в состоянии $q$ гарантирует его истинность в последующем состоянии $r$ при любом легальном переходе.
Инвариантный предикат (invariant), который остается истинным для абсолютно всех достижимых состояний автомата.

Отсюда вытекает фундаментальное правило: если предикат $P(q)$ является инвариантом (то есть он истинен во всех достижимых точках), но для некоторого конкретного состояния $r$ этот предикат ложен, то состояние $r$ гарантированно недостижимо. Это позволяет опровергать разрешимость задач без необходимости перебирать миллионы вариантов.

Для связи сохраняемости и инвариантности используется «принцип инвариантности». Он гласит: если предикат истинен в начальном состоянии $q_0$ и при этом обладает свойством сохраняемости, то он является инвариантом для всей системы. По сути, данный принцип представляет собой обобщение классической математической индукции. Если применить принцип инвариантности к простейшему автомату-счетчику, где состояния — это натуральные числа, а переходы — прибавление единицы, мы получим чистую аксиому индукции, где проверка начального состояния заменяет базу индукции, а сохраняемость — индукционный шаг.

📐 Математическое доказательство принципа инвариантности 22:23

Сам принцип инвариантности также можно строго доказать с помощью индукции, выбрав в качестве индукционной гипотезы утверждение: «для любого исполнения длины $n$ предикат в конечном состоянии $q_n$ истинен». Профессор Демейн подробно расписывает этот процесс по шагам, демонстрируя классическую структуру математического доказательства. Рассматривая исполнения, аналитики начинают с коротких цепочек шагов и постепенно продвигаются к более длинным последовательностям.

Доказательство состоит из следующих этапов:

База индукции. Рассматривается гипотеза для исполнения длины 0. Существует лишь одно такое исполнение, состоящее исключительно из стартовой точки $q_0$, где система просто остается на месте. Истинность предиката $P(q_0)$ в этой точке верна по исходному предположению теоремы.
Индукционный шаг. Математики предполагают, что гипотеза справедлива для исполнений длины $n - 1$, и стремятся доказать ее для длины $n$. Для этого берется произвольное исполнение, состоящее из последовательности от $q_0$ до $q_n$.
Применение гипотезы. Если отсечь последний элемент, цепочка от $q_0$ до $q_{n-1}$ будет являться валидным исполнением длины $n - 1$. На основании индукционного предположения делается вывод, что в состоянии $q_{n-1}$ предикат истинен.
Финальный вывод. Поскольку шаг от $q_{n-1}$ к $q_n$ представляет собой легальный переход из множества $T$, а предикат по условию является сохраняющимся, из истинности $P(q_{n-1})$ автоматически следует истинность $P(q_n)$.

Таким образом, по закону математической индукции гипотеза признается верной для любого $n$. А поскольку любое достижимое состояние по определению имеет некоторую конечную длину пути от старта, предикат оказывается истинным для всех достижимых состояний без исключения, что и доказывает инвариантность. Данная логика формирует готовый шаблон для верификации систем: достаточно проверить истинность на старте и показать, что любой единичный шаг сохраняет это свойство.

🧮 Четность инверсий в «Пятнашках» 32:10

Возвращаясь к головоломке 3 на 3, профессор Демейн вводит специальный предикат, основанный на понятии инвертированной пары (inverted pair). Инверсией называются любые два числовых элемента головоломки (исключая пустую ячейку), для которых одновременно выполняются два условия: индекс первой фишки меньше индекса второй ($i < j$), но при этом в порядке чтения более крупная фишка появляется раньше меньшей.

Для иллюстрации лектор подсчитывает число инверсий в упомянутых ранее примерах:

В разрешимой конфигурации (1, 3, 4, 2, 5, 7, 8, 6) инвертированными являются пары (4, 2), (3, 2), (7, 6) и (8, 6) — всего 4 инверсии.
В идеальном, решенном состоянии количество инвертированных пар равно 0.
В неразрешимой конфигурации с переставленными 5 и 6 присутствует ровно 1 инверсия (пара 6 и 5).

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

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

При вертикальном перемещении (например, сдвиг фишки вниз) ситуация меняется, так как в порядке чтения фишка перемещается через целый ряд. В геометрии поля 3 на 3 это эквивалентно тому, что фишка перескакивает через два других числовых элемента. Эрик Демейн поясняет, что такое движение можно виртуально разбить на два последовательных обмена (свопа) с соседними элементами в порядке чтения. Каждый одиночный обмен соседних элементов меняет общее число инверсий строго на $+1$ или $-1$. Соответственно, два таких обмена изменят общее число инверсий на величину, равную сумме двух нечетных чисел ($\pm 1 \pm 1$), что всегда дает четное число: $+2, 0$ или $-2$. Прибавление или вычитание четного числа к нечетному оставляет результат нечетным, что полностью доказывает сохраняемость паритета. Поскольку решенное состояние имеет 0 инверсий (четное число), попасть в него из нечетного стартового состояния невозможно, что математически подтверждает исходную гипотезу.

🛑 Проблема завершаемости и алгоритмы сортировки 57:36

Вторая часть лекции посвящена феномену завершаемости (termination) алгоритмов. Продемонстрировать этот аспект авторы курса решили на примере простейшего автомата для сортировки массива из $n$ чисел в порядке возрастания. Задача формулируется стандартным образом: на вход подается хаотичный набор элементов $a_1, a_2, \dots, a_n$, который необходимо перестроить так, чтобы каждый последующий элемент был не меньше предыдущего.

Алгоритм работы этого автомата укладывается в один цикл: пока существует хотя бы один индекс $i$, для которого выполняется условие $a_i > a_{i+1}$, программа меняет эти элементы местами. На анимации видно, как элементы разной высоты постепенно выстраиваются в ровную линию по возрастанию благодаря локальным соседним обменам.

Для перевода этой логики на рельсы теории автоматов определяются базовые множества:

Множество состояний $Q$ включает в себя все возможные варианты перестановок исходных чисел (всего их $n!$).
Множество переходов $T$ разрешает операцию обмена местами элементов $a_i$ и $a_{i+1}$ тогда и только тогда, когда левый элемент строго больше правого.

Вводится понятие финального состояния — конфигурации, из которой не существует ни одного легального перехода наружу. Для сортировщика финальным является состояние, в котором массив полностью упоряочен. Если порядок нарушен, в системе гарантированно найдется пара элементов для перехода, а если массив отсортирован, то ни одного перехода совершить нельзя.

Это позволяет заявить о частичной корректности (partial correctness) машины: если автомат когда-нибудь остановится, выдав финальное состояние, ответ гарантированно будет правильным. Однако для полной корректности (total correctness) необходимо строго доказать, что автомат действительно завершит работу, а не уйдет в бесконечный цикл. Термин «завершаемость» означает отсутствие у автомата бесконечных исполнений, то есть любая траектория шагов рано или поздно утыкается в тупик финального состояния.

📉 Метод производных переменных 1:09:20

Для строгого доказательства завершаемости программ в Computer Science применяется концепция производных переменных (derived variables). Производная переменная — это функция $x(q)$, которая сопоставляет каждому состоянию автомата определенное вещественное число. В прикладных задачах математики чаще всего ограничиваются диапазоном натуральных чисел. Переменная называется строго убывающей, если для любого валидного перехода $q \to r$ значение функции в новой точке строго меньше, чем в предыдущей ($x(q) > x(r)$).

Теорема о завершаемости формулирует жесткие требования к такой переменной:

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

Если эти условия соблюдены, автомат гарантированно завершит работу за конечное число шагов. Логика доказательства этого утверждения строится от противного или через ограничение сверху: поскольку значение функции стартового состояния $x(q_0)$ конечно, а каждый шаг уменьшает это натуральное число как минимум на единицу, система физически не может совершить больше шагов, чем величина $x(q_0)$. Рано или поздно значение опустится до минимального уровня, и переходы станут невозможны. Профессор подчеркивает, что теорема перестанет работать, если разрешить функции принимать отрицательные или дробные значения, так как в этих случаях уменьшаться можно бесконечно, никогда не достигая барьера.

Для автомата сортировки такой производной переменной вновь становится общее число инверсий в массиве, то есть пар индексов $i < j$, для которых $a_i > a_j$ (в данном случае рассматриваются вообще все пары, а не только соседние). Эту концепцию удобно визуализировать с помощью диаграммы высот, где от каждого элемента влево проводятся горизонтальные лучи. Каждый шаг алгоритма по определению попарно меняет местами элементы $a_i > a_{i+1}$, что устраняет ровно одну инверсию между ними, никак не влияя на их взаимоотношения с остальными цифрами массива. Таким образом, с каждым переходом значение переменной уменьшается ровно на 1, функция является натуральным числом и строго убывает, что полностью доказывает неизбежность успешного завершения сортировки за конечное время.

📝 Организационные объявления курса 1:20:20

В самом конце лекции профессор Демейн делает важное объявление, касающееся правил сдачи домашних заданий в семестре. На текущей неделе ассистенты курса публикуют официальные эталонные решения к первому набору задач (Problem Set 1). Специфика регламента MIT 6.1200 позволяет студентам сдавать этот первый блок заданий в любой момент вплоть до окончания учебного семестра.

Правила ознакомления с готовыми ответами включают жесткие требования академической честности:

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

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