Logic Programming

Abelson & Sussman · 1996 · SICP §4.4

Programs as queries against a database of facts and rules. Unification matches patterns with variables. Programming becomes asking questions, not giving instructions.

Deductive information retrieval

A database of assertions (facts) and rules (implications). A query is a pattern with variables. The system finds all ways to bind the variables so the pattern matches the database. This is Prolog's core idea.

Scheme

; A tiny fact database and pattern matcher.
; Facts are lists. Variables start with ?.

(define facts
  '((job (Hacker Alyssa P) (computer programmer))
    (job (Fect Cy D) (computer programmer))
    (job (Bitdiddle Ben) (computer wizard))
    (job (Tweakit Lem E) (computer technician))
    (supervisor (Hacker Alyssa P) (Bitdiddle Ben))
    (supervisor (Fect Cy D) (Bitdiddle Ben))
    (supervisor (Tweakit Lem E) (Bitdiddle Ben))
    (salary (Bitdiddle Ben) 60000)
    (salary (Hacker Alyssa P) 40000)
    (salary (Fect Cy D) 35000)))

; Simple pattern match: does pattern match datum?
(define (match? pattern datum bindings)
  (cond ((eq? bindings 'failed) 'failed)
        ((equal? pattern datum) bindings)
        ((variable? pattern)
         (extend-bindings pattern datum bindings))
        ((and (pair? pattern) (pair? datum))
         (match? (cdr pattern) (cdr datum)
                 (match? (car pattern) (car datum) bindings)))
        (else 'failed)))

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))
(define (extend-bindings var val bindings) (cons (cons var val) bindings))

; Query: who is a computer programmer?
(define (query-simple pattern)
  (filter (lambda (f) (not (eq? (match? pattern f '()) 'failed))) facts))

(display "Computer programmers:")
(newline)
(for-each (lambda (f) (display "  ") (display f) (newline))
          (query-simple '(job ?who (computer programmer))))

; A tiny fact database and pattern matcher.
; Facts are lists. Variables start with ?.

(define facts
  '((job (Hacker Alyssa P) (computer programmer))
    (job (Fect Cy D) (computer programmer))
    (job (Bitdiddle Ben) (computer wizard))
    (job (Tweakit Lem E) (computer technician))
    (supervisor (Hacker Alyssa P) (Bitdiddle Ben))
    (supervisor (Fect Cy D) (Bitdiddle Ben))
    (supervisor (Tweakit Lem E) (Bitdiddle Ben))
    (salary (Bitdiddle Ben) 60000)
    (salary (Hacker Alyssa P) 40000)
    (salary (Fect Cy D) 35000)))

; Simple pattern match: does pattern match datum?
(define (match? pattern datum bindings)
  (cond ((eq? bindings 'failed) 'failed)
        ((equal? pattern datum) bindings)
        ((variable? pattern)
         (extend-bindings pattern datum bindings))
        ((and (pair? pattern) (pair? datum))
         (match? (cdr pattern) (cdr datum)
                 (match? (car pattern) (car datum) bindings)))
        (else 'failed)))

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))
(define (extend-bindings var val bindings) (cons (cons var val) bindings))

; Query: who is a computer programmer?
(define (query-simple pattern)
  (filter (lambda (f) (not (eq? (match? pattern f '()) 'failed))) facts))

(display "Computer programmers:")
(newline)
(for-each (lambda (f) (display "  ") (display f) (newline))
          (query-simple '(job ?who (computer programmer))))

Python

# Fact database and pattern matching in Python

facts = [
    ("job", ("Hacker", "Alyssa"), ("computer", "programmer")),
    ("job", ("Fect", "Cy"), ("computer", "programmer")),
    ("job", ("Bitdiddle", "Ben"), ("computer", "wizard")),
    ("job", ("Tweakit", "Lem"), ("computer", "technician")),
    ("supervisor", ("Hacker", "Alyssa"), ("Bitdiddle", "Ben")),
    ("salary", ("Bitdiddle", "Ben"), 60000),
    ("salary", ("Hacker", "Alyssa"), 40000),
]

def is_var(x):
    return isinstance(x, str) and x.startswith("?")

def match(pattern, datum, bindings):
    if bindings is None:
        return None
    if pattern == datum:
        return bindings
    if is_var(pattern):
        return dict(list(bindings.items()) + [(pattern, datum)])
    if isinstance(pattern, tuple) and isinstance(datum, tuple):
        if len(pattern) != len(datum):
            return None
        for p, d in zip(pattern, datum):
            bindings = match(p, d, bindings)
            if bindings is None:
                return None
        return bindings
    return None

# Query: who is a computer programmer?
pattern = ("job", "?who", ("computer", "programmer"))
print("Computer programmers:")
for f in facts:
    b = match(pattern, f, {})
    if b is not None:
        print(f"  {b['?who']}")

# Fact database and pattern matching in Python

facts = [
    ("job", ("Hacker", "Alyssa"), ("computer", "programmer")),
    ("job", ("Fect", "Cy"), ("computer", "programmer")),
    ("job", ("Bitdiddle", "Ben"), ("computer", "wizard")),
    ("job", ("Tweakit", "Lem"), ("computer", "technician")),
    ("supervisor", ("Hacker", "Alyssa"), ("Bitdiddle", "Ben")),
    ("salary", ("Bitdiddle", "Ben"), 60000),
    ("salary", ("Hacker", "Alyssa"), 40000),
]

def is_var(x):
    return isinstance(x, str) and x.startswith("?")

def match(pattern, datum, bindings):
    if bindings is None:
        return None
    if pattern == datum:
        return bindings
    if is_var(pattern):
        return dict(list(bindings.items()) + [(pattern, datum)])
    if isinstance(pattern, tuple) and isinstance(datum, tuple):
        if len(pattern) != len(datum):
            return None
        for p, d in zip(pattern, datum):
            bindings = match(p, d, bindings)
            if bindings is None:
                return None
        return bindings
    return None

# Query: who is a computer programmer?
pattern = ("job", "?who", ("computer", "programmer"))
print("Computer programmers:")
for f in facts:
    b = match(pattern, f, {})
    if b is not None:
        print(f"  {b['?who']}")

How the query system works — unification

Pattern matching is one-directional: the pattern has variables, the datum doesn't. Unification generalizes this: both sides can have variables. Two patterns unify if there exists a substitution that makes them equal. This is the engine behind Prolog and the query language.

Scheme

; Unification: find substitution making two patterns equal.
; Both sides can contain variables.

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))

(define (lookup var bindings)
  (let ((pair (assoc var bindings)))
    (if pair (cdr pair) #f)))

(define (walk x bindings)
  (if (variable? x)
      (let ((val (lookup x bindings)))
        (if val (walk val bindings) x))
      x))

(define (unify x y bindings)
  (let ((x (walk x bindings))
        (y (walk y bindings)))
    (cond ((eq? bindings 'failed) 'failed)
          ((equal? x y) bindings)
          ((variable? x) (cons (cons x y) bindings))
          ((variable? y) (cons (cons y x) bindings))
          ((and (pair? x) (pair? y))
           (unify (cdr x) (cdr y)
                  (unify (car x) (car y) bindings)))
          (else 'failed))))

; Examples:
(display "Unify (?x 2) with (1 ?y): ")
(display (unify '(?x 2) '(1 ?y) '()))
(newline)
; => ((?y . 2) (?x . 1))

(display "Unify (?x ?x) with (1 1): ")
(display (unify '(?x ?x) '(1 1) '()))
(newline)
; => ((?x . 1))

(display "Unify (?x ?x) with (1 2): ")
(display (unify '(?x ?x) '(1 2) '()))
(newline)
; => failed

(display "Unify (?x ?y) with (?y 3): ")
(display (unify '(?x ?y) '(?y 3) '()))
; => ((?y . 3) (?x . ?y))  — ?x = ?y = 3

; Unification: find substitution making two patterns equal.
; Both sides can contain variables.

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))

(define (lookup var bindings)
  (let ((pair (assoc var bindings)))
    (if pair (cdr pair) #f)))

(define (walk x bindings)
  (if (variable? x)
      (let ((val (lookup x bindings)))
        (if val (walk val bindings) x))
      x))

(define (unify x y bindings)
  (let ((x (walk x bindings))
        (y (walk y bindings)))
    (cond ((eq? bindings 'failed) 'failed)
          ((equal? x y) bindings)
          ((variable? x) (cons (cons x y) bindings))
          ((variable? y) (cons (cons y x) bindings))
          ((and (pair? x) (pair? y))
           (unify (cdr x) (cdr y)
                  (unify (car x) (car y) bindings)))
          (else 'failed))))

; Examples:
(display "Unify (?x 2) with (1 ?y): ")
(display (unify '(?x 2) '(1 ?y) '()))
(newline)
; => ((?y . 2) (?x . 1))

(display "Unify (?x ?x) with (1 1): ")
(display (unify '(?x ?x) '(1 1) '()))
(newline)
; => ((?x . 1))

(display "Unify (?x ?x) with (1 2): ")
(display (unify '(?x ?x) '(1 2) '()))
(newline)
; => failed

(display "Unify (?x ?y) with (?y 3): ")
(display (unify '(?x ?y) '(?y 3) '()))
; => ((?y . 3) (?x . ?y))  — ?x = ?y = 3

Python

# Unification in Python

def is_var(x):
    return isinstance(x, str) and x.startswith("?")

def walk(x, bindings):
    while is_var(x) and x in bindings:
        x = bindings[x]
    return x

def unify(x, y, bindings):
    if bindings is None:
        return None
    x = walk(x, bindings)
    y = walk(y, bindings)
    if x == y:
        return bindings
    if is_var(x):
        return dict(list(bindings.items()) + [(x, y)])
    if is_var(y):
        return dict(list(bindings.items()) + [(y, x)])
    if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
        for a, b in zip(x, y):
            bindings = unify(a, b, bindings)
            if bindings is None:
                return None
        return bindings
    return None

print(unify(("?x", 2), (1, "?y"), {}))
# => {'?x': 1, '?y': 2}

print(unify(("?x", "?x"), (1, 1), {}))
# => {'?x': 1}

print(unify(("?x", "?x"), (1, 2), {}))
# => None (failed)

print(unify(("?x", "?y"), ("?y", 3), {}))
# => {'?x': '?y', '?y': 3}

# Unification in Python

def is_var(x):
    return isinstance(x, str) and x.startswith("?")

def walk(x, bindings):
    while is_var(x) and x in bindings:
        x = bindings[x]
    return x

def unify(x, y, bindings):
    if bindings is None:
        return None
    x = walk(x, bindings)
    y = walk(y, bindings)
    if x == y:
        return bindings
    if is_var(x):
        return dict(list(bindings.items()) + [(x, y)])
    if is_var(y):
        return dict(list(bindings.items()) + [(y, x)])
    if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
        for a, b in zip(x, y):
            bindings = unify(a, b, bindings)
            if bindings is None:
                return None
        return bindings
    return None

print(unify(("?x", 2), (1, "?y"), {}))
# => {'?x': 1, '?y': 2}

print(unify(("?x", "?x"), (1, 1), {}))
# => {'?x': 1}

print(unify(("?x", "?x"), (1, 2), {}))
# => None (failed)

print(unify(("?x", "?y"), ("?y", 3), {}))
# => {'?x': '?y', '?y': 3}

Rules — deduction from facts

A rule says: if you can satisfy the body, you can conclude the head. (rule (can-replace ?x ?y) (and (job ?x ?j) (job ?y ?j) (not (same ?x ?y)))). The query system chains rules to derive new facts from existing ones.

Scheme

; Rules: derive new facts from existing ones.
; A rule is (head . body-conditions).

(define facts
  '((parent tom bob)
    (parent tom liz)
    (parent bob ann)
    (parent bob pat)
    (parent pat kim)))

; Rule: grandparent ?x ?z if (parent ?x ?y) and (parent ?y ?z)
(define (query-parent db x y bindings)
  (filter (lambda (b) (not (eq? b 'failed)))
    (map (lambda (f)
           (if (eq? (car f) 'parent)
               (unify (list x y) (cdr f) bindings)
               'failed))
         db)))

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))
(define (walk x b) (if (variable? x) (let ((v (assoc x b))) (if v (walk (cdr v) b) x)) x))
(define (unify x y b)
  (let ((x (walk x b)) (y (walk y b)))
    (cond ((eq? b 'failed) 'failed) ((equal? x y) b)
          ((variable? x) (cons (cons x y) b))
          ((variable? y) (cons (cons y x) b))
          ((and (pair? x) (pair? y)) (unify (cdr x) (cdr y) (unify (car x) (car y) b)))
          (else 'failed))))

(define (grandparents db)
  (apply append
    (map (lambda (b1)
           (let ((mid (walk '?mid b1)))
             (map (lambda (b2)
                    (list 'grandparent
                          (walk '?gp b2)
                          (walk '?gc b2)))
                  (query-parent db mid '?gc b1))))
         (query-parent db '?gp '?mid '()))))

(display "Grandparent relations:") (newline)
(for-each (lambda (g) (display "  ") (display g) (newline))
          (grandparents facts))

; Rules: derive new facts from existing ones.
; A rule is (head . body-conditions).

(define facts
  '((parent tom bob)
    (parent tom liz)
    (parent bob ann)
    (parent bob pat)
    (parent pat kim)))

; Rule: grandparent ?x ?z if (parent ?x ?y) and (parent ?y ?z)
(define (query-parent db x y bindings)
  (filter (lambda (b) (not (eq? b 'failed)))
    (map (lambda (f)
           (if (eq? (car f) 'parent)
               (unify (list x y) (cdr f) bindings)
               'failed))
         db)))

(define (variable? x) (and (symbol? x) (char=? (string-ref (symbol->string x) 0) #?)))
(define (walk x b) (if (variable? x) (let ((v (assoc x b))) (if v (walk (cdr v) b) x)) x))
(define (unify x y b)
  (let ((x (walk x b)) (y (walk y b)))
    (cond ((eq? b 'failed) 'failed) ((equal? x y) b)
          ((variable? x) (cons (cons x y) b))
          ((variable? y) (cons (cons y x) b))
          ((and (pair? x) (pair? y)) (unify (cdr x) (cdr y) (unify (car x) (car y) b)))
          (else 'failed))))

(define (grandparents db)
  (apply append
    (map (lambda (b1)
           (let ((mid (walk '?mid b1)))
             (map (lambda (b2)
                    (list 'grandparent
                          (walk '?gp b2)
                          (walk '?gc b2)))
                  (query-parent db mid '?gc b1))))
         (query-parent db '?gp '?mid '()))))

(display "Grandparent relations:") (newline)
(for-each (lambda (g) (display "  ") (display g) (newline))
          (grandparents facts))

Is logic programming mathematical logic?

Not quite. Logic programming uses a closed-world assumption: anything not in the database is false. Mathematical logic has no such default. Also, rule application order matters — an infinite loop is possible if rules are written carelessly. The query system is a computational interpretation of logic, not a faithful implementation.

Scheme

; The closed-world assumption: not-in-database = false.
; Also: rule order matters — naive recursion can loop.

; Demonstrate with a simple "not" via failure to find.

(define db '((likes alice bob)
             (likes alice carol)
             (likes bob carol)))

(define (query-likes db who whom)
  (filter (lambda (f)
            (and (eq? (car f) 'likes)
                 (eq? (cadr f) who)
                 (eq? (caddr f) whom)))
          db))

(define (likes? who whom) (not (null? (query-likes db who whom))))

; Closed-world: if it's not in the database, it's false
(display "alice likes bob?   ") (display (likes? 'alice 'bob))   (newline)
(display "alice likes carol? ") (display (likes? 'alice 'carol)) (newline)
(display "bob likes alice?   ") (display (likes? 'bob 'alice))   (newline)
; => #f — not because Bob doesn't like Alice,
;    but because the database doesn't say he does.

; Negation as failure
(define (not-likes? who whom) (not (likes? who whom)))
(display "bob NOT likes alice? ") (display (not-likes? 'bob 'alice))

; The closed-world assumption: not-in-database = false.
; Also: rule order matters — naive recursion can loop.

; Demonstrate with a simple "not" via failure to find.

(define db '((likes alice bob)
             (likes alice carol)
             (likes bob carol)))

(define (query-likes db who whom)
  (filter (lambda (f)
            (and (eq? (car f) 'likes)
                 (eq? (cadr f) who)
                 (eq? (caddr f) whom)))
          db))

(define (likes? who whom) (not (null? (query-likes db who whom))))

; Closed-world: if it's not in the database, it's false
(display "alice likes bob?   ") (display (likes? 'alice 'bob))   (newline)
(display "alice likes carol? ") (display (likes? 'alice 'carol)) (newline)
(display "bob likes alice?   ") (display (likes? 'bob 'alice))   (newline)
; => #f — not because Bob doesn't like Alice,
;    but because the database doesn't say he does.

; Negation as failure
(define (not-likes? who whom) (not (likes? who whom)))
(display "bob NOT likes alice? ") (display (not-likes? 'bob 'alice))

Implementing the query system

The query evaluator processes compound queries (and, or, not) by combining streams of bindings. An and query pipes the output of one sub-query into the next. An or query merges streams. not filters out bindings that succeed.

Scheme

; Compound queries: and, or, not — combining binding streams.

(define db '((job alice programmer)
             (job bob designer)
             (job carol programmer)
             (job dave manager)
             (dept alice engineering)
             (dept bob design)
             (dept carol engineering)
             (dept dave engineering)))

(define (query-all rel db)
  (filter (lambda (f) (eq? (car f) rel)) db))

; AND: programmers in engineering
(define programmers
  (map caddr (filter (lambda (f) (eq? (caddr f) 'programmer))
                     (query-all 'job db))))

(define engineers
  (map cadr (filter (lambda (f) (eq? (caddr f) 'engineering))
                    (query-all 'dept db))))

(define (intersection a b)
  (filter (lambda (x) (memq x b)) a))

(display "Programmers AND engineering: ")
(display (intersection programmers engineers))
(newline)

; OR: programmers or managers
(define managers
  (map cadr (filter (lambda (f) (eq? (caddr f) 'manager))
                    (query-all 'job db))))

(define (union a b)
  (append a (filter (lambda (x) (not (memq x a))) b)))

(display "Programmers OR managers: ")
(display (union (map cadr (filter (lambda (f) (eq? (caddr f) 'programmer))
                                  (query-all 'job db)))
                managers))
(newline)

; NOT: engineering but not programmer
(display "Engineering NOT programmer: ")
(display (filter (lambda (x) (not (memq x programmers))) engineers))

; Compound queries: and, or, not — combining binding streams.

(define db '((job alice programmer)
             (job bob designer)
             (job carol programmer)
             (job dave manager)
             (dept alice engineering)
             (dept bob design)
             (dept carol engineering)
             (dept dave engineering)))

(define (query-all rel db)
  (filter (lambda (f) (eq? (car f) rel)) db))

; AND: programmers in engineering
(define programmers
  (map caddr (filter (lambda (f) (eq? (caddr f) 'programmer))
                     (query-all 'job db))))

(define engineers
  (map cadr (filter (lambda (f) (eq? (caddr f) 'engineering))
                    (query-all 'dept db))))

(define (intersection a b)
  (filter (lambda (x) (memq x b)) a))

(display "Programmers AND engineering: ")
(display (intersection programmers engineers))
(newline)

; OR: programmers or managers
(define managers
  (map cadr (filter (lambda (f) (eq? (caddr f) 'manager))
                    (query-all 'job db))))

(define (union a b)
  (append a (filter (lambda (x) (not (memq x a))) b)))

(display "Programmers OR managers: ")
(display (union (map cadr (filter (lambda (f) (eq? (caddr f) 'programmer))
                                  (query-all 'job db)))
                managers))
(newline)

; NOT: engineering but not programmer
(display "Engineering NOT programmer: ")
(display (filter (lambda (x) (not (memq x programmers))) engineers))

Notation reference

Query language	Python	Meaning
(job ?x ?dept)	for r in db if r[0]=="job"	Query with pattern variables
(and q1 q2)	set1 & set2	Both queries must match
(or q1 q2)	set1 \| set2	Either query matches
(not q)	set1 - set2	Negation as failure
(rule (head) body)	def head(): body	Derive new facts from existing

Neighbors

Translation notes

Logic programming inverts the usual programming flow: you specify what relates to what, and the system figures out how to compute it. Python has no built-in unification, so the translation uses explicit loops and set operations. Unification generalizes both pattern matching and equation solving. In Python, the closest built-in is dictionary merging, but it lacks the bidirectional variable binding that makes unification powerful.

Ready for the real thing? Read SICP §4.4.

← Nondeterministic Computing by june.kim Register Machines · 18 of 22 →