Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0056 — Bitemporal rules: rule validity over time

Naming. The substrate concept is domain-neutral: a rule is a bitemporal fact, and its valid-time is the interval over which it is in effect — exactly as a fact has a valid-time. The language surface and engine use neutral names only (at #DATE# on a rule head; rule_vt; query_derive_at; “the rules in effect at a point”). The legal-informatics vocabulary in the motivation and citations below — enactment-time, abrogation, annulment, “the law as it stood” — names the motivating domain (audit / defensibility / statutory reasoning) and the prior art (Governatori, LegalRuleML), not any Argon construct. The feature works identically for contract terms, pricing schedules, policy versions, or configuration regimes; none of those are “law.”

  • State: accepted
  • Depends on: RFD 0053 (the standalone concurrent engine — Phase 5 as-of-past derived reads is the first consumer), RFD 0047 (the temporal value library / bitemporal substrate this extends to the rule plane), RFD 0028 (defeasibility — rule strengths, proof tags, the superiority/defeat graph this must compose with), RFD 0017 (refinement where/iff — definitional scope, the adjacent scoped-redefinition arc), RFD 0020 (runtime engine / Engine::evaluate), RFD 0018 (DBSP reasoner)
  • Tracks: issue #1019
  • Prior art: Governatori & Rotolo, “Changing Legal Systems: Abrogation and Annulment. Part II: Temporalised Defeasible Logic” (DEON 2008) — the canonical four-temporal-slot proof-tag and the abrogation/annulment dichotomy; Governatori, Palmirani, Riveret, Rotolo & Sartor, “Back to the Future: Variants of Temporal Defeasible Logic for Modelling Norm Modifications” (ICAIL 2007) — the second (repository/viewpoint) temporal axis; Governatori, “Logics for Legal Dynamics” (in Araszkiewicz & Płeszka eds., 2015) — the two-dimension reduction (in-force vs. viewpoint); Cristani, Olivieri & Rotolo (ICAIL 2017) — the six-cell norm-change operator family; LegalRuleML (Athan, Governatori, Palmirani, Paschke & Wyner, OASIS 2013) — efficacy / enforcement / validity / assertion temporal dimensions; Akoma Ntoso / LegalDocML — point-in-time consolidation of legislation; bitemporal databases (Snodgrass–Ahn 1985; Jensen–Snodgrass 1999; SQL:2011 system-versioned tables); Lawsky, “A Logic for Statutes” (2017) — defeasible, scoped statutory reasoning

Question

RFD 0053 Phase 5 reconstructs derived facts at a past transaction time tt by checkpoint-and-replay (Q1). That reconstruction is only correct if it replays the rules in force at that tt — the law as it then stood. Replay current rules over past facts and the system answers a counterfactual no auditor asked for: today’s law applied retroactively.

The data plane is already bitemporal: a fact carries a valid-time interval (when it holds in the world) and a transaction-time interval (when the system recorded it), and a read pins a (vt, tt) point (AsOf, event_visible_at). Rules are not. They compile flat into the Module — compiled_rules: BTreeMap<String, Vec<CompiledRule>> keyed by head name — and Module::compiled_rules() returns all of them with no temporal predicate. Rule selection is timeless.

What temporal structure does a rule need so that “what did the system derive as of the original filing date, under the law as it then stood?” is a first-class, validated question — and how does that structure compose with defeasibility, scoped redefinition, the decidability tier ladder, and the Phase 0/1/4 commit-and-checkpoint machinery Phase 5 reuses?

Context

How many temporal dimensions a legal norm carries, and what they are, is not an open design question — the legal-informatics literature settled it, and the answers converge:

  • Governatori 2015 reduces a norm to two temporal dimensions: when the norm is in force (efficacy) and when the norm exists in the normative system from a given viewpoint (the repository/transaction axis).
  • LegalRuleML names four — efficacy, enforcement, validity, assertion — which collapse onto bitemporal at the substrate: efficacy = valid-time; validity (repealed/annulled status) + assertion (enactment origin) = transaction-time; and enforcement (the statute-of-limitations window in which an authority may act) is an application-layer concern, not a substrate axis.
  • Governatori–Rotolo 2008 tags a defeasible conclusion ±∂^{t_d}@{t_r} l_{t_l} with four temporal slots, of which three are stored coordinates and one is the query instant: literal valid-time t_l, rule time-of-force t_v (the rule’s valid-time), repository time t_r (transaction-time), and derivation time t_d (the “now” at which the inference is drawn — provenance, not a selection axis).

The load-bearing consequence: “enactment-time” is the rule’s valid-time (its efficacy / in-force window), not its transaction-time. A statute enacted in 2025 but effective from 2020 has rule-valid-time [2020, …) and rule-transaction-time [2025-commit, …). Modelling enactment as transaction-time makes retroactive legislation — the motivating audit case — inexpressible.

What already exists

  • The data plane is bitemporal. Every AxiomEvent carries a BitemporalExtent { vt_start, vt_end, tx_from, tx_to } (oxc-protocol), and this rides on every axiom kind — including the rule-declaration kinds (RuleDecl, QueryDecl, …). Rule events already have the storage shape; nothing reads their valid-time.
  • The visibility predicate is general. event_visible_at(event, vt, tt) (oxc-runtime) filters any event by (vt, tt); event_visible_at_valid_time is the valid-time half (vt_start > vt ⇒ out, vt_end ≤ vt ⇒ out).
  • Defeasibility is built. Rules carry rule_strength (strict/defeasible/defeater), label, is_default, defeats edges, and defeat_strategy (RuleDeclBody); the superiority/defeat graph is resolved and acyclicity-checked at elaboration, and compiled three-stratum (Governatori). The temporal-defeat preservation theorem (temporal_defeat_complete_preserves) and the abrogation default are already established in the RP-004 exploration.
  • The commit boundary is explicit. Phase 0 publishes a per-scope visible watermark advanced after maintenance; Phase 1 binds maintain → advance as a contract (“a read pinned at the published watermark observes a derived model consistent with exactly the committed base facts at that tt”); Phase 4 checkpoints the maintainer’s read-model, keyed (module_fingerprint, storage_gen).

What is missing

The rule’s valid-time has no semantics and no consumer. Module::compiled_rules() is a timeless flatten. There is no way to select the rule-set in force at a target point, so the Phase-5 replay path cannot replay the law as it then stood.

Decision

A rule is bitemporal exactly as a fact is. Give the rule-event’s already-present valid-time the efficacy / in-force semantics, and make rule selection at evaluation a function of the read-point instead of a constant. This extends the shipped data-plane bitemporal model to the rule plane; it invents no new axis and adds no parallel catalog.

1. Representation

Rules remain bitemporal axiom events in the one event log. On a RuleDecl event:

  • extent.vt_* is the efficacy window — when the law is in force. Enactment with effective date D sets vt_start = D (retroactive enactment is vt_start < tx_from, the existing data-plane “retroactive correction” shape). Prospective repeal / sunset sets vt_end forward.
  • extent.tx_* is the viewpoint — when the rule text was recorded or corrected — already populated by the commit path.

No versioned rule-set keyed by enactment time: the log is the version axis, and a keyed structure would only re-pose retroactive enactment, which is precisely bitemporality.

The single behavioural change is the selection seam. Module::compiled_rules() (the timeless flatten) gains a read-point-parameterised sibling that runs the existing event_visible_at over rule events:

compiled_rules_at(read) = { rule | event_visible_at(rule_event, read.law_vt, read.tt) }

Engine::evaluate(&[CompiledRule], …) is unchanged — it already takes a borrowed rule slice, so only the caller’s selection changes. The reasoner core and the tier classifier stay temporally oblivious.

2. The time axis (the crux): three coordinates, one default coupling

A read names a point in a bitemporal rule plane and a bitemporal fact plane that share one transaction-time. Per Governatori’s two-dimension reduction and bitemporal-database orthodoxy (transaction-time is a property of the repository, singular), the viewpoint is not split per plane. The selection coordinates are three:

  • fact-VT — which facts held in the world (exists today: AsOf vt);
  • rule-VT — which rules were in effect (new);
  • viewpoint-TT — which recorded state of the repository (facts and rule transcriptions) we believe (exists today: AsOf tt).

The derivation instant t_d (Governatori’s fourth slot) is the replay/query “now”; it is recorded in the derived tuple’s provenance (proof_tag channel), not a read knob.

Default coupling. AsOf stays the (fact-VT, viewpoint-TT) point, wire-compatible; a read adds one optional coordinate, rule_vt: Option<Time>, defaulting to fact-VT. So:

  • as_of vt ⇒ facts valid at vt, under the law in force at vt — the headline audit query, free, no extra surface;
  • Now ⇒ current facts, current law (the conservativity case);
  • explicit rule_vt unlocks the counterfactual quadrant — old facts under today’s law (fact-VT past, rule-VT = now), which is also where retroactive annulment lives.

There is no separate “law-TT” to default: a correction to the transcribed statute text is a viewpoint advance of the one repository, visible at tt ≥ the correction exactly as a fact correction is. The decoupling auditors need — old law vs. current law over old facts — is a valid-time decoupling (rule-VT ≠ fact-VT), not a second transaction-time.

3. Composition

Defeasibility / priority. The superiority/defeat graph stays static, file-local, acyclicity-checked at elaboration. Enactment-time does not touch the graph; it filters which rules are in force at the read-point, inducing a subgraph. A defeat edge whose target is not in force is inert; acyclicity of the whole graph implies acyclicity of every subgraph, so the build-time check still suffices — no new decidability burden, and superiority need not become dynamic. The defeat algebra (team defeat, ambiguity blocking, defeated-defeaters) is time-invariant; only its inputs are time-indexed (mechanized: defeat_preserved_under_full_inForce). The default is abrogation — forward-only: a defeater (or repeal) effective at t₂ closes a warrant from t₂ forward; warrants before t₂ stand. Lex posterior (“later rule wins”) is expressed as enactment-VT ordering plus explicit defeat edges — not time-stamped derivable preferences (Olivieri 2025), which would force superiority dynamic and is out of scope.

Annulment (retroactive invalidation, ab initio) is the separate operation: a transaction-time retraction (forget) across viewpoints with dependency cascade. It escalates to tier:fol and is out of scope for #1019 — the Phase-5 audit story is abrogation-complete. It is a tracked follow-on requiring its own conservativity (AnnulmentExtraction).

Scoped redefinition (definitional scope / Lawsky). Scope and enactment-time are orthogonal and resolve at different stages: scope guards resolve at elaboration (which definition applies in which region); enactment-time resolves at evaluation (which region-scoped rule is in force at the read-point). A rule may carry both. Resolve scope first, filter by read-point second; they never unify.

Lockstep / checkpoint. Phase 1’s invariant extends from “consistent with the committed base facts at that tt” to “…under exactly the rules in force at that read-point.” The Phase-4 checkpoint key folds in the active-rule-set digest at the checkpoint’s read-point, so a checkpoint is never replayed across a law change (a repeal between checkpoint and target invalidates reuse exactly as a schema change does). Phase-5 replay: restore the nearest checkpoint whose read-point matches → replay the base-log suffix → at each step derive with compiled_rules_at(read).

4. Decidability and cost

Tier is a structural property of each rule (RuleDeclBody.main_tier, pre-classified at enactment), independent of enactment time. Selecting a subset of rules can only hold-or-lower the module tier (max over a subset ≤ max over all), so an as-of-past read never escalates cost above the present module’s, and replay over a subset is ≤ replay over the full set. Selection is O(rules) filtering against event_visible_at, memoizable per distinct read-point. Enactment-VT is meta-level (which rules exist) and orthogonal to the object-level temporal sub-tier (since/until inside rule bodies); a rule’s efficacy window must not be conflated with a metric-temporal interval in its body.

5. Mechanization plan (Lean → reference → RFD → code)

Per the substrate workflow and the discipline of mechanizing a novel soundness frame in scratch-Lean first, with a differential oracle gating the implementation.

Conservativity property (central theorem and differential gate). Present-law evaluation is bit-identical to today’s flat behaviour:

when every rule is in force at the read-point, compiled_rules_at(read) returns the full rule-set, so evaluation equals Engine::evaluate over the flat compiled_rules().

Supporting properties. Forward-only enactment: a rule effective from t₂ changes no active set, hence no derivation, at any read-point < t₂ (abrogation; no dependency closure needed). Defeasibility composition: on the in-force subgraph the gated warrant coincides with the ungated warrant.

A core-only scratch-Lean sketch of all three is established (the bitemporal RP-004 exploration): activeAt_eq_all_of_all_inForce / eval_eq_flat_of_all_inForce (conservativity), enactment_forward_only / eval_invariant_forward_only, and defeat_preserved_under_full_inForce — the last proved through the canonical temporal_defeat_complete_preserves. Zero sorry, zero axiom.

Phases, with RFD 0053 Phase 5 as the first consumer:

  • A — scratch-Lean (done, never-merged): bitemporal rule selection + the conservativity and forward-only theorems + defeasibility composition.
  • B — reference: the AsOf/as-of-semantics chapter gains the rule_vt coordinate and the default coupling; a rule-efficacy section in the temporal substrate.
  • C — RFD: this document.
  • D — code: efficacy semantics on the rule-event valid-time in oxc-instantiate; compiled_rules_at(read) in oxc-runtime reusing event_visible_at; the rule_vt coordinate threaded through the serve/query path; the active-rule digest folded into the Phase-4 checkpoint key; Phase-5 replay selecting per read-point. Differential oracle = the Phase-1 lockstep oracle extended along the in-force axis: an as-of-past derived read equals from-scratch Engine::evaluate over the base facts and rules visible at that read-point.

Resolved questions

These were posed as open and are resolved by the prior-art convergence above:

  • Enactment = valid-time, not transaction-time. Retroactive legislation forces it; the issue text (#1019) is corrected accordingly.
  • One shared viewpoint, not a per-plane transaction-time. The audit decoupling is valid-time (rule-VT ≠ fact-VT); there is no separate law-TT to default.
  • Default coupling is rule-VT ← fact-VT.
  • #1019 scope is abrogation (efficacy valid-time windows, tier:recursive); annulment is a tier:fol follow-on.

Open questions

  • OQ1 — Checkpoint forcing. Should a rule-efficacy or rule-transcription change force a Phase-4 checkpoint, bounding replay distance to within one law regime? A correctness-neutral cadence choice (RFD 0053 Q1 makes cadence operator-tunable); leaning yes.
  • OQ2 — Surface spelling. Resolved (Phase B). A rule’s validity is authored with the existing fact at #DATE# qualifier on the rule head (derive H(x) at #DATE# :- …); the read-side coordinate is ReadPoint { data: AsOf, rule_vt: Option<DateTime> } with None tracking the data point’s valid time, and the in-process API is query_derive_at(.., rule_vt). Specified in the reference manual’s Rule validity over time (temporal substrate) and AsOf semantics sections.
  • OQ3 — Annulment follow-on shape. The tier:fol retroactive path and its conservativity (AnnulmentExtraction) are deferred; file as a tracked follow-on when Phase 5 lands.