Индукция и инварианты: доказываем корректность кода для каждого n
Индукция доказывает утверждение для каждого n через базовый случай и шаг n→n+1; сильная индукция опирается на все меньшие случаи. Инвариант цикла — та же схема: истинен до цикла, сохраняется каждым проходом, на выходе гарантирует корректность.
Ревью кода, четверг после обеда. Дифф — аккуратный маленький цикл, пакетно выгружающий пользовательские записи, тесты проходят — на 3 записях, на 10, на 100. Ревьюер оставляет один комментарий: «Почему это работает для миллиона записей? Вы протестировали три размера». Автор несколько раз набирает и удаляет ответы. «Это очевидно обобщается» — не аргумент; миллион тест-кейсов не влезут в CI; и у всех в памяти живёт момент, когда пагинация работала на каждой тестовой фикстуре, а потом молча теряла одну строку на страницу в проде — промах на единицу, в масштабе, шесть недель. Из этого угла есть выход, и это тот же приём, которым математики с семнадцатого века делают утверждения о бесконечно многих числах, не проверяя каждое по отдельности. Ревьюер просил не тесты. Он просил инвариант.
После этого урока ты умеешь сформулировать два части индуктивного доказательства и объяснить, почему обе необходимы, описать, что добавляет сильная индукция, определить инвариант цикла и разрядить три обязательства доказательства (инициализация, поддержание, завершение) на простом цикле.
Математическая индукция состоит из двух частей: базового случая и индуктивного шага. Как доказать утверждение для каждого натурального числа за конечное время? Математическая индукция делает ровно два дела. Базовый случай: покажите, что утверждение выполняется для первого значения, обычно n = 0 или n = 1. Индуктивный шаг: покажите, что если утверждение выполняется для произвольного n (это индукционная гипотеза), то оно выполняется и для n + 1. Два конечных доказательства, бесконечное покрытие. Стандартный образ: ряд домино. База опрокидывает первое. Шаг гарантирует, что каждое упавшее домино опрокидывает следующее. Оба условия выполнены — падают все, включая миллионное, которого никто не трогал напрямую.
Обе части несущие. Пропустите базовый случай — и можно «доказать» нонсенс: шаг «если n чётно, то n + 2 чётно» безупречен, но, начав с 1, он порождает только нечётные числа — идеальная цепочка домино, которую никто не опрокинул. Пропустите общность шага — и получите классическое сломанное доказательство, что все лошади одного цвета: рассуждение молча предполагает, что две группы перекрываются, а это неверно ровно при n = 2 — одна ступенька лестницы треснула, всё выше падает.
Сильная индукция позволяет шагу использовать все меньшие случаи — идеально для рекурсии. Иногда «это работало для n» — недостаточное топливо для шага. Сильная индукция усиливает гипотезу: предположим, что утверждение выполняется для всех значений до n, затем докажем его для n + 1. Это естественная форма для рекурсии: рекурсивная функция, которая обрабатывает базовый случай и корректна, когда её рекурсивные вызовы на любых меньших входах корректны, — корректна, точка. Каждый раз, когда вы доверяете mergeSort на половинах, пока пишете merge, вы рассуждаете по сильной индукции.
Инвариант цикла — это индукция в коде: инициализация, поддержание, завершение. Инвариант цикла — утверждение о переменных программы, которое истинно каждый раз, когда цикл проверяет своё условие. Доказательство корректности цикла с помощью инварианта точно отражает индукцию: инициализация (инвариант выполняется до первой итерации — базовый случай), поддержание (если он выполняется в начале итерации, то выполняется в начале следующей — индуктивный шаг), завершение (цикл завершается, и на выходе инвариант плюс ложное условие цикла вместе влекут нужный результат). Три небольшие проверки — и функция корректна для каждого входа, включая пустой массив и массив из миллиона элементов, которого ни одна фикстура не обхватывает.
Докажем корректность цикла накопленной суммы с помощью инварианта.
function sumFirst(nums) {
let total = 0;
let i = 0;
// ИНВАРИАНТ: total === сумма nums[0..i-1] (первых i элементов)
while (i < nums.length) {
total += nums[i];
i += 1;
// total теперь включает nums[i-1]: всё ещё сумма первых i элементов
}
return total;
}Инициализация: до цикла i = 0 и total = 0. Сумма нуля элементов равна 0. Инвариант выполняется.
Поддержание: предположим, инвариант выполняется в начале итерации — total равно сумме первых i элементов. Тело делает total += nums[i], затем i += 1, значит total теперь сумма первых новых i элементов. Инвариант сохранён.
Завершение: цикл завершается, когда i === nums.length. В этот момент инвариант читается как total === сумма nums[0..nums.length-1] — сумма всех элементов. Именно это функция и возвращает. Кроме того, nums.length - i строго убывает при каждом проходе, поэтому завершение гарантировано.
Теперь найдите баг промаха на единицу: инициализируйте i = 1 «потому что первый элемент уже учтён в total». Проверка инициализации: total = 0, i = 1, но сумма первого 1 элемента — nums[0] ≠ 0. Инвариант нарушается ещё до запуска цикла — доказательство сразу указывает на баг.
▸Почему это работает
Почему этот способ рассуждения называется доказательством, а «работало на стейдже» — нет? Потому что индукция — это просто наряженный modus ponens, валидная форма из предыдущего урока. Шаг доказывает универсальное условное — для каждого n, P(n) → P(n+1) — а базовый случай поставляет P(0). Применяем modus ponens раз: P(1). Ещё раз: P(2). Для любого целевого n цепочка — конечный, полностью валидный вывод. Тестирование, напротив, устанавливает P в разрозненных точках без связывающего их условного — вот почему три пройденных размера ничего не говорят о четвёртом.
Индуктивное доказательство показывает P(0) и P(n) → P(n+1). Доказано ли P(1000000)? Введите да или нет.
Что происходит при пропуске базового случая в индуктивном доказательстве?
Назовите три обязательства доказательства инварианта цикла.
Каков инвариант цикла «суммируем первые i элементов в total»?
Если проверка инициализации не выполняется, где находится баг?
Что именно нужно установить об инварианте цикла, чтобы заключить, что цикл выдаёт правильный ответ?
Математическая индукция доказывает утверждение о каждом натуральном числе с помощью двух конечных частей: базового случая (утверждение выполняется при n = 0) и индуктивного шага (если выполняется для произвольного n, то для n + 1), после чего любое конкретное n достигается конечной цепочкой modus ponens. Обе части обязательны: идеальный шаг без базы — неопрокинутый ряд домино, а шаг, доказанный лишь на примерах, — ошибка всех-лошадей с трещиной на одной ступеньке. Сильная индукция усиливает гипотезу до всех значений до n — равносильна по мощности, но естественна для задач, разбивающихся на произвольно меньшие части: разложение на простые, сортировка слиянием, любая рекурсивная функция, корректная, когда её вызовы на меньших входах корректны. Инвариант цикла переносит доказательство в код: сформулируйте, что означают переменные при каждой проверке условия, затем разрядите инициализацию (истинен до цикла; базовый случай), поддержание (каждая итерация сохраняет; индуктивный шаг) и завершение (строго убывающая величина гарантирует выход, где инвариант плюс ложное условие цикла влекут ответ). Выигрыш перед тестированием категорический: доказательство покрывает каждый вход, и когда обязательство не выполняется — оно указывает на виновную строку: инициализируйте индекс с 1 в цикле суммы, и сама инициализация откажет, обнажив промах на единицу до первого прохода. Пишите инвариант комментарием; поставляйте причину, а не только код.
Практика
Начни сверху. Задачи идут от простого к сложному: вспомнить факт, применить к случаю, затем senior-уровень. Открой, попробуй, потом открой ответ.
Что-то непонятно?
Задай вопрос по этому уроку. Вопросы анонимны и попадают напрямую автору — урок станет лучше.