Residential lease: a breach / fulfillment calculus

Area: Capstone Teaches: the worked, end-to-end legal model — a UFO-L deontic theory of a residential lease where concepts, first-class relations, refined collections, mod structure, cumulative aggregation, and recursion-through-negation rules combine to decide, per obligation, whether it is breached or fulfilled as of a date. The capstone of the corpus. Prerequisites: first-class relations, refined collections and from-fields (see refined collections), derive rule bodies with aggregates and negation, and the in-package vocabulary pattern (pub metatype, see legal vocabulary). Run: ox build examples/residential_lease_breach && ox run-scenario examples/residential_lease_breach

This is the example the rest of the corpus builds toward. The others isolate one idea — a relation carries data, a #[defeats] plane resolves a conflict, a check reads a warranted extent. Here those ideas carry a single working legal model: a residential lease, transcribed faithfully from a propositional-content theory in the UFO-L tradition of Griffo/Guizzardi. The question the model answers is the one a lease actually poses — given what was owed, what was paid, and what day it is, which obligations are in breach? — and it answers it by running, not by hand-waving.

The package is two modules: root.ar (mod lease;) and lease.ar, which holds the whole hierarchy, the calculus, the seeding mutations, and the queries.

The UFO vocabulary is declared in-package, not built in

UFO’s classifiers are not Argon language surface. Even the std::core baseline type/rel is opt-in — this package’s ox.toml lists them in its prelude (RFD 0038 D4; the baseline is no longer ambient). A category/kind/relator introducer then resolves against pub metatype declarations visible in scope — an introducer with no visible declaration is refused (OE0605). The example declares the three UFO metatypes it uses locally — the external-vocabulary-package pattern, where a real UFO package authored with the UFO authors would ship these and be imported instead:

pub metatype category = { };   // a rigid non-sortal classifier
pub metatype kind     = { };   // a rigid sortal supplying an identity principle
pub metatype relator  = { };   // the truth-maker of material relations

Everything downstream is vocabulary, not keyword: pub category Endurant;, pub kind Person <: LegalAgent { name: String }, pub relator CorrelativePositionPair <: LegalRelator { … }. The compiler never reads the word “category” as special — it reads a metatype declared one screen up.

What to read in lease.ar

Cumulative tracking is built from records, accounts, and a book. A Record carries a value and a closed day-window [startsOn, endsOn]. An expected record says what is owed in a period; a satisfaction record says what was performed. An account holds records as a refined collection navigated through a relation — the from recordInAccount.range field is the collection of records reachable across that relation:

pub category Record { mut value: Real, mut startsOn: Int, mut endsOn: Int }
pub category RecordAccount { records: [Record] from recordInAccount.range }
pub rel recordInAccount(account: RecordAccount, record: Record);

A CorrelativePositionBook separates the two sides through bookExpectedAccount and bookSatisfactionAccount, so the calculus can compare what is owed against what was realized.

Legal positions are Hohfeldian relators. A right–duty pair is the truth-maker that links an advantaged holder, a burdened holder, the tracking book, and the propositional content that supplies its legal meaning. For rent the landlord is advantaged, the tenant burdened:

pub relator CorrelativePositionPair <: LegalRelator {
    advantageHolder: LegalAgent,
    burdenHolder: LegalAgent,
}
pub relator RightDutyPair <: CorrelativePositionPair;

The propositional content hierarchy is a named cover. The = A | B | … transcribes the source theory’s partition blocks — the alternatives are disjoint and exhaustive. A content is either an occurrence-referring content (positive or negative), a conditional, a conjunction, or a disjunction:

pub category PropositionalContent =
    OccurrenceReferringPropositionalContent |
    ConditionalPropositionalContent |
    Conjunction |
    Disjunction

Positive content is fulfilled by matching satisfaction (rent paid); negative content by the absence of a forbidden occurrence (no subletting). Conjuncts and disjuncts are refined collections too, with cardinality on the slot — a conjunction needs at least two conjuncts, a disjunction at most two disjuncts:

pub category Conjunction <: PropositionalContent {
    conjunct: [PropositionalContent; >= 2] from conjunctOf.range
}

The calculus is the set of derive rules. An expected record is Met when the cumulative realized value in its satisfaction account covers the expected value — a sum aggregate over the navigated collection:

pub derive Met(e: ExpectedSatisfactionRecord) :-
    recordInAccount(expectedAccount, e),
    bookExpectedAccount(book, expectedAccount),
    bookSatisfactionAccount(book, satisfactionAccount),
    e.value <= sum(r.value for r in satisfactionAccount.records);

Breach is as of an instant. PastCurrent(e, t) holds when e’s window has closed on or before t (the obligation is due, so non-satisfaction now counts). Positive content is breached as of t when a past-due expected record is not Met — negation over the aggregate-defined Met:

pub derive BreachedAt(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    contentBook(pc, book),
    bookExpectedAccount(book, expectedAccount),
    recordInAccount(expectedAccount, e),
    PastCurrent(e, t),
    not Met(e);

Fulfillment is the negation of breach, and composition is per the deontic logic. Positive content is fulfilled as of t when it is not BreachedAt; a conjunction is breached when any conjunct is breached (existential), and a disjunction is fulfilled when at least one disjunct is fulfilled:

pub derive Fulfilled(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
    PositiveOccurrencePropositionalContent(pc), Instant(t), not BreachedAt(pc, t);

pub derive BreachedAt(conj: Conjunction, t: Instant) :- conjunctOf(conj, c), BreachedAt(c, t);
pub derive Fulfilled(disj: Disjunction, t: Instant) :- disjunctOf(disj, d), Fulfilled(d, t);

Each a.b.c navigation in the source theory becomes one join per hop over the relation that is that navigation (contentBook, bookExpectedAccount, …) — semantically identical, and how the relations materialize anyway.

Running it

The harness sets the clock to day 45 and opens three rent obligations, each €1000 due on day 31 (so all are past-due as of day 45). They differ only in what was paid, plus two composites over { rentPaid, rentUnpaid }:

rentUnpaid   paid 0           → not met → BREACHED   as of day 45
rentPaid     paid 600 + 400   → met     → FULFILLED  as of day 45
rentPartial  paid 600         → not met → BREACHED   as of day 45
bothRents    (rentPaid AND rentUnpaid)  → BREACHED   (one conjunct breached)
eitherRent   (rentPaid OR  rentUnpaid)  → FULFILLED  (one disjunct fulfilled)

ox run-scenario applies the nine mutations and reports the three query extents (individual ids elided; the subjects are named here for reading):

scenario: applied 9 mutation(s) from examples/residential_lease_breach/demo.toml
query lease::breached: 3 row(s)   — { rentUnpaid, rentPartial, bothRents } each as of `today`
query lease::fulfilled: 2 row(s)  — { rentPaid, eitherRent } each as of `today`
query lease::met: 1 row(s)        — { expPaid }  (the only fully-covered expected record)

The decisive reads: rentPartial is breached even though €600 was paid, because cumulative satisfaction (600) does not cover the expected 1000 — the sum-defined Met fails and not Met fires. rentPaid is met because 600 + 400 = 1000 covers it, so BreachedAt finds no unmet past-due record and Fulfilled (its negation) holds. And composition runs through: bothRents is breached because one conjunct (rentUnpaid) is, while eitherRent is fulfilled because one disjunct (rentPaid) is.

Honest caveats (what runs today)

The model declares more of the calculus than the v0.1 executor evaluates, and the source surfaces each residual loudly rather than approximating it silently:

• The universal halves of composition are commented out. “A conjunction is fulfilled when all conjuncts are” and its disjunction dual recurse through a forall/aggregate over the very predicate they define (Fulfilled of a conjunction counts over Fulfilled of its conjuncts). Argon evaluates a genuine restricted forall, but stratified-aggregate semantics require the aggregated predicate in a strictly-lower stratum, so ox build refuses this cycle as OE1317 (recursion through aggregation) rather than evaluating something ill-founded. The supported rephrasing is NAF double-negation (a counter-example helper, then negate it), evaluated under well-founded semantics; adopting it reshapes the rule surface and is deliberate follow-up. The existential halves — conjunction-breached, disjunction-fulfilled — are what evaluate, and the demo exercises exactly those.
• Conditional vesting is declared and admitted but not exercised by the pinned demo. A conditional’s breach depends on its guard being fulfilled, and fulfillment is not breached — a genuine recursion-through-negation cycle, inherent to the deontic logic. The stratifier now flags such SCCs and evaluates them under well-founded semantics (the Van Gelder alternating fixpoint), so the rules pass ox check verbatim; they are left commented only to keep the pinned demo extents stable. The ConditionalPropositionalContent type and its guardOf / consequentOf relations remain in the hierarchy.
• Dates are Int day-numbers. Ordering and interval comparison — all the calculus needs — are exact; day-numbers keep the example runnable because the demo harness cannot yet seed the Date primordial.
• One book per obligation period. A satisfaction account’s records all count toward its period, so Met is the cumulative sum over the account. The intra-account Allen-relation window filter (for accounts spanning many periods) needs multi-condition comprehension where, a documented residual.

This example is compiled and run in CI; its Met / BreachedAt / Fulfilled extents under cumulative aggregation, negation, and existential composition are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs) to exactly {expPaid} / {rentUnpaid, rentPartial, bothRents} / {rentPaid, eitherRent}. If the language changes underneath it, the build breaks rather than the docs going stale.