---
title: Implementing Prolog
subtitle: A λ-Nantes Workshop
author: arnaud@pankzsoft.com - @abailly.bsky.social
date: 2025-12-10
---

# Usage

![](star-wars.jpg)

## Example

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

## Example - Facts

Simple facts asserting the gender of some characters.

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

## Example - Facts

More complex facts asserting a `child`hood _relation_ between some characters.

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

## Example - Rules

_Rules_ (or _Clauses_) allowing to infer some relation from other relations.

```prolog
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

```prolog
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

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

## Example - Query

A Prolog query can have several answers:

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

## Example - Query

Or no answer:

```prolog
> ?- 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_:
   a. _Unify_ goal with the _head_ of _clause_ with _fresh_ variables
   b. 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 $t_1$ and $t_2$ with _free variables_ $fv(t_1)$, $fv(t_2)$,
unification is the process of defining a _substitution_ between variables and _terms_

$$
\sigma : fv(t_1) \cup fv(t_2) \rightarrow 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

* $\sigma(X, Y) = \{ X \mapsto Y \}$
* $\sigma(X, foo) = \{ X \mapsto foo \}$
* $\sigma(foo, X) = \{ X \mapsto foo \}$
* $\sigma(foo(bar, Y), foo(X, Z)) = \{ X \mapsto bar, Y \mapsto Z \}$

# Practice

![](workbench.jpg)

## References

* [NanoProlog](https://github.com/norm2782/NanoProlog)
* [hslogic](https://github.com/abailly/hslogic)
* [miniprolog](https://github.com/andrejbauer/plzoo/tree/master/src/miniprolog)