open atlas
↑ К треку
Логика с нуля LOGIC · 02 · 02

Кванторы: для-всех, существует и почему «все тесты прошли» может лгать

∀ означает каждый случай, ∃ — хотя бы один. Отрицание переставляет квантор: не-все = существует-контрпример. Порядок кванторов меняет смысл. В коде: .every() и .some(); .every() на пустом массиве даёт true — «все тесты прошли» может значить «тестов не было».

LOGIC Основы ◷ 16 min
Уровень
ОсновыJuniorMiddleSenior

Баннер CI зелёный: «Все тесты прошли». Релиз выкатывается, и меньше чем через час чекаут ломается в трёх странах. Расследование делает унизительный поворот: рефакторинг переименовал директорию с тестами, glob ранера не поймал ни одного файла, и набор прогнался на нуле тестов. Проверка пайплайна буквально results.every(t => t.passed) — а .every() на пустом массиве возвращает true. «Все нулевые тесты прошли» — по холодным правилам логики истинное утверждение. Никто не задал другой вопрос, тот, что один символ бы решил: хотя бы один тест вообще запускался?

Цель

После этого урока ты умеешь различать ∀ и ∃, механически применять оба закона отрицания кванторов, объяснять, почему .every() на пустом массиве истинно, описывать, что меняется при смене порядка кванторов, и писать двухчастную CI-проверку, которая исключает инцидент с зелёным баннером.

1

∀ утверждает каждый случай; ∃ — хотя бы один. Квантифицированное высказывание говорит о целой коллекции. Кванторов ровно два. («для всех») утверждает, что свойство выполняется для каждого элемента: ∀t P(t) — каждый тест прошёл. («существует») утверждает, что свойство выполняется хотя бы для одного: ∃t P(t) — какой-то тест прошёл. Каждое предложение спека, которое вы когда-либо читали, строится из этих двух: «все запросы должны быть аутентифицированы» — это ∀; «администратор может превысить лимит» — это ∃; «каждый заказ содержит хотя бы одну строку» — это ∀ вокруг ∃.

2

Бремя доказательства для двух кванторов — противоположное. Чтобы установить ∀, нужно проверить каждый случай — но чтобы опровергнуть, достаточно одного контрпримера. Чтобы установить ∃, нужен лишь один свидетель — но чтобы опровергнуть, придётся перебрать всю коллекцию. Именно эта асимметрия объясняет, почему тестирование способно доказать наличие багов (один провальный кейс сносит «∀ входов код корректен»), но никогда — их отсутствие: никакая конечная пачка прошедших тестов не устанавливает ∀ над бесконечным пространством входов.

3

Отрицание перескакивает квантор и отрицает содержимое. Отрицание «у каждого пользователя есть подтверждённый email» — это не «у каждого пользователя нет подтверждённого email». Это «у некоторого пользователя нет подтверждённого email» — один контрпример. Формально: ¬∀x P(x) ≡ ∃x ¬P(x), и симметрично ¬∃x P(x) ≡ ∀x ¬P(x). Механически: отрицание, проходя сквозь квантор, переворачивает его — ∀ становится ∃, ∃ становится ∀ — и отрицает тело. В коде: !items.every(isValid) означает «какой-то элемент невалиден», а не «все элементы невалидны».

4

Порядок кванторов меняет смысл высказывания. Когда высказывание содержит два квантора, их порядок важен. Сравните: ∀ сервис ∃ инженер — у каждого сервиса есть дежурный инженер (возможно, разные). ∃ инженер ∀ сервис — существует один инженер, дежурящий за все сервисы (единая точка отказа). Более поздний квантор может зависеть от более раннего. Импликация односторонняя: ∃∀ влечёт ∀∃ (если один инженер покрывает всё — у каждого сервиса есть дежурный), но не наоборот.

Законы отрицания кванторов — и их аналоги в коде
ЛогикаСмыслАналог в коде
¬∀x P(x)Не у всех есть свойство P!arr.every(P)
∃x ¬P(x)Какой-то элемент лишён Parr.some(x => !P(x))
¬∃x P(x)Ни один элемент не имеет P!arr.some(P)
∀x ¬P(x)Каждый элемент лишён Parr.every(x => !P(x))
Разбор примера

Исправьте инцидент с зелёным баннером с помощью обоих кванторов.

Сломанная проверка:

const suiteIsGreen = results.every(t => t.passed);  // на пустом — true!

Это утверждение ∀: «все тесты прошли». На пустом массиве оно вакуумно истинно.

Исправление соединяет проверку ∀ с проверкой ∃:

const suiteIsGreen = results.length > 0 && results.every(t => t.passed);
// вопрос ∃: хотя бы один тест запускался  (results.length > 0)
// вопрос ∀: все они прошли                (results.every(...))

Вопрос ∃ (results.length > 0) уничтожает вакуумный случай: пустой массив сразу же его проваливает, и операция AND по короткой схеме возвращает false — баннер краснеет, когда ничего не запустилось.

Аналогично, «ни один тест не провалился» и «все тесты прошли» — одно утверждение для непустого набора, но расходятся для пустого:

!results.some(t => !t.passed)  // ¬∃ — вакуумно истинно на пустом
results.every(t => t.passed)   // ∀  — вакуумно истинно на пустом
results.length > 0 && results.every(t => t.passed)  // безопасно
Почему это работает

Почему .every() на пустом массиве возвращает true, а не что-то более безопасное? Потому что математике нужно, чтобы ¬∀ = ∃¬ выполнялось всегда, без исключений для пустых коллекций. «Все члены пустого множества фиолетовые» не имеет контрпримера — нет ни одного члена, который провалил бы это условие, — поэтому по закону отрицания это должно считаться истиной. Логики называют это вакуумной истинностью. Соглашение сохраняет алгебру чистой — и тихо требует от инженеров задавать вопросы ∃ («что-то запускалось?») параллельно с вопросами ∀ («всё прошло?»).

Практика 0 / 5

Спека говорит «каждый запрос несёт trace id». Чтобы это опровергнуть, сколько контрпримеров нужно? Введите число.

Чему равно отрицание «∀x P(x)»? Введите формулу.

Одно ли и то же !items.every(isValid) и items.every(i => !isValid(i))? Введите да или нет.

«∀ сервис ∃ инженер» и «∃ инженер ∀ сервис» — какое влечёт другое?

[].every(x => x > 0) в JavaScript — true или false?

Проверь себя
Викторина

Спека говорит: каждый запрос несёт trace id. QA хочет опровергнуть это утверждение. Что именно нужно предъявить?

Итог

Кванторы — два способа высказывания говорить о целой коллекции: ∀ («для всех») утверждает, что свойство выполняется для каждого элемента, и сносится одним контрпримером; ∃ («существует») утверждает хотя бы одного свидетеля, и сносится лишь перебором всего множества. Отрицание переставляет оба при проходе вовнутрь: ¬∀ = ∃¬ (не-все-прошли значит кто-то-провалился, а не все-провалились) и ¬∃ = ∀¬ (ни-один-не-провалился значит все-прошли). В коде .every() — это ∀, а .some() — это ∃, и .every() на пустом массиве вакуумно истинно — цена сохранения закона отрицания без исключений. Лекарство — пара каждой проверки ∀ с вопросом ∃ results.length > 0 и пара каждого универсального утверждения в спеке с вопросами «над каким конкретно множеством?» и «это множество непусто?». Порядок важен, когда кванторы стоят в стопке: ∀s ∃e (у каждого сервиса свой дежурный) против ∃e ∀s (один человек покрывает всё), и импликация идёт только от ∃∀ к ∀∃.

Практика

Начни сверху. Задачи идут от простого к сложному: вспомнить факт, применить к случаю, затем senior-уровень. Открой, попробуй, потом открой ответ.

вспомнитьприменитьуглубить0 из 5 завершено

Что-то непонятно?

Задай вопрос по этому уроку. Вопросы анонимны и попадают напрямую автору — урок станет лучше.

хоткеи развернуть
поиск
K
пред. пьеса
k
след. пьеса
j
тиры
t
это меню
?
sources3
expand
  1. 01
  2. 02
  3. 03

Trademarks belong to their respective owners. Editorial reference only.