Skip to the content

EXECUTED, WITH ASSERTIONS

This program was run during verification and its results asserted. The runner that does it is tools/run_ai_labs.py.

The code

Straight from labs/course-13a-ai/01_family_tree.py, unchanged.

"""Experiment 1 — A family tree, executed as a logic program.

This is NOT a simulation. pytholog implements SLD resolution over Horn
clauses, so the recursive ancestor/2 rule below is genuinely resolved the way
Prolog would resolve it -- including finding kiran, who is three levels down
and reachable only by recursion.
"""
import pytholog as pl

from fixtures import FAMILY_FACTS, FAMILY_RULES


def build():
    kb = pl.KnowledgeBase("family")
    kb(FAMILY_FACTS + FAMILY_RULES)
    return kb


def answers(kb, goal, var="X"):
    """Sorted distinct bindings for one variable -- Prolog's setof/3."""
    result = kb.query(pl.Expr(goal))
    if result in (["No"], []):
        return []
    return sorted({r[var] for r in result if isinstance(r, dict) and var in r})


def facts_and_simple_rules():
    kb = build()

    assert answers(kb, "parent(ram, X)") == ["asha", "ravi"]
    assert answers(kb, "father(X, asha)", "X") == ["ram"]
    assert answers(kb, "mother(X, asha)", "X") == ["sita"]
    assert answers(kb, "grandparent(ram, X)") == ["bhanu", "kiran", "meena"]

    print(f"  parent(ram, X)        -> {answers(kb, 'parent(ram, X)')}")
    print(f"  father(X, asha)       -> {answers(kb, 'father(X, asha)', 'X')}")
    print(f"  mother(X, asha)       -> {answers(kb, 'mother(X, asha)', 'X')}")
    print(f"  grandparent(ram, X)   -> {answers(kb, 'grandparent(ram, X)')}")
    print("       father/2 and mother/2 are the SAME rule with a different")
    print("       guard. That is what makes logic programming compact")


def recursion_is_what_makes_ancestor_work():
    """The point of the experiment: kiran is reachable only by recursing."""
    kb = build()

    descendants = answers(kb, "ancestor(ram, X)")
    assert descendants == ["asha", "bhanu", "kiran", "meena", "ravi"], descendants

    # One level down is the base case; two and three need the recursive clause.
    direct = answers(kb, "parent(ram, X)")
    assert set(direct) == {"asha", "ravi"}
    assert {"kiran", "meena", "bhanu"} <= set(descendants)
    assert {"kiran", "meena", "bhanu"} & set(direct) == set()

    print(f"  parent(ram, X)   -> {direct}                (1 level)")
    print(f"  ancestor(ram, X) -> {descendants}")
    print("       kiran, meena and bhanu are TWO levels down and appear only")
    print("       through the recursive clause. Delete it and they vanish.")
    print("       This is genuine SLD resolution, not a table lookup")


def base_case_must_come_first():
    """Clause ORDER matters in Prolog, and does not matter in logic."""
    good = pl.KnowledgeBase("good")
    good(FAMILY_FACTS + [
        "anc(X, Y) :- parent(X, Y)",                   # base case FIRST
        "anc(X, Y) :- parent(X, Z), anc(Z, Y)",
    ])
    result = good.query(pl.Expr("anc(ram, X)"))
    found = sorted({r["X"] for r in result if isinstance(r, dict)})
    assert found == ["asha", "bhanu", "kiran", "meena", "ravi"], found

    print(f"  base case first -> {found}")
    print("       with the RECURSIVE clause first, SWI-Prolog recurses before")
    print("       it can ever reach a fact, and a left-recursive rule such as")
    print("       'anc(X,Y) :- anc(X,Z), parent(Z,Y)' loops for ever.")
    print("       Clause order matters in Prolog and does NOT matter in logic --")
    print("       because Prolog is backward chaining with DEPTH-FIRST search")


def sibling_needs_the_inequality_guard():
    kb = build()
    siblings = answers(kb, "sibling(asha, X)")
    assert siblings == ["ravi"], siblings
    assert "asha" not in siblings, "the neq guard stops asha being her own sibling"

    # Without the guard, everyone is their own sibling.
    loose = pl.KnowledgeBase("loose")
    loose(FAMILY_FACTS + ["sib(X, Y) :- parent(P, X), parent(P, Y)"])
    bad = sorted({r["X"] for r in loose.query(pl.Expr("sib(asha, X)"))
                  if isinstance(r, dict)})
    assert "asha" in bad, bad

    print(f"  sibling(asha, X)  with the guard -> {siblings}")
    print(f"  without the guard                -> {bad}   <- asha is her own sibling")
    print("       every parent(P,X), parent(P,Y) pair unifies with X = Y unless")
    print("       you forbid it. In SWI-Prolog the guard is X \\\\= Y")


def duplicate_solutions_are_real():
    """asha and ravi share TWO parents, so Prolog proves sibling twice."""
    kb = build()
    raw = kb.query(pl.Expr("sibling(asha, X)"))
    bindings = [r["X"] for r in raw if isinstance(r, dict) and "X" in r]
    distinct = sorted(set(bindings))

    assert distinct == ["ravi"]
    assert len(bindings) >= 1

    print(f"  raw solutions for sibling(asha, X): {bindings}")
    print(f"  distinct                          : {distinct}")
    print("       asha and ravi share BOTH ram and sita, so in SWI-Prolog the")
    print("       goal succeeds once per shared parent -- one solution per PROOF,")
    print("       not per answer. setof/3 collapses them, and this is a property")
    print("       of resolution rather than a bug")


def cousins_expose_an_engine_limitation():
    """Two encodings of the same logic. One of them breaks pytholog.

    This is worth seeing rather than hiding: the .pl file uses the idiomatic
    nested form, which SWI-Prolog handles correctly. pytholog does not
    propagate neq/2 correctly through a nested derived predicate, so the same
    rule returns wrong answers here -- and the FLAT formulation, which asks
    the same question without an intermediate rule, gets it right.
    """
    # (a) The flat form: kiran and Y have different parents who share a parent.
    flat = pl.KnowledgeBase("flat")
    flat(FAMILY_FACTS + [
        "cousin(X, Y) :- parent(A, X), parent(B, Y), "
        "parent(G, A), parent(G, B), neq(A, B)"])
    flat_answers = sorted({r["X"] for r in flat.query(pl.Expr("cousin(kiran, X)"))
                           if isinstance(r, dict)})
    assert flat_answers == ["bhanu"], flat_answers

    # (b) The nested form, which is what the .pl file uses.
    nested = pl.KnowledgeBase("nested")
    nested(FAMILY_FACTS + [
        "sib(X, Y) :- parent(P, X), parent(P, Y), neq(X, Y)",
        "cousin(X, Y) :- parent(A, X), parent(B, Y), sib(A, B)"])
    nested_answers = sorted({r["X"] for r in nested.query(pl.Expr("cousin(kiran, X)"))
                             if isinstance(r, dict)})
    assert nested_answers == ["bhanu", "kiran", "meena"], nested_answers
    assert "kiran" in nested_answers, "kiran is returned as his OWN cousin"

    print(f"  flat rule   (no intermediate predicate) -> {flat_answers}   CORRECT")
    print(f"  nested rule (calls sib/2)               -> {nested_answers}")
    print("       the nested answer is WRONG: kiran is not his own cousin, and")
    print("       meena is his SISTER. pytholog does not propagate neq/2")
    print("       correctly through a nested derived predicate.")
    print("       SWI-Prolog handles the nested form correctly, and the .pl file")
    print("       uses it because it is the idiomatic encoding. This is an")
    print("       ENGINE limitation, not a flaw in the logic -- and it is why")
    print("       the .pl file is the deliverable and this file is the check")


def main():
    print("Experiment 1 -- A family tree as a logic program")
    # Step 1: State the facts and simple rules
    facts_and_simple_rules()
    # Step 2: Resolve the recursive ancestor/2
    recursion_is_what_makes_ancestor_work()
    # Step 3: Put the base case first
    base_case_must_come_first()
    # Step 4: Guard sibling/2 against X = Y
    sibling_needs_the_inequality_guard()
    # Step 5: Count one solution per proof
    duplicate_solutions_are_real()
    # Step 6: Find cousins, and pytholog's limit
    cousins_expose_an_engine_limitation()


if __name__ == "__main__":
    main()

Where this sits

One experiment from the Artificial Intelligence lab. The rest of them, and the theory behind this one, are on the lab page.