Tense and Aspect Systems

[Dec91b] [Rei47]

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 Tense.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.

Tense System

class 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 Tense.Domain
• anchor: the role of the anchor TO (the TO that tense locates the situation against). For [Rei47] (extended with Kiparsky's P) this is .perspective; for [Dec91b] 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 : α → Tense.Domain Time Role

  Lift the schema into a temporal domain.

• anchor : Role

  The role of the anchor TO.

• located : Role

  The role of the located TO — the TO that tense locates relative to the anchor. For Reichenbach this is .topic (R); for Declerck it is .situation (TO_sit). Named located rather than situation because it does not generally denote the situation time E (Orientation.situation): for Reichenbach it is R, not E.

• anchor_mem (a : α) : anchor α ∈ (toDomain a).labels

  Law: the anchor role is present in every lifted domain. (No analogous law for located: Declercian schemas with an empty TO-chain lift to domains whose labels are just [utterance, perspective], so the located role can be absent — a real asymmetry between the two instances, visible here.)

Aspect System

class 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 Tense.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 : α → Tense.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.

Generic tense and aspect predicates

Defined once over the classes via Domain.relatedByName with Allen atom-sets, so any tense framework that instantiates TenseSystem / AspectSystem gets them for free — and rival frameworks can agree or disagree about a single predicate instead of each defining its own. Because Domain is interval-native, these are interval-correct; point-based schemas (Reichenbach) satisfy them in the degenerate point-collapse of the Allen algebra (see the ReichenbachFrame specialization lemmas), and isImperfective is unsatisfiable there (ReichenbachFrame.not_aspectSystem_isImperfective).

def TenseSystem.isPast {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [TenseSystem α Time Role] (a : α) : Prop

Generic PAST: the located TO precedes the anchor TO.

Equations

• TenseSystem.isPast a = (TenseSystem.toDomain a).relatedByName AllenRelation.precedesSet (TenseSystem.located α) (TenseSystem.anchor α)

def TenseSystem.isPresent {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [TenseSystem α Time Role] (a : α) : Prop

Generic PRESENT: the located TO equals the anchor TO. (Point approximation of present-as-overlap; an interval instance wanting overlap semantics should use AllenRelation.overlapSet directly.)

Equations

• TenseSystem.isPresent a = (TenseSystem.toDomain a).relatedByName AllenRelation.equalSet (TenseSystem.located α) (TenseSystem.anchor α)

def TenseSystem.isFuture {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [TenseSystem α Time Role] (a : α) : Prop

Generic FUTURE: the anchor TO precedes the located TO.

Equations

• TenseSystem.isFuture a = (TenseSystem.toDomain a).relatedByName AllenRelation.precedesSet (TenseSystem.anchor α) (TenseSystem.located α)

def AspectSystem.isPerfect {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [AspectSystem α Time Role] (a : α) : Prop

Generic PERFECT: the event TO precedes the reference TO.

Equations

• AspectSystem.isPerfect a = (AspectSystem.toDomain a).relatedByName AllenRelation.precedesSet (AspectSystem.event α) (AspectSystem.reference α)

def AspectSystem.isPerfective {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [AspectSystem α Time Role] (a : α) : Prop

Generic PERFECTIVE: the event TO equals the reference TO (point approximation of E ⊆ R).

Equations

• AspectSystem.isPerfective a = (AspectSystem.toDomain a).relatedByName AllenRelation.equalSet (AspectSystem.event α) (AspectSystem.reference α)

def AspectSystem.isProspective {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [AspectSystem α Time Role] (a : α) : Prop

Generic PROSPECTIVE: the reference TO precedes the event TO.

Equations

• AspectSystem.isProspective a = (AspectSystem.toDomain a).relatedByName AllenRelation.precedesSet (AspectSystem.reference α) (AspectSystem.event α)

def AspectSystem.isImperfective {α : Type u} {Time : Type v} {Role : Type w} [LinearOrder Time] [DecidableEq Role] [AspectSystem α Time Role] (a : α) : Prop

Generic IMPERFECTIVE ([Kle94]): the reference TO (topic time) is properly contained in the event TO (situation time) — TT ⊂ TSit. Genuinely interval-level: unsatisfiable when both TOs are points (TO.not_pure_properContainment), which is the formal statement of why point-based frames cannot represent the imperfective.

Equations

• AspectSystem.isImperfective a = (AspectSystem.toDomain a).relatedByName AllenRelation.properContainmentSet (AspectSystem.reference α) (AspectSystem.event α)