Recursive Rules

A recursive rule is a rule whose head predicate also appears in its body. Recursive rules let a small ruleset describe patterns of unbounded depth: “an ancestor is a parent, or the parent of an ancestor”; “a node is reachable if there is any edge-connected path to it”; “the factorial of N is N times the factorial of N−1”. They are what makes a rule-based engine genuinely expressive rather than just a pattern matcher.

The Reasoning Layer supports recursive rules natively in both backward chaining (goal-directed queries) and forward chaining (data-driven materialization). No special syntax — just add a rule whose head sort is also mentioned in the antecedents.

The shape of a recursive rule

Most recursive definitions need two rules: a base case that grounds the recursion in known facts, and a recursive step that reduces the problem to a smaller version of itself.

The canonical example is ancestry:

ancestor(X, Y) :- parent(X, Y).                   -- base case
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).   -- recursive step

Read aloud: “X is an ancestor of Y if X is a parent of Y. Or, X is an ancestor of Y if X is a parent of some Z who is in turn an ancestor of Y.”

In the Reasoning Layer, both clauses are regular rules:

import { psi, ReasoningLayerClient } from '@kortexya/reasoninglayer';

const client = new ReasoningLayerClient({
  baseUrl: 'https://platform.ovh.reasoninglayer.ai',
  tenantId: 'your-tenant-uuid',
  auth: { mode: 'cookie' },
});

// Base case: a parent is an ancestor
await client.inference.addRule({
  term: psi('ancestor', { person: '?X', descendant: '?Y' }),
  antecedents: [
    psi('parent', { person: '?X', child: '?Y' }),
  ],
});

// Recursive step: parent of an ancestor is an ancestor
await client.inference.addRule({
  term: psi('ancestor', { person: '?X', descendant: '?Y' }),
  antecedents: [
    psi('parent',   { person: '?X', child: '?Z' }),
    psi('ancestor', { person: '?Z', descendant: '?Y' }),  // head reused in body
  ],
});

The second rule is recursive because ancestor appears in both head and body. With the facts parent(Alice, Bob) and parent(Bob, Charlie), the engine will correctly derive ancestor(Alice, Bob), ancestor(Bob, Charlie), and ancestor(Alice, Charlie).

Backward chaining over recursive rules

When you pose a goal, backward chaining expands rules whose head unifies with the goal, then recursively tries to prove each antecedent. For a recursive rule this would, naively, loop forever. The engine avoids this with two mechanisms running together:

Tabling (memoization). Every proven sub-goal is cached as a Ψ-term. If the same sub-goal is encountered again along a different proof path, the cached answer is reused instead of re-expanding the rule. This turns an exponential search tree into polynomial-time evaluation and — crucially — guarantees termination on well-founded recursive rules.
Cycle detection. The engine tracks which goals are currently being proved further up the call stack. If a goal is encountered that is already in flight along the same branch, it is failed rather than expanded, which prevents infinite descent on ill-founded recursion.
Depth bound. As a final safety net, maxDepth (default 100) caps the recursion depth. Any proof branch exceeding it is cut off.

Tabling is enabled by default. It is what allows the engine to handle left-recursive rules — notoriously pathological in naive Prolog — such as reach(X, Y) :- reach(X, Z), edge(Z, Y).

A recursive query looks no different from any other:

const result = await client.inference.backwardChain({
  goal: psi('ancestor', {
    person: '?Ancestor',
    descendant: 'Charlie',
  }),
  maxSolutions: 100,
  maxDepth: 50,
});

for (const solution of result.solutions) {
  for (const b of solution.substitution.bindings) {
    console.log(`${b.variableName} = ${b.boundToDisplay}`);
  }
}

The proof tree returned on each solution is itself a recursive structure — each subproof can have its own subproofs — which mirrors the shape of the derivation that produced the answer.

Forward chaining over recursive rules

Forward chaining computes the least fixpoint of the ruleset: it repeatedly applies all rules to the working memory, adding newly derived facts, until no rule can produce anything new. Recursive rules are the natural fit for this model — they are exactly the rules that can keep firing as new consequences become available.

Given the two ancestor rules and two parent facts, forward chaining materialises the entire ancestor relation in a bounded number of iterations:

const result = await client.inference.forwardChain({
  maxIterations: 100,
  maxFacts: 10_000,
  persistDerived: true,
});

console.log(`Derived ${result.derivedCount} new facts in ${result.iterations} iterations`);

The engine uses semi-naive evaluation: each iteration only re-matches rules against the facts that were newly derived in the previous iteration, not the entire working memory. This makes fixpoint computation cheap even for large, densely-connected knowledge bases.

Fixpoint is guaranteed to terminate whenever the recursion is well-founded — i.e. whenever the recursive rule cannot produce an unbounded number of fresh terms. Transitive-closure-style rules over a finite fact base always terminate. Rules that invent new values (e.g. successor(N+1) over integers) do not, and must be bounded by maxIterations and maxFacts.

Common recursive patterns

Transitive closure

Any “X relates to Y if there is a chain of relations from X to Y” relationship follows the ancestor pattern: base case over the direct relation, recursive step composing one direct step with the transitive relation.

// reachable(X, Y) :- edge(X, Y).
// reachable(X, Y) :- edge(X, Z), reachable(Z, Y).
await client.inference.bulkAddRules({
  rules: [
    {
      term: psi('reachable', { from: '?X', to: '?Y' }),
      antecedents: [psi('edge', { from: '?X', to: '?Y' })],
    },
    {
      term: psi('reachable', { from: '?X', to: '?Y' }),
      antecedents: [
        psi('edge',      { from: '?X', to: '?Z' }),
        psi('reachable', { from: '?Z', to: '?Y' }),
      ],
    },
  ],
});

Path with accumulated cost

Accumulate a value along the recursion by threading it through a feature:

// path(X, Y, D) :- edge(X, Y, D).
// path(X, Y, D) :- edge(X, Z, D1), path(Z, Y, D2), D = D1 + D2.

Arithmetic constraints (D = D1 + D2) can be attached via constrained variables — see Constrained Variables.

Arithmetic recursion

Recursion is not limited to graph-style rules. Numeric definitions compose the same way:

factorial(0, 1).
factorial(N, F) :- N > 0, factorial(N - 1, F1), F = N * F1.

Tabling memoises intermediate answers, so factorial(10) computes each smaller factorial(k) at most once.

Termination and safety

Recursive rules are powerful, which means they also give you the ability to ask questions with no finite answer (“list every path in an infinite graph”). The engine exposes three independent controls — use them as expected bounds on well-formed queries, not as escape hatches:

Setting	Default	What it bounds
`maxDepth` (backward chaining)	`100`	Depth of the proof tree
`maxIterations` (forward chaining)	`1000`	Fixpoint iterations
`maxFacts` (forward chaining)	`500_000`	Total facts in working memory

You can also set timeoutMs on a backward-chaining request; if the wall clock fires, the engine returns whatever solutions it has already found. Tabling makes partial results meaningful — the proven sub-goals accumulated so far are all correct, just not necessarily complete.

When recursion doesn’t terminate

Well-founded recursion has a decreasing measure: every recursive call reduces some quantity (shorter remaining path, smaller number, smaller subset). If no such measure exists, the engine will run until it hits one of the bounds above.

Common causes:

Missing base case. ancestor with only the recursive rule never grounds out. Always check that the non-recursive clauses can fire on your facts.
Symmetric rules without guards. sibling(X, Y) :- sibling(Y, X) loops forever. Either add an asymmetry (X < Y) or derive siblings from a shared parent instead.
Value-generating recursion. Rules that synthesise fresh terms (succ(N) → succ(succ(N))) have no finite fixpoint and must be bounded externally.