Декларативное и логическое программирование

В функциональном программировании мы убрали изменяемое состояние, но порядок вычислений всё ещё писали руками: map, потом filter, потом fold. В императивном мы писали и состояние, и порядок. Декларативная парадигма делает следующий шаг и забирает у программиста последнее — управление.

Формулировка, которая объясняет всю эту статью, принадлежит Роберту Ковальски (1979):

Algorithm = Logic + Control

Алгоритм состоит из двух независимых частей: логики (что считается правильным ответом) и управления (в каком порядке и какими шагами его добывать). Императивный код смешивает их в каждой строчке. Декларативный — разрезает: вы пишете логику, движок подставляет управление. Работа «Algorithm = Logic + Control» в CACM — короткая, стоит прочитать целиком.

Отсюда сразу следуют и сила, и главная боль парадигмы. Сила: одна спецификация переживает десять поколений оптимизаторов. Боль: когда движок выбирает плохое управление, у вас нет строчки кода, которую можно исправить.

Что считать декларативным: рабочий критерий

«Описывать что, а не как» — слоган, а не определение. По нему map(f, xs) декларативен относительно цикла for, а цикл for декларативен относительно ассемблерных переходов. Декларативность относительна, это не бинарный признак языка.

Полезнее операциональный критерий: программа декларативна в той мере, в какой её текст остаётся верным при смене стратегии выполнения.

• SELECT * FROM t WHERE x > 5 останется корректным, если PostgreSQL завтра переставит соединения местами и распараллелит скан. Высокая декларативность.
• Цикл с i++ перестанет быть корректным, если рантайм решит выполнять итерации в другом порядке. Нулевая декларативность.
• Prolog-программа с отсечением ! формально описывает логику, но её смысл зависит от порядка обхода дерева поиска. Декларативность частичная — и это ровно та трещина, о которой будет отдельный раздел.

Разброс огромный: от академического Prolog до .tf-файлов, которые пишет каждый второй инженер. Их объединяет одна структура — декларация + движок, который её исполняет. Дальше мы разберём эту структуру на нескольких уровнях глубины.

Логическое программирование: вычисление как доказательство

Логическое программирование — самая радикальная форма декларативности. Идея: программа есть множество логических утверждений, а выполнение — поиск доказательства.

Основой служит хорновская клауза — импликация вида «Голова истинна, если истинны Тело₁, …, Телоₙ»:

H :- B1, B2, ..., Bn.

Три типа клауз: факт (пустое тело), правило (непустое) и запрос (пустая голова — то, что мы просим доказать). Ограничение ровно одним предикатом в голове не случайно: для хорновских клауз существует эффективная процедура доказательства, а для произвольной логики первого порядка — нет.

Первая программа

% Факты — безусловные истины базы знаний.
родитель(том, боб).
родитель(том, лиза).
родитель(боб, анна).
родитель(лиза, петя).

мужчина(том).  мужчина(боб).  мужчина(петя).
женщина(лиза). женщина(анна).

% Правила. Заглавные буквы — переменные, запятая — конъюнкция.
отец(X, Y) :- родитель(X, Y), мужчина(X).

% Рекурсия: базовый случай и шаг.
предок(X, Y) :- родитель(X, Y).
предок(X, Z) :- родитель(X, Y), предок(Y, Z).

% Двое — siblings, если у них общий родитель и это разные люди.
сиблинги(X, Y) :- родитель(P, X), родитель(P, Y), X \= Y.

Ключевая особенность, ради которой всё затевалось: предикаты не имеют направления. Функция f(x) принимает вход и отдаёт выход. Предикат предок/2 — это отношение, и запрашивать его можно с любой стороны:

?- предок(том, анна).      % проверка: true
?- предок(том, X).         % кто потомки тома? X = боб ; X = лиза ; X = анна ; X = петя
?- предок(X, анна).        % кто предки анны? X = боб ; X = том
?- предок(X, Y).           % перечислить все пары вообще

Один и тот же код работает как проверка, как прямой поиск, как обратный поиск и как генератор. В любом языке с функциями это четыре разные реализации. Здесь — одна. Это называется обратимостью и является главным практическим козырем парадигмы.

Унификация: механизм, который всё это делает возможным

Унификация — не присваивание и не сравнение. Это поиск подстановки, при которой два терма становятся синтаксически идентичными.

Классический алгоритм Робинсона (1965) наивен и в худшем случае экспоненциален по времени и памяти — на термах вида f(X1,...,Xn) против f(g(X0,X0), g(X1,X1), ...) результат имеет экспоненциальный размер. Алгоритм Мартелли — Монтанари (1982) с union-find и разделением структуры даёт практически линейное время O(n·α(n)); линейный алгоритм Патерсона — Вегмана существует, но на практике проигрывает из-за констант.

Если пришли из Elixir или Erlang — там вы уже пользуетесь сопоставлением с образцом ({:ok, value} = result). Это унификация, урезанная до односторонней: связывать переменные можно только слева. Prolog связывает с обеих сторон одновременно. Подробности сопоставления в BEAM — в треке по Elixir.

SLD-резолюция и поиск с возвратом

Как система доказывает цель? Стратегия называется SLD-резолюция (Selective Linear resolution for Definite clauses):

1. Взять самую левую цель из списка.
2. Перебирать клаузы базы сверху вниз, унифицируя голову с целью.
3. При успехе заменить цель на тело клаузы (с применённой подстановкой) и уйти вглубь.
4. При неудаче — откатиться к последней точке выбора и попробовать следующую клаузу.

Получается обход дерева в глубину. Порядок клауз в файле и порядок целей в теле — это и есть «control» из формулы Ковальски: логика от них не зависит, а поведение — целиком.

Видно, куда уходит время: дерево ветвится по числу подходящих клауз, а глубина не ограничена ничем. Сложность SLD-резолюции в общем случае не просто экспоненциальна — задача неразрешима: программа на чистом Prolog эквивалентна машине Тьюринга, и вопрос «завершится ли запрос» неразрешим. Практическая стоимость одного шага — унификация цели с головой, O(размер термов); практическая стоимость запроса — число посещённых узлов дерева.

Собираем движок сами: 40 строк на Python

Лучший способ перестать считать логическое программирование магией — реализовать его. Ниже — работающий SLD-решатель.

from dataclasses import dataclass
from itertools import count

@dataclass(frozen=True)
class Var:
    name: str
    gen: int = 0            # «поколение» — для переименования при каждом применении правила

@dataclass(frozen=True)
class Term:
    functor: str
    args: tuple = ()

def walk(t, subst):
    """Разыменование: идём по цепочке связываний, пока переменная связана."""
    while isinstance(t, Var) and t in subst:
        t = subst[t]
    return t

def unify(a, b, subst):
    """Возвращает расширенную подстановку или None. Занимает O(размера термов)."""
    a, b = walk(a, subst), walk(b, subst)
    if a == b:
        return subst
    if isinstance(a, Var):
        return {**subst, a: b}          # occurs check пропущен — как в стандартном Prolog
    if isinstance(b, Var):
        return {**subst, b: a}
    if (isinstance(a, Term) and isinstance(b, Term)
            and a.functor == b.functor and len(a.args) == len(b.args)):
        for x, y in zip(a.args, b.args):
            subst = unify(x, y, subst)
            if subst is None:           # конфликт в подтерме — весь терм не унифицируется
                return None
        return subst
    return None                          # разные функторы или арность

_gen = count()

def rename(t, g):
    """Каждое применение правила использует свежие переменные — иначе рекурсия склеится."""
    if isinstance(t, Var):
        return Var(t.name, g)
    return Term(t.functor, tuple(rename(a, g) for a in t.args))

def solve(goals, rules, subst):
    """SLD-резолюция. Генератор: каждый yield — очередное решение (как ';' в Prolog)."""
    if not goals:
        yield subst                      # целей не осталось — доказательство найдено
        return
    goal, rest = goals[0], goals[1:]     # выбираем САМУЮ ЛЕВУЮ цель
    for head, body in rules:             # клаузы перебираем СВЕРХУ ВНИЗ
        g = next(_gen)
        head, body = rename(head, g), [rename(b, g) for b in body]
        s = unify(goal, head, subst)
        if s is not None:
            yield from solve(body + rest, rules, s)   # вглубь; исчерпав — откат сам собой

Проверим на той же базе:

def t(f, *args):
    return Term(f, args)

X, Y, Z, Q = Var("X"), Var("Y"), Var("Z"), Var("Q")

rules = [
    (t("родитель", t("том"), t("боб")),  []),
    (t("родитель", t("том"), t("лиза")), []),
    (t("родитель", t("боб"), t("анна")), []),
    (t("родитель", t("лиза"), t("петя")), []),
    (t("предок", X, Y), [t("родитель", X, Y)]),
    (t("предок", X, Z), [t("родитель", X, Y), t("предок", Y, Z)]),
]

for s in solve([t("предок", t("том"), Q)], rules, {}):
    print(walk(Q, s).functor)     # боб, лиза, анна, петя

Обратите внимание: отката в коде нет. Возврат обеспечивается самой семантикой генераторов — когда вложенный solve исчерпан, цикл for просто переходит к следующей клаузе. Ленивость и backtracking — это одна и та же вещь, увиденная с двух сторон.

Теперь переставьте цели во втором правиле предка местами:

    (t("предок", X, Z), [t("предок", X, Y), t("родитель", Y, Z)]),   # левая рекурсия

Логика идентична: отношение то же самое. Программа зависает мгновенно, потому что первая же цель — снова предок, и рекурсия уходит вниз без единого шага к фактам. Это и есть цена смешения логики с управлением: текст выражает истину, а поведение определяется порядком.

Отсечение, отрицание и замкнутый мир

Три конструкции, вокруг которых ломается «чистая» декларативность Prolog.

Отсечение (!) фиксирует все выборы, сделанные до него в текущей клаузе, и запрещает откат. Различают:

• зелёное отсечение — отсекает заведомо провальные ветки, множество решений не меняется, только ускоряется поиск;
• красное отсечение — меняет множество решений, то есть управление начинает влиять на логику.

% Красное отсечение: без ! второй вариант тоже сработал бы при X >= 0.
модуль(X, X) :- X >= 0, !.
модуль(X, Y) :- Y is -X.

Такой код перестаёт быть обратимым и читается только вместе с моделью выполнения. Практическое правило: красных отсечений избегайте, а условие делайте явным (X < 0 во второй клаузе) — потеряете чуть-чуть скорости, получите программу, о которой можно рассуждать.

Отрицание как неудача (\+ Goal) истинно, когда Goal не удаётся доказать. Это не логическое отрицание. Работает предположение о замкнутом мире (closed-world assumption): всё, чего нет в базе, считается ложью. В базе данных сотрудников это разумно; в базе знаний о реальном мире — источник неверных выводов.

Хуже: \+ некорректен на несвязанных переменных (эффект называется floundering).

?- \+ родитель(X, анна).      % false — «не существует X» вместо ожидаемого «для некоторого X»
?- родитель(X, анна), \+ мужчина(X).   % корректно: X уже связан к моменту проверки

Правило: отрицание применяйте только к полностью конкретизированным целям.

Зацикливание лечится табулированием (SLG-резолюция): движок мемоизирует вызовы и уже вычисленные ответы, превращая обход дерева в вычисление неподвижной точки. В SWI-Prolog достаточно директивы:

:- table предок/2.
предок(X, Z) :- предок(X, Y), родитель(Y, Z).   % теперь левая рекурсия завершается
предок(X, Y) :- родитель(X, Y).

Табулирование — это ровно тот же приём, что мемоизация в динамическом программировании, поднятый на уровень стратегии выполнения.

Datalog: отказ от полноты по Тьюрингу как фича

Prolog слишком мощен, чтобы давать гарантии. Datalog — его подмножество, в котором намеренно убраны две вещи: функциональные символы (нельзя строить новые термы вроде s(s(0))) и отрицание без стратификации. Плюс требование безопасности: каждая переменная головы должна встречаться в положительном литерале тела.

Что за это получаем:

Множество выводимых фактов конечно: не более чем |константы|^арность кортежей на предикат. Наивная оценка повторяет применение правил, пока множество фактов не перестанет расти; семинаивная (semi-naive) на каждой итерации использует только новые факты предыдущего шага, убирая переоткрытие уже известного — на порядки быстрее и является стандартом в промышленных движках.

% Классика статического анализа: достижимость по графу вызовов.
достижимо(X, Y) :- ребро(X, Y).
достижимо(X, Z) :- достижимо(X, Y), ребро(Y, Z).

Здесь левая рекурсия абсолютно безопасна: порядок не имеет значения, движок сам выбирает стратегию. Ровно та программа, которая вешала наш Prolog-решатель.

Где Datalog живёт в проде — и это не академия:

• Soufflé — компилирует Datalog в параллельный C++. На нём построен Doop — эталонный анализ указателей для Java; правила анализа занимают сотни строк вместо десятков тысяч строк императивного кода.
• Polonius — переформулировка borrow checker в Rust на Datalog: правила заимствований описаны декларативно, движок выводит конфликты.
• Glean в Meta — хранилище фактов о коде с языком запросов Angle, родственным Datalog; на нём работает навигация по монорепозиторию.
• Datomic и CozoDB — базы данных с Datalog вместо SQL; естественны для графовых обходов и темпоральных запросов.
• Differential Datalog — инкрементальная оценка: при изменении входных фактов пересчитывается только дельта вывода. Применялась в сетевой верификации VMware.

Практический смысл: как только задача формулируется как «вывести все следствия из набора правил и фактов» — рекурсивные запросы к графу, анализ доступов, проверка политик, транзитивные зависимости — Datalog даёт код в 10–50 раз короче императивного и не может зациклиться. В SQL то же самое выражается через WITH RECURSIVE, но многословнее и обычно медленнее на глубоких обходах.

SQL: самая успешная декларативная технология в истории

Мы пользуемся ей каждый день и редко думаем о ней как о парадигме. А зря: SQL — это буквально реализация формулы Ковальски. Вы пишете реляционную алгебру (логика); планировщик выбирает физические операторы (управление).

Практические следствия, которые отделяют инженера от «пишущего запросы»:

1. Спецификация стабильна, план — нет. Запрос, работавший 12 мс на 10 тысячах строк, на 10 миллионах может выбрать другой план и уйти в 40 секунд. Это не деградация железа, это смена решения оптимизатора.
2. EXPLAIN (ANALYZE, BUFFERS) — обязательный инструмент. Он показывает, что́ движок выбрал за вас, и главное — расхождение между rows= оценкой и actual rows. Расхождение в 100 раз означает, что статистика врёт, и дальше оптимизатор считает стоимость по фантазии.
3. Ваши рычаги — не в тексте запроса, а вокруг него: индексы, ANALYZE, расширенная статистика по коррелированным столбцам, партиционирование, переформулировка через EXISTS вместо IN. Лучший систематический справочник — Use The Index, Luke.
4. Императивщина, просочившаяся в SQL, убивает декларативность. Курсоры, LIMIT в цикле приложения, N+1 из ORM — это возврат управления в код, где оптимизатора нет.

-- Императивно по духу: приложение делает 1 + N запросов, план оптимален для каждого,
-- а суммарно — катастрофа из-за сетевых round-trip.
SELECT id FROM users WHERE active;
-- ... затем в цикле для каждого id:
SELECT count(*) FROM orders WHERE user_id = $1;

-- Декларативно: одна спецификация, движок сам выбирает hash aggregate и один проход.
SELECT u.id, count(o.id) AS orders
FROM users u
LEFT JOIN orders o ON o.user_id = u.id
WHERE u.active
GROUP BY u.id;

Разница в 100–1000 раз по времени, при этом второй вариант короче. Это типичная сигнатура удачной декларативной абстракции.

Ограничения и солверы: когда поиск отдают целиком

Следующий шаг после логического программирования — программирование в ограничениях (constraint programming). Вы описываете переменные, их домены и ограничения; решатель ищет присваивание, а как именно — его дело.

CP-SAT: расписание, которое вы не программировали

from ortools.sat.python import cp_model

employees = ["Аня", "Борис", "Вера", "Глеб"]
days = range(7)
shifts = ["утро", "вечер", "ночь"]
E, S = range(len(employees)), range(len(shifts))
night = shifts.index("ночь")

model = cp_model.CpModel()
# x[e, d, s] = 1, если сотрудник e в день d работает смену s
x = {(e, d, s): model.NewBoolVar(f"x[{e},{d},{s}]") for e in E for d in days for s in S}

# 1. Каждую смену каждого дня закрывает ровно один человек.
for d in days:
    for s in S:
        model.AddExactlyOne(x[e, d, s] for e in E)

# 2. Не больше одной смены в день на человека.
for e in E:
    for d in days:
        model.AddAtMostOne(x[e, d, s] for s in S)

# 3. После ночной смены — обязательный выходной.
for e in E:
    for d in days[:-1]:
        for s in S:
            model.AddImplication(x[e, d, night], x[e, d + 1, s].Not())

# 4. Нагрузка справедлива: 21 смена на четверых -> каждому 5 или 6.
for e in E:
    total = sum(x[e, d, s] for d in days for s in S)
    model.Add(total >= 5)
    model.Add(total <= 6)

# 5. Мягкое предпочтение: минимизируем суммарное число ночных смен у Ани.
model.Minimize(sum(x[0, d, night] for d in days))

solver = cp_model.CpSolver()
solver.parameters.max_time_in_seconds = 10.0
solver.parameters.num_search_workers = 8
status = solver.Solve(model)

if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
    for d in days:
        row = [employees[e] for s in S for e in E if solver.Value(x[e, d, s])]
        print(f"день {d}: {row}")

В этом коде нет ни одного шага поиска. Есть только описание правильного расписания. Императивная реализация с эвристиками и откатами заняла бы сотни строк и при добавлении шестого ограничения потребовала бы переписывания. Здесь добавление ограничения — это добавление трёх строк.

Сложность: задача NP-трудна, и никакой солвер этого не меняет. Что меняет солвер — константу и практическую применимость: CP-SAT сочетает распространение ограничений (propagation), CDCL-обучение из SAT, лениво генерируемые объяснения конфликтов и портфельный параллельный поиск. Расписания на десятки тысяч булевых переменных решаются за секунды — но гарантий времени нет, и max_time_in_seconds в проде обязателен.

SMT: доказать, а не протестировать

SMT-решатели (satisfiability modulo theories) добавляют к булевой логике теории — целые числа, битовые векторы, массивы, строки. Продемонстрируем на классической ошибке в бинарном поиске:

from z3 import BitVec, ZeroExt, LShR, ULE, Solver, sat

a, b = BitVec("a", 32), BitVec("b", 32)   # беззнаковые 32-битные индексы
s = Solver()
s.add(ULE(a, b))                          # предполагаем корректный отрезок: a <= b

exact = LShR(ZeroExt(32, a) + ZeroExt(32, b), 1)   # эталон: середина, посчитанная в 64 битах
buggy = ZeroExt(32, LShR(a + b, 1))                # (a + b) / 2 в 32 битах — сумма переполняется

s.add(exact != buggy)                     # ищем вход, где реализация расходится с эталоном
print(s.check())                          # sat — контрпример существует
print(s.model())                          # напр. a = 2147483648, b = 2147483648

# Исправленный вариант — a + (b - a) / 2 — расхождений не имеет:
fixed = ZeroExt(32, a + LShR(b - a, 1))
s2 = Solver(); s2.add(ULE(a, b), exact != fixed)
print(s2.check())                         # unsat — доказано для ВСЕХ 2^64 пар входов

unsat здесь — не «тесты прошли», а доказательство отсутствия контрпримера во всём пространстве входов. Именно эта разница делает SMT промышленным инструментом:

• AWS применяет автоматическое доказательство к политикам IAM и сетевым правилам — сервис Zelkova отвечает на вопрос «может ли эта политика хоть при каких-то условиях открыть доступ наружу».
• Компиляторы верифицируют оптимизации пиперхолов (проект Alive для LLVM).
• Символьное исполнение (KLEE, angr) генерирует входы, достигающие конкретных веток.
• Dafny и F* проверяют контракты функций на этапе компиляции через Z3.

Порог входа ниже, чем кажется: Z3 Guide от Microsoft Research позволяет начать за вечер.

Декларативная конфигурация: та же идея в инфраструктуре

Terraform, Kubernetes, Nix, Ansible, Bazel — это всё та же парадигма, просто предметная область другая. Вы описываете желаемое состояние, а движок вычисляет разницу с фактическим и применяет действия.

# Ни одного действия. Только утверждение о том, каким должен быть мир.
apiVersion: apps/v1
kind: Deployment
metadata:
  name: api
spec:
  replicas: 3               # «должно быть три пода», а не «запусти три пода»
  strategy:
    type: RollingUpdate
    rollingUpdate:
      maxUnavailable: 0     # ограничение на путь перехода, а не на цель
      maxSurge: 1
  template:
    spec:
      containers:
        - name: api
          image: registry.example.com/api:1.42.0
          resources:
            requests: { cpu: "250m", memory: "256Mi" }
            limits:   { memory: "512Mi" }

Разница между «запусти три пода» и «должно быть три пода» — фундаментальная. Первое выполняется один раз. Второе — инвариант, который непрерывно восстанавливается. Убили под руками — контроллер поднимет новый; упала нода — поды переедут. Это паттерн контроллера, и он же — суть Terraform и GitOps.

Из этой картинки вытекают все практические правила декларативной инфраструктуры:

• Ручное изменение — это баг. Любое kubectl edit мимо репозитория будет затёрто следующим reconcile либо, что хуже, создаст дрейф, который вылезет в неудобный момент. Отсюда GitOps: единственный источник истины — репозиторий.
• Провайдер обязан быть идемпотентным. Ресурс, чей create не идемпотентен, при повторе цикла плодит дубликаты.
• Декларативность не отменяет порядок. У ресурсов есть зависимости; Terraform строит DAG и обходит его — это тот же «control», просто выведенный автоматически. depends_on — ручное вмешательство в управление, полный аналог отсечения в Prolog.
• Прочитайте план перед применением. terraform plan — прямой аналог EXPLAIN: он показывает, какое «как» движок вывел из вашего «что». Пропуск этого шага — источник большинства инцидентов.

Цена: где абстракция протекает

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

Отсюда — правила эксплуатации:

1. Всегда ставьте бюджет. statement_timeout в PostgreSQL, max_time_in_seconds у солвера, лимит инференций в Prolog. Декларативная система без таймаута — это неограниченный риск.
2. Мониторьте план, а не только время. Внезапная смена плана — событие, достойное алерта, часто раньше, чем деградация станет видна пользователю.
3. Знайте рычаги своего движка и применяйте их в порядке возрастания насилия: сначала статистика и индексы, затем переформулировка, и только в крайнем случае hints/!/depends_on, которые прибивают управление гвоздями и лишают вас будущих улучшений оптимизатора.
4. Понимайте модель выполнения. «Декларативно» не значит «можно не знать, как работает». Значит «можно не писать, как работает». Разница огромна.

Типичные ошибки

• Считать декларативность бинарной. Она относительна. Полезный вопрос не «декларативен ли язык», а «какие решения он забирает у меня и вернёт ли обратно, когда понадобится».
• Левая рекурсия в Prolog. Логически верно, операционно — зависание. Либо ставьте базовый случай первым и рекурсивную цель последней, либо включайте табулирование.
• Красное отсечение как способ «сделать if». Программа перестаёт быть обратимой и читаемой. Пишите явные взаимоисключающие условия.
• \+ по несвязанным переменным. Даёт молча неверный ответ. Сначала конкретизируйте, потом отрицайте.
• Забыть про closed-world assumption. «Нет в базе» ≠ «ложно в реальности». Для баз знаний с неполнотой нужны другие формализмы (OWL, вероятностные модели).
• Нестратифицированное отрицание в Datalog. p :- \+ q. q :- \+ p. не имеет единственной модели. Промышленные движки такие программы отвергают — и правильно делают.
• Рекурсивный SQL без ограничителя глубины. WITH RECURSIVE на графе с циклом крутится вечно. Ведите массив посещённых узлов или ставьте лимит уровня.
• Ожидать гарантий времени от NP-трудного солвера. Инстанс на 200 переменных может решиться за 5 мс, соседний — за час. В проде это всегда «лучшее решение за отведённый бюджет», а не «оптимум».
• Императивные острова внутри декларативной системы. N+1 из ORM, курсоры, local-exec в Terraform, ручные kubectl — каждый такой остров отключает движок ровно там, где он был нужнее всего.
• Переносить декларативность туда, где нет движка. DSL без оптимизатора — это не декларативность, а просто конфигурация с плохим синтаксисом. Про границы такого дизайна — в статье об обобщённом программировании и метапрограммировании.

Как выбирать: где парадигма реально выигрывает

Берите декларативный подход, когда выполняются два условия сразу: (1) пространство решений велико и структурировано, и (2) существует зрелый движок, который обходит его лучше, чем вы напишете руками. Практически это: запросы к данным (SQL); вывод следствий из правил — анализ кода, политики доступа, транзитивные зависимости (Datalog, рекурсивный SQL); комбинаторное распределение — расписания, маршруты, раскрой (CP-SAT, MiniZinc); доказательство свойств (Z3); управление инфраструктурой (Terraform, Kubernetes, Nix); разбор и валидация (грамматики, JSON Schema).

И не берите, когда: логика по природе последовательна (ввод-вывод, протоколы, UI-взаимодействия — там уместнее реактивный подход); когда нужна жёсткая гарантия времени отклика; когда команда не готова отлаживать через план вместо отладчика; когда задача проще движка, который вы тащите ради неё.

Реалистичная архитектура — гибрид: декларативное ядро (запросы, правила, ограничения) внутри императивной оболочки, которая занимается вводом-выводом, таймаутами и деградацией. Ровно та же структура, что «функциональное ядро — императивная оболочка» из статьи про ФП. Как их сочетать осознанно — тема финальной статьи трека.

Мини-итог

• Algorithm = Logic + Control. Декларативность — это передача управления движку, а не «отсутствие как».
• Декларативность относительна и измеряется устойчивостью текста программы к смене стратегии выполнения.
• Логическое программирование строится на трёх вещах: хорновские клаузы, унификация (двусторонняя, O(n·α(n)) при правильной реализации), SLD-резолюция с обходом в глубину и откатом.
• Обратимость предикатов — уникальный козырь: одна программа работает как проверка, поиск в обе стороны и генератор.
• Отсечение, \+ и замкнутый мир — места, где чистая декларативность Prolog ломается; красных отсечений избегайте, отрицание применяйте только к связанным переменным.
• Datalog жертвует полнотой по Тьюрингу и получает гарантии: завершение всегда, PTIME по данным, независимость от порядка клауз. Отсюда его промышленный успех в статическом анализе и графовых запросах.
• SQL — самая массовая декларативная технология; EXPLAIN обязателен, потому что план меняется, а текст запроса — нет.
• Солверы (CP-SAT, Z3) решают NP-трудные задачи практически, но без гарантий времени — бюджет обязателен.
• Декларативная инфраструктура — это цикл согласования; отсюда требование идемпотентности и запрет ручных изменений.
• Главная цена: потеря локального контроля над производительностью. Компенсируется знанием модели выполнения, наблюдаемостью плана и таймаутами.

Источники

• Robert Kowalski. Algorithm = Logic + Control (CACM, 1979) — работа, задающая рамку всей парадигмы.
• J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle (JACM, 1965) — резолюция и унификация.
• Alberto Martelli, Ugo Montanari. An Efficient Unification Algorithm (TOPLAS, 1982).
• Leon Sterling, Ehud Shapiro. «The Art of Prolog», 2-е изд. — лучший учебник по логическому программированию.
• Ivan Bratko. «Prolog Programming for Artificial Intelligence», 4-е изд. — практический уклон.
• Serge Abiteboul, Richard Hull, Victor Vianu. Foundations of Databases — бесплатно; главы 12–15 про Datalog и его сложность.
• Todd J. Green и др. Datalog and Recursive Query Processing (Foundations and Trends in Databases, 2013).
• SWI-Prolog: документация и раздел про tabling.
• Soufflé — Datalog для статического анализа; Polonius — borrow checker Rust на Datalog.
• Glean — индексация кода на фактах и правилах.
• Google OR-Tools: CP-SAT и MiniZinc — программирование в ограничениях.
• Z3 Guide и репозиторий Z3; Dafny — верификация через SMT.
• Zelkova: автоматическое доказательство для политик AWS.
• Markus Winand. Use The Index, Luke — как влиять на планировщик SQL, не ломая декларативность.
• PostgreSQL: Using EXPLAIN и планировщик.
• Kubernetes: Controllers — цикл согласования как парадигма.
• Joel Spolsky. The Law of Leaky Abstractions.

Что дальше

Мы отдали движку управление порядком вычислений — и увидели, что это работает, пока движок один и он умнее нас. Но существует класс задач, где порядок не выбирается оптимизатором, а определяется внешним миром: несколько потоков управления идут одновременно, и «правильного» порядка попросту нет. Этим занимается следующая статья трека: Конкурентные парадигмы: акторы, CSP, STM, разделяемая память. Там мы увидим, как парадигмы предлагают разные ответы на один вопрос — что делать с состоянием, к которому обращаются одновременно, — и почему модель, в которой состояния попросту нет, оказалась самой живучей.