Перейти к основному содержимому

Логика

ОБЯЗАТЕЛЬНОДЛЯ НОВИЧКОВ
Архитектору Инженеру

Логика — наука о формальных правилах корректного рассуждения. В IT она не "философский факультатив", а язык, на котором описывают условия в коде, контракты API, инварианты и требования. Любой if, while или switch — это логическое выражение, записанное синтаксисом языка.

Начальный уровень (высказывания, таблицы истинности, кванторы) — в базовой информатике, алгебра логики.

Обзор всего блока: Математическая основа IT.

Два уровня в разработке​

УровеньЧто описываетПримеры в практике
Пропозициональная (булева)Целые утверждения: истина или ложьisActive and not isBlocked
ПредикатнаяСвойства объектов с параметрами и кванторамидля всех активных пользователей доступ разрешён

Пропозициональной логики достаточно для ветвлений и рефакторинга условий. Предикатная нужна для спецификаций, SQL WHERE, LINQ-фильтров и формальных методов (TLA+, Alloy).

// Допуск в личный кабинет (бытовой пример тех же правил, что в if)

если пользователь_залогинен И НЕ аккаунт_заблокирован то
  ПоказатьКабинет()
иначе
  ПоказатьОшибку()
конец

// Закон де Моргана: "не (A и B)" = "не A или не B"
если НЕ (оплачен И доставлен) то
  // эквивалентно: не оплачен ИЛИ не доставлен
  ОтправитьНапоминание()
конец

Логические операции​

Отрицание (NOT, ¬)​

Инвертирует значение. Инволютивность: ¬(¬A) ≡ A. В коде !flag или not flag; двойное отрицание в JS (!!x) — приведение к boolean, а не логическая необходимость.

Конъюнкция (AND, ∧)​

Истина только когда оба операнда истинны: A ∧ B. В коде: &&, and. Свойства — коммутативность, ассоциативность, дистрибутивность относительно OR, идемпотентность A ∧ A ≡ A.

Дизъюнкция (OR, ∨)​

Ложь только когда оба ложны. В коде: ||, or. В большинстве языков — short-circuit: второй операнд может не вычисляться (false && f() не вызовет f). Это важно для побочных эффектов и производительности.

Исключающее ИЛИ (XOR, ⊕)​

Истина, когда ровно один операнд истинен: A ⊕ B ≡ (A ∨ B) ∧ ¬(A ∧ B). Применение — чётность, сравнение битовых флагов, криптография. В C#/Java есть ^ для целых; отдельного логического XOR в JavaScript нет.

Импликация и эквивалентность​

СвязкаОбозначениеИстинна когдаВ коде / спецификации
ИмпликацияA → Bложь только при A истинно и B ложно"если A, то B"; контракты API
ЭквивалентностьA ↔ Bоба операнда совпадают по истинности"A тогда и только тогда B"

A → B эквивалентно ¬A ∨ B. Импликация удобна для инвариантов: isLoggedIn → hasValidSession. Эквивалентность — для рефакторинга условий: две формулы можно менять местами, если они эквивалентны на всех входах (проверка таблицей истинности).

Законы булевой алгебры​

  1. Исключённое третье: A ∨ ¬A ≡ истина (в классической логике).
  2. Противоречие: A ∧ ¬A ≡ ложь — нарушение в спецификации = фатальная ошибка модели.
  3. Де Морган:
    • ¬(A ∧ B) ≡ ¬A ∨ ¬B
    • ¬(A ∨ B) ≡ ¬A ∧ ¬B
  4. Поглощение: A ∨ (A ∧ B) ≡ A, A ∧ (A ∨ B) ≡ A.

Типичный рефакторинг:

# было
if not (user.is_blocked or not user.is_active):
    ...

# стало (де Морган)
if not user.is_blocked and user.is_active:
    ...

Таблицы истинности​

Для n переменных — 2^n строк. Таблица задаёт функцию однозначно и позволяет:

  • проверить эквивалентность двух формул;
  • найти тавтологии (всегда истина) и противоречия;
  • построить набор тестов (каждая строка — вход для покрытия условий).

Play ITЗагрузка интерактивного демо…

Нормальные формы​

  • ДНФ — дизъюнкция конъюнкций литералов: (A ∧ ¬B) ∨ (C ∧ D).
  • КНФ — конъюнкция дизъюнкций: (A ∨ B) ∧ (¬C ∨ D).
  • Совершенная ДНФ (СДНФ) — по одной конъюнкте на каждую строку таблицы истинности, где функция равна 1.

Любое булево выражение можно привести к ДНФ или КНФ. Это основа SAT-решателей и формальной верификации. Минимальная ДНФ содержит меньше литералов при той же функции — её ищут склеиванием в СДНФ, матрицей Квайна или картой Карно для 2–4 переменных (удобно при проектировании схем и упрощении сложных if с несколькими флагами).

Карта Карно (идея)

Ячейки таблицы размещают так, чтобы соседние отличались одной переменной (код Грея).

Соседние единицы объединяют в прямоугольники степени двойки — получают более короткую формулу.

Для пяти и более переменных на практике переходят к алгоритмам минимизации в САПР или к SAT, а не к ручной карте.

Тождества над множествами (A ∪ B, A ∩ B, дополнение) можно проверять, переводя их в формулы алгебры логики — тот же закон де Моргана связывает ¬(A ∩ B) в логике и Ā ∪ B̄ для множеств.

Предикаты и кванторы​

Предикат — функция из предметной области в {истина, ложь} — CanAccess(user, resource), IsEven(n).

КванторЧтениеПример
∀для всех∀u ∈ Users: u.isActive ⇒ u.canLogin
∃существует∃file: file.isLocked

Отрицание кванторов (де Морган):

  • ¬(∀x P(x)) ≡ ∃x ¬P(x) — "не все прошли проверку" ⇔ "найдётся хотя бы один непроверенный".
  • ¬(∃x P(x)) ≡ ∀x ¬P(x).

Порядок кванторов важен — ∀x ∃y R(x,y) и ∃y ∀x R(x,y) — разные утверждения.

Связь с кодом и тестами​

  • Упрощайте условия алгебраически, сохраняя семантику — меньше веток, выше читаемость.
  • Таблица истинности для 3–4 флагов — честный способ не забыть комбинацию в тестах.
  • Отрицание "для всех" переводите в конструктивное "найти контрпример" — так формулируют проверки безопасности и валидации.

Углубление: алгебра логики — нормальные формы и схемы. Дальше: формальный слой множеств → дискретная математика.

Содержание