Краткий курс логики предикатов

Хиллел Уэйн написал Logic for Programmers, потому что не смог найти толкового материала по логике, ориентированного на программистов. Когда книга вышла, оставалось сделать бесплатный вводный материал. Поэтому 2026-09-01 он опубликовал вторую главу в виде поста в блоге, добавив в сноски редакторские комментарии, которых нет в самой книге crash-course-predicate-logic. В главе разбираются базовые вещи, на которые опирается остальная часть книги: предикаты, оператор импликации, множества, оба квантора и правила перезаписи, позволяющие упрощать формулы так же, как в арифметике. В конце он подчёркивает: на этом основы формальной логики заканчиваются, а самое сложное - это практика применения. Одно дело знать операцию деления, и совсем другое - сообразить, что пересчёт рецепта с пяти яиц на три сводится к делению.

Обозначения, выбранные для программистов

Уэйн отказывается от символов, которых нет на клавиатуре. И, ИЛИ и НЕ записываются как &&, || и !, импликация - как =>, а кванторы обозначаются словами all и some вместо ∀ и ∃. Объединение, пересечение и разность множеств заимствуют знаки |, & и -. Предикаты пишутся в TitleCase, обычные функции - в snake_case. Описания множеств (set comprehensions) используют явную форму с отображением и фильтрацией, {x^2 for x in set: x > 2}, поскольку новички часто путают, какая часть стандартной записи {f(x) | P(x)} отвечает за отображение, а какая за фильтрацию.

В последнем разделе книги этот подход обосновывается. Логика - это язык, и придумывать новые конструкции вполне допустимо, если они непротиворечивы и понятно объяснены. Уэйн добавляет диапазоны, 1..=100 и 1..<100, разрешая неоднозначные случаи: a..=b считается пустым при a > b. Для длинных требований он вводит нумерованные списки конъюнкций, где цифры и буквы означают И, а префикс || отмечает альтернативные варианты.

Предикаты - это не функции

В первом приближении предикат - это функция, возвращающая булево значение. Разница в том, что предикат лишь определяет, каков ответ, тогда как функция в программе обязана его вычислить. Благодаря этому предикаты могут варьироваться от конкретных (Positive(x) = x > 0) до таких, которые никто не способен вычислить, - например, шёл ли где-то в Канаде дождь в конкретную дату или существуют ли инопланетяне. Абстрактные формулировки Уэйн заключает в обратные кавычки, благодаря чему предикат может оставаться полунеформальным, пока требования ещё уточняются.

В качестве наглядного примера он приводит реальное требование, с которым однажды столкнулся: "Компьютер должен иметь достаточно оперативной памяти и быстрый процессор или хорошую видеокарту". Запись в виде RAM(c) && CPU(c) || GPU(c) показывает, что у этой фразы есть два прочтения:

# way 1
CanRunProgram(c) = RAM(c) && (CPU(c) || GPU(c))

# way 2
CanRunProgram(c) = (RAM(c) && CPU(c)) || GPU(c)

Таблица истинности для всех восьми комбинаций входов показывает, что результаты расходятся в двух строках - там, где у машины хорошая видеокарта, но не хватает памяти. Обе трактовки укладываются в обычную человеческую речь. Поставщик мог иметь в виду первый вариант, покупатель понял фразу во втором смысле, программа падает из-за нехватки памяти, и покупатель решает, что поставщик его обманул. differential-spec-analysis разбирает подобные неявные решения уже в масштабе всей системы, сравнивая несколько реализаций, написанных по одной спецификации.

Импликация

P => Q определяется как !P || Q: смотреть на Q нужно только тогда, когда выполняется P. Уэйн приходит к этому не через таблицу истинности, а через практическое требование. Программе, существующей в нативной и веб-версиях, мощный компьютер нужен только для нативной сборки, то есть !Native(p) || Beefy(c). Эта конструкция встречается настолько часто, что в математике для неё завели отдельный оператор. => связывает слабее, чем && и ||, поэтому A && B => C означает (A && B) => C.

Импликация также выражает, что одно утверждение сильнее другого. Код, который падает на нуле, гарантированно содержит ошибку, тогда как код с ошибкой вовсе не обязан на чём-то падать - ошибка на единицу (off-by-one) всё равно остаётся ошибкой:

CrashesOnInput(code, 0) => HasBug(code)

Кроме того, она транзитивна: из CanRenderVideo(c) => CPU(c) && RAM(c) следует CanRenderVideo(c) => CanRunProgram(c) без необходимости вникать в смысл предикатов.

Множества и кванторы

Предикаты не типизированы, поэтому CanRunProgram(poodle) - вполне корректный вопрос, и если приклеить к пуделю хорошую видеокарту, предикат вернёт истину. Множества решают эту проблему: c in Computer, сокращённо CanRunProgram(c: Computer). Подмножества соответствуют подтипам. В главе отмечается, что математики строят из множеств пары, а затем списки в качестве фундамента, тогда как программисты могут пропустить этот шаг и напрямую использовать более богатые структуры данных.

Кванторы вводятся через правило объединения веток (merge rule). Требование "Пулреквест должен быть проверен перед слиянием" превращается в some d in Developer: ReviewedBy(pr, d). Более строгая политика - что каждый, кто проверяет код, обязан его одобрить - содержит главную ловушку этой главы. Очевидная запись

EveryoneApproves(pr: PullRequest) =
  all d in Developer: Approved(pr, d)

требует одобрения от каждого разработчика в компании, включая тех, кто на больничном или в декретном отпуске. Исправление ограничивает квантор all только ревьюерами с помощью импликации: all d in Developer: ReviewedBy(pr, d) => Approved(pr, d). Уэйн отмечает, что именно так обычно формулируют квантификацию по подмножеству. Но это исправление открывает вторую ловушку, которую читателю предлагается найти в упражнении. Если никто не проверял пулреквест, утверждение "все, кто его проверял, одобрили" истинно, поэтому условие SomeoneReviewed всё равно нужно проверять отдельно. В общем случае all x in {}: P(x) всегда истинно, а some x in {}: P(x) всегда ложно.

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

Баланс возможностей и гарантий

Определив оба квантора, Уэйн замечает: some с большей вероятностью выполняется на большом множестве, а all - на малом, поэтому подмножество гарантирует свойства, которых нет у надмножества. ASCII гарантирует один байт на символ, а Unicode - нет. Доступ только на чтение гарантирует, что файл не изменится. Формулы, построенные только из булевых значений, И, ИЛИ и НЕ, всегда имеют таблицу истинности, чего нельзя сказать о выражении some x in Nat: OddPerfectNumber(x). При этом для эмодзи нужен Unicode, для обновлений нужны права на запись, а для содержательных предикатов нужны кванторы. Он называет это компромиссом между возможностями и гарантиями (ability-guarantee tradeoff) и отмечает, что он проявляется почти в каждой главе книги. Этому понятию посвящена отдельная страница, ability-guarantee-tradeoff.

Правила перезаписи и доказательства

В логике есть правила упрощения, аналогичные арифметическим. Три из них, по словам автора, будут использоваться в книге чаще всего: законы де Моргана (!(p && q) эквивалентно !p || !q), контрапозиция (p => q эквивалентно !q => !p) и дуальность кванторов (all x: !P(x) эквивалентно !(some x: P(x))). Дистрибутивность кванторов работает только в одну сторону для каждой пары: some дистрибутивен относительно ||, а all - относительно &&. Контрпримеры для других комбинаций строятся на множестве всех людей, когда-либо живших на Земле. Кто-то жив, а кто-то мёртв, но никто не является одновременно живым и мёртвым. Каждый человек либо жив, либо мёртв, но неверно, что все живы или что все мертвы.

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

Что осталось за рамками главы

В заключительных примечаниях уточняется название логики: это логика первого порядка, в которой предикаты не могут быть элементами множеств или аргументами других предикатов. Логики высших порядков дают больше возможностей, но меньше гарантий. Логика, содержащая только булевы значения, И, ИЛИ и НЕ, называется логикой высказываний. Для более глубокого погружения он рекомендует (в порядке возрастания сложности) книги A Tour Through Mathematical Logic Роберта Вольфа (Robert S. Wolf), Logic in Computer Science Майкла Хата и Марка Райана (Michael Huth, Mark Ryan) и Classical Mathematical Logic Ричарда Эпштейна (Richard Epstein).

Интервью Уэйна с инженерами, перешедшими в разработку ПО из других сфер, законспектированы на странице we-are-not-special.