Логическое программирование

Что если бы вместо написания алгоритма поиска можно было просто описать, что нужно найти, и компьютер сам разобрался как? Именно это делает логическое программирование. Sudoku на Prolog - 10 строк. SEND+MORE=MONEY - 15 строк. Timetabling для университета - 50 строк.

• **Erlang**: синтаксис pattern matching и унификации прямо из Prolog - Ericsson сделал из Prolog-идей производительный concurrent язык для телекоммуникаций
• **TypeScript type inference**: алгоритм вывода типов использует унификацию - когда TS выводит тип generic функции, это тот же алгоритм Робинсона что и в Prolog
• **Google Optimization Tools (OR-Tools)**: constraint programming внутри решает задачи fleet routing для Google Maps, vehicle scheduling для логистики Amazon

Prolog и Resolution

В Prolog программа - это набор фактов и правил (Horn clauses). Запрос - цель, которую система пытается доказать. Вместо написания алгоритма программист описывает отношения между объектами, а Prolog сам ищет решение через SLD-resolution.

Prolog используется в: IBM Watson (частично), Erlang (синтаксис заимствован), GNU Prolog для constraint solving. Amazon Alexa использует Prolog-подобный движок для NLP.

Унификация

Унификация - алгоритм нахождения подстановки переменных, при которой два терма становятся идентичными. Это ключевая операция в Prolog, а также в системах типов (Hindley-Milner type inference) и pattern matching.

Алгоритм Робинсона (1965) для унификации: O(n) с union-find. Hindley-Milner type inference в Haskell/OCaml использует ту же унификацию для вывода типов. Когда GHC говорит 'Cannot match Int with Bool' - это провал унификации.

Бэктрекинг

Когда Prolog не может доказать цель с текущими привязками, он откатывается (backtrack) к последней точке выбора и пробует следующую альтернативу. Это автоматический поиск в пространстве решений через depth-first search.

Prolog бэктрекинг - DFS по дереву доказательств. Для задачи N Queens с N=8 Prolog решает за миллисекунды. Для N=20 - может потребоваться секунды без оптимизаций. Constraint Logic Programming резко сокращает пространство поиска.

Constraint Logic Programming

CLP расширяет Prolog ограничениями (constraints) вместо чистой унификации. Вместо перебора всех значений система распространяет ограничения и сразу отсекает невозможные области. CLP(FD) для целых чисел, CLP(R) для вещественных.

Современные применения: Minizinc (constraint modeling language) для scheduling, timetabling, resource allocation. Google OR-Tools (C++/Python) использует CLP внутри. Clojure.core.logic - миниатюрный Prolog в Clojure.

Ключевые идеи

• **Prolog** - декларативная парадигма: описываем что верно (факты + правила), система сама доказывает через SLD-resolution
• **Унификация** - алгоритм нахождения подстановки переменных. Та же основа у Hindley-Milner type inference в Haskell/OCaml
• **Бэктрекинг** - автоматический DFS по дереву доказательств. cut (!) прекращает бэктрекинг
• **CLP** - ограничения вместо перебора. SEND+MORE=MONEY: 10^8 -> ~1000 проверок благодаря propagation

Связанные темы

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

• Системы типов — Hindley-Milner type inference - это унификация, заимствованная из логического программирования
• Верификация программ — Model checking и theorem provers используют те же формальные методы

Вопросы для размышления

• Унификация в Prolog и type inference в Haskell используют один алгоритм. Что это говорит о глубинной связи между логикой и системами типов?
• Бэктрекинг - сложный инструмент, но может быть экспоненциально медленным. Когда стоит использовать CLP вместо чистого Prolog?
• Clojure.core.logic позволяет вставлять логическое программирование в обычный Clojure код. Как бы вы использовали это для задачи поиска конфигурации в системе с зависимостями?

Связанные уроки

• logic-29-predicates-intro