Logic Programming in Swift
Today I opensourced Logician, a Swift logic programming library. Since I suspect most people don’t know much about logic programming, I wanted to explain a bit about logic programming, what it’s good for, and how it works.
Why Logic Programming?
Most programs tell a computer exactly what to do, step by step:
Set
sum
to0
; seti
to0
; check thati
is less thanarray.count
; addarray[i]
tosum
; repeat.
This is imperative programming.
Declarative programming tells the computer what something is without describing all the individual steps:
sum
is the reduction ofarray
that starts with0
and adds each element to the total.
Logic programming is a form of declarative programming that describes the solution instead of the calculation. Based on that description, the computer solves the problem. Describing a solution to a problem can be a far easier than devising a method to solve it, which is why logic programming can be appealing.
Example Applications
I find most logic programming examples to be uninteresting and uninspiring. Usually they mention artificial intelligence and involve some sort of fact database. Since I can’t imagine ever needing to solve a problem like that, I had never been very interested in logic programming.
But there are other problems that can be solved with logic programming. Here are a few examples that I find more interesting and the constraints that describe the solution:
N Queens (Logician implementation)
 Each queen is on a different row
 Each queen is on a different column
 Each queen is on a different forward diagonal
 Each queen is on a different backward diagonal
Sudoku (Logician implementation)
 All numbers are 1 through 9
 Each row has exactly one of each number
 Each column has exactly one of each number
 Each subgrid has exactly one of each number

 Each region is one of n colors
 Each region is different from all of its neighbors
Dependency Resolver
 Each project is one of a set number of versions
 Each dependency can have one of a set of predefined constraints
Most of us don’t solve these sorts of problems in our day to day work, but these problems do need to be solved occasionally. And while I can envision solving them with logic programming, solving them imperatively or functionally would be quite a bit of work.
How Logic Programming Works
In logic programming, constraints establish relationships between variables (unknowns) and values (knowns). To solve a problem, you express the constraints and ask the solver for valid solutions.
This is not unlike algebra: x * 2 + y * 2 == 16
can be thought of as a constraint. Solving the problem establishes a value for all variables. In this case, valid solutions include (x = 1, y = 7)
, (x = 2, y = 6)
, etc.
Constraints are stored in a data structure that we'll call State
. Finding solutions requires two different operations on the state:
Reification: Resolving the nonvariable value of a variable
If
a == b
andb == 7
, the reified value ofa
is7
, even though it might be stored asa == b
. Ifa == b
is the only constraint, thena
andb
have no reified value.Unification: Combining two sets of constraints, erroring if they're inconsistent
a == 5
andb == 6
unify, buta == 5
anda == 7
are inconsistent—a
can't have two different values. The state signals that a constraint has been violated by throwing or returning an error.
There are a number of ways that you can implement unification and reification. One simple way is to use a dictionary of variables to variables/values.
/// An unknown value used in a logic problem.
/// The identity of the object serves as the identity of the variable.
class Variable: Hashable {
static func ==(lhs: Variable, rhs: Variable) > Bool {
return lhs === rhs
}
var hashValue: Int {
return ObjectIdentifier(self).hashValue
}
}
class State {
/// An assignment of a value/variable to a variable. Since the
/// value can be either a variable or a value, an enum is used.
enum Term {
case variable(Variable)
case value(Int)
}
/// The assignments of variables/values to variables. This is just
/// one possible approach.
var substitutions: [Variable: Term]
/// Look up the actual value of a variablefollowing intermediate
/// variables until the actual value is found.
func reify(_ variable: Variable) > Int? {
switch substitutions[variable] {
case let .variable(variable)?:
return reify(variable)
case let .value(value)?:
return value
case .none:
return nil
}
}
/// Unify two variables, erroring if they have inconsistent values.
mutating func unify(_ a: Variable, _ b: Variable) throws {
if let a = reify(a), let b = reify(b), a != b {
throw Inconsistent
}
substitutions[a] = Term.variable(b)
}
/// Unify a variable and a value, erroring if the variable has an
/// existing, inconsistent value.
mutating func unify(_ a: Variable, _ b: Int) throws {
if let a = reify(a), a != b {
throw Inconsistent
}
substitutions[a] = Term.value(b)
}
}
A solver uses unification and reification to find solutions to logic problems. This is a complex subject, with room for lots of optimization. But a simple approach, modeled by μKanren, is to represent constraints with goals—blocks that build an infinite lazy stream.
/// Something that generates values and can be iterated over.
class Generator<Value>: IteratorProtocol {
func next() > Value?
}
/// A block that takes a state and produces a generator (stream) of
/// possible states.
typealias Goal = (State) > Generator<State>
If a goal returns an empty stream, it yields no solutions; if it returns a stream with multiple values, there are multiple viable solutions.
Creating a goal is easy.
func goal(_ block: @escaping (State) throws > (State)) > Goal {
return { state in
do {
let state = try block(state)
return Generator(values: [ state ])
} catch {
return Generator()
}
}
}
func == (variable: Variable, value: Int) > Goal {
// A goal that will return either 0 or 1 values.
return goal { try $0.unifying(variable, value) }
}
Goals handle the unification, but we still need to reify the solutions. To do so, we use a solve
function that introduces a new variable, solves for a goal, and then reifies that variable.
extension Generator {
/// Apply a function to every value created by the generator,
/// resulting in a new generator that returns the the new
/// non`nil` values.
func flatMap<New>(_ transform: (Value) > New?) > Generator<New>
}
func solve<Value>(_ block: (Variable) > Goal) > Generator<Int> {
let variable = Variable()
let goal = block(variable)
let initial = State()
return goal(initial).flatMap { return $0.reify(variable) }
}
That's all it takes. (But you probably want a few more constraints—at least &&
and 
.) This is a simplified version of Logician's current solver, but it highlights the core concepts.
Logician has many more features, including different value types (not just Int
s), inequality constraints, mapping over variables, constraints on properties of a variable, etc. It’s still very naïve; but I hope that it can develop into a sophisticated logic solver.
Read More
If you’d like to learn more about logic programming, the Logician README has a Learn More section with links to some great resources.