Lease obligations: lex specialis as stratified negation

Area: Defeasible reasoning Teaches: expressing lex specialis (a specific exemption overriding a general breach norm) with stratified negation rather than the #[defeats] directive plane — the form you reach for when a module also imports a check-bearing vocabulary. Plus a real breach calculus over an imported deontic vocabulary. Prerequisites: lex specialis via #[defeats], defeat plane + check, and cross-package vocabulary (use legal_vocab_v0::…). Run: ox build examples/legal_obligations_v0 && ox run-scenario examples/legal_obligations_v0

This is the flagship legal-obligations model: a lease creates a rent obligation running from a tenant (debtor) to a landlord (creditor), declared against the separate legal_vocab_v0 deontic vocabulary. An obligation past its due date and unperformed is in breach — unless a force-majeure exemption applies. That “unless” is lex specialis again, but written a different way than the previous two examples, and the why is the lesson.

What to read in lease.ar

Lex specialis as stratified negation. The general breach norm fires unless the specific exemption holds; the exemption lives in a strictly-lower stratum, so not exempt(o) is well-defined:

pub derive outstanding(o) :- o: RentObligation, o.performed == false, o.due < today();
pub derive exempt(o)      :- o: ExemptObligation, outstanding(o);
pub derive breach(o)      :- outstanding(o), not exempt(o);

The resolution is identical to the #[defeats] lex-specialis in legal_priority_v0 — the specific rule wins for exactly the exempt obligations — but expressed with negation instead of a defeat directive.

Why not #[defeats] here? This package imports the check-bearing legal_vocab_v0, and ox build refuses any module that has both a check and a #[defeats]/#[default] plane in scope (check-discharge runs the strict path only). So when a defeat plane and an imported check can’t coexist in one build, stratified negation gives the same lex-specialis resolution and composes with the vocabulary’s catalog checks. (The composing case — defeat plane and check in one module, post-fix — is legal_obligations_compose_v0.)

A second, additive breach path for a long-stale obligation, still subtracting the exemption:

pub derive breach(o) :-
    o: RentObligation, o.performed == false, not exempt(o),
    o.due + 365.days < today();

The force-majeure exemption protects the obligor on this path too — it is not unconditionally overridden by staleness.

A derived penalty value bound in the rule head, rate × days-late, staying in the exact numeric tower:

pub derive penaltyOwed(o, amount) :- breach(o), amount = o.rate * o.daysLate;

Running it

The scenario opens four obligations against an evaluation clock of “today”:

ob1  due 2020-01-01, unperformed, NOT exempt   → breach (long-overdue path keeps it in at every clock)
ob2  due 2026-05-01, unperformed, EXEMPT        → not in breach (lex specialis subtracts it)
ob3  due 2026-05-01, unperformed, NOT exempt    → breach (outstanding, not exempt)
ob4  due 2026-05-01, PERFORMED                   → not in breach (discharged)

The queries report:

query lease::outstanding_obligations: 3 row(s)   — { ob1, ob2, ob3 }   (ob4 performed)
query lease::exempt_obligations:      1 row(s)   — { ob2 }
query lease::breached_obligations:    2 row(s)   — { ob1, ob3 }        (ob2 exempt; ob4 performed)
query lease::penalties:               2 row(s)   — (ob1, 1500) and (ob3, 250)

ob2 is outstanding but exempt, so the exemption subtracts it from breach on both paths — the lex-specialis point. The penalties are rate × daysLate: ob1 is 50.00 × 30 = 1500, ob3 is 25.00 × 10 = 250, both exact Decimal × Int.

Honest caveats (what runs today)

• #[defeats] and check are mutually exclusive in one build (the wall this model documents). The canonical RFD 0028 spelling of lex specialis is the #[defeats] directive plane, proven standalone in legal_priority_v0; it cannot be used here because this package imports a check-bearing vocabulary. Stratified negation is the composing form.
• Days-late is recorded, not computed from the dates. A penalty cannot be derived from elapsed time inside a rule: there is no Duration → Int day-count extractor, and today()/now() as a rule-body operand is refused with OE1316. So daysLate is stamped as an Int at breach time (recordBreach) rather than computed from today() - due.

This example is compiled and run in CI; the breach calculus over the cross-package vocabulary — the {ob1, ob3} breach extent and the 1500/250 penalties — is pinned by a CLI-pipeline test (oxc-driver/tests/cli_pipeline.rs), so the lex-specialis-via-negation behavior can’t drift.