Logic Programming

What if, instead of writing a search algorithm, you could just describe what to find and the computer figured out how? That is exactly what logic programming does. Sudoku in Prolog: 10 lines. SEND+MORE=MONEY: 15 lines. University timetabling: 50 lines.

• **Erlang**: pattern matching and unification syntax came directly from Prolog. Ericsson turned Prolog ideas into a high-performance concurrent language for telecoms
• **TypeScript type inference**: the type inference algorithm uses unification. When TS infers the type of a generic function, it runs the same Robinson algorithm as Prolog
• **Google OR-Tools**: constraint programming inside solves fleet routing for Google Maps and vehicle scheduling for Amazon logistics

Prolog and Resolution

In Prolog a program is a set of facts and rules (Horn clauses). A query is a goal the system tries to prove. Instead of writing an algorithm, the programmer describes relationships between objects and Prolog finds the solution itself via SLD-resolution.

Prolog is used in IBM Watson (in part), Erlang (which borrowed its syntax), and GNU Prolog for constraint solving. Amazon Alexa uses a Prolog-style engine for NLP.

Unification

Unification is the algorithm for finding a variable substitution that makes two terms identical. It is the key operation in Prolog, and the same operation drives type systems (Hindley-Milner type inference) and pattern matching.

Robinson's algorithm (1965) does unification in O(n) with union-find. Hindley-Milner type inference in Haskell/OCaml uses the same unification to infer types. When GHC says 'Cannot match Int with Bool', it is reporting a unification failure.

Backtracking

When Prolog cannot prove a goal with the current bindings, it backtracks to the last choice point and tries the next alternative. This is automatic search through the solution space via depth-first search.

Prolog backtracking is DFS over a proof tree. For N Queens with N=8, Prolog finishes in milliseconds. For N=20, it can take seconds without optimizations. Constraint Logic Programming shrinks the search space dramatically.

Constraint Logic Programming

CLP extends Prolog with constraints instead of plain unification. Rather than enumerating every value, the system propagates constraints and immediately prunes impossible regions. CLP(FD) handles integers, CLP(R) handles reals.

Modern uses include Minizinc (a constraint modeling language) for scheduling, timetabling, and resource allocation. Google OR-Tools (C++/Python) uses CLP internally. Clojure.core.logic is a miniature Prolog embedded in Clojure.

Key Ideas

• **Prolog**: a declarative paradigm. We describe what is true (facts plus rules), and the system proves it via SLD-resolution
• **Unification**: an algorithm for finding a variable substitution. The same machinery underlies Hindley-Milner type inference in Haskell/OCaml
• **Backtracking**: automatic DFS over the proof tree. The cut (!) stops backtracking
• **CLP**: constraints replace brute force. SEND+MORE=MONEY: 10^8 down to ~1000 checks thanks to propagation

Related Topics

Logic programming influences type systems and other languages:

• Type systems — Hindley-Milner type inference is unification, borrowed from logic programming
• Program verification — Model checking and theorem provers use the same formal methods

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

• Unification in Prolog and type inference in Haskell use the same algorithm. What does this say about the deep link between logic and type systems?
• Backtracking is a powerful tool, yet it can be exponentially slow. When should you reach for CLP rather than plain Prolog?
• Clojure.core.logic lets you drop logic programming into ordinary Clojure code. How would you use it to search for a configuration in a system with dependencies?

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

• logic-29-predicates-intro