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 0024 — Allen interval algebra as a library (std::allen), not substrate operators

  • State: committed
  • Opened: 2026-06-08
  • Decides: Allen’s interval algebra is a standard-library theory (std::allen), written in pure .ar over the scalar Date/Duration value layer (#159) — not reserved infix operators in the substrate. The currently-committed-but-unbuilt Allen operators (Syntax/Operators.lean::AllenOp, Syntax/Expr.lean::RuleAtom.allenAtom, the tier:expressive grammar in book §7.3.1, and OE0713 AllenOverMTLDerived) are removed.

This is the temporal counterpart of the principle RFD 0009 / RP-003 already apply to higher-order theories: the substrate stays ontology-neutral; specific theories are libraries. MLT, UFO, and BFO are std::* packages, not language features. Allen’s interval algebra is a theory of time, and the same rule applies. Settled in discussion (the .ar value layer it rests on landed first, by design).

Question

Argon currently carries Allen’s 13 interval relations two ways at once: as reserved substrate operators (infix a before b, mechanized in Lean, drift-gated, tier-classified) and, implicitly, as something a modeler would otherwise define over interval boundaries. The substrate form is committed but unbuilt — no parser, elaborator, or executor path. With the scalar Date/Duration value layer now real (#159), an Allen relation is definable as an ordinary rule over {startsOn, endsOn} boundaries. So:

Does Allen’s interval algebra belong in the substrate (reserved operators), or as a library over the value layer?

Context

  • What is committed today (unbuilt). AllenOp enumerates 12 relations (before/after/meets/metBy/overlaps/overlappedBy/during/contains/starts/startedBy/ finishes/finishedBy — note it omits Allen’s 13th, equals) at spec/lean/Argon/Syntax/Operators.lean:79; the surface atom RuleAtom.allenAtom : FieldPath → AllenOp → FieldPath at Syntax/Expr.lean:222; the field-path allen-op field-path grammar at tier:expressive in book §7.3.1 (07-rules.md:127-150); and OE0713 AllenOverMTLDerived (Allen applied to an MTL-windowed predicate — ill-typed). All @[language_interface] and drift-gated; none of it is parsed, elaborated, or evaluated.
  • Allen reduces to boundary comparisons. a before b ≡ a.endsOn < b.startsOn; a meets b ≡ a.endsOn == b.startsOn; a equals b ≡ a.startsOn == b.startsOn ∧ a.endsOn == b.endsOn; and so on for all 13. Each is a conjunction of chronological comparisons on Date boundaries — exactly what the value layer of #159 now evaluates correctly (and which, pre-#159, the reasoner did as a silent lexicographic string compare).
  • The substrate’s stated posture. Argon is “ontology-neutral (UFO/MLT/BFO are stdlib theory packages, not language features)” (AGENTS.md). The substrate provides value computation (Money/Decimal/Date arithmetic, comparison); theories are libraries. Allen is a theory.
  • Allen is not the only interval algebra. There are variants — point vs. proper intervals, open vs. closed, fuzzy/probabilistic Allen, the coarser INDU and convex-relation algebras. A reserved operator set privileges one (and the committed set is already incomplete: no equals). A library is choosable and extensible.

Decision

  1. std::allen is a library, pure .ar, over #159. It models intervals and defines the 13 Allen relations (and any convenience dispatch) as ordinary derive rules over Date boundaries. It requires nothing from the engine beyond the scalar value layer that already shipped.
  2. Remove the reserved Allen operators from the substrate. AllenOp, RuleAtom.allenAtom, the §7.3.1 grammar, the tier:expressive Allen classification, and OE0713 are deleted. They are unbuilt and have no users, so this is a no-cost reversal taken now while it is free (no migration, nothing to break).
  3. No infix sugar. Library Allen is call/UFCS syntax (a.before(b) or before(a, b)), not infix a before b. For a niche qualitative algebra this is an acceptable — arguably clearer — trade for a smaller, neutral substrate. (Argon does not offer user-defined infix operators, and adding them for one library is not justified.)

The std::allen library (sketch)

Built on #159’s Date/Duration values + chronological comparison. An interval is modeled as a concept with two Date boundaries (a real entity, so its fields project in rule bodies; an opaque inline struct would not):

// std::allen (or std::time::allen)
pub kind TimeInterval { startsOn: Date, endsOn: Date }

pub derive before(a: TimeInterval, b: TimeInterval)  :- a.endsOn < b.startsOn;
pub derive meets(a: TimeInterval, b: TimeInterval)   :- a.endsOn == b.startsOn;
pub derive during(a: TimeInterval, b: TimeInterval)  :- b.startsOn < a.startsOn, a.endsOn < b.endsOn;
pub derive equals(a: TimeInterval, b: TimeInterval)  :- a.startsOn == b.startsOn, a.endsOn == b.endsOn;
// … the remaining relations + inverses, all boundary comparisons.
  • No relation-name magic. A user-declared pub rel AllenHolds(...) stays ordinary data; it gains meaning only if the model defines it from these rules (pub derive AllenHolds(a, Before, b) :- before(a, b);). The substrate never special-cases the name AllenHolds, nor sniffs {startsOn, endsOn} field names.
  • dateInterval / shift are library helpers; until the fn return-of-constructed-value surface matures, the robust form is to shift a boundary inline in the comparison — e.g. the workflow’s `allenAfter(timeInterval
    • relativeTime, dateInterval(checkDate))is(iv.startsOn + relativeTime) > checkDate (after ≡ a.startsOn > b.endsOn; a point interval's endsOn` is the date itself).
  • The library can be complete (all 13 relations incl. equals) and may offer an allenHolds(a, rel, b) dispatch over an AllenRelationType value — neither requires substrate support.

What is removed / changed

A surface change, so Lean-first (per the AGENTS.md workflow: surface decision → Lean → reference → drift mirror → parser/grammar):

  • Lean: delete AllenOp (Syntax/Operators.lean) and RuleAtom.allenAtom (Syntax/Expr.lean); drop the Allen arm from the tier classifier (Decidability/) and any Expr/@[language_interface] references.
  • Reference: remove the Allen grammar + prose from §7.3.1 (07-rules.md:127-150) and Allen mentions in §6/§15/crash-course; document std::allen in §15 (stdlib) instead.
  • Drift / Rust mirror: drop the AllenOp mirror in oxc-ast and its drift-gate entry; the parser/grammar never recognized the operators, so there is little Rust to remove.
  • Diagnostics: retire OE0713 AllenOverMTLDerived (it only exists to police an Allen×MTL interaction that no longer has substrate operators). Leave a tombstone in grammar.toml per code-allocation hygiene, or reclaim the number — decide at implementation.

Non-goals

  • Not the temporal reasoner. This is orthogonal to DatalogMTL metric operators (since/until/ever), bitemporal valid-time, and temporal modal operators — the “temporal operators” tracked separately. Allen here is qualitative interval relations as value-level boolean rules.
  • Not interval types in the substrate. The substrate gains no Interval type; an interval is a library concept with two Date fields.
  • No infix operators, no fuzzy/INDU variants in scope (those are further libraries if wanted).
  • DateTime/Time intervals and calendar-relative durations are out of scope — they ride the #159 follow-ons (sub-day resolution, P1M/P1Y).

Alternatives considered

  • Keep Allen in the substrate (status quo). Rejected: it privileges one interval theory, is library- definable with zero engine support, and the committed set is already incomplete. Mechanizing + drift-gating a theory the substrate doesn’t need is debt.
  • Ship Allen as built-in stdlib functions (allenBefore, …) wired into the engine. Rejected: same neutrality problem one layer down, and it would fork the algebra against the reserved operators. A pure-.ar library is cleaner and needs nothing special.
  • Leave the operators reserved-but-unbuilt. Rejected: a dangling surface that will fork against std::allen the moment the library exists; removing it now (unbuilt, no users) is the cheapest it will ever be.

Sequencing

  1. (Done — prerequisite) Scalar Date/Duration value layer + chronological comparison, #159.
  2. Remove the reserved Allen operators (Lean → reference → drift mirror → grammar), per What is removed.
  3. Ship std::allen as a pure-.ar package over #159.

Related: RFD 0009 (theories-as-libraries), RFD 0016 (the value tower this builds on), RP-003 (substrate neutrality). The today()/now() evaluation-context for date-relative rules is a separate RFD (deliberately out of scope here).