Logic Programming: How Prolog Answers a Query

in progressThis lesson is still being built - content, demos, and checkpoints may change before release.

Logic programming

Loading interactive demo…

The tree is the search: the query at the top, and below each node one child per clause whose head unified with its first goal, labelled by the goal selected there, with the clause number on the edge. The sheet is the program, and the goals strip the list still to prove at this step, first goal first; the solutions strip collects the answers found.Take the tour, or press and explore. Legend:

The panel beside the stage is the real BackwardChainer class from the published library executing in your browser, with the current line highlighted.

The node and clause at work this step.
A solution leaf, and a clause whose head just unified.
A failed leaf, a clause that did not match, a branch cut by the depth cap; the tapped clause's edges.
A node still open, with clauses left to try.

solutions counts the answers found, goals the goals selected so far, backtracks the returns to an earlier choice, depth the current branch's depth against the cap. Tap a clause to light its edges.

The code panel shows bare executable code by default. The bar above it names the file (hover the name for the full published path); options holds the toggles: comments, the tracer instrumentation that produces this visualization, and verbose names for the terse identifiers (display only: the default is the byte-exact published file). The view switch adds plain-English narration: both interleaves it with the code, pseudo shows only the pseudocode. hide code collapses the panel; the rail it leaves behind brings it back.

Keys: Space play/pause · ←/→ step · Home/End jump · R reset · F fullscreen · G guided tour

Clauses as procedures. A definite clause $H \leftarrow B_1, \dots, B_n$ reads two ways. Logically: $H$ holds if every $B_i$ does. Procedurally: to solve a call matching $H$ , solve the calls $B_1 \dots B_n$ in turn. A fact is a clause with no body; a query $\leftarrow G_1, \dots, G_k$ is a clause with no head, the negation of what is to be proved. Resolution between a query and a clause is one procedure call.

SLD resolution. Select the first goal $G_1$ (the S), find a clause whose head unifies with it under the most general unifier $\theta$ (the L for linear: the query is always one parent), and replace $G_1$ by the clause's body, applying $\theta$ to everything, with the clause's variables first renamed apart (the D for definite). The empty query is the empty clause: a refutation, so the original query follows, and $\theta$ composed along the branch, restricted to the query's variables, is the answer.

The search tree. Each node is a goal list; each child applies one clause to the first goal. Prolog walks this tree depth-first in clause order, which makes the search a stack of choice points. A failed leaf, a goal no clause matches, backtracks to the most recent choice point and tries its next clause, undoing the bindings made since. A solution is also followed by backtracking, because the user may ask for more.

Completeness and its loss. SLD resolution is complete for definite programs: if a query follows, some branch of the tree succeeds. Depth-first search is not complete: an infinite branch to the left of a success is never left. The left-recursive path rule calls path before edge and recurses forever on the first clause; the same rule with the edge first terminates. The depth cap here makes that branch visible instead of fatal. Breadth-first or iterative-deepening search would be complete but is far more expensive, and Datalog sidesteps the issue by evaluating bottom-up, as the forward chaining lesson did.

Cost. Each step is a unification, linear in the terms with sharing, and the tree can be exponential in the program. Real systems index clauses by the first argument so a goal tries only the clauses that could match, keep a trail of bindings to undo on backtracking, and compile clauses to the Warren Abstract Machine. The stage's chainer tries every clause in order and copies bindings instead of trailing them; the trace is the same.

Choices worth reading closely in the implementation (the code panel's comments and tracer checkboxes reveal the full published file):

Clauses are renamed on every use, with a running suffix, so a recursive clause's X in one call never collides with its X in the next; Prolog does the same with fresh heap cells.
Unification is the previous lesson's Unifier, untraced, called on the selected goal with the bindings already applied, so its result merges straight into the branch's bindings.
Backtracking is the recursion returning: no trail, since each branch carries its own map of bindings; a real system undoes bindings in place instead of copying.
A depth cap and a solution cap keep the trace finite: the left-recursive program hits the first, and the search stops after three answers rather than enumerating forever.

Resolution proved theorems but gave no control over the search. In 1972 Alain Colmerauer's group in Marseille built a system for natural language processing whose grammar rules were Horn clauses and whose parser was a resolution prover, and Robert Kowalski showed that such clauses can be read as procedures: a rule's head is a call, its body the calls it makes, and resolution with the first goal and the first clause is the execution. That reading made Prolog a programming language, and David Warren's abstract machine made it fast. The chainer here is the reading in full.

1972Alain Colmerauer and Philippe Roussel - The first Prolog, in Marseille, runs Horn clauses as a language for parsing French.source
1974Robert Kowalski - 'Predicate Logic as Programming Language' gives the procedural reading of Horn clauses and names SLD resolution.source
1977David H. D. Warren - DEC-10 Prolog compiles clauses to native code and matches Lisp in speed, the implementation that spread the language.source
1983David H. D. Warren - The Warren Abstract Machine: registers, a heap, a trail for undoing bindings on backtracking, and choice points, still the model for Prolog compilers.source
1986Datalog - Prolog without function symbols, evaluated bottom-up, becomes the query language of deductive databases and, later, program analysis.source

Used today

Prolog and its descendants - SWI-Prolog, SICStus, and the constraint logic languages run this search with a trail, choice points, and clause indexing; the depth cap here stands in for the stack.
Datalog engines - Souffle, CodeQL, and Datomic answer queries over Horn rules without function symbols, bottom-up instead of this top-down search, so recursion cannot loop.
Type class and trait resolution - Haskell's instance search and Rust's trait solver are backward chaining over instance declarations, with the same renaming and unification.

program

depth cap6

solutions: 2
goals: 3
backtracks: 4
depth: 2 of 6

backward-chainer.ts

import type { Tracer } from "../trace";import { applySubstitution, termText, termVariables, variable, type Term } from "./terms";import { Unifier } from "./unifier";/** A program clause: a head that holds when every body goal does; a fact has no body. */export interface ProgramClause {  head: Term;  body: Term[];}export interface LogicProgram {  clauses: ProgramClause[];}export interface SldResult {  /** Each solution as the query's variables bound, `W = ann`, or `yes` for a ground query. */  solutions: string[];  /** Goals selected. */  steps: number;  /** Whether some branch hit the depth cap, so the search was not exhaustive. */  limited: boolean;}/** The most goals a run selects: a safety net beneath the depth cap. */export const MAX_SLD_STEPS = 300;/** * SLD resolution, how Prolog answers a query: take the first goal, * try the program's clauses in order, rename a clause's variables so * two uses never share one, unify its head with the goal, and replace * the goal by the clause's body under the bindings. No goals left is * a solution, read off the query's variables; a goal no clause * unifies with fails, and the search backtracks to the next clause * of the nearest choice. Depth-first in clause order, which is what * makes a left-recursive clause loop; a depth cap turns that loop * into a visible limit. * * Time: exponential in the worst case. Space: O(depth). */export class BackwardChainer {  private steps = 0;  private nodes = 0;  private limited = false;  private solutions: string[] = [];  constructor(    private readonly tracer?: Tracer,    private readonly maxDepth = 8,    private readonly maxSolutions = 3,  ) {}  query(program: LogicProgram, goals: readonly Term[]): SldResult {    this.steps = 0;    this.nodes = 0;    this.limited = false;    this.solutions = [];    const asked = goals.reduce<string[]>((vars, goal) => termVariables(goal, vars), []);    this.search(program, [...goals], new Map(), 0, this.nodes++, asked);    return { solutions: [...this.solutions], steps: this.steps, limited: this.limited };  }  private search(program: LogicProgram, goals: Term[], bindings: ReadonlyMap<string, Term>, depth: number, node: number, asked: readonly string[]): void {    if (goals.length === 0) {      const answer = asked.length === 0 ? "yes" : asked.map((name) => `${name} = ${termText(applySubstitution(variable(name), bindings))}`).join(", ");      this.solutions.push(answer);      // ▸ no goals left: the bindings are an answer      this.tracer?.emit("solution", { node, answer, count: this.solutions.length });      return;    }    const [first, ...rest] = goals;    const [first, ...remainingGoals] = goals;    const selected = applySubstitution(first!, bindings);    this.steps += 1;    // ▸ the first goal is the one to prove next    this.tracer?.emit("select-goal", { node, goal: termText(selected), goals: goals.map((g) => termText(applySubstitution(g, bindings))), depth });    if (depth >= this.maxDepth) {      this.limited = true;      // ▸ too deep: give up on this branch      this.tracer?.emit("depth-limit", { node, goal: termText(selected), depth });      return;    }    if (this.steps >= MAX_SLD_STEPS) return;    for (let index = 0; index < program.clauses.length && this.solutions.length < this.maxSolutions; index++) {      const renamed = BackwardChainer.rename(program.clauses[index]!, depth + 1);      const freshClause = BackwardChainer.rename(program.clauses[index]!, depth + 1);      // ▸ rename the clause's variables and try its head      this.tracer?.emit("try-clause", { node, clause: index, head: termText(renamed.head), goal: termText(selected) });      this.tracer?.emit("try-clause", { node, clause: index, head: termText(freshClause.head), goal: termText(selected) });      // Head first, so a head variable binds to the goal's and the goal's own variables survive in the resolvent.      const result = new Unifier().unify(renamed.head, selected);      const result = new Unifier().unify(freshClause.head, selected);      if (!result.unified) {        // ▸ the head does not unify: next clause        this.tracer?.emit("fail", { node, clause: index, reason: result.failure });        continue;      }      const merged = new Map([...bindings, ...result.bindings]);      const next = [...renamed.body, ...rest];      const next = [...freshClause.body, ...remainingGoals];      const child = this.nodes++;      // ▸ the head unifies: the goal becomes the clause body      this.tracer?.emit("unify", { node, clause: index, child, bindings: Unifier.text(result.bindings), goals: next.map((g) => termText(applySubstitution(g, merged))) });      this.search(program, next, merged, depth + 1, child, asked);      // ▸ that branch is done: try the next clause      if (this.solutions.length < this.maxSolutions) this.tracer?.emit("backtrack", { node, clause: index, goal: termText(selected) });    }  }  /**   * The clause with every variable suffixed by the depth it is used at, so two uses of one clause   * along a branch never share a variable; siblings may, since each branch keeps its own bindings.   */  private static rename(clause: ProgramClause, depth: number): ProgramClause {    const suffix = `${depth}`;    const fresh = (term: Term): Term => (term.kind === "variable" ? { kind: "variable", name: term.name + suffix } : { kind: "function", name: term.name, args: term.args.map(fresh) });    return { head: fresh(clause.head), body: clause.body.map(fresh) };  }}

solutions =: 2
steps =: 3

2 solutions to grandparent(tom, W): W = ann, W = pat, after 3 goals.

import type { Tracer } from "../trace";import { applySubstitution, termText, termVariables, variable, type Term } from "./terms";import { Unifier } from "./unifier";/** A program clause: a head that holds when every body goal does; a fact has no body. */export interface ProgramClause { head: Term; body: Term[];}export interface LogicProgram { clauses: ProgramClause[];}export interface SldResult { /** Each solution as the query's variables bound, `W = ann`, or `yes` for a ground query. */ solutions: string[]; /** Goals selected. */ steps: number; /** Whether some branch hit the depth cap, so the search was not exhaustive. */ limited: boolean;}/** The most goals a run selects: a safety net beneath the depth cap. */export const MAX_SLD_STEPS = 300;/** * SLD resolution, how Prolog answers a query: take the first goal, * try the program's clauses in order, rename a clause's variables so * two uses never share one, unify its head with the goal, and replace * the goal by the clause's body under the bindings. No goals left is * a solution, read off the query's variables; a goal no clause * unifies with fails, and the search backtracks to the next clause * of the nearest choice. Depth-first in clause order, which is what * makes a left-recursive clause loop; a depth cap turns that loop * into a visible limit. * * Time: exponential in the worst case. Space: O(depth). */export class BackwardChainer { private steps = 0; private nodes = 0; private limited = false; private solutions: string[] = []; constructor( private readonly tracer?: Tracer, private readonly maxDepth = 8, private readonly maxSolutions = 3, ) {} query(program: LogicProgram, goals: readonly Term[]): SldResult { this.steps = 0; this.nodes = 0; this.limited = false; this.solutions = []; const asked = goals.reduce<string[]>((vars, goal) => termVariables(goal, vars), []); this.search(program, [...goals], new Map(), 0, this.nodes++, asked); return { solutions: [...this.solutions], steps: this.steps, limited: this.limited }; } private search(program: LogicProgram, goals: Term[], bindings: ReadonlyMap<string, Term>, depth: number, node: number, asked: readonly string[]): void { if (goals.length === 0) { const answer = asked.length === 0 ? "yes" : asked.map((name) => `${name} = ${termText(applySubstitution(variable(name), bindings))}`).join(", "); this.solutions.push(answer); // ▸ no goals left: the bindings are an answer this.tracer?.emit("solution", { node, answer, count: this.solutions.length }); return; } const [first, ...rest] = goals; const [first, ...remainingGoals] = goals; const selected = applySubstitution(first!, bindings); this.steps += 1; // ▸ the first goal is the one to prove next this.tracer?.emit("select-goal", { node, goal: termText(selected), goals: goals.map((g) => termText(applySubstitution(g, bindings))), depth }); if (depth >= this.maxDepth) { this.limited = true; // ▸ too deep: give up on this branch this.tracer?.emit("depth-limit", { node, goal: termText(selected), depth }); return; } if (this.steps >= MAX_SLD_STEPS) return; for (let index = 0; index < program.clauses.length && this.solutions.length < this.maxSolutions; index++) { const renamed = BackwardChainer.rename(program.clauses[index]!, depth + 1); const freshClause = BackwardChainer.rename(program.clauses[index]!, depth + 1); // ▸ rename the clause's variables and try its head this.tracer?.emit("try-clause", { node, clause: index, head: termText(renamed.head), goal: termText(selected) }); this.tracer?.emit("try-clause", { node, clause: index, head: termText(freshClause.head), goal: termText(selected) }); // Head first, so a head variable binds to the goal's and the goal's own variables survive in the resolvent. const result = new Unifier().unify(renamed.head, selected); const result = new Unifier().unify(freshClause.head, selected); if (!result.unified) { // ▸ the head does not unify: next clause this.tracer?.emit("fail", { node, clause: index, reason: result.failure }); continue; } const merged = new Map([...bindings, ...result.bindings]); const next = [...renamed.body, ...rest]; const next = [...freshClause.body, ...remainingGoals]; const child = this.nodes++; // ▸ the head unifies: the goal becomes the clause body this.tracer?.emit("unify", { node, clause: index, child, bindings: Unifier.text(result.bindings), goals: next.map((g) => termText(applySubstitution(g, merged))) }); this.search(program, next, merged, depth + 1, child, asked); // ▸ that branch is done: try the next clause if (this.solutions.length < this.maxSolutions) this.tracer?.emit("backtrack", { node, clause: index, goal: termText(selected) }); } } /** * The clause with every variable suffixed by the depth it is used at, so two uses of one clause * along a branch never share a variable; siblings may, since each branch keeps its own bindings. */ private static rename(clause: ProgramClause, depth: number): ProgramClause { const suffix = `${depth}`; const fresh = (term: Term): Term => (term.kind === "variable" ? { kind: "variable", name: term.name + suffix } : { kind: "function", name: term.name, args: term.args.map(fresh) }); return { head: fresh(clause.head), body: clause.body.map(fresh) }; }}