Temporal Domains

@cite{declerck-2006} @cite{reichenbach-1947}

A temporal domain: a central time of orientation (TO) — the binding TO of the domain — together with related sub-TOs. The same shape covers @cite{reichenbach-1947}'s S/P/R/E and Declerck's binding-TO + sub-TOs; a Domain is what they share.

Concepts

• TO (Time of orientation): a temporal anchor. Realized as Interval Time; degenerate intervals (start = finish) model point times like Reichenbach's S/P/R/E, while non-degenerate intervals model extended times-of-situation (Declerck's T-sit).
• NamedTO: a TO together with a typed Role label. The Role is abstract (any DecidableEq type), so role-based access stays type-safe across frameworks: Orientation (the canonical universal vocabulary) instantiates Role for both Reichenbach and Declerck, but a domain-specific framework could use its own enum.
• Domain: a central NamedTO + list of sub-NamedTOs. Pairwise Allen relations are computed from the underlying linear order on Time via Interval.allenRel; the domain does not store a relation table.

What's not here

This file is foundational: it does not add tense semantics, aspect, or sector classification. Domain is the substrate; the domain-shaped theories build on top.

@[reducible, inline]

abbrev Core.Time.TO (Time : Type u_1) [LinearOrder Time] : Type u_1

A time of orientation (TO, @cite{declerck-2006}): a temporal anchor used by tense/aspect frameworks. Realized as Interval Time so the same type covers both point times (degenerate intervals via Interval.point) and extended times-of-situation (general intervals).

Allen relations between TOs are unique on non-degenerate pairs (AllenRelation.holds_unique), so Domain APIs that depend on uniqueness add a non-degeneracy hypothesis where needed. For point-time TOs (Reichenbach), the Allen algebra collapses to {precedes, equal, precededBy}.

Equations

• Core.Time.TO Time = Core.Time.Interval Time

@[reducible, inline]

abbrev Core.Time.TO.point {Time : Type u_1} [LinearOrder Time] (t : Time) : TO Time

Construct a point TO from a single time (degenerate interval).

Equations

• Core.Time.TO.point t = Core.Time.Interval.point t

structure Core.Time.NamedTO (Time : Type u_1) (Role : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A TO with an identifying typed role label. The Role parameter is abstract: framework-specific role types (Orientation for Reichenbach/Declerck; framework-private enums elsewhere) all instantiate it. Using a typed role rather than a String makes role mismatches a compile-time error.

• name : Role

  The role label (e.g. Orientation.perspective, .topic).

• span : TO Time

  The TO itself.

@[reducible, inline]

abbrev Core.Time.NamedTO.start {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (n : NamedTO Time Role) : Time

The starting time of a NamedTO.

Equations

• n.start = n.span.start

@[reducible, inline]

abbrev Core.Time.NamedTO.finish {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (n : NamedTO Time Role) : Time

The ending time of a NamedTO.

Equations

• n.finish = n.span.finish

def Core.Time.NamedTO.ofPoint {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (name : Role) (t : Time) : NamedTO Time Role

Build a point NamedTO from a label and a single time.

Equations

• Core.Time.NamedTO.ofPoint name t = { name := name, span := Core.Time.TO.point t }

structure Core.Time.Domain (Time : Type u_1) (Role : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A temporal domain (@cite{declerck-2006}): a central time of orientation (the binding TO of the domain) together with a list of related sub-TOs. The Allen relations between any pair of TOs are computed on-demand from the underlying linear order on Time via Interval.allenRel; no relation table is stored.

Two design choices worth noting:

1. No relation storage. TOs are intervals on a LinearOrder, so their Allen relation is determined by the order. Storing relations would either be redundant (when consistent with the order) or contradictory (when inconsistent). We compute on demand.

2. NamedTO list, not record. Different domain-shaped theories use different role-sets: Reichenbach has 4 roles (S/P/R/E), Declerck has a variable count (T₀ + sectors + sub-TOs). A label-keyed list lets Domain cover both without tying the structure to one role-set; downstream wrappers (ReichenbachFrame, DeclercianSchema) commit to a fixed role-set on top.

ReichenbachFrame is recast as a Domain with central = S (point) and sub-TOs = [P, R, E] (each a point); DeclercianSchema is recast as a Domain plus a Zone-classifier function.

• central : NamedTO Time Role

  The central TO — the binding TO of the domain. For matrix clauses this is typically speech time (S); under attitude embedding it shifts to the matrix event time.

• subTOs : List (NamedTO Time Role)

  The other TOs in the domain (reference times, event times, sub-TOs, secondary anchors, …).

def Core.Time.Domain.all {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (d : Domain Time Role) : List (NamedTO Time Role)

All TOs in the domain (central first, then sub-TOs).

Equations

• d.all = d.central :: d.subTOs

@[simp]

theorem Core.Time.Domain.all_central {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (d : Domain Time Role) : d.central ∈ d.all

@[simp]

theorem Core.Time.Domain.all_sub {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (d : Domain Time Role) (t : NamedTO Time Role) (h : t ∈ d.subTOs) : t ∈ d.all

def Core.Time.Domain.find? {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] [DecidableEq Role] (d : Domain Time Role) (r : Role) : Option (TO Time)

Look up a TO by its role label. Returns none if no TO has that role; some of the first matching TO otherwise. (Roles are not required to be unique at the type level — a wrapper like ReichenbachFrame can prove uniqueness as a separate invariant.)

Equations

• d.find? r = Option.map (fun (x : Core.Time.NamedTO Time Role) => x.span) (List.find? (fun (x : Core.Time.NamedTO Time Role) => x.name == r) d.all)

def Core.Time.Domain.labels {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] (d : Domain Time Role) : List Role

The role label of every TO in the domain — useful for stating role-set invariants.

Equations

• d.labels = List.map (fun (x : Core.Time.NamedTO Time Role) => x.name) d.all

def Core.Time.Domain.relatedBy {Time : Type u_1} [LinearOrder Time] (S : List AllenRelation) (i j : TO Time) : Prop

"TO i is related to TO j by some atom in the named set S." Lifts AllenRelation.holdsIn to the domain level.

Equations

• Core.Time.Domain.relatedBy S i j = Core.Time.AllenRelation.holdsIn S i j

def Core.Time.Domain.relatedByName {Time : Type u_1} {Role : Type u_2} [LinearOrder Time] [DecidableEq Role] (d : Domain Time Role) (S : List AllenRelation) (rI rJ : Role) : Prop

Lookup-and-relate: do the two role-labelled TOs both exist in the domain and stand in some atom of S? Used to phrase tense predicates like "topic precedes perspective" against a domain by role.

Equations

• d.relatedByName S rI rJ = ∃ (i : Core.Time.TO Time) (j : Core.Time.TO Time), d.find? rI = some i ∧ d.find? rJ = some j ∧ Core.Time.Domain.relatedBy S i j

Convenience constructors for the canonical Reichenbach role-set, using Orientation as the universal Role type: utterance = S, perspective = P, topic = R, situation = E.

def Core.Time.Domain.reichenbachLabels : List Orientation

The four canonical Reichenbach role labels (extended with @cite{kiparsky-2002}'s perspective time P) as Orientation values: utterance (S), perspective (P), topic (R), situation (E).

Equations

• Core.Time.Domain.reichenbachLabels = [Core.Time.Orientation.utterance, Core.Time.Orientation.perspective, Core.Time.Orientation.topic, Core.Time.Orientation.situation]

def Core.Time.Domain.ofReichenbachPoints {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : Domain Time Orientation

Build a domain from four point times in the Reichenbach convention. S/P/R/E map to .utterance/.perspective/.topic/.situation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Core.Time.Domain.ofReichenbachPoints_labels {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : (ofReichenbachPoints S P R E).labels = reichenbachLabels

@[simp]

theorem Core.Time.Domain.ofReichenbachPoints_findUtterance {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : (ofReichenbachPoints S P R E).find? Orientation.utterance = some (TO.point S)

@[simp]

theorem Core.Time.Domain.ofReichenbachPoints_findPerspective {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : (ofReichenbachPoints S P R E).find? Orientation.perspective = some (TO.point P)

@[simp]

theorem Core.Time.Domain.ofReichenbachPoints_findTopic {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : (ofReichenbachPoints S P R E).find? Orientation.topic = some (TO.point R)

@[simp]

theorem Core.Time.Domain.ofReichenbachPoints_findSituation {Time : Type u_1} [LinearOrder Time] (S P R E : Time) : (ofReichenbachPoints S P R E).find? Orientation.situation = some (TO.point E)