Контрпримеры и утверждения: на ком лежит бремя доказательства
Форма квантора задаёт бремя доказательства: ∀-утверждение убивает один контрпример, и его не доказать примерами; ∃-утверждение доказывает один свидетель. Упавший тест — это контрпример, крайние значения — их среда обитания, а утверждение без квантора нельзя даже обсуждать.
«Я прогнал на десяти входах — работает». PR смержили на этом предложении. Наутро клиент дошёл до оформления заказа с пустой корзиной, и итог вышел NaN. Один пользователь, один вход — и утверждение «работает» мертво. Заметьте асимметрию: десять зелёных примеров не смогли утвердить заявление, а один красный его уничтожил. Это не невезение — это логика. «Работает» втайне означает для всех входов код ведёт себя правильно — ∀-утверждение, а они играют на жестоком табло: примеры «за» не стоят почти ничего, один пример «против» заканчивает игру. ∃-утверждения играют на зеркальном табло, где один пример выигрывает сразу.
После этого урока ты можешь прочесть квантор утверждения и назначить правильное бремя доказательства, предъявить контрпример к ложному ∀-утверждению, предъявить свидетеля для ∃-утверждения, определить, где живут контрпримеры, и переписать нефальсифицируемое утверждение в квантифицированную форму, пригодную для спора.
Квантор решает, на ком бремя доказательства.
| Форма утверждения | Один пример доказывает? | Один пример убивает? |
|---|---|---|
| ∀x P(x) | никогда — примеры лишь поддерживают | да: контрпример — x с ¬P(x) |
| ∃x P(x) | да: свидетель — x с P(x) | никогда — неудачные поиски лишь неудачны |
Чтобы доказать ∀-утверждение: рассуждение, покрывающее каждого члена области, или исчерпывающий перебор когда область мала и конечна. Чтобы опровергнуть: один контрпример. Зеркало точное: ¬∀x P(x) ≡ ∃x ¬P(x) — опровергнуть всеобщее значит доказать существование, поэтому одного объекта и хватает.
Контрпримеры живут на краях. Стандартный зоопарк, который стоит выучить как чек-лист: 0, 1, −1, пустая коллекция, одноэлементная коллекция, границы (первый/последний индекс, мин/макс значения), дубликаты, отсортированные и обратно отсортированные входы, юникод за пределами ASCII, null/отсутствующие поля. Авторы пишут ∀-утверждения, воображая типичный вход, — но квантор пробегает все входы, включая каждый, которого никто не вообразил. Зоопарк — каталог невоображённых.
// Утверждение: для каждого массива чисел xs функция average(xs) возвращает конечное число.
function average(xs) {
let sum = 0;
for (const x of xs) sum += x;
return sum / xs.length;
}
average([2, 4, 9]); // 5 — поддерживающий пример
average([7]); // 7 — пережило клетку одиночек
average([]); // NaN — 0/0. Контрпример. ∀-утверждение мертво.Одна красная строка перевешивает любое количество зелёных.
Квантифицируй утверждение, прежде чем о нём спорить. «API быстрый» — ни одно наблюдение его не опровергнет. Любой медленный запрос можно отмахнуть как «я не это имел в виду». Утверждение, которое не может опровергнуть никакое свидетельство, — нефальсифицируемое, а нефальсифицируемые утверждения непригодны для спора: в них можно лишь верить или не верить. Лечение механично: для каждого запроса GET /search под номинальной нагрузкой p95-латентность в любом 5-минутном окне не превышает 200 мс. Теперь есть область, измеримый предикат и квантор. Контрпример — конкретное 5-минутное окно с p95 выше 200 мс. Та же операция лечит «миграция безопасна», «на практике не бывает», «кэш ускоряет».
«Я проверил десять случаев» — ∀-утверждение выборкой не разрешается никогда. Что его разрешает положительно: доказательство — рассуждение обо всех входах; или исчерпывающий перебор по-настоящему малой конечной области (все 256 значений байта — пожалуйста; все пары 64-битных float — никогда). Дейкстра сжал весь урок в одно предложение: тестирование показывает наличие багов, но никогда — их отсутствие. Это логика кванторов. Практическая стойка: держите тесты как дешёвых охотников за контрпримерами; будьте точны в том, что означает зелёный: пока пережил охоту.
Охота за контрпримером к правдоподобной теореме.
Утверждение. Каждая функция с n корнями имеет степень не меньше n.
Звучит правильно. Прямая (степень 1) пересекает ноль не более одного раза, парабола — не более двух. Но охотьтесь: какую самую странную функцию ему можно скормить? Попробуйте f(x) = 0 — нулевую функцию. Каждый вход — корень: бесконечно много корней. Степень? Нулевой многочлен степени не имеет (по соглашению иногда −∞) — уж точно не «не меньше n». Один вырожденный объект — ∀-утверждение мертво.
Что смерть купила: контрпример не уничтожил идею — он нашёл её границу. Починенное утверждение — каждый ненулевой многочлен с n различными корнями имеет степень не меньше n — настоящая теорема. Относитесь к каждому найденному контрпримеру как к бесплатному консультанту, размечающему, где на самом деле кончается область вашего утверждения.
▸Почему это работает
Инструменты property-based-тестирования — Hypothesis в Python, fast-check в JavaScript, QuickCheck в Haskell — автоматизируют охоту. Вы формулируете свойство как настоящее ∀-утверждение, и инструмент обстреливает его тысячами смещённых к зоопарку входов. При падении он усаживает вход до минимального — часто ровно пустого массива или нуля. Честная оговорка: зелёный прогон — всё ещё примеры, не доказательство. Автоматизирован зоопарк, а не доказательство.
Доказывает ли один прошедший тест ∀-утверждение? Ответьте «да» или «нет».
Доказывает ли один свидетель ∃-утверждение? Ответьте «да» или «нет».
average([]) возвращает NaN. Это контрпример к «average всегда возвращает конечное число»? Ответьте «да» или «нет».
Коллега фаззит 100 000 случайных входов, падений нет. Опровергает ли это «существует вход, ронящий парсер»? Ответьте «да» или «нет».
Перепишите «кэш делает вещи быстрее» в квантифицированную фальсифицируемую форму. Что обязательно нужно добавить?
Утверждение: «существует вход, на котором этот парсер падает». Коллега фаззит 100 000 случайных входов, падений не видит и объявляет утверждение опровергнутым. Что не так?
Квантор утверждения назначает бремя доказательства до начала любого спора. ∀x P(x) доказывается только рассуждением, покрывающим всю область, или исчерпывающим перебором малой конечной — и гибнет от одного контрпримера; никакая груда поддерживающих примеров его не доказывает. ∃x P(x) зеркально: один свидетель доказывает, и лишь рассуждение о том, что каждый кандидат не подходит, опровергает. Зеркало — это эквивалентность ¬∀ и ∃¬. Контрпримеры живут на краях — 0, 1, −1, пустота, одиночка, границы, дубликаты, юникод, null — потому что квантор пробегает все входы, а автор воображает типичный. Контрпример редко уничтожает идею: он размечает границу, и починенное утверждение говорит точно, где живёт истина. Упавший тест — контрпример; зелёный набор — список выживших; property-based-инструменты автоматизируют зоопарк и усаживают падения до минимальных контрпримеров, но зелёный прогон по-прежнему не доказывает ничего. И прежде чем спорить о любом утверждении, квантифицируйте его: «API быстрый» не опровергается никаким наблюдением, а утверждение, которое нельзя проиграть, нельзя и выиграть.
Практика
Начни сверху. Задачи идут от простого к сложному: вспомнить факт, применить к случаю, затем senior-уровень. Открой, попробуй, потом открой ответ.
Что-то непонятно?
Задай вопрос по этому уроку. Вопросы анонимны и попадают напрямую автору — урок станет лучше.