Markdown for LLMs

LDC-E4101 — A rule head with an unbound variable

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# 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

```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

```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:

```text
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](/constructs/rule-strict/) — how a strict rule reads its body.
- [Defeasible rules](/constructs/rule-defeasible-unless/) — how a rule yields to an exception.