← Cours 6 : Mini jQuery Cours 7 : Mini Prolog →

Mini Prolog

unification, backtracking et logique en OCaml

1. Introduction

Et si on écrivait un programme qui raisonne ? C'est la promesse de Prolog (1972, Alain Colmerauer) : décrire des faits et des règles, et laisser le moteur d'inférence trouver les solutions par unification et backtracking.

Dans ce cours — le dernier de la série — on va construire un mini moteur Prolog en OCaml. On va voir que :

Les termes de Prolog sont des ADT (cours 2).
L'unification est un pattern matching généralisé.
Le backtracking, c'est la monade Liste (cours 3, section 4).
Tout tient en moins de 200 lignes d'OCaml.

Prolog a été l'un des premiers langages de programmation logique. Il a été utilisé en intelligence artificielle, en traitement du langage naturel, et même dans le système de type de certains langages (Datalog pour les analyses statiques). C'est aussi le langage avec lequel j'ai perdu le plus de nuits de sommeil — et gagné le plus de respect.

Pré-requis : cours 2 (ADT, listes, map/filter/fold), cours 3 (monades, surtout la monade Liste).

2. Termes

En Prolog, tout est terme. Un terme est soit un atome (constante symbolique), soit une variable, soit un terme composé (foncteur + arguments).

2.1 Atomes & variables

OCaml

---------- Termes Prolog ----------

type term =
  | Atom    of string             // atome : jean, paris, 42 *)
  | Var     of string             // variable : X, Personne, L *)
  | Struct  of string * term list  // terme composé *)

// Exemples *)
let ex_atom  = Atom "jean"
let ex_var   = Var "X"
let ex_fact  = Struct ("pere", [Atom "jean"; Atom "paul"])
  // père(jean, paul) *)
let ex_rule  = Struct ("grandpere",
                  [Var "X"; Var "Y"])
  // grand-père(X, Y) *)

// Afficher un terme *)
let rec show_term t =
  match t with
  | Atom s           -> s
  | Var s            -> s
  | Struct (f, [])   -> f
  | Struct (f, args) ->
      f ^ "(" ^ (args |> List.map show_term
                       |> String.concat ", ") ^ ")"

Les variables en Prolog sont comme nos variables OCaml : des emplacements qui peuvent être liés à une valeur. Mais en Prolog, une variable non liée peut être unifiée avec n'importe quoi — et une fois liée, elle ne l'est plus (c'est de la logique, pas de l'impératif).

2.2 Termes composés

Un terme composé Struct(f, args) représente un prédicat ou une structure de données. Par exemple, plus(succ(0), succ(succ(0)), succ(succ(succ(0)))) représente 1 + 2 = 3.

OCaml

// Quelques termes utiles *)
let ex_list =
  Struct (".", [Atom "a";
            Struct (".", [Atom "b";
                      Struct (".", [Atom "c"; Atom "[]"])])])
  // .(a, .(b, .(c, []))) — la liste [a, b, c] en Prolog *)

// Variables libres dans un terme *)
let rec free_vars t =
  match t with
  | Atom _        -> []
  | Var s          -> [s]
  | Struct (_, args) ->
      args |> List.map free_vars |> List.flatten |> dedup

2.3 Substitution

Une substitution est un ensemble de liaisons variable → terme. Appliquer une substitution à un terme remplace chaque variable par son terme lié :

OCaml

---------- Substitution ----------

// Une substitution : variable → terme *)
type subst = (string * term) list

// Substitution vide *)
let empty_subst = []

// Appliquer une substitution à un terme *)
let rec apply s t =
  match t with
  | Atom _ -> t
  | Var x  ->
      (try apply s (List.assoc x s)
       with Not_found -> t)
  | Struct (f, args) ->
      Struct (f, List.map (apply s) args)

// Composer deux substitutions s1 puis s2 *)
let compose s1 s2 =
  List.map (fun (x, t) -> (x, apply s1 t)) s2
  @ s1  // s1 écrase s2 en cas de conflit *)

Une substitution, c'est comme votre calendrier de réunions : chaque variable (créneau) est liée à un terme (réunion). Et comme dans le métro parisien, les substitutions se composent : après avoir remplacé X par Y et Y par "déjeuner", X devient "déjeuner". Magique, non ?

3. Unification

L'unification est l'algorithme qui trouve une substitution rendant deux termes égaux. C'est le cœur de Prolog. Si père(jean, X) et père(jean, paul) s'unifient avec {X → paul}, alors "jean est le père de qui ?" → "paul".

3.1 Algorithme d'unification

OCaml

---------- Unification ----------

exception UnifyError

// Unifier deux termes : retourne la substitution la plus générale (MGU) *)
let rec unify t1 t2 s =
  let t1 = apply s t1 in
  let t2 = apply s t2 in
  match (t1, t2) with
  | Atom a, Atom b when a = b -> s
  | Var x, t
  | t, Var x ->
      if t = Var x then s                        // déjà égal *)
      else (x, t) :: s                           // lier X → t *)
  | Struct (f1, a1), Struct (f2, a2) when f1 = f2
                                              && List.length a1 = List.length a2 ->
      List.fold_left2 unify s a1 a2
  | _ -> raise UnifyError

// Version sécurisée (avec option) *)
let unify_opt t1 t2 =
  try Some (unify t1 t2 empty_subst)
  with UnifyError -> None

// Tests *)
let _ = unify_opt (Atom "a") (Atom "a")
  // = Some [] *)

let _ = unify_opt (Atom "a") (Atom "b")
  // = None *)

let _ = unify_opt (Var "X") (Atom "jean")
  // = Some [("X", Atom "jean")] *)

let _ = unify_opt
  (Struct ("pere", [Var "X"; Atom "paul"]))
  (Struct ("pere", [Atom "jean"; Var "Y"]))
  // = Some [("X", Atom "jean"); ("Y", Atom "paul")] *)

L'unification est au Prolog ce que le pattern matching est à OCaml : une façon de décomposer et lier des valeurs. La différence ? En OCaml, le pattern matching est dirigé par le motif (une variable lie toujours). En Prolog, l'unification est symétrique — les deux côtés peuvent avoir des variables, et c'est l'algorithme qui trouve la substitution.

3.2 Occurs check

Un problème classique de l'unification naïve : peut-on unifier X avec f(X) ? La substitution {X → f(X)} crée un terme infini f(f(f(...))). L'occurs check vérifie qu'une variable n'apparaît pas dans le terme qu'on lui assigne :

OCaml

---------- Occurs check ----------

// Vérifier si une variable apparaît dans un terme *)
let rec occurs x t =
  match t with
  | Atom _        -> false
  | Var y          -> x = y
  | Struct (_, args) ->
      List.exists (occurs x) args

// Unification avec occurs check *)
let rec unify_occ t1 t2 s =
  let t1 = apply s t1 in
  let t2 = apply s t2 in
  match (t1, t2) with
  | Atom a, Atom b when a = b -> s
  | Var x, t
  | t, Var x ->
      if t = Var x then s
      else if occurs x t then raise UnifyError
      else (x, t) :: s
  | Struct (f1, a1), Struct (f2, a2) when f1 = f2
                                              && List.length a1 = List.length a2 ->
      List.fold_left2 unify_occ s a1 a2
  | _ -> raise UnifyError

Prolog traditionnel (comme SWI-Prolog) n'implémente pas l'occurs check par défaut pour des raisons de performance. C'est source de bugs subtils. Certains dialectes (comme Prolog II) l'ont rendu obligatoire. Notre version OCaml l'inclut — parce qu'on est des gens sérieux.

4. Base de connaissances

Une base de connaissances Prolog est un ensemble de faits et de règles. Un fait est une clause sans corps : père(jean, paul). Une règle a un corps : grand-père(X, Z) :- père(X, Y), père(Y, Z). (si X est père de Y et Y est père de Z, alors X est grand-père de Z).

4.1 Faits

OCaml

---------- Base de connaissances ----------

// Une clause : tête (terme) et corps (liste de termes) *)
type clause = {
  head : term;         // père(jean, paul) *)
  body : term list;   // [] pour un fait *)
}

// Une base de connaissance : liste de clauses *)
type knowledge_base = clause list

// Créer un fait *)
let fact h = { head = h; body = [] }

// Créer une règle *)
let rule h b = { head = h; body = b }

Exemple : la base de notre arbre généalogique.

OCaml

// Quelques faits *)
let famille = [
  fact (Struct ("pere",   [Atom "jean";  Atom "paul"]));
  fact (Struct ("pere",   [Atom "jean";  Atom "alice"]));
  fact (Struct ("mere",   [Atom "marie"; Atom "paul"]));
  fact (Struct ("mere",   [Atom "marie"; Atom "alice"]));
  fact (Struct ("homme",  [Atom "jean"]));
  fact (Struct ("homme",  [Atom "paul"]));
  fact (Struct ("femme",  [Atom "marie"]));
  fact (Struct ("femme",  [Atom "alice"]));
]

4.2 Règles

Les règles définissent des relations dérivées. Par exemple "X est parent de Y si X est père de Y ou X est mère de Y" :

OCaml

// Règles *)
let regles = [
  // parent(X, Y) :- pere(X, Y). *)
  rule (Struct ("parent", [Var "X"; Var "Y"]))
       [Struct ("pere", [Var "X"; Var "Y"])];

  // parent(X, Y) :- mere(X, Y). *)
  rule (Struct ("parent", [Var "X"; Var "Y"]))
       [Struct ("mere", [Var "X"; Var "Y"])];

  // grandpere(X, Z) :- pere(X, Y), parent(Y, Z). *)
  rule (Struct ("grandpere", [Var "X"; Var "Z"]))
       [Struct ("pere", [Var "X"; Var "Y"]);
        Struct ("parent", [Var "Y"; Var "Z"])];

  // frere(X, Y) :- homme(X), parent(Z, X), parent(Z, Y), X \= Y. *)
  // (on ignore la différence pour l'instant) *)
]

Les règles Prolog, c'est comme les équations mathématiques du collège : "si X est le père de Y, alors X est un parent de Y". La différence, c'est que Prolog les exécute dans tous les sens — et trouve TOUTES les solutions. Pas comme mon prof de maths qui n'en acceptait qu'une.

5. Backtracking

Le backtracking est le mécanisme qui permet à Prolog d'explorer toutes les solutions possibles. Quand une branche échoue, il revient en arrière et essaie une autre clause. Ce comportement non-déterministe est parfaitement capturé par la monade Liste du cours 3.

5.1 Backtracking = monade Liste

Rappel du cours 3 : la monade Liste modélise le non-déterminisme. return x = [x], bind xs f = List.flatten (List.map f xs). Une requête Prolog est une fonction qui prend une substitution et retourne la liste de toutes les substitutions qui satisfont la requête.

OCaml

---------- Monade Liste (cours 3) ----------

let (>>=) xs f = List.flatten (List.map f xs)
let return x = [x]
let fail    = []

// Choisir une clause dont la tête s'unifie avec le but *)
// Retourne la liste des substitutions possibles *)
let choose_clause kb goal =
  kb |> List.filter_map (fun cl ->
    match unify_occ cl.head goal empty_subst with
    | None -> None
    | Some s -> Some (s, cl))

5.2 Moteur de preuve

Le moteur de preuve résout un but (ou une conjonction de buts) en explorant l'espace de recherche avec la monade Liste :

OCaml

---------- Moteur de preuve ----------

// Résoudre une conjonction de buts étant donné une substitution *)
let rec prove kb goals s =
  match goals with
  | []      -> return s                // Succès : toutes les preuves *)
  | g :: gs ->
      // Appliquer la substitution courante au but *)
      let g = apply s g in
      // Choisir une clause qui s'unifie *)
      kb |> List.filter_map (fun cl ->
        match unify_occ cl.head g empty_subst with
        | None   -> None
        | Some s' ->
            // Composer avec la substitution courante *)
            let s'' = compose s' s in
            // Ajouter les buts du corps et continuer *)
            Some (cl.body @ gs, s''))
      |> List.map (fun (new_goals, s') ->
            prove kb new_goals s')
      |> List.flatten

// Lancer une requête *)
let query kb goal =
  prove kb [goal] empty_subst

// Questions à notre base "famille" *)
let reponses = query famille
  (Struct ("pere", [Atom "jean"; Var "X"]))
// = [ [("X", Atom "paul")]; [("X", Atom "alice")] ] *)
// "Qui sont les enfants de Jean ?" → Paul et Alice *)

Le backtracking par la monade Liste, c'est l'exemple parfait de la puissance des abstractions : un concept complexe (recherche avec retour arrière) se réduit à List.map + List.flatten. On doit cette élégance aux catégories — mais en pratique, c'est juste du bind bien utilisé.

Mais attention, ce moteur simple a un problème : il peut boucler indéfiniment sur des règles récursives. En Prolog, on utilise la récursion gardée (les cas de base avant les cas récursifs) et le cut ! pour contrôler la recherche. En OCaml, on peut ajouter une profondeur maximale :

OCaml

// Moteur avec profondeur maximale *)
let prove_depth kb max_depth goals s depth =
  if depth > max_depth then fail
  else
    match goals with
    | [] -> return s
    | g :: gs ->
        let g = apply s g in
        kb |> List.filter_map (fun cl ->
          match unify_occ cl.head g empty_subst with
          | None -> None
          | Some s' ->
              Some (cl.body @ gs, compose s' s))
        |> List.map (fun (ng, s') ->
              prove_depth kb max_depth ng s' (depth + 1))
        |> List.flatten

Notre moteur est maintenant complet : il unifie, backtracke, et ne boucle pas (sauf si on veut). Le cœur de la logique tient en une dizaine de lignes — le reste, c'est de l'ADT.

6. Exemples

6.1 Arbre généalogique

Chargeons notre base famille avec les règles et posons des questions :

OCaml

---------- Requêtes ----------

let kb = famille @ regles

// 1. Qui sont les enfants de Jean ? *)
let r1 = query kb (Struct ("pere", [Atom "jean"; Var "X"]))
// → X = paul, X = alice *)

// 2. Qui est le grand-père de qui ? *)
let r2 = query kb (Struct ("grandpere", [Var "X"; Var "Y"]))
// → X = jean, Y = paul ; X = jean, Y = alice *)
// Jean est grand-père de Paul et Alice *)

// 3. Est-ce que Marie est parent de Paul ? *)
let r3 = query kb (Struct ("parent", [Atom "marie"; Atom "paul"]))
// → [] (succès avec substitution vide) *)
// La requête a des solutions — c'est un fait *)

// 4. Qui sont les parents de Paul ? *)
let r4 = query kb (Struct ("parent", [Var "X"; Atom "paul"]))
// → X = jean, X = marie *)

On vient de faire un système expert en 150 lignes d'OCaml. Prolog a révolutionné l'IA des années 80 avec ça. Aujourd'hui, on appelle ça un "moteur d'inférence" et on le vend 10 000€ aux entreprises. Mais nous, on sait que c'est juste une monade Liste et un fold sur des substitutions.

6.2 Nombres naturels (Peano)

En Prolog, on peut définir les entiers naturels à la Peano (comme au cours 2) :

OCaml

// 0 = zéro, s(0) = 1, s(s(0)) = 2, ... *)
let zero  = Atom "o"
let succ n = Struct ("s", [n])

let un  = succ zero
let deux = succ un

// Base de connaissances Peano *)
let peano = [
  // plus(o, Y, Y).          (0 + Y = Y) *)
  fact (Struct ("plus", [zero; Var "Y"; Var "Y"]));

  // plus(s(X), Y, s(Z)) :- plus(X, Y, Z). *)
  rule (Struct ("plus",
          [succ (Var "X"); Var "Y"; succ (Var "Z")]))
       [Struct ("plus", [Var "X"; Var "Y"; Var "Z"])];
]

// Requêtes *)
let _ = query peano
  (Struct ("plus", [un; deux; Var "R"]))
// → R = s(s(s(o))) = 3. 1 + 2 = 3. ✓ *)

Le plus fascinant : la même base peut aussi soustraire :

OCaml

// "Quels sont les nombres X et Y tels que X + Y = 3 ?" *)
let _ = query peano
  (Struct ("plus", [Var "X"; Var "Y";
              succ (succ (succ zero))]))
// → X=o,   Y=s(s(s(o)))  (0 + 3 = 3) *)
// → X=s(o), Y=s(s(o))     (1 + 2 = 3) *)
// → X=s(s(o)), Y=s(o)     (2 + 1 = 3) *)
// → X=s(s(s(o))), Y=o     (3 + 0 = 3) *)

Ce n'est plus une addition — c'est une relation qui marche dans tous les sens. Bienvenue en programmation logique.

Et après ? Avec ce moteur, on peut construire : un analyseur de langage naturel (DCG = Definite Clause Grammar), un solveur de contraintes, un système de types basé sur l'unification (comme celui d'OCaml), ou un jeu d'échecs avec recherche en profondeur (Minimax + alphabeta = monade Liste avec élagage).

7. Conclusion

Ce septième et dernier cours de la série a montré comment construire un mini moteur Prolog en OCaml :

Brique	Source	Usage dans Mini Prolog
ADT	Cours 2	Type `term`, `clause`, `subst`
Récursion structurelle	Cours 2	`apply`, `free_vars`, `show_term`
Fold	Cours 2	`List.fold_left2` pour l'unification
Monade Liste	Cours 3	`prove` = `bind` + `return` + `fail`
Pattern matching	Cours 1/2	`unify` décompose les termes récursivement

Ce qu'il faut retenir

Les termes Prolog sont un ADT — trois constructeurs suffisent.
L'unification est un pattern matching symétrique avec occurs check.
Le backtracking = monade Liste. bind explore toutes les branches.
Un moteur d'inférence tient en 20 lignes — le génie est dans l'abstraction, pas dans la complexité.

Et voilà. On a parcouru les 7 cours : du lambda-calcul à Prolog, en passant par les ADT, les monades, les parseurs, Excel, jQuery... Tout ça en OCaml, tout ça avec des types forts, et tout ça en moins de 1000 lignes de code par cours.

Merci d'avoir suivi cette série "Du Lambda à OCaml". Vous avez maintenant les clés pour comprendre la programmation fonctionnelle, les langages spécifiques (DSL), et la programmation logique. Le reste, c'est de la pratique. Allez coder quelque chose de beau.

Fin de la série « Du λ à OCaml »

λ → ADT → Monades → Parseurs → Excel → jQuery → Prolog

Fait avec ❤️, des fix et des let rec

← Cours 6 : Mini jQuery Retour au début →