Tense and Aspect Systems

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

Type classes that abstract over specific tense and aspect frameworks. TenseSystem α Time Role says "the type α is a way of describing tense over a Time line, using Role as its TO vocabulary"; it commits to (i) how to lift α into a Core.Time.Domain and (ii) which two roles its tense operators target (the anchor and situation TOs). AspectSystem α Time Role is the analogous abstraction for the event/reference relation.

These typeclasses do not derive generic isPast/isPerfect/etc. predicates — those live concretely on each schema (e.g. ReichenbachFrame.isPast), where the relevant per-paper bridge theorems (isPast_iff_relatedByName) connect them to the Allen algebra via Domain.relatedByName. The typeclass exists to give schema-generic toDomain dispatch and to commit each framework to a consistent role vocabulary; predicate-level abstraction is left to the concrete schemas.

The class is parameterized in the mathlib style — the carrier type is the main parameter; Time and Role are outParams, so writing f : ReichenbachFrame ℤ lets the elaborator find Time = ℤ and Role = Orientation automatically. Instances are unique per (carrier, Time, Role) triple: there is only one canonical TenseSystem interpretation per schema type.

class Core.Time.TenseSystem (α : Type u) (Time : outParam (Type v)) (Role : outParam (Type w)) [LinearOrder Time] [DecidableEq Role] : Type (max (max u v) w)

A tense system: a framework for locating situations in time relative to a discourse anchor.

Each instance commits to:

• toDomain: how to lift the schema into a Core.Time.Domain
• anchor: the role of the anchor TO (the TO that tense locates the situation against). For @cite{reichenbach-1947} (extended with Kiparsky's P) this is .perspective; for @cite{declerck-1991} the binding-TO TO₁ also plays this role and is again .perspective.
• situation: the role of the situation TO. For Reichenbach this is .topic (= R); for Declerck the situation time TS coincides with .situation under the universal TS = TO_sit principle.

Time and Role are outParams: the carrier type α (e.g., ReichenbachFrame ℤ) determines the time line and the role vocabulary, so callers don't pass them explicitly.

• toDomain : α → Domain Time Role

  Lift the schema into a temporal domain.

• anchor : Role

  The role of the anchor TO.

• situation : Role

  The role of the situation TO.

class Core.Time.AspectSystem (α : Type u) (Time : outParam (Type v)) (Role : outParam (Type w)) [LinearOrder Time] [DecidableEq Role] : Type (max (max u v) w)

An aspect system: a framework for relating event time to reference (situation) time.

Each instance commits to:

• toDomain: how to lift the schema into a Core.Time.Domain
• event: the role of the event TO (Reichenbach: .situation (E); Declerck: .situation (TS))
• reference: the role of the reference TO (Reichenbach: .topic (R); Declerck: .situation (TS) — Declerck collapses E and R both to the situation TO under the universal TS = TO_sit principle, so isPerfective always holds for Declercian schemas — the perfect lives in the chain structure, not the E/R relation.)

• toDomain : α → Domain Time Role

  Lift the schema into a temporal domain.

• event : Role

  The role of the event TO.

• reference : Role

  The role of the reference TO.