Variable safety and range restriction checks for ExDatalog programs.

A Datalog rule is safe when every variable in the rule head and in constraint inputs is bound by a positive body atom. Unsafe rules produce infinite or undefined results and must be rejected.

Checks performed

1. Unsafe head variable — a variable appears in the rule head but not in any positive body atom or arithmetic constraint result. Head variables may reference any arithmetic result regardless of constraint order, because all arithmetic constraints fire before head projection.

2. Unbound constraint variable — a variable in a comparison constraint or in the input operands of an arithmetic constraint is not bound by any positive body atom or earlier arithmetic result. Constraints are validated in listed order; a result variable introduced by constraint k is only available to constraints k+1 and later.

3. Wildcard in rule head — wildcards (:wildcard) may not appear in rule heads because they do not bind a value.

Wildcards in body atoms are allowed — they match any value without binding.

Head vs. constraint asymmetry

A variable introduced by an arithmetic constraint is always available to the rule head, regardless of where the constraint appears in the list. But the same variable is only available to later constraints. This means:

# Safe: Z is bound by the constraint, head may reference it
total(X, Z) :- value(X, A), Z = A + 1

# Safe: head references Z even though Z comes from a later constraint
combined(X, Z, W) :- value(X, A), W = Z + 1, Z = A + 2

# Unsafe: W references Z at constraint position before Z is computed
bad(X, W) :- value(X, A), W = Z + 1, Z = A + 2   # ERROR: Z unbound

Examples

# Safe: X and Y are bound by positive body atoms
ancestor(X, Y) :- parent(X, Y)

# Unsafe: Z is not bound in any positive body atom
ancestor(X, Z) :- parent(X, Y)          # ERROR: Z is unsafe

# Safe: arithmetic result variable Z is bound by the constraint
total(X, Z) :- value(X, A), value(Y, A), Z = X + Y