feat(stdlib): Allen's interval algebra (D11 from DB-theory inventory)#272
Merged
Merged
Conversation
…ory inventory) Citation: Allen, J. F. "Maintaining knowledge about temporal intervals." Communications of the ACM 26(11): 832-843. November 1983. The canonical qualitative-temporal-reasoning framework: 13 mutually- exclusive base relations describing how two intervals can stand on a totally-ordered time domain. Snodgrass (1995) "The TSQL2 Temporal Query Language" applied this algebra to relational databases, motivating SQL:2011 valid-time / transaction-time period support. What lands - `type Relation` — 13 variants (Before/After, Meets/MetBy, Overlaps/OverlappedBy, Starts/StartedBy, During/Contains, Finishes/FinishedBy, Equals). - `type Interval = Interval(i64, i64)` — half-open `[start, end)`. - `make(start, end) -> Result<Interval, String>` — smart constructor that rejects `start > end`. - `start(&Interval) -> i64`, `end(&Interval) -> i64`, `duration(&Interval) -> i64` — accessors. - `relate(&Interval, &Interval) -> Relation` — total 13-way classifier in O(1) (six integer comparisons worst-case), following Allen 1983 §2's exhaustive case partition. - `inverse(Relation) -> Relation` — the foundational orientation lemma: `relate(a, b) = inverse(relate(b, a))` (proof: Coq follow-up at `formal/Allen.v`). - `is_disjoint(&Interval, &Interval) -> bool`, `has_proper_overlap(&Interval, &Interval) -> bool` — derived predicates. Why ephapax-shaped Affinely consumable: `Interval` carries no resource obligation at L1 and drops freely at L2 (Affine or Linear). Self-contained — no L1/L2/L3/L4 dependency, no proof obligations attached at landing time. The DB-theory inventory ranks this as the cleanest of the 5 "ship-this-month quick wins": zero prereqs. Future work (separate PRs) 1. Composition table (Allen 1983 §3 — 13×13 = 169-entry table). Encoding requires a set type; landing this depends on a future `stdlib/Set.eph`. 2. Coq mechanisation at `formal/Allen.v`: prove `inverse(inverse(r)) = r` (self-inverse) and the orientation lemma. Both are case-analysis on 13 variants. 3. Bitemporal extension (D12 from DB-theory inventory) — valid-time × transaction-time 2D Allen lattice (Snodgrass 1995 §4). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 71 issues detected
View findings[
{
"reason": "Issue in abi-verify.yml",
"type": "missing_timeout_minutes",
"file": "abi-verify.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in coq-build.yml",
"type": "missing_timeout_minutes",
"file": "coq-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in coq-build.yml",
"type": "missing_timeout_minutes",
"file": "coq-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in coq-build.yml",
"type": "missing_timeout_minutes",
"file": "coq-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in governance.yml",
"type": "missing_timeout_minutes",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "missing_timeout_minutes",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "missing_timeout_minutes",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in rust-ci.yml",
"type": "missing_timeout_minutes",
"file": "rust-ci.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "missing_timeout_minutes",
"file": "scorecard-enforcer.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
stdlib/Allen.eph: Allen's interval algebra (Allen 1983) — the canonical qualitative-temporal-reasoning framework, 13 mutually-exclusive base relations on intervals.The DB-theory inventory (this session's audit) ranked this as the cleanest of the 5 "ship-this-month quick wins": fully self-contained, zero prereqs, zero L1/L2/L3/L4 dependency.
What lands
type Relation— 13 variants (Before/After, Meets/MetBy, Overlaps/OverlappedBy, Starts/StartedBy, During/Contains, Finishes/FinishedBy, Equals).type Interval = Interval(i64, i64)— half-open[start, end).make / start / end / duration / relate / inverse / is_disjoint / has_proper_overlap.relate(&Interval, &Interval) -> Relation— total O(1) 13-way classifier following Allen 1983 §2.Pedigree
Future work (separate PRs)
stdlib/Set.eph.formal/Allen.v:inverse(inverse(r)) = r+ orientation lemma (relate(a,b) = inverse(relate(b,a))).Test plan
.ephfiles are not currently in any automated test harness — flagged separately in this session's TEST-NEEDS audit).formal/Allen.vproving the two foundational laws.🤖 Generated with Claude Code