Implementing Prolog

A λ-Nantes Workshop

arnaud@pankzsoft.com - @abailly.bsky.social

2025-12-10

Usage

Example

A program about Star Wars characters (including the crappy recent ones)

Example - Facts

Simple facts asserting the gender of some characters.

female(leia).
male(vader).
male(luke).
male(kylo).

Example - Facts

More complex facts asserting a childhood relation between some characters.

child(luke, vader).
child(leia, vader).
child(kylo, leia).

Example - Rules

Rules (or Clauses) allowing to infer some relation from other relations.

son(X,Y) :- male(X), child(X,Y).
daughter(X,Y) :- female(X), child(X,Y).

Example - Rules

More complex rules asserting a transitive relation

grandchild(X,Z) :- child(X,Y), child(Y,Z).

Example - Query

We can query this program, for example asking who is a grandchild of Darth Vader

> ?- grandchild(X, vader).
success. Type [Enter] to list solutions.
>
[X -> kylo]

Example - Query

A Prolog query can have several answers:

> ?- child(X, vader).
success. Type [Enter] to list solutions.
>
[X -> luke]
>
[X -> leia]

Example - Query

Or no answer:

> ?- grandchild(leia, X).
failure

Implementation

Terms

  • variables start with upper casae: X, Y…
  • symbols start with lower case: s, z, child, …
  • symbols have 0 or more arguments, e.g an arity : bob, child(X, Y), father(bob, Z)…

Clauses

  • head: a single term
  • premises: a (possibly empty) list of terms
  • a data set (or a program) is a list of clauses or facts
  • a query is a term introduced with ?-

Basic algorithm

Given a query and a set of clauses, a Prolog interpreter loop goes like:

  1. Push query on its goal stack
  2. Pop up current goal from the stack
  3. Try to match goal with each clause:
    1. Unify goal with the head of clause with fresh variables
    2. If unification succeeds, push premises of clause onto goals stack
  4. Query succeeds if stack is empty with a successful match

Unification

Given two terms t1 and t2 with free variables fv(t1), fv(t2), unification is the process of defining a substitution between variables and terms

σ : fv(t1) ∪ fv(t2) → T

Unification

  • Two variables unify with each other
  • A variable unifies with a term if not already mapped
  • Two relations unify with each other iff
    • Their symbol is the same
    • Their arguments unify with each other

Unification

  • σ(X, Y) = {X ↦ Y}
  • σ(X, foo) = {X ↦ foo}
  • σ(foo, X) = {X ↦ foo}
  • σ(foo(bar, Y), foo(X, Z)) = {X ↦ bar, Y ↦ Z}

Practice

References