SL-5 - Resolution Inverse & ILP (C#)

Jumeau C# du notebook SL-5-InverseResolution.ipynb. Marathon parite .NET ⇄ Python (#4956), EPIC #3801 Prong B. Algorithmes AIMA §19.5 (Inverse Resolution + Bottom-Clause ILP), implémentés from-scratch en C# pur (pas de lib ML), PLUS un pont SOTA (§7) vers SWI-Prolog — le moteur que le jumeau Python invoque via janus_swi pour Aleph.

Objectifs d’apprentissage

Représenter clauses Horn et prédicats en C# (atomes = (predicat, args), clause = record).
Généraliser deux exemples par LGG (Least General Generalization, Plotkin).
Vérifier la θ-subsomption (skolemisation + backtracking) pour ordonner la généralité.
Construire la clause bottom (saturation bornée + variabilisation).
Rechercher la meilleure clause consistante dans [top, bottom] (style Progol, score p − L).
Apprendre grandfather/2 puis grandmother/2 à partir d’un arbre généalogique.

Prérequis

Notions de logique du premier ordre (clauses Horn, variables, unification).
.NET 9.0 + dotnet-interactive (kernel .net-csharp).
Avoir suivi SL-1, SL-2.

Durée estimée : 65 minutes

Références

Russell & Norvig, AIMA (3e éd.), §19.5.
Muggleton, S. Inductive Logic Programming (1991-1995) — Progol, clause bottom.
Notebook Python : SL-5-InverseResolution.ipynb.

1. Représentation : atomes, clauses, couverture

Un atome = (prédicat, args) (ValueTuple) où les args sont des termes (constantes en minuscule, variables en majuscule). Une clause = record Clause(Head, Body). La clause couvre un exemple si la tête s’unifie et le corps est satisfiable sur les faits.

using System.Linq;

// Comparateur structurel d'atomes (sinon string[] compare par reference =>HashSet bug).
public class AtomEq : IEqualityComparer<(string,string[])> {
    public bool Equals((string,string[]) x, (string,string[]) y) =>
        x.Item1 == y.Item1 && x.Item2.SequenceEqual(y.Item2);
    public int GetHashCode((string,string[]) x) {
        int h = x.Item1.GetHashCode();
        foreach (var a in x.Item2) h = HashCode.Combine(h, a);
        return h;
    }
}

// Une clause Horn : tete + corps (conjonction de litteraux).
public record Clause((string,string[]) Head, List<(string,string[])> Body);

bool IsVar(string t) => t.Length > 0 && char.IsUpper(t[0]);

(string,string[]) Subst((string,string[]) atom, Dictionary<string,string> theta) =>
    (atom.Item1, atom.Item2.Select(a => theta.TryGetValue(a, out var v) ? v : a).ToArray());

// Etend theta pour que pattern devienne fact ; null si impossible.
Dictionary<string,string> MatchAtom((string,string[]) pattern, (string,string[]) fact,
                                     Dictionary<string,string> theta) {
    if (pattern.Item1 != fact.Item1 || pattern.Item2.Length != fact.Item2.Length) return null;
    var th = new Dictionary<string,string>(theta);
    for (int i = 0; i < pattern.Item2.Length; i++) {
        string p = pattern.Item2[i], f = fact.Item2[i];
        if (IsVar(p)) { if (th.TryGetValue(p, out var v) && v != f) return null; th[p] = f; }
        else if (p != f) return null;
    }
    return th;
}

bool BodySatisfiable(List<(string,string[])> body, List<(string,string[])> facts,
                     Dictionary<string,string> theta, int k = 0) {
    if (k == body.Count) return true;
    foreach (var fact in facts) {
        var th = MatchAtom(body[k], fact, theta);
        if (th != null && BodySatisfiable(body, facts, th, k + 1)) return true;
    }
    return false;
}

bool Covers(Clause clause, (string,string[]) example, List<(string,string[])> facts) {
    var th = MatchAtom(clause.Head, example, new Dictionary<string,string>());
    return th != null && BodySatisfiable(clause.Body, facts, th);
}

string Fmt((string,string[]) a) => $"{a.Item1}({string.Join(", ", a.Item2)})";
string ShowClause(Clause c) =>
    Fmt(c.Head) + (c.Body.Count > 0 ? " :- " + string.Join(", ", c.Body.Select(Fmt)) : "") + ".";

// Domaine : arbre genealogique
var FACTS = new List<(string,string[])> {
    ("parent", new[]{"tom","bob"}), ("parent", new[]{"tom","liz"}),
    ("parent", new[]{"bob","ann"}), ("parent", new[]{"bob","pat"}),
    ("parent", new[]{"liz","sue"}), ("parent", new[]{"pat","jim"}),
    ("parent", new[]{"sue","eve"}),
    ("male", new[]{"tom"}), ("male", new[]{"bob"}), ("male", new[]{"jim"}),
    ("female", new[]{"liz"}), ("female", new[]{"ann"}), ("female", new[]{"pat"}),
    ("female", new[]{"sue"}), ("female", new[]{"eve"}),
};
var POS = new List<(string,string[])> {
    ("grandfather", new[]{"tom","ann"}), ("grandfather", new[]{"tom","pat"}),
    ("grandfather", new[]{"tom","sue"}), ("grandfather", new[]{"bob","jim"}) };
var NEG = new List<(string,string[])> {
    ("grandfather", new[]{"liz","eve"}), ("grandfather", new[]{"liz","sue"}),
    ("grandfather", new[]{"bob","ann"}), ("grandfather", new[]{"pat","jim"}),
    ("grandfather", new[]{"tom","bob"}), ("grandfather", new[]{"ann","jim"}) };

// Cible (a retrouver par l'algorithme)
var target = new Clause(
    ("grandfather", new[]{"X","Y"}),
    new List<(string,string[])>{
        ("male", new[]{"X"}), ("parent", new[]{"X","Z"}), ("parent", new[]{"Z","Y"})});
Console.WriteLine($"Cible : {ShowClause(target)}\n");
Console.WriteLine($"{"exemple",24} | attendu | couvert");
Console.WriteLine(new string('-', 48));
foreach (var e in POS.Concat(NEG)) {
    string exp = POS.Contains(e, new AtomEq()) ? "+" : "-";
    string couv = Covers(target, e, FACTS) ? "oui" : "non";
    Console.WriteLine($"{Fmt(e),24} |    {exp}    |   {couv}");
}

Cible : grandfather(X, Y) :- male(X), parent(X, Z), parent(Z, Y).

                 exemple | attendu | couvert
------------------------------------------------
   grandfather(tom, ann) |    +    |   oui
   grandfather(tom, pat) |    +    |   oui
   grandfather(tom, sue) |    +    |   oui
   grandfather(bob, jim) |    +    |   oui
   grandfather(liz, eve) |    -    |   non
   grandfather(liz, sue) |    -    |   non
   grandfather(bob, ann) |    -    |   non
   grandfather(pat, jim) |    -    |   non
   grandfather(tom, bob) |    -    |   non
   grandfather(ann, jim) |    -    |   non

2. LGG — Least General Generalization (Plotkin)

La LGG de deux clauses généralise leurs termes : si deux termes diffèrent, on introduit une nouvelle variable partagée (table de mapping). C’est l’inverse de l’unification : on remonte vers le plus général.

// LGG de deux termes : meme terme -> lui-meme ; sinon variable fraiche partagee.
string LggTerm(string t1, string t2, Dictionary<(string,string),string> mapping) {
    if (t1 == t2) return t1;
    if (!mapping.ContainsKey((t1, t2))) mapping[(t1, t2)] = $"V{mapping.Count + 1}";
    return mapping[(t1, t2)];
}

(string,string[])? LggAtom((string,string[]) a1, (string,string[]) a2,
                            Dictionary<(string,string),string> mapping) {
    if (a1.Item1 != a2.Item1 || a1.Item2.Length != a2.Item2.Length) return null;
    var args = a1.Item2.Zip(a2.Item2, (x, y) => LggTerm(x, y, mapping)).ToArray();
    return (a1.Item1, args);
}

Clause LggClause(Clause c1, Clause c2) {
    var mapping = new Dictionary<(string,string),string>();
    var head = LggAtom(c1.Head, c2.Head, mapping) ?? ("nil", new string[0]);
    var body = new List<(string,string[])>();
    var seen = new HashSet<(string,string[])>(new AtomEq());
    foreach (var b1 in c1.Body)
        foreach (var b2 in c2.Body) {
            var g = LggAtom(b1, b2, mapping);
            if (g.HasValue && seen.Add(g.Value)) body.Add(g.Value);
        }
    return new Clause(head, body);
}

// Deux explications au sol de deux exemples positifs differents.
var expl1 = new Clause(
    ("grandfather", new[]{"tom","ann"}),
    new List<(string,string[])>{
        ("male", new[]{"tom"}), ("parent", new[]{"tom","bob"}), ("parent", new[]{"bob","ann"})});
var expl2 = new Clause(
    ("grandfather", new[]{"bob","jim"}),
    new List<(string,string[])>{
        ("male", new[]{"bob"}), ("parent", new[]{"bob","pat"}), ("parent", new[]{"pat","jim"})});
var g = LggClause(expl1, expl2);
Console.WriteLine("LGG des deux explications :");
Console.WriteLine($"  {ShowClause(g)}");
Console.WriteLine($"\nTaille des corps : {expl1.Body.Count} et {expl2.Body.Count} litteraux -> LGG : {g.Body.Count} litteraux");
int posCovered = POS.Count(e => Covers(g, e, FACTS));
int negCovered = NEG.Count(e => Covers(g, e, FACTS));
Console.WriteLine($"Couverture : {posCovered}/4 positifs, {negCovered}/6 negatifs");

LGG des deux explications :
  grandfather(V1, V2) :- male(V1), parent(V1, V3), parent(V4, V5), parent(bob, V6), parent(V3, V2).

Taille des corps : 3 et 3 litteraux -> LGG : 5 litteraux
Couverture : 4/4 positifs, 0/6 negatifs

3. θ-subsomption — ordre de généralité

C θ-subsume D s’il existe une substitution θ plongeant chaque littéral de C dans D. On skolémise D (variables → constantes) puis on cherche θ par backtracking. La clause la plus générale (top) subsume toutes les autres.

// C theta-subsume D ? Skolemise D, puis backtrack pour plonger les litteraux de C.
bool Subsumes(Clause c, Clause d) {
    var dVars = new HashSet<string>();
    foreach (var a in new[]{d.Head}.Concat(d.Body))
        foreach (var t in a.Item2) if (IsVar(t)) dVars.Add(t);
    var sk = dVars.ToDictionary(v => v, v => $"sk_{char.ToLower(v[0])}");
    var dHead = Subst(d.Head, sk);
    var dBody = d.Body.Select(b => Subst(b, sk)).ToList();

    var theta0 = MatchAtom(c.Head, dHead, new Dictionary<string,string>());
    if (theta0 == null) return false;
    bool Backtrack(List<(string,string[])> lits, Dictionary<string,string> theta) {
        if (lits.Count == 0) return true;
        foreach (var t in dBody) {
            var th = MatchAtom(lits[0], t, theta);
            if (th != null && Backtrack(lits.Skip(1).ToList(), th)) return true;
        }
        return false;
    }
    return Backtrack(c.Body, theta0);
}

var top = new Clause(("grandfather", new[]{"X","Y"}), new List<(string,string[])>());
var ground = expl1;
var chain = new[]{("top", top), ("cible", target), ("exemple au sol", ground)};
Console.WriteLine("Ordre de generalite top >= cible >= exemple au sol :");
for (int i = 0; i < chain.Length; i++)
for (int j = 0; j < chain.Length; j++) {
    if (i == j) continue;
    Console.WriteLine($"  {chain[i].Item1,15} subsume {chain[j].Item1,-15} ? {Subsumes(chain[i].Item2, chain[j].Item2)}");
}

Ordre de generalite top >= cible >= exemple au sol :
              top subsume cible           ? True
              top subsume exemple au sol  ? True
            cible subsume top             ? False
            cible subsume exemple au sol  ? True
   exemple au sol subsume top             ? False
   exemple au sol subsume cible           ? False

4. Clause bottom — saturation bornée

La clause bottom d’un exemple positif = on enrichit l’exemple avec tous les faits atteignables (profondeur depth), puis on variabilise les constantes. C’est la clause la plus spécifique qui couvre l’exemple ; la cible recherchée la subsume.

// Clause bottom de l'exemple : saturation bornee puis variabilisation.
(Clause clause, Dictionary<string,string> mapping) BottomClause(
        (string,string[]) example, List<(string,string[])> facts,
        HashSet<string> bodyPreds, int depth = 2) {
    var inScope = new HashSet<string>(example.Item2);
    var groundBody = new List<(string,string[])>();
    for (int step = 0; step < depth; step++) {
        foreach (var f in facts) {
            if (!bodyPreds.Contains(f.Item1)) continue;
            if (groundBody.Contains(f, new AtomEq())) continue;
            if (f.Item2.Any(a => inScope.Contains(a))) groundBody.Add(f);
        }
        foreach (var f in groundBody)
            foreach (var a in f.Item2) inScope.Add(a);
    }
    var mapping = new Dictionary<string,string>();
    string VarOf(string c) {
        if (!mapping.ContainsKey(c)) mapping[c] = $"V{mapping.Count + 1}";
        return mapping[c];
    }
    var head = (example.Item1, example.Item2.Select(VarOf).ToArray());
    var body = groundBody.Select(f => (f.Item1, f.Item2.Select(VarOf).ToArray())).ToList();
    return (new Clause(head, body), mapping);
}

var (bottom, bottomMap) = BottomClause(POS[0], FACTS, new HashSet<string>{"parent","male","female"}, depth: 2);
Console.WriteLine($"Exemple sature : {Fmt(POS[0])}");
Console.WriteLine($"\nClause bottom (profondeur 2, {bottom.Body.Count} litteraux) :");
Console.WriteLine($"  {ShowClause(bottom)}");
Console.WriteLine($"\nVariabilisation : " + string.Join(", ", bottomMap.Select(kv => $"{kv.Key} -> {kv.Value}")));
Console.WriteLine($"\nLa cible subsume-t-elle la clause bottom ? {Subsumes(target, bottom)}");

Exemple sature : grandfather(tom, ann)

Clause bottom (profondeur 2, 9 litteraux) :
  grandfather(V1, V2) :- parent(V1, V3), parent(V1, V4), parent(V3, V2), male(V1), female(V2), parent(V3, V5), parent(V4, V6), male(V3), female(V4).

Variabilisation : tom -> V1, ann -> V2, bob -> V3, liz -> V4, pat -> V5, sue -> V6

La cible subsume-t-elle la clause bottom ? True

5. Recherche Progol — meilleure clause consistante

Dans le treillis [top, bottom], on cherche la clause la plus générale consistante (couvre des positifs, aucun négatif). Score = positifs couverts − longueur du corps (biais de parcimonie). On restreint aux sous-ensembles connectés (liaison par variables) et on énumère les combinaisons.

// Chaque litteral du corps doit etre relie a la tete par les variables.
bool IsConnected((string,string[]) head, List<(string,string[])> bodySubset) {
    var reached = new HashSet<string>(head.Item2);
    var pending = new List<(string,string[])>(bodySubset);
    bool progress = true;
    while (pending.Count > 0 && progress) {
        progress = false;
        for (int i = pending.Count - 1; i >= 0; i--) {
            if (pending[i].Item2.Any(a => reached.Contains(a))) {
                foreach (var a in pending[i].Item2) reached.Add(a);
                pending.RemoveAt(i);
                progress = true;
            }
        }
    }
    return pending.Count == 0;
}

// Toutes les combinaisons de taille k (analogue itertools.combinations).
IEnumerable<List<(string,string[])>> Combinations(List<(string,string[])> items, int k) {
    if (k == 0) { yield return new List<(string,string[])>(); yield break; }
    for (int i = 0; i <= items.Count - k; i++) {
        var first = items[i];
        foreach (var rest in Combinations(items.Skip(i + 1).ToList(), k - 1)) {
            var combo = new List<(string,string[])>{first};
            combo.AddRange(rest);
            yield return combo;
        }
    }
}

// Resultat de la recherche Progol : clause candidate + score.
public record ProgolResult(Clause Clause, int P, double Score);

// Meilleure clause consistante dans [top, bottom], score = p - L.
ProgolResult? ProgolSearch(Clause bottom, List<(string,string[])> pos,
                           List<(string,string[])> neg,
                           List<(string,string[])> facts, int maxLen = 3) {
    ProgolResult? best = null;
    foreach (var sub in Enumerable.Range(1, maxLen).SelectMany(k => Combinations(bottom.Body, k))) {
        if (!IsConnected(bottom.Head, sub)) continue;
        var cl = new Clause(bottom.Head, sub);
        if (neg.Any(e => Covers(cl, e, facts))) continue;
        int p = pos.Count(e => Covers(cl, e, facts));
        if (p > 0 && (best == null || p - sub.Count > best.Score))
            best = new ProgolResult(cl, p, p - sub.Count);
    }
    return best;
}

List<Clause> ProgolLearn(List<(string,string[])> pos, List<(string,string[])> neg,
                         List<(string,string[])> facts, HashSet<string> bodyPreds,
                         int depth = 2, int maxLen = 3) {
    var remaining = new List<(string,string[])>(pos);
    var theory = new List<Clause>();
    while (remaining.Count > 0) {
        var (bottom, _) = BottomClause(remaining[0], facts, bodyPreds, depth);
        var best = ProgolSearch(bottom, remaining, neg, facts, maxLen);
        if (best == null) { Console.WriteLine($"  echec sur {Fmt(remaining[0])} : aucun candidat consistant"); break; }
        Console.WriteLine($"  bottom = {bottom.Body.Count} litteraux -> {ShowClause(best.Clause)}  (p={best.P}, score={best.Score})");
        theory.Add(best.Clause);
        remaining = remaining.Where(e => !Covers(best.Clause, e, facts)).ToList();
    }
    return theory;
}

Console.WriteLine("Apprentissage de grandfather/2 :");
var theory = ProgolLearn(POS, NEG, FACTS, new HashSet<string>{"parent","male","female"});
Console.WriteLine("\nTheorie finale :");
foreach (var c in theory) Console.WriteLine($"  {ShowClause(c)}");
int okPos = theory.Sum(c => POS.Count(e => Covers(c, e, FACTS)));
int okNeg = theory.Sum(c => NEG.Count(e => Covers(c, e, FACTS)));
Console.WriteLine($"\nVerification : {okPos}/{POS.Count} positifs couverts, {okNeg}/{NEG.Count} negatifs couverts");

Apprentissage de grandfather/2 :
  bottom = 9 litteraux -> grandfather(V1, V2) :- parent(V1, V3), parent(V3, V2), male(V1).  (p=4, score=1)

Theorie finale :
  grandfather(V1, V2) :- parent(V1, V3), parent(V3, V2), male(V1).

Verification : 4/4 positifs couverts, 0/6 negatifs couverts

6. Exemple guide — apprendre `grandmother/2`

Sur le même arbre, la seule grand-mère est liz (de eve) : liz parent de sue, sue parent de eve, et liz est female. Les autres grands-parents sont des grands-pères (male) → un seul positif. Avec un seul positif, ce sont les négatifs qui portent le signal et forcent le littéral female(X) (vs male(X) pour grandfather).

var POS_GM = new List<(string,string[])>{ ("grandmother", new[]{"liz","eve"}) };
var NEG_GM = new List<(string,string[])> {
    ("grandmother", new[]{"tom","ann"}), ("grandmother", new[]{"tom","pat"}),
    ("grandmother", new[]{"tom","sue"}), ("grandmother", new[]{"bob","jim"}),
    ("grandmother", new[]{"liz","ann"}), ("grandmother", new[]{"liz","pat"}),
    ("grandmother", new[]{"liz","sue"}), ("grandmother", new[]{"pat","jim"}),
    ("grandmother", new[]{"sue","eve"}), ("grandmother", new[]{"ann","jim"}),
};
Console.WriteLine("Apprentissage de grandmother/2 :");
var theoryGm = ProgolLearn(POS_GM, NEG_GM, FACTS, new HashSet<string>{"parent","male","female"});
Console.WriteLine("\nTheorie finale :");
foreach (var c in theoryGm) Console.WriteLine($"  {ShowClause(c)}");
int okPosGm = theoryGm.Sum(c => POS_GM.Count(e => Covers(c, e, FACTS)));
int okNegGm = theoryGm.Sum(c => NEG_GM.Count(e => Covers(c, e, FACTS)));
Console.WriteLine($"\nVerification : {okPosGm}/{POS_GM.Count} positif(s) couvert(s), {okNegGm}/{NEG_GM.Count} negatif(s) couvert(s)");
var targetGm = new Clause(
    ("grandmother", new[]{"X","Y"}),
    new List<(string,string[])>{
        ("female", new[]{"X"}), ("parent", new[]{"X","Z"}), ("parent", new[]{"Z","Y"})});
bool equiv = theoryGm.Any(c => Subsumes(c, targetGm) && Subsumes(targetGm, c));
Console.WriteLine($"Equivalente a grandmother(X,Y) :- female(X), parent(X,Z), parent(Z,Y) ? {equiv}");

Apprentissage de grandmother/2 :
  bottom = 8 litteraux -> grandmother(V1, V2) :- parent(V1, V4), parent(V4, V2), female(V1).  (p=1, score=-2)

Theorie finale :
  grandmother(V1, V2) :- parent(V1, V4), parent(V4, V2), female(V1).

Verification : 1/1 positif(s) couvert(s), 0/10 negatif(s) couvert(s)
Equivalente a grandmother(X,Y) :- female(X), parent(X,Z), parent(Z,Y) ? True

7. Pont vers le solveur SOTA : SWI-Prolog (Process.Start)

Le notebook Python SL-5-InverseResolution.ipynb invoque les vrais moteurs ILP via janus_swi : Aleph (Progol en chair et en os), Metagol, Popper — tous des programmes SWI-Prolog. L’édition précédente de ce jumeau déclarait le pont « hors scope C# pur (Prong B) » et la paire était labellisée RECOVERABLE-LOCAL (#10382). Ce verdict est révoqué : le pendant C# honnête est Process.Start sur le même exécutable (mandat #10382, bucket 2 : « le moteur est un binaire, le pendant C# honnête est Process.Start sur le même exécutable — pas une réimplémentation »).

La cellule suivante :

rejoue le programme appris par le Progol from-scratch de la cellule 6 (theoryGm) — la clause grandmother(V1,V2) :- parent(V1,V4), parent(V4,V2), female(V1) — sous forme d’un fichier Prolog chargé par SWI-Prolog ;
interroge le moteur : grandmother/2 est-il dérivé sur liz → eve (le positif) et jamais sur les 10 négatifs ?
vérifie la parité : la théorie from-scratch et le moteur SOTA s’accordent.

Axe (checklist #10459)	Réponse
1 · NuGet .NET	N/A — pas de binding SWI-Prolog officiel pour .NET
2 · P/Invoke	N/A — pas de DLL C stable documentée invocable
3 · CLI `Process.Start`	LE CANAL — `swipl.exe` (`swipl` hors Windows) est un binaire invocable
4 · IKVM	N/A — SWI-Prolog n’est pas une lib Java
5 · PythonNet	N/A — pas besoin de pont CPython, le binaire suffit
6 · lib équivalente	SWI-Prolog = le moteur SOTA utilisé par Aleph/Metagol/Popper (`janus_swi`)

Verdict : SOTA-OK (pont) — le from-scratch est conservé (il enseigne les internes de Progol), le pont est en plus, jamais à la place.

// === Pont SWI-Prolog (Process.Start) : le moteur SOTA derrière Aleph, invoqué depuis le C# ===
using System.IO;
using System.Diagnostics;

// Resout l'executable swipl : variable SWIPL_DIR -> chemins standard -> PATH -> throw.
string FindSwiplCmd()
{
    // Binaire SWI-Prolog : swipl.exe sous Windows, swipl ailleurs
    var swiplName = OperatingSystem.IsWindows() ? "swipl.exe" : "swipl";
    var envDir = Environment.GetEnvironmentVariable("SWIPL_DIR");
    if (!string.IsNullOrEmpty(envDir))
    {
        var exe = Path.Combine(envDir, swiplName);
        if (File.Exists(exe)) return exe;
    }
    // Pattern du jumeau Python (cellule 20, xplat #10646) : install portable SWI-Prolog.
    var userProfile = Environment.GetFolderPath(Environment.SpecialFolder.UserProfile);
    var candidates = new[] {
        Path.Combine(userProfile, "OneDrive", "Documents", "swipl", "bin", "swipl.exe"),
        Path.Combine(userProfile, "Documents", "swipl", "bin", "swipl.exe"),
        Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.MyDocuments), "swipl", "bin", "swipl.exe"),
        @"C:\Program Files\swipl\bin\swipl.exe",
        "/usr/bin/swipl",
        "/usr/local/bin/swipl",
    };
    foreach (var c in candidates)
        if (File.Exists(c)) return c;
    // Dernier recours, comme shutil.which("swipl") du jumeau : le PATH
    // (Homebrew /opt/homebrew/bin sur Apple Silicon, conda, nix...).
    foreach (var dir in (Environment.GetEnvironmentVariable("PATH") ?? "")
                 .Split(Path.PathSeparator, StringSplitOptions.RemoveEmptyEntries))
    {
        var exe = Path.Combine(dir, swiplName);
        if (File.Exists(exe)) return exe;
    }
    throw new FileNotFoundException(
        "SWI-Prolog introuvable. Installer SWI-Prolog (https://www.swi-prolog.org) : " +
        "Windows choco install swi-prolog  |  macOS brew install swi-prolog  |  apt install swi-prolog");
}

// C# -> Prolog : les variables de theoryGm sont deja en MAJUSCULES (V1, V2...),
// les constantes et predicats en minuscules -- le format est directement valide.
string PrologFact((string,string[]) a) => $"{a.Item1}({string.Join(",", a.Item2)}).";
string PrologRule(Clause c) => c.Body.Count == 0
    ? $"{Fmt(c.Head)}."
    : $"{Fmt(c.Head)} :- {string.Join(",", c.Body.Select(Fmt))}.";

// 1. Programme Prolog : faits du domaine + theorie apprise par le Progol from-scratch (cellule 6)
string plPath = Path.Combine(Path.GetTempPath(), $"sl5_grandmother_{Guid.NewGuid():N}.pl");
var plLines = new List<string>();
foreach (var f in FACTS) plLines.Add(PrologFact(f));
foreach (var r in theoryGm) plLines.Add(PrologRule(r));
File.WriteAllText(plPath, string.Join("\n", plLines));

// 2. Invocation SWI-Prolog : charger le programme, imprimer les derivations grandmother/2, quitter
string swipl = FindSwiplCmd();
var goal = "findall((X,Y), grandmother(X,Y), L), " +
           "forall(member((X,Y), L), format('gm(~w,~w).~n', [X,Y])), halt.";
var psi = new ProcessStartInfo(swipl)
{
    RedirectStandardOutput = true, RedirectStandardError = true,
    UseShellExecute = false, CreateNoWindow = true,
    WorkingDirectory = Path.GetDirectoryName(plPath) ?? Path.GetTempPath(),
};
psi.ArgumentList.Add("-q");
psi.ArgumentList.Add("-f");
psi.ArgumentList.Add(Path.GetFileName(plPath));
psi.ArgumentList.Add("-g");
psi.ArgumentList.Add(goal);
var proc = Process.Start(psi);
string stdout = proc.StandardOutput.ReadToEnd();
string stderr = proc.StandardError.ReadToEnd();
proc.WaitForExit();

// 3. Parse des atomes "gm(X,Y)." imprimes par Prolog
var derived = new HashSet<(string,string)>();
foreach (var line in stdout.Split('\n'))
{
    string s = line.Trim();
    if (s.StartsWith("gm(") && s.EndsWith(")."))
    {
        var inner = s.Substring(3, s.Length - 3 - 2);
        var parts = inner.Split(',');
        derived.Add((parts[0], parts[1]));
    }
}

// 4. Verdict de parite : la theorie from-scratch derive-t-elle exactement les positifs ?
Console.WriteLine("===== Pont SWI-Prolog (Process.Start) =====");
Console.WriteLine($"Programme Prolog ({plLines.Count} lignes) :");
foreach (var l in plLines) Console.WriteLine($"  {l}");
Console.WriteLine($"Solveur : {Path.GetFileName(swipl)}");
Console.WriteLine();
Console.WriteLine($"grandmother/2 derivees par SWI-Prolog : {derived.Count}");
foreach (var (x, y) in derived.OrderBy(d => d.Item1).ThenBy(d => d.Item2))
    Console.WriteLine($"  grandmother({x}, {y})");
Console.WriteLine();
int posCovers = POS_GM.Count(e => derived.Contains((e.Item2[0], e.Item2[1])));
int negLeaks = NEG_GM.Count(e => derived.Contains((e.Item2[0], e.Item2[1])));
Console.WriteLine($"POSITIVES couverts : {posCovers}/{POS_GM.Count}");
Console.WriteLine($"NEGATIVES atteints  : {negLeaks}/{NEG_GM.Count}");
Console.WriteLine($"Verdict parite : {(posCovers == POS_GM.Count && negLeaks == 0 ? "theorie from-scratch == SWI-Prolog (SOTA) sur grandmother/2" : "ECART - investiguer")}");

===== Pont SWI-Prolog (Process.Start) =====
Programme Prolog (16 lignes) :
  parent(tom,bob).
  parent(tom,liz).
  parent(bob,ann).
  parent(bob,pat).
  parent(liz,sue).
  parent(pat,jim).
  parent(sue,eve).
  male(tom).
  male(bob).
  male(jim).
  female(liz).
  female(ann).
  female(pat).
  female(sue).
  female(eve).
  grandmother(V1, V2) :- parent(V1, V4),parent(V4, V2),female(V1).
Solveur : swipl

grandmother/2 derivees par SWI-Prolog : 1
  grandmother(liz, eve)

POSITIVES couverts : 1/1
NEGATIVES atteints  : 0/10
Verdict parite : theorie from-scratch == SWI-Prolog (SOTA) sur grandmother/2

Lecture du résultat : théorie from-scratch ≡ SWI-Prolog (SOTA)

SWI-Prolog dérive exactement 1 couple : grandmother(liz, eve) — le seul positif POS_GM. Les 10 négatifs (tom→ann, liz→sue, pat→jim, …) ne sont jamais dérivés. La règle apprise par le Progol from-scratch de la cellule 6 — grandmother(V1,V2) :- parent(V1,V4), parent(V4,V2), female(V1) — coïncide donc avec le moteur SOTA sur ce problème. C’est le même moteur (SWI-Prolog) que le jumeau Python invoque via janus_swi pour Aleph : la parité est ici native-both (les deux jumeaux référencent un moteur externe).

Le from-scratch garde sa valeur pédagogique : il montre comment Progol construit la clause bottom et explore le treillis [top, bottom]. Le pont vérifie que ce que la théorie apprend est bien ce que le moteur réel dérive.

Exercice : apprendre `uncle/2`

Appliquez ProgolLearn pour apprendre uncle(X, Y) (X oncle de Y : X frère du parent de Y). Définissez les positifs/négatifs sur l’arbre, puis vérifiez que la clause apprise est équivalente à uncle(X,Y) :- male(X), parent(Z,Y), parent(Z,X) où Z est le parent commun.

Indice : sur cet arbre, bob est frère de liz, liz est mère de sue → bob est oncle de sue. Les négatifs doivent exclure (a) les tantes (female), (b) le père lui-même (parent direct), (c) les grands-pères.

// EXERCICE : apprendre uncle/2
// var POS_UNCLE = new List<(string,string[])>{
//     ("uncle", new[]{"bob","sue"}),  // bob frere de liz, liz mere de sue
//     // TODO etudiant : autres oncles de l'arbre
// };
// var NEG_UNCLE = new List<(string,string[])>{
//     // TODO etudiant : exclure tantes (female), parents directs, grands-peres
// };
// var theoryUncle = ProgolLearn(POS_UNCLE, NEG_UNCLE, FACTS, new HashSet<string>{"parent","male","female"});
Console.WriteLine("Exercice uncle/2 a completer (voir indice ci-dessus).");

Exercice uncle/2 a completer (voir indice ci-dessus).

// EXERCICE 2 : profondeur de la clause bottom (cf. cellule 16 : "profondeur de la clause bottom").
// On teste BottomClause avec depth=1 vs depth=3 sur l'exemple grandmother de la cellule 12.
// Questions : combien de litteraux dans chaque clause bottom ? La cible (grandmother) subsume-t-elle
// toujours la clause bottom a profondeur 1 ? Pourquoi une profondeur importante cree une explosion
// combinatoire dans ProgolSearch ?
// Indice : BottomClause renvoie (Clause clause, Dictionary<string,string> mapping) ; le nombre de
//          litteraux du corps = clause.Body.Count. A depth=1 seuls les faits relies directement a
//          l'exemple sont satures ; a depth=3 la fermeture s'etend (explosion).

// TODO etudiant : comparez les deux profondeurs sur l'exemple grandmother/2.
void Compare_BottomClause_Depth() {
    // Etape 1 : reprendre l'exemple positif grandmother (POS_GM, FACTS de la cellule 12).
    // Etape 2 : appeler BottomClause(..., depth:1) puis BottomClause(..., depth:3).
    // Etape 3 : afficher le nombre de litteraux du corps pour chaque profondeur.
    // Etape 4 : conclure sur l'explosion combinatoire.
}

Console.WriteLine("Exercice 2 a completer : profondeur de la clause bottom (depth 1 vs 3).");

Exercice 2 a completer : profondeur de la clause bottom (depth 1 vs 3).

// EXERCICE 3 : tolerance au bruit (cf. cellule 16 : "tolerance au bruit").
// On ajoute un exemple positif erronne (ex : ("grandfather", new[]{"ann","jim"}) alors qu'ann est
// female) au jeu grandmother. Que se passe-t-il avec ProgolLearn (qui rejette toute clause couvrant
// un negatif) ? Proposez un mecanisme de tolerance : score p - n - L autorisant quelques negatifs
// couverts, au lieu de tout rejeter.
// Indice : ProgolLearn cherche la clause couvrant le max de positifs SANS couvrir aucun negatif.
//          Pour tolerer le bruit, autoriser une clause qui couvre <= k negatifs (k petit), et
//          penaliser le score de n (negatifs couverts) au lieu de l'annuler.

// TODO etudiant : implementez une variante tolerante du score Progol.
List<string> ProgolLearn_Noise_Tolerant(
        List<(string,string[])> pos, List<(string,string[])> neg,
        List<(string,string[])> facts, HashSet<string> bodyPreds, int k = 1) {
    // Etape 1 : reprendre la recherche de clauses de ProgolLearn.
    // Etape 2 : autoriser une clause qui couvre <= k negatifs (au lieu de 0).
    // Etape 3 : score = positifs_couverts - negatifs_couverts - longueur_clause.
    // Etape 4 : renvoyer la meilleure theorie tolerante.
    return new List<string>();  // TODO etudiant
}

Console.WriteLine("Exercice 3 a completer : tolerance au bruit (k=1 negatif autorise).");

Exercice 3 a completer : tolerance au bruit (k=1 negatif autorise).

Bilan

Ce notebook a présenté la résolution inverse et l’ILP from-scratch en C#, jumeau du notebook Python :

Représentation des clauses Horn (record Clause) + couverture par unification (Covers).
LGG (Plotkin) : généraliser deux explications en une variable partagée.
θ-subsomption : skolemisation + backtracking pour ordonner la généralité.
Clause bottom : saturation bornée + variabilisation (clause la plus spécifique).
Recherche Progol : meilleure clause consistante, score p − L, mode connecté.
Apprentissage de grandfather/2 et grandmother/2 (négatifs = signal).

Parité : jumeau C# de SL-5-InverseResolution.ipynb. Les deux implémentent les mêmes algorithmes from-scratch (pas de lib ML). Marathon parité .NET ⇄ Python (#4956), EPIC #3801 (Prong B).

Exercices supplémentaires

Exercice 2 : profondeur de la clause bottom

Testez BottomClause avec depth=1 vs depth=3. Combien de littéraux ? La cible subsume-t-elle toujours la clause bottom à profondeur 1 ? Pourquoi une profondeur importante crée-t-elle une explosion combinatoire dans ProgolSearch ?

Exercice 3 : tolérance au bruit

Ajoutez un exemple positif erroné (ex : ("grandfather", new[]{"ann","jim"})). Que se passe-t-il ? Proposez un mécanisme de tolérance (ex : score p − n − L autorisant quelques négatifs couverts, au lieu de tout rejeter).

Exercice 4 : réduction de Plotkin

Implémentez une réduction de théorie : si une clause C θ-subsume une autre D dans la théorie apprise, retirer la plus spécifique. Pourquoi cela évite-t-il la prolifération de clauses redondantes ?

Références

Russell & Norvig, AIMA (3e éd.), §19.5.
Plotkin, G. D. A Note on Inductive Generalization (1970) — LGG, θ-subsomption.
Muggleton, S. Inverse Entailment and Progol (1995) — clause bottom.
Notebook Python : SL-5-InverseResolution.ipynb.
Marathon parité : #4956.

Retour au sommet

Objectifs d’apprentissage

Prérequis

Durée estimée : 65 minutes

Références

1. Représentation : atomes, clauses, couverture

2. LGG — Least General Generalization (Plotkin)

3. θ-subsomption — ordre de généralité

4. Clause bottom — saturation bornée

5. Recherche Progol — meilleure clause consistante

6. Exemple guide — apprendre grandmother/2

7. Pont vers le solveur SOTA : SWI-Prolog (Process.Start)

Lecture du résultat : théorie from-scratch ≡ SWI-Prolog (SOTA)

Exercice : apprendre uncle/2

Bilan

Exercices supplémentaires

Exercice 2 : profondeur de la clause bottom

Exercice 3 : tolérance au bruit

Exercice 4 : réduction de Plotkin

Références

6. Exemple guide — apprendre `grandmother/2`

Exercice : apprendre `uncle/2`