LDC-E4101 — A rule head with an unbound variable

What it means

A rule may conclude only about values its body actually produces: every variable in the head must be bound by a positive body conjunct over a finite source. A head variable with no such binder ranges over everything at once, and the rule would conclude infinitely much from finite premises. The compiler refuses the rule at the rule itself and names the unbound variables.

The fix binds each head variable in the body — through a relation atom, an enumeration member, or another finite positive source. Negated and status-tested conjuncts never bind, so adding one around the same variable changes nothing.

Example

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

relation p(x: Text) kind institutional;
relation q(x: Text) kind institutional;
relation r(x: Text) kind institutional;
rule R defeasible { for x: Text; for y: Text; when q(x); then p(y); }

Fix

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

relation p(x: Text) kind institutional;
relation q(x: Text) kind institutional;
relation r(x: Text) kind institutional;
rule R defeasible { for x: Text; for y: Text; when q(x) and r(y); then p(y); }

Engine message

The engine reports this in its own wording:

Output

example.law:8:6: error LDC-E4101: R: head uses unbound variables [y] — the rule is not range-restricted (§190: binding only by a positive established conjunct of a finite source)

Related

• Strict rules — how a strict rule reads its body.
• Defeasible rules — how a rule yields to an exception.