diff --git a/crates/temporal_core/Cargo.toml b/crates/temporal_core/Cargo.toml index 7135b8101..f5da690a1 100644 --- a/crates/temporal_core/Cargo.toml +++ b/crates/temporal_core/Cargo.toml @@ -17,6 +17,7 @@ publish = false jiff.workspace = true serde.workspace = true serde_json.workspace = true +uuid.workspace = true [dev-dependencies] serde_json.workspace = true diff --git a/crates/temporal_core/src/error.rs b/crates/temporal_core/src/error.rs index a0ae60920..d97eb8fd4 100644 --- a/crates/temporal_core/src/error.rs +++ b/crates/temporal_core/src/error.rs @@ -16,6 +16,8 @@ pub enum TemporalError { EmptyInterval, /// Interval boundaries, precision, and certainty disagreed. InvalidIntervalCertainty, + /// Qualitative relation classification received a nonproper or open interval. + RelationRequiresProperBoundedInterval, /// A JSON wire payload was malformed, incomplete, or contained unknown fields. InvalidWirePayload, /// A JSON wire payload used a schema version this crate does not support. @@ -32,6 +34,9 @@ impl fmt::Display for TemporalError { Self::InvalidIntervalOrder => "invalid temporal interval order", Self::EmptyInterval => "temporal interval is empty", Self::InvalidIntervalCertainty => "invalid temporal interval certainty", + Self::RelationRequiresProperBoundedInterval => { + "temporal relation requires proper bounded intervals" + } Self::InvalidWirePayload => "invalid temporal wire payload", Self::UnsupportedWireVersion => "unsupported temporal wire version", Self::ClockTypeMismatch => "temporal clock type mismatch", diff --git a/crates/temporal_core/src/lib.rs b/crates/temporal_core/src/lib.rs index 3eda04fc6..ede257114 100644 --- a/crates/temporal_core/src/lib.rs +++ b/crates/temporal_core/src/lib.rs @@ -1,6 +1,6 @@ #![forbid(unsafe_code)] #![deny(missing_docs)] -//! Six nominal clocks, strict absolute instants, and uncertain intervals. +//! Six nominal clocks, strict absolute instants, uncertain intervals, and bounded temporal reasoning. //! //! TEPP distinguishes the time at which an event occurred, a claim was made, //! a document was created, the platform observed data, evidence became @@ -20,11 +20,18 @@ //! semantics. Known intervals retain source precision; unknown intervals do not //! claim containment. JSON interchange is explicit, versioned, clock-specific, //! and reconstructed through the same domain validation boundary. +//! +//! Proper bounded intervals can be classified with Allen's thirteen elementary +//! relations. Relation sets support inverse and complete composition, while a +//! resource-bounded path-consistency reasoner preserves direct assertions, +//! derived narrowing, and conservative supporting-assertion provenance. mod clock; mod error; mod instant; mod interval; +mod reasoner; +mod relation; mod wire; /// The time at which a source asserted a claim about an event or state. @@ -53,5 +60,29 @@ pub use interval::TemporalCertainty; pub use interval::TemporalInterval; /// The source precision retained for a temporal value or interval. pub use interval::TemporalPrecision; +/// Summary of one successful bounded closure operation. +pub use reasoner::ClosureReport; +/// An opaque identifier for one accepted relation assertion. +pub use reasoner::ConstraintId; +/// One observed or derived relation returned by the reasoner. +pub use reasoner::DerivedRelation; +/// The bounded resource whose configured maximum was exceeded. +pub use reasoner::ReasonerLimitKind; +/// Evidence that a qualitative temporal network has no possible relation. +pub use reasoner::TemporalContradiction; +/// A bounded qualitative interval-constraint network. +pub use reasoner::TemporalReasoner; +/// A fail-closed temporal-reasoner error. +pub use reasoner::TemporalReasonerError; +/// Explicit capacity bounds for one temporal reasoner instance. +pub use reasoner::TemporalReasonerLimits; +/// An opaque identifier for one interval variable in a reasoner instance. +pub use reasoner::TemporalVariableId; +/// One of Allen's thirteen elementary relations between proper intervals. +pub use relation::AllenRelation; +/// A compact set of possible elementary interval relations. +pub use relation::RelationSet; +/// Classify two proper, two-sided, nonzero intervals with Allen's algebra. +pub use relation::classify_interval_relation; /// The only temporal JSON wire-schema version accepted by this crate. pub use wire::TEMPORAL_WIRE_SCHEMA_VERSION; diff --git a/crates/temporal_core/src/reasoner.rs b/crates/temporal_core/src/reasoner.rs new file mode 100644 index 000000000..9f0e88239 --- /dev/null +++ b/crates/temporal_core/src/reasoner.rs @@ -0,0 +1,540 @@ +//! Bounded path-consistency closure for qualitative interval constraints. + +use crate::RelationSet; +use std::collections::BTreeSet; +use std::fmt; +use uuid::Uuid; + +#[derive(Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +struct ReasonerInstanceId(Uuid); + +impl ReasonerInstanceId { + fn new() -> Self { + Self(Uuid::now_v7()) + } +} + +/// An opaque identifier for one interval variable in a reasoner instance. +#[derive(Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct TemporalVariableId { + reasoner_instance_id: ReasonerInstanceId, + variable_index: usize, +} + +/// An opaque identifier for one accepted relation assertion. +#[derive(Clone, Copy, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct ConstraintId { + reasoner_instance_id: ReasonerInstanceId, + constraint_index: usize, +} + +/// The bounded resource whose configured maximum was exceeded. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum ReasonerLimitKind { + /// The maximum number of interval variables. + Variables, + /// The maximum number of accepted constraints. + Constraints, + /// The maximum number of path-consistency propagation steps. + PropagationSteps, +} + +/// Explicit capacity bounds for one temporal reasoner instance. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub struct TemporalReasonerLimits { + variable_limit: usize, + constraint_limit: usize, + propagation_budget: usize, +} + +impl TemporalReasonerLimits { + /// Validate nonzero variable, constraint, and propagation limits. + /// + /// # Errors + /// + /// Returns [`TemporalReasonerError::InvalidLimits`] when any maximum is + /// zero. + pub const fn new( + maximum_variables: usize, + maximum_constraints: usize, + maximum_propagation_steps: usize, + ) -> Result { + if maximum_variables == 0 || maximum_constraints == 0 || maximum_propagation_steps == 0 { + Err(TemporalReasonerError::InvalidLimits) + } else { + Ok(Self { + variable_limit: maximum_variables, + constraint_limit: maximum_constraints, + propagation_budget: maximum_propagation_steps, + }) + } + } +} + +/// Evidence that a qualitative temporal network has no possible relation. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct TemporalContradiction { + left: TemporalVariableId, + right: TemporalVariableId, + support: Vec, + attempted_relations: Option, +} + +impl TemporalContradiction { + /// Return the left variable of the contradictory pair. + #[must_use] + pub const fn left(&self) -> TemporalVariableId { + self.left + } + + /// Return the right variable of the contradictory pair. + #[must_use] + pub const fn right(&self) -> TemporalVariableId { + self.right + } + + /// Return accepted assertions supporting the contradiction. + #[must_use] + pub fn support(&self) -> &[ConstraintId] { + &self.support + } + + /// Return the rejected direct assertion when contradiction occurred before closure. + #[must_use] + pub const fn attempted_relations(&self) -> Option { + self.attempted_relations + } + + fn from_support( + left: TemporalVariableId, + right: TemporalVariableId, + support: BTreeSet, + attempted_relations: Option, + ) -> Self { + Self { + left, + right, + support: support.into_iter().collect(), + attempted_relations, + } + } +} + +impl fmt::Display for TemporalContradiction { + fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result { + formatter.write_str("temporal relation network is contradictory") + } +} + +impl std::error::Error for TemporalContradiction {} + +/// A fail-closed temporal-reasoner error. +#[derive(Clone, Debug, Eq, PartialEq)] +#[non_exhaustive] +pub enum TemporalReasonerError { + /// One or more configured resource limits were zero. + InvalidLimits, + /// A variable identifier does not belong to this reasoner instance. + UnknownVariable, + /// An asserted constraint supplied no possible elementary relation. + EmptyRelationSet, + /// A configured reasoner resource maximum was exceeded. + LimitExceeded(ReasonerLimitKind), + /// An assertion or propagation step proved that no relation remains possible. + Contradiction(TemporalContradiction), +} + +impl fmt::Display for TemporalReasonerError { + fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result { + let message = match self { + Self::InvalidLimits => "invalid temporal reasoner limits", + Self::UnknownVariable => "unknown temporal reasoner variable", + Self::EmptyRelationSet => "temporal relation set is empty", + Self::LimitExceeded(_) => "temporal reasoner resource limit exceeded", + Self::Contradiction(_) => "temporal relation network is contradictory", + }; + formatter.write_str(message) + } +} + +impl std::error::Error for TemporalReasonerError {} + +/// One observed or derived relation returned by the reasoner. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct DerivedRelation { + relations: RelationSet, + observed: bool, + support: Vec, +} + +impl DerivedRelation { + /// Return the currently possible elementary relations. + #[must_use] + pub const fn relations(&self) -> RelationSet { + self.relations + } + + /// Return whether at least one direct assertion exists for this ordered pair. + #[must_use] + pub const fn is_observed(&self) -> bool { + self.observed + } + + /// Return the conservative accepted-assertion support for this relation. + #[must_use] + pub fn support(&self) -> &[ConstraintId] { + &self.support + } +} + +/// Summary of one successful bounded closure operation. +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub struct ClosureReport { + revisions: usize, + propagation_steps: usize, +} + +impl ClosureReport { + /// Return whether closure narrowed at least one relation set. + #[must_use] + pub const fn changed(self) -> bool { + self.revisions != 0 + } + + /// Return the number of relation-set revisions. + #[must_use] + pub const fn revisions(self) -> usize { + self.revisions + } + + /// Return the number of bounded path-consistency checks performed. + #[must_use] + pub const fn propagation_steps(self) -> usize { + self.propagation_steps + } +} + +#[derive(Clone, Debug)] +struct RelationCell { + relations: RelationSet, + observed: bool, + support: BTreeSet, +} + +impl RelationCell { + fn unconstrained() -> Self { + Self { + relations: RelationSet::all(), + observed: false, + support: BTreeSet::new(), + } + } + + fn identity() -> Self { + Self { + relations: RelationSet::singleton(crate::AllenRelation::Equals), + observed: false, + support: BTreeSet::new(), + } + } +} + +/// A bounded qualitative interval-constraint network. +/// +/// The reasoner stores direct assertions separately from derived narrowing, +/// propagates inverse relations, and applies path consistency until stable. +/// Failed closure is atomic: contradiction or resource exhaustion restores the +/// network to its pre-closure state. Opaque variable and constraint identifiers +/// are scoped to one reasoner instance and fail closed when mixed across +/// instances. +pub struct TemporalReasoner { + reasoner_instance_id: ReasonerInstanceId, + limits: TemporalReasonerLimits, + cells: Vec>, + constraint_count: usize, +} + +impl TemporalReasoner { + /// Create an empty reasoner with validated explicit limits. + #[must_use] + pub fn with_limits(limits: TemporalReasonerLimits) -> Self { + Self { + reasoner_instance_id: ReasonerInstanceId::new(), + limits, + cells: Vec::new(), + constraint_count: 0, + } + } + + /// Add one interval variable. + /// + /// # Errors + /// + /// Returns [`TemporalReasonerError::LimitExceeded`] when the configured + /// variable capacity is exhausted. + pub fn add_variable(&mut self) -> Result { + if self.cells.len() >= self.limits.variable_limit { + return Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::Variables, + )); + } + + let identifier = self.variable_id(self.cells.len()); + for row in &mut self.cells { + row.push(RelationCell::unconstrained()); + } + let mut new_row = vec![RelationCell::unconstrained(); self.cells.len() + 1]; + new_row[identifier.variable_index] = RelationCell::identity(); + self.cells.push(new_row); + Ok(identifier) + } + + /// Assert a nonempty relation set for an ordered variable pair. + /// + /// The reverse pair is narrowed by the inverse relation set. The returned + /// identifier is retained as provenance for later derived relations. + /// Rejected assertions neither consume constraint capacity nor receive an + /// accepted [`ConstraintId`]. + /// + /// # Errors + /// + /// Returns an unknown-variable, empty-set, capacity, or contradiction error + /// when the assertion cannot be accepted. + pub fn assert_relation( + &mut self, + left: TemporalVariableId, + right: TemporalVariableId, + relations: RelationSet, + ) -> Result { + self.validate_pair(left, right)?; + if relations.is_empty() { + return Err(TemporalReasonerError::EmptyRelationSet); + } + if self.constraint_count >= self.limits.constraint_limit { + return Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::Constraints, + )); + } + + let narrowed = self.cells[left.variable_index][right.variable_index] + .relations + .intersection(relations); + if narrowed.is_empty() { + let support = self.cells[left.variable_index][right.variable_index] + .support + .clone(); + return Err(TemporalReasonerError::Contradiction( + TemporalContradiction::from_support(left, right, support, Some(relations)), + )); + } + + let identifier = self.constraint_id(self.constraint_count); + let inverse_was_observed = self.cells[right.variable_index][left.variable_index].observed; + let mut support = self.cells[left.variable_index][right.variable_index] + .support + .clone(); + support.insert(identifier); + self.cells[left.variable_index][right.variable_index] = RelationCell { + relations: narrowed, + observed: true, + support: support.clone(), + }; + self.cells[right.variable_index][left.variable_index] = RelationCell { + relations: narrowed.inverse(), + observed: inverse_was_observed || left == right, + support, + }; + self.constraint_count += 1; + Ok(identifier) + } + + /// Apply bounded path-consistency closure atomically. + /// + /// # Errors + /// + /// Returns contradiction evidence when a pair becomes impossible, or a + /// propagation-step limit error when closure exceeds its configured budget. + pub fn close(&mut self) -> Result { + let snapshot = self.cells.clone(); + match self.close_in_place() { + Ok(report) => Ok(report), + Err(error) => { + self.cells = snapshot; + Err(error) + } + } + } + + /// Return the current relation and conservative provenance for an ordered pair. + /// + /// # Errors + /// + /// Returns [`TemporalReasonerError::UnknownVariable`] when either identifier + /// does not belong to this reasoner. + pub fn relation( + &self, + left: TemporalVariableId, + right: TemporalVariableId, + ) -> Result { + self.validate_pair(left, right)?; + let cell = &self.cells[left.variable_index][right.variable_index]; + Ok(DerivedRelation { + relations: cell.relations, + observed: cell.observed, + support: cell.support.iter().copied().collect(), + }) + } + + fn variable_id(&self, variable_index: usize) -> TemporalVariableId { + TemporalVariableId { + reasoner_instance_id: self.reasoner_instance_id, + variable_index, + } + } + + fn constraint_id(&self, constraint_index: usize) -> ConstraintId { + ConstraintId { + reasoner_instance_id: self.reasoner_instance_id, + constraint_index, + } + } + + fn validate_pair( + &self, + left: TemporalVariableId, + right: TemporalVariableId, + ) -> Result<(), TemporalReasonerError> { + // Variable indices are private to this reasoner and only issued by + // `add_variable`. Public API therefore cannot construct an in-instance + // out-of-range index; identity isolation is the enforceable fail-closed + // boundary for foreign or forged identifiers. + if left.reasoner_instance_id != self.reasoner_instance_id + || right.reasoner_instance_id != self.reasoner_instance_id + { + Err(TemporalReasonerError::UnknownVariable) + } else { + debug_assert!(left.variable_index < self.cells.len()); + debug_assert!(right.variable_index < self.cells.len()); + Ok(()) + } + } + + fn close_in_place(&mut self) -> Result { + let mut revisions = 0_usize; + let mut propagation_steps = 0_usize; + let variable_count = self.cells.len(); + + loop { + let mut changed = false; + for left in 0..variable_count { + for right in 0..variable_count { + if left == right { + continue; + } + for middle in 0..variable_count { + if middle == left || middle == right { + continue; + } + if propagation_steps >= self.limits.propagation_budget { + return Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::PropagationSteps, + )); + } + propagation_steps += 1; + + let composed = self.cells[left][middle] + .relations + .compose(self.cells[middle][right].relations); + let current = self.cells[left][right].relations; + let narrowed = current.intersection(composed); + if narrowed.is_empty() { + let support = union_support([ + &self.cells[left][right].support, + &self.cells[left][middle].support, + &self.cells[middle][right].support, + ]); + return Err(TemporalReasonerError::Contradiction( + TemporalContradiction::from_support( + self.variable_id(left), + self.variable_id(right), + support, + None, + ), + )); + } + if narrowed == current { + continue; + } + + let support = union_support([ + &self.cells[left][right].support, + &self.cells[left][middle].support, + &self.cells[middle][right].support, + ]); + let observed = self.cells[left][right].observed; + let inverse_observed = self.cells[right][left].observed; + self.cells[left][right] = RelationCell { + relations: narrowed, + observed, + support: support.clone(), + }; + self.cells[right][left] = RelationCell { + relations: narrowed.inverse(), + observed: inverse_observed, + support, + }; + revisions += 1; + changed = true; + } + } + } + if !changed { + return Ok(ClosureReport { + revisions, + propagation_steps, + }); + } + } + } +} + +fn union_support( + supports: [&BTreeSet; COUNT], +) -> BTreeSet { + let mut result = BTreeSet::new(); + for support in supports { + result.extend(support.iter().copied()); + } + result +} + +#[cfg(test)] +mod tests { + use super::{ + TemporalReasoner, TemporalReasonerError, TemporalReasonerLimits, TemporalVariableId, + }; + + #[test] + fn validate_pair_rejects_each_foreign_instance_position() { + let limits = TemporalReasonerLimits::new(2, 2, 10).expect("limits must validate"); + let mut local = TemporalReasoner::with_limits(limits); + let mut foreign = TemporalReasoner::with_limits(limits); + let local_variable = local.add_variable().expect("local variable must fit"); + let foreign_variable = foreign.add_variable().expect("foreign variable must fit"); + + assert_eq!( + local.validate_pair(foreign_variable, local_variable), + Err(TemporalReasonerError::UnknownVariable) + ); + assert_eq!( + local.validate_pair(local_variable, foreign_variable), + Err(TemporalReasonerError::UnknownVariable) + ); + assert_eq!(local.validate_pair(local_variable, local_variable), Ok(())); + // Keep the opaque identifier constructor path exercised for documentation. + let _ = TemporalVariableId { + reasoner_instance_id: local.reasoner_instance_id, + variable_index: local_variable.variable_index, + }; + } +} diff --git a/crates/temporal_core/src/relation.rs b/crates/temporal_core/src/relation.rs new file mode 100644 index 000000000..3462f04d9 --- /dev/null +++ b/crates/temporal_core/src/relation.rs @@ -0,0 +1,325 @@ +//! Allen-style qualitative relations over proper bounded temporal intervals. + +use crate::{TemporalBoundary, TemporalCertainty, TemporalClock, TemporalError, TemporalInterval}; +use serde::{Deserialize, Serialize}; +use std::cmp::Ordering; +use std::sync::OnceLock; + +const ELEMENTARY_RELATION_COUNT: usize = 13; +const ALL_RELATION_BITS: u16 = (1_u16 << ELEMENTARY_RELATION_COUNT) - 1; + +/// One of Allen's thirteen elementary relations between proper intervals. +#[derive(Clone, Copy, Debug, Deserialize, Eq, Hash, Ord, PartialEq, PartialOrd, Serialize)] +#[repr(u8)] +#[serde(rename_all = "snake_case")] +pub enum AllenRelation { + /// The left interval ends before the right interval starts. + Before = 0, + /// The left interval starts after the right interval ends. + After = 1, + /// The left interval ends exactly when the right interval starts. + Meets = 2, + /// The left interval starts exactly when the right interval ends. + MetBy = 3, + /// The left interval starts first, intersects the right interval, and ends first. + Overlaps = 4, + /// The right interval starts first, intersects the left interval, and ends first. + OverlappedBy = 5, + /// Both intervals start together and the left interval ends first. + Starts = 6, + /// Both intervals start together and the right interval ends first. + StartedBy = 7, + /// The left interval is strictly inside the right interval. + During = 8, + /// The right interval is strictly inside the left interval. + Contains = 9, + /// Both intervals end together and the left interval starts later. + Finishes = 10, + /// Both intervals end together and the right interval starts later. + FinishedBy = 11, + /// Both interval endpoints are equal. + Equals = 12, +} + +impl AllenRelation { + /// Every elementary relation in stable bit-index order. + pub const ALL: [Self; ELEMENTARY_RELATION_COUNT] = [ + Self::Before, + Self::After, + Self::Meets, + Self::MetBy, + Self::Overlaps, + Self::OverlappedBy, + Self::Starts, + Self::StartedBy, + Self::During, + Self::Contains, + Self::Finishes, + Self::FinishedBy, + Self::Equals, + ]; + + /// Return the relation obtained by swapping the left and right intervals. + #[must_use] + pub const fn inverse(self) -> Self { + match self { + Self::Before => Self::After, + Self::After => Self::Before, + Self::Meets => Self::MetBy, + Self::MetBy => Self::Meets, + Self::Overlaps => Self::OverlappedBy, + Self::OverlappedBy => Self::Overlaps, + Self::Starts => Self::StartedBy, + Self::StartedBy => Self::Starts, + Self::During => Self::Contains, + Self::Contains => Self::During, + Self::Finishes => Self::FinishedBy, + Self::FinishedBy => Self::Finishes, + Self::Equals => Self::Equals, + } + } + + const fn bit(self) -> u16 { + 1_u16 << (self as u8) + } + + const fn index(self) -> usize { + self as usize + } +} + +/// A compact set of possible elementary interval relations. +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] +pub struct RelationSet(u16); + +impl RelationSet { + /// Return the empty relation set. + #[must_use] + pub const fn empty() -> Self { + Self(0) + } + + /// Return the universal set containing all thirteen elementary relations. + #[must_use] + pub const fn all() -> Self { + Self(ALL_RELATION_BITS) + } + + /// Return a set containing exactly one elementary relation. + #[must_use] + pub const fn singleton(relation: AllenRelation) -> Self { + Self(relation.bit()) + } + + /// Build a set from a slice of elementary relations. + #[must_use] + pub fn from_relations(relations: &[AllenRelation]) -> Self { + let mut result = Self::empty(); + for relation in relations { + result = result.with(*relation); + } + result + } + + /// Return whether this set contains `relation`. + #[must_use] + pub const fn contains(self, relation: AllenRelation) -> bool { + self.0 & relation.bit() != 0 + } + + /// Return the number of elementary relations in this set. + #[must_use] + pub const fn len(self) -> usize { + self.0.count_ones() as usize + } + + /// Return whether this set contains no relation. + #[must_use] + pub const fn is_empty(self) -> bool { + self.0 == 0 + } + + /// Iterate over contained relations once in stable elementary order. + pub fn iter(self) -> impl Iterator { + AllenRelation::ALL + .into_iter() + .filter(move |relation| self.contains(*relation)) + } + + /// Return the intersection of two relation sets. + #[must_use] + pub const fn intersection(self, other: Self) -> Self { + Self(self.0 & other.0) + } + + /// Return the union of two relation sets. + #[must_use] + pub const fn union(self, other: Self) -> Self { + Self(self.0 | other.0) + } + + /// Return the relation set obtained by swapping the left and right intervals. + #[must_use] + pub fn inverse(self) -> Self { + let mut result = Self::empty(); + for relation in AllenRelation::ALL { + if self.contains(relation) { + result = result.with(relation.inverse()); + } + } + result + } + + /// Compose this left-to-middle set with a middle-to-right set. + /// + /// The result contains every elementary left-to-right relation compatible + /// with at least one relation from each input set. + #[must_use] + pub fn compose(self, other: Self) -> Self { + let table = composition_table(); + let mut result = Self::empty(); + for left in AllenRelation::ALL { + if !self.contains(left) { + continue; + } + for right in AllenRelation::ALL { + if other.contains(right) { + result = result.union(table[left.index()][right.index()]); + } + } + } + result + } + + const fn with(self, relation: AllenRelation) -> Self { + Self(self.0 | relation.bit()) + } +} + +/// Classify two proper, two-sided, nonzero intervals with Allen's algebra. +/// +/// Boundary inclusion does not change the qualitative endpoint relation. Exact, +/// open-ended, and explicitly unknown intervals are rejected because Allen's +/// elementary interval algebra assumes proper intervals with distinct starts +/// and ends. +/// +/// # Errors +/// +/// Returns [`TemporalError::RelationRequiresProperBoundedInterval`] when either +/// interval is not a proper two-sided bounded interval. +pub fn classify_interval_relation( + left: &TemporalInterval, + right: &TemporalInterval, +) -> Result { + let (left_start, left_end) = proper_endpoints(left)?; + let (right_start, right_end) = proper_endpoints(right)?; + Ok(classify_endpoints( + left_start, + left_end, + right_start, + right_end, + )) +} + +fn proper_endpoints( + interval: &TemporalInterval, +) -> Result<(i128, i128), TemporalError> { + if interval.certainty() != TemporalCertainty::Bounded { + return Err(TemporalError::RelationRequiresProperBoundedInterval); + } + let Some(start) = boundary_nanosecond(interval.lower()) else { + return Err(TemporalError::RelationRequiresProperBoundedInterval); + }; + let Some(end) = boundary_nanosecond(interval.upper()) else { + return Err(TemporalError::RelationRequiresProperBoundedInterval); + }; + Ok((start, end)) +} + +fn boundary_nanosecond(boundary: TemporalBoundary) -> Option { + match boundary { + TemporalBoundary::Unbounded => None, + TemporalBoundary::Included(value) | TemporalBoundary::Excluded(value) => { + Some(value.instant().as_nanosecond()) + } + } +} + +fn classify_endpoints( + left_start: i128, + left_end: i128, + right_start: i128, + right_end: i128, +) -> AllenRelation { + if left_end < right_start { + AllenRelation::Before + } else if left_start > right_end { + AllenRelation::After + } else if left_end == right_start { + AllenRelation::Meets + } else if left_start == right_end { + AllenRelation::MetBy + } else if left_start == right_start { + match left_end.cmp(&right_end) { + Ordering::Less => AllenRelation::Starts, + Ordering::Greater => AllenRelation::StartedBy, + Ordering::Equal => AllenRelation::Equals, + } + } else if left_end == right_end { + if left_start > right_start { + AllenRelation::Finishes + } else { + AllenRelation::FinishedBy + } + } else if left_start < right_start { + if left_end < right_end { + AllenRelation::Overlaps + } else { + AllenRelation::Contains + } + } else if left_end < right_end { + AllenRelation::During + } else { + AllenRelation::OverlappedBy + } +} + +fn composition_table() +-> &'static [[RelationSet; ELEMENTARY_RELATION_COUNT]; ELEMENTARY_RELATION_COUNT] { + static TABLE: OnceLock<[[RelationSet; ELEMENTARY_RELATION_COUNT]; ELEMENTARY_RELATION_COUNT]> = + OnceLock::new(); + TABLE.get_or_init(build_composition_table) +} + +fn build_composition_table() -> [[RelationSet; ELEMENTARY_RELATION_COUNT]; ELEMENTARY_RELATION_COUNT] +{ + let mut table = [[RelationSet::empty(); ELEMENTARY_RELATION_COUNT]; ELEMENTARY_RELATION_COUNT]; + + for left_start in 0_i128..6 { + for left_end in (left_start + 1)..6 { + for middle_start in 0_i128..6 { + for middle_end in (middle_start + 1)..6 { + let left_relation = + classify_endpoints(left_start, left_end, middle_start, middle_end); + for right_start in 0_i128..6 { + for right_end in (right_start + 1)..6 { + let right_relation = classify_endpoints( + middle_start, + middle_end, + right_start, + right_end, + ); + let composed_relation = + classify_endpoints(left_start, left_end, right_start, right_end); + let current = table[left_relation.index()][right_relation.index()]; + table[left_relation.index()][right_relation.index()] = + current.with(composed_relation); + } + } + } + } + } + } + + table +} diff --git a/crates/temporal_core/tests/error_contract.rs b/crates/temporal_core/tests/error_contract.rs index a3ecf2d7b..25b3d316b 100644 --- a/crates/temporal_core/tests/error_contract.rs +++ b/crates/temporal_core/tests/error_contract.rs @@ -22,6 +22,10 @@ fn every_temporal_error_has_a_stable_content_redacting_message() { TemporalError::InvalidIntervalCertainty, "invalid temporal interval certainty", ), + ( + TemporalError::RelationRequiresProperBoundedInterval, + "temporal relation requires proper bounded intervals", + ), ( TemporalError::InvalidWirePayload, "invalid temporal wire payload", diff --git a/crates/temporal_core/tests/reasoner_contract.rs b/crates/temporal_core/tests/reasoner_contract.rs new file mode 100644 index 000000000..73b273da7 --- /dev/null +++ b/crates/temporal_core/tests/reasoner_contract.rs @@ -0,0 +1,275 @@ +//! Bounded temporal-reasoner closure and provenance contracts. + +use temporal_core::{ + AllenRelation, ReasonerLimitKind, RelationSet, TemporalReasoner, TemporalReasonerError, + TemporalReasonerLimits, +}; + +fn limits( + maximum_variables: usize, + maximum_constraints: usize, + maximum_propagation_steps: usize, +) -> TemporalReasonerLimits { + TemporalReasonerLimits::new( + maximum_variables, + maximum_constraints, + maximum_propagation_steps, + ) + .expect("test limits must validate") +} + +#[test] +fn closure_derives_inverse_relations_with_conservative_provenance() { + let mut reasoner = TemporalReasoner::with_limits(limits(8, 16, 1_000)); + let first = reasoner.add_variable().expect("variable must fit"); + let second = reasoner.add_variable().expect("variable must fit"); + let third = reasoner.add_variable().expect("variable must fit"); + + let first_constraint = reasoner + .assert_relation(first, second, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate"); + let second_constraint = reasoner + .assert_relation(second, third, RelationSet::singleton(AllenRelation::Meets)) + .expect("constraint must validate"); + + let report = reasoner.close().expect("network must be consistent"); + assert!(report.changed()); + assert!(report.revisions() > 0); + assert!(report.propagation_steps() >= report.revisions()); + + let observed = reasoner + .relation(first, second) + .expect("observed relation must exist"); + assert_eq!( + observed.relations(), + RelationSet::singleton(AllenRelation::Before) + ); + assert!(observed.is_observed()); + assert_eq!(observed.support(), &[first_constraint]); + + let derived = reasoner + .relation(first, third) + .expect("derived relation must exist"); + assert_eq!( + derived.relations(), + RelationSet::singleton(AllenRelation::Before) + ); + assert!(!derived.is_observed()); + assert!(derived.support().contains(&first_constraint)); + assert!(derived.support().contains(&second_constraint)); + + let inverse = reasoner + .relation(third, first) + .expect("inverse relation must exist"); + assert_eq!( + inverse.relations(), + RelationSet::singleton(AllenRelation::After) + ); + assert_eq!(inverse.support(), derived.support()); + + let second_report = reasoner.close().expect("closed network must remain valid"); + assert!(!second_report.changed()); + assert_eq!(second_report.revisions(), 0); +} + +#[test] +fn contradictory_cycles_return_the_supporting_assertions() { + let mut reasoner = TemporalReasoner::with_limits(limits(8, 16, 1_000)); + let first = reasoner.add_variable().expect("variable must fit"); + let second = reasoner.add_variable().expect("variable must fit"); + let third = reasoner.add_variable().expect("variable must fit"); + + let first_constraint = reasoner + .assert_relation(first, second, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate"); + let second_constraint = reasoner + .assert_relation(second, third, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate"); + let third_constraint = reasoner + .assert_relation(third, first, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate before closure"); + + let TemporalReasonerError::Contradiction(contradiction) = + reasoner.close().expect_err("cycle must contradict before") + else { + panic!("expected contradiction evidence"); + }; + + assert!(contradiction.support().contains(&first_constraint)); + assert!(contradiction.support().contains(&second_constraint)); + assert!(contradiction.support().contains(&third_constraint)); + assert_eq!(contradiction.attempted_relations(), None); + assert_ne!(contradiction.left(), contradiction.right()); + assert_eq!( + contradiction.to_string(), + "temporal relation network is contradictory" + ); +} + +#[test] +fn direct_contradiction_is_atomic_and_does_not_fabricate_an_accepted_identifier() { + let mut reasoner = TemporalReasoner::with_limits(limits(2, 3, 100)); + let left = reasoner.add_variable().expect("left variable must fit"); + let right = reasoner.add_variable().expect("right variable must fit"); + let before = RelationSet::singleton(AllenRelation::Before); + let after = RelationSet::singleton(AllenRelation::After); + + let first_constraint = reasoner + .assert_relation(left, right, before) + .expect("first assertion must validate"); + let TemporalReasonerError::Contradiction(contradiction) = reasoner + .assert_relation(left, right, after) + .expect_err("incompatible direct assertion must fail") + else { + panic!("expected direct contradiction evidence"); + }; + + assert_eq!(contradiction.left(), left); + assert_eq!(contradiction.right(), right); + assert_eq!(contradiction.support(), &[first_constraint]); + assert_eq!(contradiction.attempted_relations(), Some(after)); + + let unchanged = reasoner + .relation(left, right) + .expect("rejected assertion must leave relation intact"); + assert_eq!(unchanged.relations(), before); + assert_eq!(unchanged.support(), &[first_constraint]); + + let second_constraint = reasoner + .assert_relation(left, right, before) + .expect("a later compatible assertion must remain admissible"); + assert_ne!(first_constraint, second_constraint); + let repeated = reasoner + .relation(left, right) + .expect("accepted repeated assertion must be observable"); + assert_eq!(repeated.support(), &[first_constraint, second_constraint]); + + let mut other = TemporalReasoner::with_limits(limits(2, 1, 100)); + let other_left = other.add_variable().expect("other left must fit"); + let other_right = other.add_variable().expect("other right must fit"); + let other_constraint = other + .assert_relation(other_left, other_right, before) + .expect("other assertion must validate"); + assert_ne!(first_constraint, other_constraint); +} + +#[test] +fn reasoner_rejects_invalid_limits_foreign_variables_empty_relations_and_capacity_overflow() { + for invalid_limits in [(0, 1, 1), (1, 0, 1), (1, 1, 0)] { + assert_eq!( + TemporalReasonerLimits::new(invalid_limits.0, invalid_limits.1, invalid_limits.2), + Err(TemporalReasonerError::InvalidLimits) + ); + } + + let mut bounded = TemporalReasoner::with_limits(limits(2, 1, 10)); + let first = bounded.add_variable().expect("first variable must fit"); + let second = bounded.add_variable().expect("second variable must fit"); + assert_eq!( + bounded.add_variable(), + Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::Variables + )) + ); + + bounded + .assert_relation(first, second, RelationSet::singleton(AllenRelation::Before)) + .expect("first constraint must fit"); + assert_eq!( + bounded.assert_relation(first, second, RelationSet::empty()), + Err(TemporalReasonerError::EmptyRelationSet) + ); + assert_eq!( + bounded.assert_relation(first, second, RelationSet::singleton(AllenRelation::Meets)), + Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::Constraints + )) + ); + + let mut other = TemporalReasoner::with_limits(limits(2, 2, 10)); + let foreign_same_index = other.add_variable().expect("foreign variable must fit"); + assert_eq!( + bounded.relation(first, foreign_same_index), + Err(TemporalReasonerError::UnknownVariable) + ); + assert_eq!( + bounded.relation(foreign_same_index, first), + Err(TemporalReasonerError::UnknownVariable) + ); + assert_eq!( + bounded.assert_relation( + first, + foreign_same_index, + RelationSet::singleton(AllenRelation::Before), + ), + Err(TemporalReasonerError::UnknownVariable) + ); +} + +#[test] +fn propagation_work_is_bounded_and_failure_restores_the_preclosure_network() { + let mut reasoner = TemporalReasoner::with_limits(limits(3, 3, 1)); + let first = reasoner.add_variable().expect("variable must fit"); + let second = reasoner.add_variable().expect("variable must fit"); + let third = reasoner.add_variable().expect("variable must fit"); + + reasoner + .assert_relation(first, second, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate"); + reasoner + .assert_relation(second, third, RelationSet::singleton(AllenRelation::Before)) + .expect("constraint must validate"); + + assert_eq!( + reasoner.close(), + Err(TemporalReasonerError::LimitExceeded( + ReasonerLimitKind::PropagationSteps + )) + ); + let restored = reasoner + .relation(first, third) + .expect("rollback must preserve an unconstrained pair"); + assert_eq!(restored.relations(), RelationSet::all()); + assert!(!restored.is_observed()); + assert!(restored.support().is_empty()); +} + +#[test] +fn reasoner_error_messages_are_stable_and_content_redacting() { + let errors = [ + ( + TemporalReasonerError::InvalidLimits, + "invalid temporal reasoner limits", + ), + ( + TemporalReasonerError::UnknownVariable, + "unknown temporal reasoner variable", + ), + ( + TemporalReasonerError::EmptyRelationSet, + "temporal relation set is empty", + ), + ( + TemporalReasonerError::LimitExceeded(ReasonerLimitKind::Variables), + "temporal reasoner resource limit exceeded", + ), + ]; + + for (error, message) in errors { + assert_eq!(error.to_string(), message); + } + + let mut reasoner = TemporalReasoner::with_limits(limits(1, 1, 10)); + let variable = reasoner.add_variable().expect("variable must fit"); + let contradiction = reasoner + .assert_relation( + variable, + variable, + RelationSet::singleton(AllenRelation::Before), + ) + .expect_err("self-before must contradict identity"); + assert_eq!( + contradiction.to_string(), + "temporal relation network is contradictory" + ); +} diff --git a/crates/temporal_core/tests/reasoner_observation_contract.rs b/crates/temporal_core/tests/reasoner_observation_contract.rs new file mode 100644 index 000000000..f71ab4457 --- /dev/null +++ b/crates/temporal_core/tests/reasoner_observation_contract.rs @@ -0,0 +1,122 @@ +//! Direct-observation provenance contracts for inverse temporal relations. + +use temporal_core::{AllenRelation, RelationSet, TemporalReasoner, TemporalReasonerLimits}; + +fn reasoner() -> TemporalReasoner { + let limits = TemporalReasonerLimits::new(8, 16, 1_000).expect("limits must validate"); + TemporalReasoner::with_limits(limits) +} + +#[test] +fn inverse_propagation_does_not_fabricate_direct_observation() { + let mut reasoner = reasoner(); + let left = reasoner.add_variable().expect("left variable must fit"); + let right = reasoner.add_variable().expect("right variable must fit"); + + reasoner + .assert_relation(left, right, RelationSet::singleton(AllenRelation::Before)) + .expect("direct assertion must validate"); + + assert!( + reasoner + .relation(left, right) + .expect("forward relation must exist") + .is_observed() + ); + assert!( + !reasoner + .relation(right, left) + .expect("inverse relation must exist") + .is_observed() + ); +} + +#[test] +fn direct_assertions_in_both_directions_remain_observed() { + let mut reasoner = reasoner(); + let left = reasoner.add_variable().expect("left variable must fit"); + let right = reasoner.add_variable().expect("right variable must fit"); + + reasoner + .assert_relation(left, right, RelationSet::singleton(AllenRelation::Before)) + .expect("forward assertion must validate"); + reasoner + .assert_relation(right, left, RelationSet::singleton(AllenRelation::After)) + .expect("reverse assertion must validate"); + + assert!( + reasoner + .relation(left, right) + .expect("forward relation must exist") + .is_observed() + ); + assert!( + reasoner + .relation(right, left) + .expect("reverse relation must exist") + .is_observed() + ); +} + +#[test] +fn closure_preserves_observation_on_the_direction_actually_asserted() { + let mut reasoner = reasoner(); + let first = reasoner.add_variable().expect("first variable must fit"); + let middle = reasoner.add_variable().expect("middle variable must fit"); + let last = reasoner.add_variable().expect("last variable must fit"); + + reasoner + .assert_relation( + last, + first, + RelationSet::from_relations(&[AllenRelation::After, AllenRelation::MetBy]), + ) + .expect("reverse-direction assertion must validate"); + reasoner + .assert_relation(first, middle, RelationSet::singleton(AllenRelation::Before)) + .expect("first path assertion must validate"); + reasoner + .assert_relation(middle, last, RelationSet::singleton(AllenRelation::Before)) + .expect("second path assertion must validate"); + + reasoner.close().expect("network must close consistently"); + + let derived_forward = reasoner + .relation(first, last) + .expect("derived forward relation must exist"); + assert_eq!( + derived_forward.relations(), + RelationSet::singleton(AllenRelation::Before) + ); + assert!(!derived_forward.is_observed()); + + let observed_reverse = reasoner + .relation(last, first) + .expect("observed reverse relation must exist"); + assert_eq!( + observed_reverse.relations(), + RelationSet::singleton(AllenRelation::After) + ); + assert!(observed_reverse.is_observed()); +} + +#[test] +fn direct_identity_assertion_remains_observed() { + let mut reasoner = reasoner(); + let variable = reasoner.add_variable().expect("variable must fit"); + + reasoner + .assert_relation( + variable, + variable, + RelationSet::singleton(AllenRelation::Equals), + ) + .expect("identity assertion must validate"); + + assert!( + reasoner + .relation(variable, variable) + .expect("identity relation must exist") + .is_observed() + ); +} diff --git a/crates/temporal_core/tests/relation_contract.rs b/crates/temporal_core/tests/relation_contract.rs new file mode 100644 index 000000000..bdf909488 --- /dev/null +++ b/crates/temporal_core/tests/relation_contract.rs @@ -0,0 +1,211 @@ +//! Allen interval-relation and composition contracts. + +use temporal_core::{ + AllenRelation, EventTime, RelationSet, TemporalBoundary, TemporalError, TemporalInterval, + TemporalPrecision, classify_interval_relation, +}; + +fn time(second: u8) -> EventTime { + EventTime::parse_rfc3339(&format!("2026-01-01T00:00:{second:02}Z")) + .expect("test instant must parse") +} + +fn proper_interval(start: u8, end: u8) -> TemporalInterval { + TemporalInterval::bounded( + TemporalBoundary::Included(time(start)), + TemporalBoundary::Included(time(end)), + TemporalPrecision::Second, + ) + .expect("proper test interval must validate") +} + +#[test] +fn every_elementary_relation_has_the_expected_inverse() { + let inverse_pairs = [ + (AllenRelation::Before, AllenRelation::After), + (AllenRelation::Meets, AllenRelation::MetBy), + (AllenRelation::Overlaps, AllenRelation::OverlappedBy), + (AllenRelation::Starts, AllenRelation::StartedBy), + (AllenRelation::During, AllenRelation::Contains), + (AllenRelation::Finishes, AllenRelation::FinishedBy), + (AllenRelation::Equals, AllenRelation::Equals), + ]; + + for (relation, inverse) in inverse_pairs { + assert_eq!(relation.inverse(), inverse); + assert_eq!(inverse.inverse(), relation); + } + assert_eq!(AllenRelation::ALL.len(), 13); +} + +#[test] +fn concrete_proper_intervals_classify_all_thirteen_relations() { + let examples = [ + ((1, 2), (3, 4), AllenRelation::Before), + ((3, 4), (1, 2), AllenRelation::After), + ((1, 2), (2, 4), AllenRelation::Meets), + ((2, 4), (1, 2), AllenRelation::MetBy), + ((1, 3), (2, 4), AllenRelation::Overlaps), + ((2, 4), (1, 3), AllenRelation::OverlappedBy), + ((1, 3), (1, 4), AllenRelation::Starts), + ((1, 4), (1, 3), AllenRelation::StartedBy), + ((2, 3), (1, 4), AllenRelation::During), + ((1, 4), (2, 3), AllenRelation::Contains), + ((2, 4), (1, 4), AllenRelation::Finishes), + ((1, 4), (2, 4), AllenRelation::FinishedBy), + ((1, 4), (1, 4), AllenRelation::Equals), + ]; + + for ((left_start, left_end), (right_start, right_end), expected) in examples { + let left = proper_interval(left_start, left_end); + let right = proper_interval(right_start, right_end); + assert_eq!( + classify_interval_relation(&left, &right).expect("relation must classify"), + expected + ); + } + + let excluded = TemporalInterval::bounded( + TemporalBoundary::Excluded(time(1)), + TemporalBoundary::Excluded(time(2)), + TemporalPrecision::Second, + ) + .expect("excluded proper interval must validate"); + assert_eq!( + classify_interval_relation(&excluded, &proper_interval(3, 4)) + .expect("boundary inclusion must not change endpoint classification"), + AllenRelation::Before + ); +} + +#[test] +fn qualitative_classification_rejects_exact_open_and_unknown_intervals() { + let exact = TemporalInterval::exact(time(1), TemporalPrecision::Second) + .expect("exact interval must validate"); + let upper_open = TemporalInterval::bounded( + TemporalBoundary::Included(time(1)), + TemporalBoundary::Unbounded, + TemporalPrecision::Second, + ) + .expect("upper-open interval must validate"); + let lower_open = TemporalInterval::bounded( + TemporalBoundary::Unbounded, + TemporalBoundary::Included(time(2)), + TemporalPrecision::Second, + ) + .expect("lower-open interval must validate"); + let unknown = TemporalInterval::::unknown(); + let proper = proper_interval(1, 2); + + for invalid in [exact, upper_open, lower_open, unknown] { + assert_eq!( + classify_interval_relation(&invalid, &proper), + Err(TemporalError::RelationRequiresProperBoundedInterval) + ); + assert_eq!( + classify_interval_relation(&proper, &invalid), + Err(TemporalError::RelationRequiresProperBoundedInterval) + ); + } +} + +#[test] +fn relation_sets_support_inverse_intersection_and_complete_composition() { + let overlaps_twice = RelationSet::singleton(AllenRelation::Overlaps) + .compose(RelationSet::singleton(AllenRelation::Overlaps)); + assert_eq!( + overlaps_twice, + RelationSet::from_relations(&[ + AllenRelation::Before, + AllenRelation::Meets, + AllenRelation::Overlaps, + ]) + ); + + assert_eq!( + RelationSet::singleton(AllenRelation::Before) + .compose(RelationSet::singleton(AllenRelation::Before)), + RelationSet::singleton(AllenRelation::Before) + ); + assert_eq!( + RelationSet::singleton(AllenRelation::Meets) + .compose(RelationSet::singleton(AllenRelation::Meets)), + RelationSet::singleton(AllenRelation::Before) + ); + assert_eq!( + RelationSet::singleton(AllenRelation::Starts) + .compose(RelationSet::singleton(AllenRelation::Finishes)), + RelationSet::singleton(AllenRelation::During) + ); + + let selected = RelationSet::from_relations(&[AllenRelation::Before, AllenRelation::Meets]); + assert_eq!( + selected.inverse(), + RelationSet::from_relations(&[AllenRelation::After, AllenRelation::MetBy]) + ); + assert_eq!( + selected.intersection(RelationSet::singleton(AllenRelation::Meets)), + RelationSet::singleton(AllenRelation::Meets) + ); + assert_eq!( + RelationSet::singleton(AllenRelation::Before) + .union(RelationSet::singleton(AllenRelation::Meets)), + selected + ); + assert!(selected.contains(AllenRelation::Before)); + assert!(!selected.contains(AllenRelation::After)); + assert_eq!(selected.len(), 2); + assert!(!selected.is_empty()); + assert!(RelationSet::empty().is_empty()); + assert_eq!(RelationSet::from_relations(&[]), RelationSet::empty()); + assert_eq!(RelationSet::all().len(), 13); +} + +#[test] +fn composition_and_inverse_obey_the_converse_law_for_every_relation_pair() { + for left in AllenRelation::ALL { + for right in AllenRelation::ALL { + let composed = RelationSet::singleton(left) + .compose(RelationSet::singleton(right)) + .inverse(); + let reversed = RelationSet::singleton(right.inverse()) + .compose(RelationSet::singleton(left.inverse())); + assert_eq!(composed, reversed); + assert!(!composed.is_empty()); + } + } +} + +#[test] +fn composition_matches_an_exhaustive_endpoint_oracle_for_every_relation_pair() { + let intervals: Vec<_> = (0_u8..8) + .flat_map(|start| ((start + 1)..8).map(move |end| proper_interval(start, end))) + .collect(); + let mut expected = [[RelationSet::empty(); 13]; 13]; + + for left_interval in &intervals { + for middle_interval in &intervals { + let left_relation = classify_interval_relation(left_interval, middle_interval) + .expect("proper intervals must classify"); + for right_interval in &intervals { + let right_relation = classify_interval_relation(middle_interval, right_interval) + .expect("proper intervals must classify"); + let composed_relation = classify_interval_relation(left_interval, right_interval) + .expect("proper intervals must classify"); + expected[left_relation as usize][right_relation as usize] = expected + [left_relation as usize][right_relation as usize] + .union(RelationSet::singleton(composed_relation)); + } + } + } + + for left_relation in AllenRelation::ALL { + for right_relation in AllenRelation::ALL { + assert_eq!( + RelationSet::singleton(left_relation) + .compose(RelationSet::singleton(right_relation)), + expected[left_relation as usize][right_relation as usize] + ); + } + } +} diff --git a/crates/temporal_core/tests/relation_iteration_contract.rs b/crates/temporal_core/tests/relation_iteration_contract.rs new file mode 100644 index 000000000..6e247b4f6 --- /dev/null +++ b/crates/temporal_core/tests/relation_iteration_contract.rs @@ -0,0 +1,24 @@ +//! Stable iteration contracts for qualitative relation sets. + +use temporal_core::{AllenRelation, RelationSet}; + +#[test] +fn relation_sets_iterate_once_in_stable_elementary_order() { + let selected = RelationSet::from_relations(&[ + AllenRelation::Meets, + AllenRelation::Before, + AllenRelation::Meets, + AllenRelation::Equals, + ]); + + assert_eq!( + selected.iter().collect::>(), + vec![ + AllenRelation::Before, + AllenRelation::Meets, + AllenRelation::Equals, + ] + ); + assert_eq!(RelationSet::empty().iter().next(), None); + assert_eq!(RelationSet::all().iter().count(), AllenRelation::ALL.len()); +} diff --git a/docs/research/task-4-interval-algebra-foundations.md b/docs/research/task-4-interval-algebra-foundations.md new file mode 100644 index 000000000..a00fc0415 --- /dev/null +++ b/docs/research/task-4-interval-algebra-foundations.md @@ -0,0 +1,171 @@ +# Task 4 Qualitative Interval Algebra Foundations + +## Purpose + +This doctoring note traces TEPP's executable qualitative interval relation and bounded closure contracts to primary temporal-reasoning literature and the current published OWL-Time vocabulary. References use APA 7th style. + +Task 4 is a storage-independent Rust domain slice. It implements Allen's thirteen elementary relations for proper bounded intervals, relation-set inverse and composition, and a resource-bounded path-consistency network with conservative provenance. It does not implement event ontology, transition-policy validation, bitemporal persistence, leakage-safe snapshots, metric temporal constraints, complete scenario search, or probabilistic uncertainty. + +## Implemented relation contract + +### Proper interval domain + +Allen's interval calculus assumes proper intervals whose start precedes their end. TEPP therefore classifies only `TemporalInterval` values that are: + +- bounded on both sides; +- nonzero in duration; +- validated by one nominal clock type; and +- represented as `TemporalCertainty::Bounded`. + +Exact instants, one-sided intervals, and explicitly unknown intervals fail closed with `RelationRequiresProperBoundedInterval`. Included versus excluded boundary metadata does not alter the endpoint ordering relation; TEPP's qualitative relation is defined over ordered endpoints rather than set-theoretic overlap at a boundary instant. + +### Thirteen elementary relations + +The executable enum contains the thirteen jointly exhaustive endpoint-order cases: + +```text +before after +meets met_by +overlaps overlapped_by +starts started_by +during contains +finishes finished_by +equals +``` + +Every relation has an exact inverse. `equals` is self-inverse. The stable enum order is also the private bit index used by `RelationSet`; callers cannot construct relation bits outside the thirteen reviewed values. + +### Composition table + +For relations \(R_{xy}\) and \(R_{yz}\), composition returns every elementary relation \(R_{xz}\) admitted by at least one compatible triple of proper intervals: + +\[ +R_{xy} \circ R_{yz} += +\{R_{xz}: \exists x,y,z\; R_{xy}(x,y) \land R_{yz}(y,z)\}. +\] + +The production table is generated once from all proper intervals over six ordered endpoint ranks. Six ranks are sufficient because three proper intervals contain at most six distinct endpoints; every equality and strict-order pattern can be order-preservingly mapped into those ranks. The result is deterministic and immutable after `OnceLock` initialization. + +The implementation is independently checked against: + +- classification examples for all thirteen elementary relations; +- known composition entries; +- the converse law + \[ + (R \circ S)^{-1}=S^{-1}\circ R^{-1}; + \] +- nonempty composition for every elementary pair; and +- a separate exhaustive oracle built from all proper intervals over eight endpoint ranks. + +The eight-rank oracle is deliberately not the production table generator. It is a larger independent enumeration used to detect truncation or table-construction errors. + +## Bounded path-consistency contract + +For every distinct variable triple \((i,k,j)\), closure applies the monotone narrowing rule + +\[ +R_{ij} +\leftarrow +R_{ij}\cap(R_{ik}\circ R_{kj}). +\] + +The reverse cell is updated with the exact inverse relation set. Iteration continues until no relation set changes, a pair becomes empty, or the configured propagation budget is exhausted. + +### What successful closure means + +A successful `close()` result establishes a path-consistent local network under the implemented relation algebra. It does **not** certify global satisfiability for unrestricted disjunctive Allen networks. General interval-algebra consequence and satisfiability problems are computationally intractable, and local consistency is not a complete decision procedure for the full algebra (Vilain & Kautz, 1986). + +Accordingly: + +- an empty narrowed relation set is sound contradiction evidence; +- a nonempty path-consistent network is not described as a proof that a concrete global interval assignment exists; +- complete scenario search and tractable-fragment detection remain separate future work; and +- user-facing APIs and documentation must preserve this claim boundary. + +### Resource and failure boundaries + +Every reasoner instance has explicit nonzero maxima for: + +- interval variables; +- accepted direct constraints; and +- propagation checks. + +Closure snapshots the relation matrix before propagation. Contradiction or budget exhaustion restores the pre-closure matrix, so a failed closure cannot expose a partially narrowed network. Constraint capacity is consumed only by accepted assertions. + +Opaque variable and constraint identifiers include a reasoner-instance UUIDv7. Identifiers from another reasoner fail closed even when their numeric indices happen to match. + +### Provenance contract + +Each ordered relation cell records: + +- the current possible relation set; +- whether at least one direct assertion was accepted for that pair; and +- a conservative ordered set of accepted assertion identifiers supporting its current narrowing. + +Derived support is the union of the current pair support and the two composing path supports. This is intentionally conservative: it preserves sufficient accepted evidence for audit and contradiction reporting but does not claim a minimal proof core. + +Direct contradictions report the rejected attempted relation set separately and do not fabricate an accepted `ConstraintId`. Propagation contradictions report the conservative accepted-assertion support that led to the empty pair. + +## OWL-Time interoperability boundary + +OWL-Time publishes interval relation vocabulary aligned with Allen-style temporal topology, including before, after, meets, met by, overlaps, overlapped by, starts, started by, during, contains, finishes, finished by, and equals. TEPP can map its reviewed relations to that outward vocabulary in a later JSON-LD or RDF adapter. + +OWL-Time does not define TEPP's in-memory bit layout, resource limits, provenance semantics, atomic rollback, or Rust API. Those are TEPP engineering decisions. The latest published OWL-Time document is a W3C Candidate Recommendation Draft, so its status must be recorded accurately rather than described as a final Recommendation. + +## Security and operational behavior + +Adversarial relation graphs can cause high propagation cost or intentionally inconsistent cycles. Task 4 therefore: + +- rejects zero resource limits; +- rejects empty direct relation sets; +- scopes identifiers to one reasoner instance; +- bounds variables, constraints, and propagation work; +- restores state after failed closure; +- returns content-redacting stable errors; +- avoids recursion in closure; and +- keeps the production relation set closed over thirteen reviewed values. + +The implementation does not deserialize arbitrary relation bit masks and does not accept user-defined relation semantics. + +## Verification mapping + +| Evidence | Representative verification | +|---|---| +| relation partition | concrete proper intervals classify all thirteen relations | +| inverse | every inverse pair round-trips exactly | +| composition | known entries, all-pair converse law, and eight-rank exhaustive oracle | +| proper-interval boundary | exact, open-ended, and unknown intervals fail closed | +| inverse propagation | accepted and derived reverse cells are exact inverses | +| path consistency | multi-edge networks narrow until stable | +| idempotence | a second closure on a stable network performs no revision | +| contradiction | impossible cycles and direct conflicts return conservative support | +| atomicity | propagation-budget failure restores the pre-closure network | +| provenance | observed and derived relations remain distinguishable | +| identity isolation | foreign variables fail closed despite matching indices | +| resource limits | variable, constraint, and propagation maxima are enforced | + +Production line and branch coverage remain merge gates, but coverage is not treated as proof of global satisfiability or completeness. + +## Deferred research boundary + +Later slices must separately doctor and implement, where required: + +- tractable Allen subalgebra recognition; +- complete backtracking scenario search; +- minimal contradiction cores; +- metric temporal constraints and continuous durations; +- event-transition edge policies; +- persistence and historical snapshots; +- uncertainty-weighted or probabilistic relation evidence; and +- performance benchmarks for large sparse networks. + +## References + +Allen, J. F. (1983). Maintaining knowledge about temporal intervals. *Communications of the ACM, 26*(11), 832–843. https://doi.org/10.1145/182.358434 + +Cox, S., & Little, C. (Eds.). (2022). *Time ontology in OWL* (W3C Candidate Recommendation Draft). World Wide Web Consortium. https://www.w3.org/TR/owl-time/ + +Dechter, R., Meiri, I., & Pearl, J. (1991). Temporal constraint networks. *Artificial Intelligence, 49*(1–3), 61–95. https://doi.org/10.1016/0004-3702(91)90006-6 + +Vilain, M. B., & Kautz, H. A. (1986). Constraint propagation algorithms for temporal reasoning. In *Proceedings of the Fifth National Conference on Artificial Intelligence* (pp. 377–382). American Association for Artificial Intelligence. https://www.aaai.org/Papers/AAAI/1986/AAAI86-063.pdf