Temporal substrate

Why bitemporal

The substrate before this section operates on a single state mapping concepts to extents. The mutation grammar (mutate) advances the state from snapshot to snapshot; prior snapshots are not addressable. This section introduces the bitemporal substrate: every fact carries a valid time and a transaction time. Bare queries default to the current snapshot; explicit temporal operators address the past, the future, and the historical record of the system’s beliefs.

The formalism is DatalogMTL (Wałęga et al., IJCAI 2019) with stratified negation (Tena Cucala et al., AAAI 2021) over the integer timeline; the reference reasoner is MeTeoR (Wałęga et al., AAAI 2022).

Valid time and transaction time

Two interval annotations on every fact (and every relation tuple):

• Valid time (VT) — when the fact holds in the world. [VT_start, VT_end], with open-ended [VT_start, ∞] for ongoing.
• Transaction time (TT) — when the system recorded the fact. [TT_start, TT_end], with open-ended [TT_start, ∞] for current belief.

The snapshot view is the projection ${,\mathsf{iof}(x, T),\mid,VT_{\text{start}} \le \mathit{now} \le VT_{\text{end}} ;\wedge; TT_{\text{start}} \le \mathit{now} \le TT_{\text{end}},}$. Bare rule atoms and bare queries default to this view.

The bitemporal extension applies uniformly to all relations, not just iof. A pub rel Enrolment(s: Person, u: University) tuple carries VT and TT just like an iof fact.

Mechanized at spec/lean/Argon/Reasoning/Temporal.lean (BiState as the bitemporal State; TTHistory and TTMonotone for the transaction-time invariant). The bitemporal extension is additive — the termination machinery of Argon.Reasoning.State lifts pointwise without modification.

Retroactive correction and audit

Mutations that close a VT interval retroactively (delete iof(x, T) at #PAST-DATE#) do not erase the prior record. They close its TT interval at now and append a new record with the corrected VT. Audit queries as of TT = #PAST-DATE# reconstruct what the system believed at any past point. The substrate is append-only by default; explicit erasure (forget), crypto-shredding (#[shred_on_forget]), and #[retention(…)] bounds are storage-layer concerns specified in mutate and Storage layer.

Rule validity over time

A rule carries valid time and transaction time just as a fact does. Its valid time is the interval over which the rule is in effect; its transaction time is when the rule was recorded or its text corrected. This is the bitemporal model of any fact — when it holds versus when the system recorded it — applied to rules, with transaction time serving as the shared viewpoint across facts and rules.

A rule’s start-of-validity is written with the same at #DATE# qualifier a fact uses, placed on the head:

pub derive eligible(x) at #2018-01-01# :- enrolled(x), in_good_standing(x);

Without the qualifier a rule has unbounded validity — in effect at every point — so a program that dates none of its rules behaves exactly as one with no validity windows at all. A rule’s record time, when it entered the system, is the separate transaction-time axis and is never folded into its validity: an undated rule is in effect at past points too, not merely from the moment it was written.

Evaluating derived facts at a chosen rule valid-time point selects exactly the rules in effect at that point, by the same valid-time visibility the data plane applies to facts (VT_start ≤ t ∧ t < VT_end). Reading at the present selects every currently-in-effect rule, so present-time evaluation is unchanged by the feature. A reconstruction of what was derived at a past point replays under the rules in effect then, not the rules in effect now.

A prospective retirement closes a rule’s VT_end going forward; it is forward-only: derived facts that held while the rule was in effect stand, and only points at or after the close lose that rule’s support. Retroactive invalidation — removing a rule as if it had never been in effect — is a distinct, transaction-time operation outside this section.

A rule’s validity window is a property of the rule — which rules apply — and is independent of any metric-temporal operator (since, until) appearing inside a rule body, which constrains when within the world timeline a body atom holds.

Three-valued evaluation under OWA

Under open-world assumption, temporal atoms evaluate to Is | Not | Can. The since and until operators (see Temporal rule atoms) lift to three-valued via the strong-Kleene meet/join tables that truth values defines, composed pointwise across the interval. Unknown temporal extent projects to Can, never to Both — there are no conflicting witnesses, just single-source uncertainty.

Temporal sub-tier

Temporal expressiveness is an orthogonal sub-tier on top of the main tier ladder. Every program has a tier pair (main, temporal) — see Tier ladder.

Metric-timeline resolution

The metric temporal operators (since, until, and the box/diamond bounded forms) reason over a discrete integer timeline whose tick is a package-declared resolution, set in ox.toml:

[temporal.metric]
resolution = "week"   # or "day" (default), "hour", "nanosecond", "2weeks", …

The tick is a package-global choice (one metric axis is shared by every rule and fact), mirroring default_world. It lives under [temporal] — the umbrella for temporal-reasoning config — rather than a bare [metric], so the precise word metric stays scoped to the metric-operator family (distinct from the modal box/diamond family) and leaves room for future siblings ([temporal.modal], …). It is a cost/coarsening lever: a metric operator’s work scales with the number of ticks between interval endpoints, so a program reasoning over long spans can declare a coarser tick. Because decidability rests on discreteness — not on the tick equalling a day — any positive-integer tick keeps the metric fragment decidable (see Decidability).

• Snapshot reads are unaffected. “The fact valid at instant t” (see AsOf semantics) stays a full-nanosecond integer comparison; it never consults the tick. The tick governs only the metric operators.
• Bounds are authored in days (.days/.weeks, or a bare integer) and coarsened onto the tick. A bound that is not an integer multiple of the tick loud-refuses rather than rounding — since[3 days] under a week tick refuses (3⁄7 is not a whole number of weeks); since[14 days] is two ticks.
• The default is day, so a package that declares no [temporal.metric] table behaves exactly as before.
• An unrecognized resolution value is a non-fatal manifest warning (it falls back to the day default), per the manifest-honesty convention.

The design record is RFD 0067 §6.