Meta-Interpreters¶
A meta-interpreter is an interpreter written in the same language it interprets. in_ logic programming, this means a Prolog (or Clausal) program that evaluates another logic program represented as data. Meta-interpreters are a classical demonstration of logic programming's homoiconicity: programs and data share the same representation.
This page follows the structure of Markus Triska's A Couple of Meta-Interpreters in Prolog, adapting the examples to Clausal syntax.
Clausal vs Prolog syntax
Clausal and Prolog syntax may slightly differ — for example, variables are
ALLCAPS, rules use <- instead of :-, and lists are Python-style. Keep
this in mind when comparing with Prolog resources.
The full source is in clausal/examples/metainterpreters.clausal.
Object Programs as Data¶
The key idea is to represent an object-level program — the program being interpreted — as a list of clauses, where each clause is a pair [Head, Body]. Head is a term, Body is a list of goals (also terms).
in_ Clausal, object-level terms are ordinary predicate instances. We declare private functor classes for the object level so they are treated purely as data, not called directly:
A program is then a list of such clauses:
This encodes the two-clause natural number predicate:
Similarly, a graph reachability program:
GraphProgram(PROGRAM) <- (
PROGRAM is [
[Edge("a", "b"), []],
[Edge("b", "c"), []],
[Edge("b", "d"), []],
[Path(X, Y), [Edge(X, Y)]],
[Path(X, Y), [Edge(X, Z), Path(Z, Y)]]
]
)
Clause Matching¶
All meta-interpreters share a helper that finds a clause in the program whose head unifies with a given goal, returning a fresh copy of the body (to avoid variable clashes between different resolution steps):
MatchClause(GOAL, FRESH_BODY, PROGRAM) <- (
CLAUSE in PROGRAM,
copy_term(CLAUSE, [FRESH_HEAD, FRESH_BODY]),
GOAL is FRESH_HEAD,
)
copy_term renames all variables in the clause, so the same clause can be used multiple times without its variables interfering with each other. Unifying GOAL is FRESH_HEAD then binds the fresh variables to match the current goal.
1. Vanilla Meta-Interpreter¶
The simplest meta-interpreter processes a list of goals, replacing each goal with the body of a matching clause, and recursing until the list is empty.
Solve([], _PROGRAM),
Solve([GOAL, *GOALS], PROGRAM) <- (
MatchClause(GOAL, BODY, PROGRAM),
append(BODY, GOALS, ALL_GOALS),
Solve(ALL_GOALS, PROGRAM),
)
The base case: an empty goal list means all goals are proved. The recursive case: take the first goal, find a matching clause, prepend its body to the remaining goals, and continue. This is the list-based form (mi_list2 in Triska's article), which is tail-recursive and avoids the overhead of a conjunction stack.
Querying it:
from clausal.examples.metainterpreters import NatnumProgram, GraphProgram
from clausal.examples.metainterpreters import Solve, Natnum, succ, Path, Edge
# Does natnum(s(s(0))) hold?
p = next(NatnumProgram.query())
result = list(Solve.query(goals=[Natnum(succ(succ(0)))], program=p))
# → one solution (the proof succeeds)
# Is there a path from a to c?
g = next(GraphProgram.query())
result = list(Solve.query(goals=[Path("a", "c")], program=g))
# → one solution
2. Inference-Counting Meta-Interpreter¶
By adding a counter argument, we can count the number of resolution steps (clause applications) the interpreter performs:
SolveCount([], _PROGRAM, 0),
SolveCount([GOAL, *GOALS], PROGRAM, COUNT) <- (
MatchClause(GOAL, BODY, PROGRAM),
append(BODY, GOALS, ALL_GOALS),
SolveCount(ALL_GOALS, PROGRAM, SUB_COUNT),
COUNT == SUB_COUNT + 1,
)
Each recursive call adds one to the count after the sub-proof completes. The count accumulates bottom-up as the recursion unwinds.
Examples:
| Query | Steps |
|---|---|
Natnum(0) |
1 — one fact applied |
Natnum(succ(0)) |
2 — recursive clause + base fact |
Natnum(succ(succ(0))) |
3 — two recursive steps + base |
Edge("a","b") |
1 — one fact |
Path("a","b") |
2 — one path clause + one edge fact |
Path("a","c") |
4 — path + edge + path + edge |
3. Depth-Limited Meta-Interpreter¶
The vanilla interpreter will loop forever on programs that have cycles or infinite derivations. Adding a depth limit causes it to fail rather than diverge:
SolveLimit([], _PROGRAM, _MAX),
SolveLimit([GOAL, *GOALS], PROGRAM, MAX) <- (
MAX > 0,
MAX1 == MAX - 1,
MatchClause(GOAL, BODY, PROGRAM),
append(BODY, GOALS, ALL_GOALS),
SolveLimit(ALL_GOALS, PROGRAM, MAX1),
)
Each resolution step decrements the depth counter. when MAX reaches zero, the guard MAX > 0 fails, cutting off that branch.
Examples:
SolveLimit([Natnum(succ(0))], P, 1) → fails (needs 2 steps)
SolveLimit([Natnum(succ(0))], P, 2) → succeeds
SolveLimit([Path("a","c")], P, 3) → fails (needs 4 steps)
SolveLimit([Path("a","c")], P, 4) → succeeds
4. Iterative Deepening¶
Iterative deepening combines the completeness of breadth-first search with the space efficiency of depth-first search. It repeatedly tries increasing depth limits until a proof is found:
SolveIterativeDeepening(GOALS, PROGRAM) <- (
between(0, 1000, DEPTH),
SolveLimit(GOALS, PROGRAM, DEPTH),
)
between generates 0, 1, 2, … in order. For each candidate depth, SolveLimit either finds a proof or fails. On failure, backtracking increments the depth and tries again. The first depth at which a proof exists is found, and the proof is returned.
The key advantage is completeness on programs where naive DFS would loop. Consider a cyclic graph where the only successful path clause is listed after the recursive one:
CyclicProgram(PROGRAM) <- (
PROGRAM is [
[Edge("a", "b"), []],
[Edge("b", "a"), []],
[Path(X, Y), [Edge(X, Z), Path(Z, Y)]], # recursive — tried first
[Path(X, Y), [Edge(X, Y)]] # base — tried second
]
)
Solve([Path("a","b")], CyclicProgram) loops forever — the recursive clause is always tried first, generating a→b→a→b→…. But SolveIterativeDeepening([Path("a","b")], CyclicProgram) succeeds at depth 2, because at depth 1 both branches are exhausted, and at depth 2 a→b is found via the base clause.
5. Proof Tree Meta-Interpreter¶
The proof tree interpreter extends the vanilla interpreter to build a trace of the proof — a tree recording which clause was used to resolve each goal, and how its body was proved:
SolveTree([], _PROGRAM, []),
SolveTree([GOAL, *GOALS], PROGRAM, [[GOAL, BODY_TREE], *GOALS_TREE]) <- (
MatchClause(GOAL, BODY, PROGRAM),
SolveTree(BODY, PROGRAM, BODY_TREE),
SolveTree(GOALS, PROGRAM, GOALS_TREE),
)
Each node in the tree is [Goal, SubTree] where SubTree is the proof tree for the body goals that were used to resolve Goal. Facts (clauses with empty body) produce leaf nodes [Goal, []].
Example: Path("a","c")
in_ Clausal list notation:
Test("tree path(a,c) transitive") <- (
GraphProgram(P),
TreeSolve(P, path("a", "c")),
TREE is solve_tree(P, path("a", "c")),
nonvar(TREE)
)
Example: Natnum(s(s(0)))
Key Design Points¶
Object programs as actual terms — unlike some presentations that use assert/clause to store the object program in the Prolog database, these interpreters pass the program as an explicit list. This makes the interpretation transparent: the program being interpreted is visible data that can be inspected, transformed, or generated.
copy_term for fresh variables — without freshening, reusing a clause that contains X twice would unify all occurrences of X across different resolution steps. copy_term renames all variables in a clause before unification, exactly as a real Prolog interpreter would.
Composability — each interpreter is a small, self-contained predicate. They can be combined: for example, SolveCount could be extended with a depth limit (producing a counted, depth-bounded interpreter) by merging the two patterns. These interpreters can also be specialized via partial deduction to eliminate interpretation overhead.
Source and tests
Full source: clausal/examples/metainterpreters.clausal
The file contains 30 Test clauses covering all five interpreters across the natural number and graph programs, including the iterative deepening completeness test on the cyclic graph.
See also: Tabling — built-in memoisation for left-recursive predicates. See also: Meta-Predicates — findall, bagof, setof, forall. See also: Term Inspection — copy_term, term_variables, numbervars.