Logic programming and other paradigms

Most of this course has treated programs as functions or as sequences of commands. Logic programming takes a different view: a program is a set of facts and rules in a fragment of first-order logic, and running it means asking whether a query follows from them. The programmer says what is true; the language's search procedure works out how to find answers. This lesson builds a working miniature Prolog in Python, using the unification algorithm from lesson 8, and uses it to explore resolution, backtracking, relations that run in several directions, and the cut. It then looks at constraint programming and Datalog, close relatives of Prolog, and closes with the main concurrency paradigms: shared memory, message passing with channels, actors and event loops. SWI-Prolog is not installed here, so every logic program below runs on our own engine.

Facts, rules and queries

Prolog was created by Alain Colmerauer and Philippe Roussel in Marseille in 1972, building on Robert Kowalski's procedural interpretation of logic. A Prolog program consists of clauses. A fact such as parent(tom, bob). states something true. A rule such as grandparent(X, Z) :- parent(X, Y), parent(Y, Z). reads 'X is a grandparent of Z if X is a parent of some Y and Y is a parent of Z'. Variables start with a capital letter and are implicitly universally quantified over the clause. A query such as ?- grandparent(tom, W). asks for all W that make the goal true. Clauses of this shape, with one conclusion and a conjunction of conditions, are Horn clauses, named after Alfred Horn, and they are what makes efficient proof search possible.

The meaning of a logic program can be given in two equivalent ways, echoing lesson 3. The declarative (model-theoretic) semantics says that the program denotes its least Herbrand model: the smallest set of ground facts closed under the rules. The operational semantics is SLD resolution, Selective Linear Definite clause resolution: to prove a list of goals, select the first goal, find a clause whose head unifies with it, and replace the goal with that clause's body under the unifier. Kowalski and Maarten van Emden proved in 1976 that the two semantics agree.

A Prolog engine in Python

Our engine represents terms as Python values: a capitalized string is a variable, a lower-case string is an atom, and a tuple is a compound term whose first element is the functor. Unification is the algorithm from lesson 8, without an occurs check, as in standard Prolog. Each time a clause is used, its variables are renamed apart so that different uses do not interfere. The solver is a Python generator: it yields one substitution per solution, and backtracking happens naturally when the caller asks for the next one.

# A miniature Prolog: terms, unification and SLD resolution with depth-first search.
# A term is a variable "X" (capitalized string), an atom "tom", or a tuple (functor, args...).
import itertools
fresh_ids = itertools.count()

def is_var(t): return isinstance(t, str) and t[:1].isupper()

def walk(t, s):
    while is_var(t) and t in s: t = s[t]
    return t

def unify(a, b, s):
    a, b = walk(a, s), walk(b, s)
    if a == b: return s
    if is_var(a): return {**s, a: b}
    if is_var(b): return {**s, b: a}
    if isinstance(a, tuple) and isinstance(b, tuple) and len(a) == len(b) and a[0] == b[0]:
        for x, y in zip(a[1:], b[1:]):
            s = unify(x, y, s)
            if s is None: return None
        return s
    return None

def rename(t, m):                          # give each clause use its own variables
    if is_var(t): return m.setdefault(t, f"{t}_{next(fresh_ids)}")
    if isinstance(t, tuple): return (t[0],) + tuple(rename(a, m) for a in t[1:])
    return t

def solve(goals, s, db, depth=0):
    if not goals: yield s; return
    first, rest = goals[0], goals[1:]
    if first[0] == "neq":                  # built-in: succeeds if both sides differ
        if walk(first[1], s) != walk(first[2], s): yield from solve(rest, s, db, depth)
        return
    for head, body in db:
        m = {}
        h, b = rename(head, m), [rename(g, m) for g in body]
        s2 = unify(first, h, s)
        if s2 is not None:
            yield from solve(b + rest, s2, db, depth + 1)

def resolve_all(t, s):
    t = walk(t, s)
    return (t[0],) + tuple(resolve_all(a, s) for a in t[1:]) if isinstance(t, tuple) else t

facts = [("parent", "tom", "bob"), ("parent", "tom", "liz"), ("parent", "bob", "ann"),
         ("parent", "bob", "pat"), ("parent", "pat", "jim")]
db = [(f, []) for f in facts] + [
    (("grandparent", "X", "Z"), [("parent", "X", "Y"), ("parent", "Y", "Z")]),
    (("sibling", "X", "Y"), [("parent", "P", "X"), ("parent", "P", "Y"), ("neq", "X", "Y")]),
    (("ancestor", "X", "Y"), [("parent", "X", "Y")]),
    (("ancestor", "X", "Y"), [("parent", "X", "Z"), ("ancestor", "Z", "Y")]),
]

def query(goal, var):
    return [resolve_all(var, s) for s in solve([goal], {}, db)]

print("?- grandparent(tom, W).    W =", query(("grandparent", "tom", "W"), "W"))
print("?- sibling(ann, S).        S =", query(("sibling", "ann", "S"), "S"))
print("?- ancestor(A, jim).       A =", query(("ancestor", "A", "jim"), "A"))
print("?- parent(jim, _).         ", query(("parent", "jim", "Q"), "Q") or "false.")

$ python3 -I prolog.py
?- grandparent(tom, W).    W = ['ann', 'pat']
?- sibling(ann, S).        S = ['pat']
?- ancestor(A, jim).       A = ['pat', 'tom', 'bob']
?- parent(jim, _).          false.

Each query returns every answer, in the order Prolog would find them. ancestor(A, jim) finds jim's parent pat first through the base clause, then tom and bob through the recursive clause: tom comes before bob because the recursive clause tries parent facts in database order, and tom's facts come first. The last query fails, which Prolog reports as false: under the closed-world assumption, whatever cannot be proved is taken to be false. This is negation as failure, and it is not classical negation: Prolog's \+ goal succeeds when goal cannot be proved, which is sound only when the goal has no unbound variables.

The search tree

SLD resolution defines a search tree. Each node is a list of goals still to prove; each branch corresponds to a clause whose head unifies with the first goal; leaves are either success (an empty goal list) or failure (no clause matches). Prolog explores this tree depth first, trying clauses in program order and backtracking to the most recent choice point when a branch fails. The trace below prints every node for the grandparent query, indented by depth.

# SLD resolution explores a tree of goal lists depth first. Print the trace for one query.
exec(open("prolog.py").read().split("def query")[0])
def trace(goals, s, depth=0):
    shown = ", ".join(str(resolve_all(g, s)).replace("'", "") for g in goals) or "success"
    print("  " * depth + shown)
    if not goals: return
    first, rest = goals[0], goals[1:]
    for head, body in db:
        m = {}; h, b = rename(head, m), [rename(g, m) for g in body]
        s2 = unify(first, h, s)
        if s2 is not None: trace(b + rest, s2, depth + 1)
trace([("grandparent", "tom", "W")], {})

$ python3 -I trace.py
(grandparent, tom, W)
  (parent, tom, Y_3), (parent, Y_3, Z_1)
    (parent, bob, Z_1)
      success
      success
    (parent, liz, Z_1)

Depth-first search is efficient in memory but incomplete: if the tree has an infinite branch to the left of a solution, Prolog never finds the solution. Writing ancestor(X, Y) :- ancestor(Z, Y), parent(X, Z). first, with left recursion, sends Prolog into an infinite loop even though the logic is the same. So Prolog programmers must think about clause and goal order, which is a step away from purely declarative programming. Tabling, available in SWI-Prolog and XSB, memoizes goals to make such programs terminate.

Relations, not functions

Because a Prolog predicate is a relation, the same definition can often be run in several directions. The classic example is append, which relates two lists to their concatenation. Asked to concatenate, it computes; asked which two lists concatenate to a given list, it enumerates every split. Lists in Prolog are built from cons cells, written [H|T], ending in the empty list [].

# Relations run in several directions: append/3 used forwards and backwards.
exec(open("prolog.py").read().split("facts = [")[0])      # reuse the engine above

def lst(*xs):                                            # build a Prolog list [x1, ..., xn]
    t = "nil"
    for x in reversed(xs): t = ("cons", x, t)
    return t
def show(t):
    out = []
    while isinstance(t, tuple) and t[0] == "cons": out.append(t[1]); t = t[2]
    return "[" + ",".join(map(str, out)) + "]" if t == "nil" else str(t)

db = [(("append", "nil", "L", "L"), []),
      (("append", ("cons", "H", "T"), "L", ("cons", "H", "R")), [("append", "T", "L", "R")])]

s = next(solve([("append", lst(1, 2), lst(3), "Out")], {}, db))
print("append([1,2], [3], Out):  Out =", show(resolve_all("Out", s)))
for s in solve([("append", "X", "Y", lst(1, 2, 3))], {}, db):
    print("append(X, Y, [1,2,3]):    X =", show(resolve_all("X", s)).ljust(8), "Y =", show(resolve_all("Y", s)))

$ python3 -I append.py
append([1,2], [3], Out):  Out = [1,2,3]
append(X, Y, [1,2,3]):    X = []       Y = [1,2,3]
append(X, Y, [1,2,3]):    X = [1]      Y = [2,3]
append(X, Y, [1,2,3]):    X = [1,2]    Y = [3]
append(X, Y, [1,2,3]):    X = [1,2,3]  Y = []

Control: the cut

The cut, written !, is Prolog's main control operator. When a cut is reached in a clause body, Prolog commits to the choices made since the clause was selected: it will not try other clauses for the same goal, nor other solutions for goals to the left of the cut. A 'green' cut only removes branches that could not succeed anyway, so it improves efficiency without changing meaning. A 'red' cut changes the answers. For example, max(X, Y, X) :- X >= Y, !. max(X, Y, Y). works for queries like max(3, 1, M), but the query max(3, 1, 1) wrongly succeeds, because the first clause's head does not unify and the second clause, written as if the cut had already excluded the case X >= Y, accepts it. Programs that depend on red cuts lose their logical reading.

Constraint programming

Constraint logic programming, formalized by Joxan Jaffar and Jean-Louis Lassez in 1987, replaces unification over terms with constraint solving over a domain such as integers, reals or finite sets. Instead of generating candidate values and testing them, a constraint solver propagates constraints to shrink each variable's domain and only searches over what remains. SWI-Prolog's clpfd library, MiniZinc, Google's OR-Tools and the Z3 solver all work this way, and they are used for scheduling, timetabling, configuration and verification. The classic toy problem is SEND + MORE = MONEY, where each letter stands for a different digit.

# Constraint programming: SEND + MORE = MONEY by backtracking search with pruning.
import itertools, time

def solve_puzzle():
    letters = "SENDMORY"
    nodes = 0
    def value(word, a): return int("".join(str(a[c]) for c in word))
    def consistent(a):
        # prune using the units column as soon as D, E and Y are known
        if all(c in a for c in "DEY") and (a["D"] + a["E"]) % 10 != a["Y"]: return False
        if "M" in a and a["M"] != 1: return False         # the carry into MONEY's first digit
        return True
    def search(a, used):
        nonlocal nodes
        nodes += 1
        if len(a) == len(letters):
            return a if value("SEND", a) + value("MORE", a) == value("MONEY", a) else None
        c = letters[len(a)]
        for d in range(10):
            if d in used or (d == 0 and c in "SM"): continue
            a[c] = d
            if consistent(a):
                r = search(a, used | {d})
                if r: return r
            del a[c]
        return None
    return search({}, frozenset()), nodes

sol, nodes = solve_puzzle()
print(" ".join(f"{k}={v}" for k, v in sol.items()))
print(f"{''.join(str(sol[c]) for c in 'SEND')} + {''.join(str(sol[c]) for c in 'MORE')} = {''.join(str(sol[c]) for c in 'MONEY')}")
print("search nodes visited:", nodes, " versus", 10 * 9 * 8 * 7 * 6 * 5 * 4 * 3, "full assignments")

S=9 E=5 N=6 D=7 M=1 O=0 R=8 Y=2
9567 + 1085 = 10652
search nodes visited: 85228  versus 1814400 full assignments

Even two simple constraints, the units column and the leading carry, cut the search to a small fraction of the 1,814,400 possible assignments of eight distinct digits. Real solvers propagate every column's constraint, with carries, and solve this puzzle with almost no search.

Datalog and bottom-up evaluation

Datalog is Prolog without compound terms: only atoms, variables and relations. That restriction guarantees termination, since there are finitely many possible facts, and allows bottom-up evaluation: start from the facts and apply every rule repeatedly until no new facts appear, reaching the least fixed point, the least model from the declarative semantics above. Datalog is the theory behind recursive SQL queries (WITH RECURSIVE), and it is used for program analysis (the Soufflé engine and CodeQL), network configuration and access control.

# Datalog: bottom-up evaluation to a fixed point, the way deductive databases work.
edges = {("a", "b"), ("b", "c"), ("c", "d"), ("d", "b"), ("e", "a")}
path = set(edges)                           # path(X, Y) :- edge(X, Y).
rounds = 0
while True:                                 # path(X, Z) :- path(X, Y), edge(Y, Z).
    rounds += 1
    new = {(x, z) for (x, y) in path for (y2, z) in edges if y == y2} - path
    if not new: break
    path |= new
print("rounds to fixed point:", rounds)
print("reachable from e:", sorted(z for x, z in path if x == "e"))
print("on a cycle:", sorted(x for x, z in path if x == z))

rounds to fixed point: 4
reachable from e: ['a', 'b', 'c', 'd']
on a cycle: ['b', 'c', 'd']

Concurrency paradigms

Concurrency is another axis along which languages differ sharply. The oldest model is shared memory with locks, as in C with POSIX threads or Java's synchronized, which CMPUT-379 studies at the system level. Its dangers, data races and deadlocks, have pushed language designers toward models that structure communication. Tony Hoare's communicating sequential processes (CSP, 1978) connect independent processes by synchronous channels; Go's goroutines and channels follow it directly, with the motto 'do not communicate by sharing memory; share memory by communicating'.

package main

import "fmt"

// Communicating sequential processes (Hoare, 1978): goroutines share memory by communicating.
func generate(n int, out chan<- int) {
	for i := 2; i <= n; i++ {
		out <- i
	}
	close(out)
}

func filter(prime int, in <-chan int, out chan<- int) {
	for x := range in {
		if x%prime != 0 {
			out <- x
		}
	}
	close(out)
}

func main() {
	ch := make(chan int)
	go generate(50, ch)
	var primes []int
	for {
		p, ok := <-ch
		if !ok {
			break
		}
		primes = append(primes, p)
		next := make(chan int)
		go filter(p, ch, next) // a pipeline stage per prime found
		ch = next
	}
	fmt.Println(len(primes), "primes:", primes)
}

15 primes: [2 3 5 7 11 13 17 19 23 29 31 37 41 43 47]

Carl Hewitt's actor model (1973) gives each actor private state and a mailbox; actors interact only by sending asynchronous messages, and each processes its messages one at a time. Erlang, designed at Ericsson in the 1980s for telephone switches, built a whole language around actors with 'let it crash' supervision trees, and Akka brings the model to the JVM. Because only the actor touches its state, no locks are needed.

# Actors (Hewitt, 1973): isolated state, asynchronous messages, one mailbox each.
import queue, threading

class Counter(threading.Thread):
    def __init__(self):
        super().__init__(); self.mailbox = queue.Queue(); self.count = 0
    def run(self):
        while True:
            msg, reply = self.mailbox.get()
            if msg == "inc": self.count += 1           # only this thread touches count
            elif msg == "get": reply.put(self.count)
            elif msg == "stop": return

c = Counter(); c.start()
def worker():
    for _ in range(10_000): c.mailbox.put(("inc", None))
threads = [threading.Thread(target=worker) for _ in range(4)]
for t in threads: t.start()
for t in threads: t.join()
answer = queue.Queue(); c.mailbox.put(("get", answer))
print("count after 4 x 10000 increments:", answer.get())
c.mailbox.put(("stop", None))

count after 4 x 10000 increments: 40000

JavaScript takes yet another approach: one thread, an event loop and a queue of callbacks. Long operations such as timers and network requests never block; they schedule a callback for later. Promises and async/await, added in ECMAScript 2015 and 2017, let such code be written in a sequential style. The ordering rules are precise: synchronous code runs to completion first, then all pending microtasks (promise callbacks), then the next task such as a timer.

// Event-loop concurrency: one thread, callbacks and promises scheduled by the runtime.
const log = [];
const sleep = (ms, label) => new Promise(res => setTimeout(() => { log.push(label); res(label); }, ms));

async function main() {
  log.push("start");
  setTimeout(() => log.push("timer 0 ms"), 0);
  Promise.resolve().then(() => log.push("microtask"));
  log.push("synchronous end of main");
  const results = await Promise.all([sleep(30, "slow 30 ms"), sleep(10, "fast 10 ms")]);
  log.push("all done: " + results.join(", "));
  console.log(log.join("\n"));
}
main();

start
synchronous end of main
microtask
timer 0 ms
fast 10 ms
slow 30 ms
all done: slow 30 ms, fast 10 ms

Worked examples