Инварианты на практике: доказать недостижимость цели без перебора

Возьмите доску 8 × 8 и отрежьте два противоположных угла — они одного цвета, скажем оба белые. Осталось 62 клетки. Замостят ли их 31 доминошка, каждая из которых накрывает две соседние клетки?

Доказательство того, что любая попытка обязана провалиться, умещается в три предложения.

Доминошка накрывает две соседние клетки, а соседние клетки всегда разного цвета — значит, каждая положенная доминошка накрывает ровно одну чёрную и одну белую клетку, где бы ни легла. Поэтому в любой момент любой попытки замощения число накрытых чёрных клеток равно числу накрытых белых: это равенство — наш инвариант, свойство состояния, которое сохраняет каждый разрешённый ход (укладка доминошки). Но на урезанной доске 32 чёрные клетки и лишь 30 белых, так что полное замощение потребовало бы 32 накрытых чёрных против 30 белых — нарушение инварианта. Замощения не существует.

Определим точно: инвариант — свойство состояния системы, которое выполняется на старте и сохраняется каждым разрешённым ходом. Если у целевого состояния этого свойства нет, цель недостижима — точка.

Игра с перевёртыванием знаков. На доске четыре знака: +, +, −, +. Разрешённый ход: выбрать любые два и перевернуть оба. Цель: все четыре плюса.

Инвариант: посчитайте минусы и взгляните на чётность их числа. Ход переворачивает две записи, и случаев всего три: оба были плюсами (минусов стало на 2 больше), оба минусами (на 2 меньше), по одному каждого (итого 0). В каждом случае число минусов меняется на −2, 0 или +2: его чётность не меняется никогда. На старте один минус — нечётно. В цели ноль — чётно. Недостижимо: после любого числа ходов, в любом порядке.

Переливания. Два кувшина — 12 литров и 8 литров, кран и слив. Можно ли отмерить ровно 6 литров? Инвариант: 4 — наибольший общий делитель 12 и 8: обе ёмкости кратны 4, старт (0) кратен 4, а каждый ход лишь добавляет, вычитает или переносит объёмы, собранные из ёмкостей — кратные четырём остаются кратными четырём. Достижимые объёмы — ровно 12, и шести среди них нет. Цель отличается от старта по инвариантному свойству «каждый объём кратен НОД» — недостижима.

Каждая головоломка выше шла по одному сценарию, и его стоит записать:

1. Перечислите все разрешённые ходы, исчерпывающе — аргумент через инвариант хорош ровно настолько, насколько полон список ходов.
2. Ищите величину, которую каждый ход сохраняет: неизменную сумму, чётность, «кратность d», цветовой баланс — или величину, движущуюся только в одну сторону (только растёт, только убывает).
3. Сверьте кандидата с каждым ходом — единственный ломающий ход убивает кандидата, и эта сверка и есть настоящая работа.
4. Сравните старт и цель по инварианту — различаются, значит, цель недостижима, и в руках у вас доказательство, а не догадка.

Вы писали инварианты всё это время. Инвариант цикла суммирования: свойство «acc равен сумме первых i элементов» выполняется до старта цикла (i = 0, acc = 0, пустая сумма) и восстанавливается каждой итерацией:

let acc = 0;                      // инвариант выполнен: сумма первых 0 элементов — 0
for (let i = 0; i < xs.length; i++) {
  // инвариант здесь: acc === xs[0] + … + xs[i-1]
  acc += xs[i];                   // ход восстанавливает его для i + 1
}
// цикл кончается при i === xs.length, значит: acc === сумма всего массива

Миграция из пролога — «сохранительная» разновидность, инвариант в продакшен-одежде:

// Инвариант сохранения: перевод перемещает центы — не чеканит и не сжигает их.
function transfer(from, to, cents) {
  from.cents -= cents;
  to.cents += cents;              // списание равно зачислению — ход сохраняет сумму
}

const total = (accs) => accs.reduce((sum, a) => sum + a.cents, 0);

const before = total(accounts);
applyAllMoves(accounts);          // миллионы переводов, в каком угодно порядке
console.assert(total(accounts) === before, "cents created or destroyed");

Assert — это инвариант, ставший исполняемым. Он не проверяет какую-то конкретную последовательность ходов — он проверяет свойство, которое обязана сохранить каждая легальная последовательность, и потому ловит баги, недоступные тестам на примерах.

Одно честное ограничение: инвариант доказывает недостижимость, когда старт и цель по нему различаются. Когда совпадают — сам по себе он не доказывает ничего: цель может быть достижима, а может быть заперта другим препятствием. Шесть литров с кувшинами 12 и 8 доказуемо невозможны; а что 4 литра достижимы, всё равно показывается предъявлением ходов (наполнить 12, перелить в 8, осталось 4 — готово). Доказательство невозможности и построение — разные артефакты.