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,
modstructure, 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 andfrom-fields (see refined collections),deriverule 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 collection slots filled by navigation over the pairing relations:
pub category Conjunction <: PropositionalContent {
conjunct: [PropositionalContent] 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 (Fulfilledof a conjunction counts overFulfilledof its conjuncts). Argon evaluates a genuine restrictedforall, but stratified-aggregate semantics require the aggregated predicate in a strictly-lower stratum, soox buildrefuses this cycle asOE1317(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 checkverbatim; they are left commented only to keep the pinned demo extents stable. TheConditionalPropositionalContenttype and itsguardOf/consequentOfrelations remain in the hierarchy. - Dates are
Intday-numbers. Ordering and interval comparison — all the calculus needs — are exact; day-numbers keep the example runnable because the demo harness cannot yet seed theDateprimordial. - One book per obligation period. A satisfaction account’s records all count toward its period, so
Metis the cumulative sum over the account. The intra-account Allen-relation window filter (for accounts spanning many periods) needs multi-condition comprehensionwhere, 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.
Source
The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.
root.ar
//! Residential-lease deontic **breach / fulfillment calculus** (UFO-L).
//!
//! When is a lease obligation *breached*? When is it *fulfilled*? This
//! example models the propositional-content calculus a residential lease
//! runs on: cumulative payment tracking, past-due detection, and the
//! logical composition of obligations (and / or / if-then).
//!
//! It is a faithful, self-contained transcription of a working legal model
//! (a residential-lease propositional-content theory in the UFO-L tradition
//! of Griffo/Guizzardi). The full hierarchy and calculus build and admit;
//! a seeded scenario (`demo.toml`) makes the core *run* — see `lease.ar`
//! for the precise modeling choices and the documented residuals.
mod lease;
lease.ar
//! # Residential-lease breach / fulfillment calculus
//!
//! A UFO-L deontic model of a residential lease, centered on the
//! *propositional-content* theory that decides, for each obligation,
//! whether it is **breached** or **fulfilled** as of a given date.
//!
//! ## What the calculus says
//!
//! An obligation is carried by a *propositional content* (`PropositionalContent`).
//! A positive occurrence content (e.g. "pay €1000 rent by the 31st") tracks an
//! **expected-satisfaction account** (what is owed, by period) and a
//! **satisfaction account** (what was actually performed). The content is:
//!
//! * **Met** for an expected record when the cumulative realized value in its
//! period satisfaction account covers the expected value.
//! * **Breached** as of an instant when some past-due expected record is *not*
//! Met (positive content), or — for prohibitions — when a forbidden record
//! *is* Met.
//! * **Fulfilled** as of an instant when it is not Breached.
//!
//! Obligations compose: a **Conjunction** ("A and B") is breached if *any*
//! conjunct is, fulfilled if *all* are; a **Disjunction** ("A or B") flips both;
//! a **Conditional** ("if guard then consequent") *vests* once its guard is
//! fulfilled, after which a breached consequent breaches the conditional.
//!
//! ## Modeling choices (faithful, and noted for honesty)
//!
//! * **Dates are `Int` day-numbers.** Ordering and interval comparison — all
//! the calculus needs — are preserved exactly; the demo harness cannot seed
//! the `Date` primordial, so day-numbers keep the example runnable.
//! * **Evaluation is parameterized by an `Instant`** individual carrying a
//! `day`, rather than a free `date` variable. A derived `BreachedAt(pc, t)`
//! binds `t` over the seeded instants — the faithful "breach *as of* a date"
//! reading, made evaluable.
//! * **Navigation is by relation.** Each `a.b.c` chain in the source theory is
//! expressed as a join over the relations that *are* that navigation
//! (`contentBook`, `bookExpectedAccount`, …) — one hop per atom. Semantically
//! identical; it is also how the relations would be materialized anyway.
//! * **One book per obligation period.** A satisfaction account's records all
//! count toward that 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 (see "Residuals" below).
//!
//! ## Residuals (admit but do not yet *evaluate* on the v0.1 executor)
//!
//! * **Conditional vesting** (`Vested` / conditional `BreachedAt`) closes a
//! negation cycle `BreachedAt → Vested → Fulfilled → ¬BreachedAt`. It is
//! declared and admitted, but requires well-founded / SLG evaluation of
//! recursion-through-negation (RFD 0018) rather than strict stratification.
//! * **Multi-condition / Allen-relation comprehension filters** in `Met`
//! (issue #56). Both are surfaced *loudly* by `ox build` rather than
//! silently approximated.
// ─────────────────────────────────────────────────────────────────────────
// UFO vocabulary (declared in-package)
//
// UFO's classifiers are NOT Argon language surface — they are package
// vocabulary (§3.4, §5.2): a concept introducer resolves against `pub
// metatype` declarations visible in scope, and only `type`/`rel` are
// ambient (from `std::core`). This example declares the three UFO
// metatypes it uses locally — the external-vocabulary-package pattern;
// a real UFO package, authored with the UFO authors, would ship these
// declarations and be imported here instead.
// ─────────────────────────────────────────────────────────────────────────
/// UFO category: a rigid non-sortal classifier.
pub metatype category = { };
/// UFO kind: a rigid sortal supplying an identity principle.
pub metatype kind = { };
/// UFO relator: the truth-maker of material relations.
pub metatype relator = { };
// ─────────────────────────────────────────────────────────────────────────
// UFO foundation (minimal)
//
// The handful of upper-ontology concepts the lease layer specializes.
// ─────────────────────────────────────────────────────────────────────────
pub category Endurant;
pub category Object <: Endurant;
pub category Agent <: Object;
pub category Aspect <: Endurant;
pub category Relator <: Aspect;
// ─────────────────────────────────────────────────────────────────────────
// Lease parties
// ─────────────────────────────────────────────────────────────────────────
/// A legally relevant agent that can hold lease positions.
pub category LegalAgent <: Agent;
/// A natural person; lease participants (landlord, tenant) are persons.
pub kind Person <: LegalAgent {
name: String,
}
// ─────────────────────────────────────────────────────────────────────────
// Cumulative tracking: records, accounts, book
//
// A record carries a value and a closed window `[startsOn, endsOn]` (day
// numbers). Expected records say what is owed in a period; satisfaction records
// say what was performed.
// ─────────────────────────────────────────────────────────────────────────
pub category Record {
mut value: Real,
mut startsOn: Int,
mut endsOn: Int,
}
/// A period-specific expected value — the owed side of cumulative fulfillment.
pub category ExpectedSatisfactionRecord <: Record;
/// A period-specific realized value — appended when a payment is performed.
pub category SatisfactionRecord <: Record;
/// A tracking account holding records, navigable as a collection through the
/// `recordInAccount` relation.
pub category RecordAccount {
records: [Record] from recordInAccount.range,
}
// `account` is immutable: a record belongs to one account for the life of both
// individuals — it is never moved between accounts. `record` is `mut` because an
// account holds MANY records (one-to-many): each `recordPayment` adds a fresh
// record to the same satisfaction account, so this end is genuinely not
// lifetime-fixed per account (an immutable `record` end would refuse the second
// payment with OE1403).
pub rel recordInAccount(account: RecordAccount, mut record: Record);
/// Account for what is owed by period.
pub category ExpectedSatisfactionAccount <: RecordAccount;
/// Account for what has actually been performed.
pub category SatisfactionAccount <: RecordAccount;
/// The book of a correlative position pair: separates expected from realized.
pub category CorrelativePositionBook;
// Both ends immutable: the book/account binding is functional one-to-one,
// established once at `openRentObligation` and never rebound.
pub rel bookExpectedAccount(book: CorrelativePositionBook, account: ExpectedSatisfactionAccount);
pub rel bookSatisfactionAccount(book: CorrelativePositionBook, account: SatisfactionAccount);
// ─────────────────────────────────────────────────────────────────────────
// Correlative legal positions (Hohfeld)
//
// A right–duty pair links an advantaged holder, a burdened holder, a tracking
// book, and the propositional content that supplies its legal meaning.
// ─────────────────────────────────────────────────────────────────────────
pub relator LegalRelator <: Relator;
pub relator CorrelativePositionPair <: LegalRelator {
advantageHolder: LegalAgent,
burdenHolder: LegalAgent,
}
// Both ends immutable: a pair has one book and vice versa, bound once at
// `openRentObligation` and never rebound.
pub rel pairBook(pair: CorrelativePositionPair, book: CorrelativePositionBook);
/// A right–duty pair: for rent, the landlord is advantaged, the tenant burdened.
pub relator RightDutyPair <: CorrelativePositionPair;
// ─────────────────────────────────────────────────────────────────────────
// Propositional content hierarchy
//
// `partition` group axioms transcribe the source theory's `partition` blocks:
// the alternatives are disjoint and exhaustive (OE0242/OE0243-checked). The
// cover-body spelling (`{ A, B }` on the declaration itself) is refused
// (OE0214) until the elaborator threads it into the subkind hierarchy.
// ─────────────────────────────────────────────────────────────────────────
pub category PropositionalContent;
partition PropositionalContent {
OccurrenceReferringPropositionalContent,
ConditionalPropositionalContent,
Conjunction,
Disjunction
}
/// Content that constrains the occurrence of an event or situation. Carries the
/// tracking book whose accounts decide whether it is met.
pub category OccurrenceReferringPropositionalContent <: PropositionalContent;
partition OccurrenceReferringPropositionalContent {
PositiveOccurrencePropositionalContent,
NegativeOccurrencePropositionalContent
}
// Both ends immutable: the content/book binding is functional one-to-one,
// established once at `openRentObligation` and never rebound.
pub rel contentBook(
content: OccurrenceReferringPropositionalContent,
book: CorrelativePositionBook
);
/// Fulfilled by the presence of matching satisfaction (e.g. rent *paid*).
pub category PositiveOccurrencePropositionalContent <: OccurrenceReferringPropositionalContent;
/// Fulfilled by the *absence* of a forbidden occurrence (e.g. *no* subletting).
pub category NegativeOccurrencePropositionalContent <: OccurrenceReferringPropositionalContent;
/// "A and B": every conjunct must hold.
pub category Conjunction <: PropositionalContent {
conjunct: [PropositionalContent] from conjunctOf.range,
}
pub rel conjunctOf(mut conjunction: Conjunction, mut conjunct: PropositionalContent);
/// "A or B": at least one disjunct must hold.
pub category Disjunction <: PropositionalContent {
disjunct: [PropositionalContent] from disjunctOf.range,
}
pub rel disjunctOf(mut disjunction: Disjunction, mut disjunct: PropositionalContent);
/// "If guard then consequent": the consequent is owed once the guard is met.
pub category ConditionalPropositionalContent <: PropositionalContent;
pub rel guardOf(mut conditional: ConditionalPropositionalContent, mut guard: PropositionalContent);
pub rel consequentOf(
mut conditional: ConditionalPropositionalContent,
mut consequent: PropositionalContent
);
// ─────────────────────────────────────────────────────────────────────────
// Evaluation clock
// ─────────────────────────────────────────────────────────────────────────
/// An evaluation instant. Breach / fulfillment are computed *as of* an instant.
pub kind Instant {
mut day: Int,
}
// ─────────────────────────────────────────────────────────────────────────
// The calculus
// ─────────────────────────────────────────────────────────────────────────
/// `e`'s expected window has closed on or before instant `t` (Allen *after* the
/// check date): the obligation is due, so non-satisfaction now counts.
pub derive PastCurrent(e: ExpectedSatisfactionRecord, t: Instant) :-
ExpectedSatisfactionRecord(e),
Instant(t),
e.endsOn <= t.day;
/// `e`'s window has not closed strictly before `t` (not Allen *before* the check
/// date): for prohibitions, a forbidden satisfaction in this window still counts.
pub derive CurrentOrPastCurrent(e: ExpectedSatisfactionRecord, t: Instant) :-
ExpectedSatisfactionRecord(e),
Instant(t),
e.endsOn >= t.day;
/// An expected record is **met** when the cumulative realized value in its
/// period satisfaction account covers the expected value.
pub derive Met(e: ExpectedSatisfactionRecord) :-
recordInAccount(expectedAccount, e),
bookExpectedAccount(book, expectedAccount),
bookSatisfactionAccount(book, satisfactionAccount),
e.value <= sum(r.value for r in satisfactionAccount.records);
/// Positive content is **breached** as of `t` when a past-due expected record is
/// not met.
pub derive BreachedAt(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
contentBook(pc, book),
bookExpectedAccount(book, expectedAccount),
recordInAccount(expectedAccount, e),
PastCurrent(e, t),
not Met(e);
/// Negative (prohibition) content is **breached** as of `t` when a forbidden
/// expected record in a current-or-past window *is* met.
pub derive BreachedAt(pc: NegativeOccurrencePropositionalContent, t: Instant) :-
contentBook(pc, book),
bookExpectedAccount(book, expectedAccount),
recordInAccount(expectedAccount, e),
CurrentOrPastCurrent(e, t),
Met(e);
/// Positive content is **fulfilled** as of `t` when it is not breached.
pub derive Fulfilled(pc: PositiveOccurrencePropositionalContent, t: Instant) :-
PositiveOccurrencePropositionalContent(pc),
Instant(t),
not BreachedAt(pc, t);
/// Negative content is **fulfilled** as of `t` when it is not breached.
pub derive Fulfilled(pc: NegativeOccurrencePropositionalContent, t: Instant) :-
NegativeOccurrencePropositionalContent(pc),
Instant(t),
not BreachedAt(pc, t);
/// A conjunction is breached when *any* conjunct is breached (existential).
pub derive BreachedAt(conj: Conjunction, t: Instant) :- conjunctOf(conj, c), BreachedAt(c, t);
/// A disjunction is fulfilled when *at least one* disjunct is fulfilled (existential).
pub derive Fulfilled(disj: Disjunction, t: Instant) :- disjunctOf(disj, d), Fulfilled(d, t);
// ── Frontier: the universal halves of composition (OE1317 aggregate cycle) ──
//
// The other two composition rules are the universal duals:
//
// pub derive Fulfilled(conj: Conjunction, t: Instant) :-
// Conjunction(conj), Instant(t),
// forall c: PropositionalContent where conjunctOf(conj, c), Fulfilled(c, t);
//
// pub derive BreachedAt(disj: Disjunction, t: Instant) :-
// Disjunction(disj), Instant(t),
// forall d: PropositionalContent where disjunctOf(disj, d), BreachedAt(d, t);
//
// The executor DOES evaluate the restricted universal now: `forall v: T where
// Body, Head` lowers to the count-equality `count { v: Body, Head } ==
// count { v: Body }` (#129, #133), so a genuine ∀ — not an existential
// approximation — is available. What blocks THESE two rules is that they
// recurse *through* that aggregate: `Fulfilled` of a conjunction counts over
// `Fulfilled` of its conjuncts, and a conjunct may itself be a conjunction,
// so `Fulfilled` (dually `BreachedAt`) appears inside its own aggregate body.
// Stratified-aggregate semantics require the aggregated predicate in a
// strictly-lower stratum, so `ox check`/`ox build` refuse the cycle as OE1317
// RecursionThroughAggregation (#175) rather than evaluating something
// ill-founded. The supported rephrasing is NAF double negation — derive a
// counter-example helper (`HasUnfulfilledConjunct(conj, t) :-
// conjunctOf(conj, c), Instant(t), not Fulfilled(c, t);`), then
// `Fulfilled(conj, t) :- Conjunction(conj), Instant(t),
// not HasUnfulfilledConjunct(conj, t);` — recursion through negation,
// evaluated under well-founded semantics (§7.3 "Universals over recursive
// predicates", #185). Adopting it here is deliberate follow-up work (it
// reshapes the example's rule surface); admitting the forall form directly
// (structural stratification) is also tracked in #185. Until then the
// existential halves above (conjunction-breached, disjunction-fulfilled)
// evaluate and the demo exercises those.
// ── Conditional vesting (evaluable under well-founded semantics) ────────────
//
// The conditional's calculus is faithfully:
//
// pub derive Vested(cpc: ConditionalPropositionalContent, t: Instant) :-
// guardOf(cpc, guard), Fulfilled(guard, t);
//
// pub derive BreachedAt(cpc: ConditionalPropositionalContent, t: Instant) :-
// Vested(cpc, t), consequentOf(cpc, consequent), BreachedAt(consequent, t);
//
// pub derive Fulfilled(cpc: ConditionalPropositionalContent, t: Instant) :-
// consequentOf(cpc, consequent), Fulfilled(consequent, t);
//
// These rules close a recursion-through-negation cycle: a conditional's breach
// depends on its guard being *fulfilled*, and fulfillment is defined as *not
// breached* —
//
// BreachedAt(cpc) → Vested(cpc) → Fulfilled(guard) → ¬BreachedAt(guard)
//
// This is inherent to the deontic logic, not an artifact of the encoding. The
// strict-stratified v0.1 evaluator used to refuse such cycles (OE1309); since
// #136 the stratifier instead flags NAF-cyclic SCCs and evaluates them under
// well-founded semantics (the Van Gelder alternating fixpoint), so these rules
// now pass `ox check` verbatim. They remain commented out only to keep this
// example's pinned demo corpus stable — enabling them is uncommenting plus
// re-pinning the expected query results in the demo harness, not reasoner
// work. (Note the cycle runs through negation, not aggregation, so OE1317 —
// recursion *through aggregation*, #175 — does not apply here.) The
// `ConditionalPropositionalContent` type and its `guardOf` / `consequentOf`
// relations remain in the hierarchy above.
// ─────────────────────────────────────────────────────────────────────────
// Seeding (the demo harness drives these — see demo.toml)
// ─────────────────────────────────────────────────────────────────────────
/// Seed the evaluation instant.
pub mutate setClock(t: Instant, day: Int) {
insert iof(t, Instant);
update t: Instant set { day = day }
}
/// Set up a positive occurrence obligation with its book, accounts, and a single
/// expected record (value `owed`, due on `dueDay`). `landlord`/`tenant` populate
/// the right–duty pair that carries it.
pub mutate openRentObligation(
pair: RightDutyPair,
landlord: Person,
tenant: Person,
pc: PositiveOccurrencePropositionalContent,
book: CorrelativePositionBook,
expectedAccount: ExpectedSatisfactionAccount,
satisfactionAccount: SatisfactionAccount,
e: ExpectedSatisfactionRecord,
owed: Real,
dueDay: Int
) {
insert iof(landlord, Person);
insert iof(tenant, Person);
insert iof(pair, RightDutyPair);
insert iof(pc, PositiveOccurrencePropositionalContent);
insert iof(book, CorrelativePositionBook);
insert iof(expectedAccount, ExpectedSatisfactionAccount);
insert iof(satisfactionAccount, SatisfactionAccount);
insert iof(e, ExpectedSatisfactionRecord);
insert pairBook(pair, book);
insert contentBook(pc, book);
insert bookExpectedAccount(book, expectedAccount);
insert bookSatisfactionAccount(book, satisfactionAccount);
insert recordInAccount(expectedAccount, e);
update pair: RightDutyPair set { advantageHolder = landlord, burdenHolder = tenant }
update e: ExpectedSatisfactionRecord set { value = owed, startsOn = 1, endsOn = dueDay }
}
/// Record a rent payment of `amount` into a satisfaction account.
pub mutate recordPayment(
satisfactionAccount: SatisfactionAccount,
payment: SatisfactionRecord,
amount: Real,
paidOn: Int
) {
insert iof(satisfactionAccount, SatisfactionAccount);
insert iof(payment, SatisfactionRecord);
insert recordInAccount(satisfactionAccount, payment);
update payment: SatisfactionRecord set { value = amount, startsOn = paidOn, endsOn = paidOn }
}
/// Compose two contents into a conjunction ("both must hold").
pub mutate makeConjunction(
conj: Conjunction,
left: PropositionalContent,
right: PropositionalContent
) {
insert iof(conj, Conjunction);
insert conjunctOf(conj, left);
insert conjunctOf(conj, right);
}
/// Compose two contents into a disjunction ("either may hold").
pub mutate makeDisjunction(
disj: Disjunction,
left: PropositionalContent,
right: PropositionalContent
) {
insert iof(disj, Disjunction);
insert disjunctOf(disj, left);
insert disjunctOf(disj, right);
}
// ─────────────────────────────────────────────────────────────────────────
// Queries
// ─────────────────────────────────────────────────────────────────────────
/// Expected records whose obligation is cumulatively met.
pub query met() -> Met;
/// `(content, instant)` pairs where the content is breached as of the instant.
pub query breached() -> BreachedAt;
/// `(content, instant)` pairs where the content is fulfilled as of the instant.
pub query fulfilled() -> Fulfilled;