Logic Programming in Swift

21 December 2016

Today I open-sourced 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 to 0; set i to 0; check that i is less than array.count; add array[i] to sum; repeat.

This is imperative programming.

Declarative programming tells the computer what something is without describing all the individual steps:

sum is the reduction of array that starts with 0 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)
1. Each queen is on a different row
2. Each queen is on a different column
3. Each queen is on a different forward diagonal
4. Each queen is on a different backward diagonal
Sudoku (Logician implementation)
1. All numbers are 1 through 9
2. Each row has exactly one of each number
3. Each column has exactly one of each number
4. Each subgrid has exactly one of each number
Map Coloring
1. Each region is one of n colors
2. Each region is different from all of its neighbors
Dependency Resolver
1. Each project is one of a set number of versions
2. Each dependency can have one of a set of pre-defined 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 non-variable value of a variable

If a == b and b == 7, the reified value of a is 7, even though it might be stored as a == b. If a == b is the only constraint, then a and b have no reified value.
Unification: Combining two sets of constraints, erroring if they're inconsistent

a == 5 and b == 6 unify, but a == 5 and a == 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 variable--following 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 Ints), 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.

If you’d like to learn more about logic programming, the Logician README has a Learn More section with links to some great resources.

Matt Diephouse

Logic Programming in Swift

Why Logic Programming?

Example Applications

How Logic Programming Works

Read More