LDC-E4103 — A strict rule reading a defeasible conclusion

What it means

A strict rule runs to completion in its stratum, before any defeasible conclusion it reads has settled: defeasible reasoning may still defeat what the strict rule already consumed. A status-sensitive read — a bare atom, a negation, or an enumeration over a predicate a defeasible rule produces — therefore uses a value before both of its polarities are known. The compiler refuses the strict rule and points at the late producer.

The fix moves the read to a rule that runs after the producer settles, or reads through a monotone form that does not wait on the outcome. A strict rule over predicates no defeasible rule touches stays silent.

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 Produce defeasible { for x: Text; when q(x); then r(x); }
rule Consume strict { for x: Text; when r(x); then p(x); }

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 Produce defeasible { for x: Text; when q(x); then r(x); }
rule Consume defeasible { for x: Text; when r(x); then p(x); }

Engine message

The engine reports this in its own wording:

Output

example.law:9:6: error LDC-E4103: LATE_STATUS_PRODUCER: strict rule "Consume" reads bare "r", produced by a defeasible rule — the status is used before producers of both polarities complete (§111); in 0.1 status-sensitive consumption of defeasible conclusions from strict is unavailable (monotone supported(P) — L3)

Related

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