Reichenbach's Temporal Framework

[Kip02] [Kle94] [Rei47]

[Rei47] / [Kle94] tense–aspect parameters, extended with [Kip02]'s perspective time P.

Three (four) distinguished times:

• S (Speech time): When the utterance occurs
• P (Perspective time): Origin of temporal deixis
• R (Reference/Topic time): The time being talked about
• E (Event time): When the event occurs

Tense relates R to P; Aspect relates E to R.

Domain bridge

ReichenbachFrame is the four-slot point-time record used throughout linglib's tense modules. The toDomain builder lifts it to a generic Tense.Domain (central = S, sub-TOs = [P, R, E], all as point intervals via TO.pure). The *_iff_relatedByName bridge theorems re-express each predicate (isPast, isPerfect, …) as a Domain.relatedByName query against named atom-sets from the Allen algebra. This grounds the Reichenbach predicates in the Allen projection function (NonemptyInterval.allenRel) without changing the existing four-field record — downstream call sites continue to use f.referenceTime, f.isPast, etc., while domain-level tooling can work with f.toDomain and relatedByName.

structure Time.ReichenbachFrame (T : Type u_1) : Type u_1

Reichenbach's temporal parameters for tense/aspect analysis, extended with [Kip02]'s perspective time P.

• speechTime: When the utterance is made (S)
• perspectiveTime: Origin of temporal deixis (P, [Kip02])
• referenceTime: The time being talked about (R, Klein's "topic time")
• eventTime: When the described event occurs (E)

P = S in root clauses but diverges for flashbacks, free indirect discourse, and embedded tenses. Tense locates R relative to P (not S).

• speechTime : T

  Speech time (S): when the utterance occurs

• perspectiveTime : T

  Perspective time (P): origin of temporal deixis. Equals S in root clauses; shifts in flashback, FID, embedded tenses.

• referenceTime : T

  Reference time (R): the time under discussion

• eventTime : T

  Event time (E): when the described event occurs (E)

def Time.ReichenbachFrame.isPast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

PAST: R < P (reference time precedes perspective time) — a view of Core.Order.holds Tense.past. [Kip02]: tense locates R relative to P, not S.

Equations

• f.isPast = Core.Order.holds Tense.past f.referenceTime f.perspectiveTime

def Time.ReichenbachFrame.isPresent {T : Type u_1} (f : ReichenbachFrame T) : Prop

PRESENT: R = P (reference time equals perspective time). Present is the one tense that needs no ordering, so it stays the bare equality (frame predicates over unordered time keep typechecking); it is definitionally Core.Order.holds Tense.present.

Equations

• f.isPresent = (f.referenceTime = f.perspectiveTime)

def Time.ReichenbachFrame.isFuture {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

FUTURE: P < R (perspective time precedes reference time).

Equations

• f.isFuture = Core.Order.holds Tense.future f.referenceTime f.perspectiveTime

def Time.ReichenbachFrame.isNonpast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

NONPAST: P ≤ R (present or future) ([Kle16]) — the view of Core.Order.holds Tense.nonpast. Completes the four-way relation on frames.

Equations

• f.isNonpast = Core.Order.holds Tense.nonpast f.referenceTime f.perspectiveTime

def Time.ReichenbachFrame.isSimpleCase {T : Type u_1} (f : ReichenbachFrame T) : Prop

Simple case: P = S (root clause, no perspective shift).

Equations

• f.isSimpleCase = (f.perspectiveTime = f.speechTime)

def Time.ReichenbachFrame.defaultPR {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

Kiparsky's unmarked P–R default: P ≤ R.

Equations

• f.defaultPR = (f.perspectiveTime ≤ f.referenceTime)

def Time.ReichenbachFrame.defaultER {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

Kiparsky's unmarked E–R default: E ≤ R.

Equations

• f.defaultER = (f.eventTime ≤ f.referenceTime)

def Time.ReichenbachFrame.isPerfective {T : Type u_1} (f : ReichenbachFrame T) : Prop

Perfective: E ⊆ R (event contained in reference). Simplified to E = R for point-based times. TODO: proper interval-based perfective/imperfective distinction lives in Semantics/Aspect/Basic.lean (ViewpointAspectB).

Equations

• f.isPerfective = (f.eventTime = f.referenceTime)

def Time.ReichenbachFrame.isPerfect {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

Perfect: E < R (event precedes reference)

Equations

• f.isPerfect = (f.eventTime < f.referenceTime)

def Time.ReichenbachFrame.isProspective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

Prospective: R < E (reference precedes event)

Equations

• f.isProspective = (f.referenceTime < f.eventTime)

Unfolding lemmas and decidability

One _def simp lemma and one Decidable instance per predicate, so consumers can close concrete goals with decide and rewrite with simp only [isPast_def] instead of unfolding definitions by hand.

@[simp]

theorem Time.ReichenbachFrame.isPast_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPast ↔ f.referenceTime < f.perspectiveTime

@[simp]

theorem Time.ReichenbachFrame.isPresent_def {T : Type u_1} (f : ReichenbachFrame T) : f.isPresent ↔ f.referenceTime = f.perspectiveTime

@[simp]

theorem Time.ReichenbachFrame.isFuture_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isFuture ↔ f.perspectiveTime < f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isNonpast_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isNonpast ↔ f.perspectiveTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isSimpleCase_def {T : Type u_1} (f : ReichenbachFrame T) : f.isSimpleCase ↔ f.perspectiveTime = f.speechTime

@[simp]

theorem Time.ReichenbachFrame.defaultPR_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.defaultPR ↔ f.perspectiveTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.defaultER_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.defaultER ↔ f.eventTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isPerfective_def {T : Type u_1} (f : ReichenbachFrame T) : f.isPerfective ↔ f.eventTime = f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isPerfect_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPerfect ↔ f.eventTime < f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isProspective_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isProspective ↔ f.referenceTime < f.eventTime

theorem Time.ReichenbachFrame.isPast_simpleCase {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) (h : f.isSimpleCase) : f.isPast ↔ f.referenceTime < f.speechTime

In the simple case (P = S), isPast reduces to R < S.

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsPast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPast

Equations

• f.instDecidableIsPast = id inferInstance

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsPresent {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPresent

Equations

• f.instDecidableIsPresent = Time.ReichenbachFrame.instDecidableIsPresent._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsFuture {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isFuture

Equations

• f.instDecidableIsFuture = id inferInstance

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsNonpast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isNonpast

Equations

• f.instDecidableIsNonpast = id inferInstance

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsSimpleCase {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isSimpleCase

Equations

• f.instDecidableIsSimpleCase = Time.ReichenbachFrame.instDecidableIsSimpleCase._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableDefaultPR {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.defaultPR

Equations

• f.instDecidableDefaultPR = Time.ReichenbachFrame.instDecidableDefaultPR._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableDefaultER {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.defaultER

Equations

• f.instDecidableDefaultER = Time.ReichenbachFrame.instDecidableDefaultER._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsPerfective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPerfective

Equations

• f.instDecidableIsPerfective = Time.ReichenbachFrame.instDecidableIsPerfective._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsPerfect {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPerfect

Equations

• f.instDecidableIsPerfect = Time.ReichenbachFrame.instDecidableIsPerfect._aux_1 f

@[implicit_reducible]

instance Time.ReichenbachFrame.instDecidableIsProspective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isProspective

Equations

• f.instDecidableIsProspective = Time.ReichenbachFrame.instDecidableIsProspective._aux_1 f

Domain Bridge

def Time.ReichenbachFrame.toDomain {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Tense.Domain T Tense.Orientation

The Reichenbach frame as a generic temporal Domain over the universal Orientation role vocabulary: central = utterance (S), sub-TOs = [perspective (P), topic (R), situation (E)], every TO a point interval (degenerate via TO.pure). This is the canonical bridge from the four-field record to the framework-agnostic Domain substrate.

Proved equal to Domain.ofReichenbachPoints (toDomain_eq); the four find? simp lemmas inherited from Domain then resolve all role lookups by rfl.

Equations

• f.toDomain = Tense.Domain.ofReichenbachPoints f.speechTime f.perspectiveTime f.referenceTime f.eventTime

@[simp]

theorem Time.ReichenbachFrame.toDomain_eq {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain = Tense.Domain.ofReichenbachPoints f.speechTime f.perspectiveTime f.referenceTime f.eventTime

@[simp]

theorem Time.ReichenbachFrame.toDomain_labels {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain.labels = Tense.Domain.reichenbachLabels

@[simp]

theorem Time.ReichenbachFrame.toDomain_findUtterance {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain.find? Tense.Orientation.utterance = some (Tense.TO.pure f.speechTime)

@[simp]

theorem Time.ReichenbachFrame.toDomain_findPerspective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain.find? Tense.Orientation.perspective = some (Tense.TO.pure f.perspectiveTime)

@[simp]

theorem Time.ReichenbachFrame.toDomain_findTopic {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain.find? Tense.Orientation.topic = some (Tense.TO.pure f.referenceTime)

@[simp]

theorem Time.ReichenbachFrame.toDomain_findSituation {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.toDomain.find? Tense.Orientation.situation = some (Tense.TO.pure f.eventTime)

theorem Time.ReichenbachFrame.isPast_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPast ↔ f.toDomain.relatedByName AllenRelation.precedesSet Tense.Orientation.topic Tense.Orientation.perspective

isPast is exactly topic precedes perspective in the Allen algebra against the domain — the Reichenbach predicate grounded by construction in the Allen projection function on point intervals.

theorem Time.ReichenbachFrame.isFuture_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isFuture ↔ f.toDomain.relatedByName AllenRelation.precedesSet Tense.Orientation.perspective Tense.Orientation.topic

isFuture is exactly perspective precedes topic in the Allen algebra against the domain.

theorem Time.ReichenbachFrame.isPresent_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPresent ↔ f.toDomain.relatedByName AllenRelation.equalSet Tense.Orientation.topic Tense.Orientation.perspective

isPresent is exactly topic equal perspective in the Allen algebra against the domain.

theorem Time.ReichenbachFrame.isPerfect_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPerfect ↔ f.toDomain.relatedByName AllenRelation.precedesSet Tense.Orientation.situation Tense.Orientation.topic

isPerfect is exactly situation precedes topic in the Allen algebra against the domain.

theorem Time.ReichenbachFrame.isProspective_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isProspective ↔ f.toDomain.relatedByName AllenRelation.precedesSet Tense.Orientation.topic Tense.Orientation.situation

isProspective is exactly topic precedes situation in the Allen algebra against the domain.

theorem Time.ReichenbachFrame.isPerfective_iff_relatedByName {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPerfective ↔ f.toDomain.relatedByName AllenRelation.equalSet Tense.Orientation.situation Tense.Orientation.topic

isPerfective is exactly situation equal topic in the Allen algebra against the domain. (For the point-time approximation; the proper interval-based perfective/imperfective distinction lives in Semantics/Lexical/Verb/ViewpointAspect.lean.)

TenseSystem and AspectSystem Instances

Reichenbach as a TenseSystem (anchor = P, situation = R) and AspectSystem (event = E, reference = R) instance. The instances commit Reichenbach to the Orientation role vocabulary so generic Domain-level tooling (e.g. relatedByName-driven analyses) can dispatch over any tense or aspect framework. The concrete isPast/isPerfect/etc. predicates remain on ReichenbachFrame; the Allen bridges above (*_iff_relatedByName) show how they project into the algebra.

@[implicit_reducible]

instance Time.reichenbachFrame_tenseSystem {T : Type u_1} [LinearOrder T] : TenseSystem (ReichenbachFrame T) T Tense.Orientation

Equations

• Time.reichenbachFrame_tenseSystem = { toDomain := Time.ReichenbachFrame.toDomain, anchor := Tense.Orientation.perspective, located := Tense.Orientation.topic, anchor_mem := ⋯ }

@[implicit_reducible]

instance Time.reichenbachFrame_aspectSystem {T : Type u_1} [LinearOrder T] : AspectSystem (ReichenbachFrame T) T Tense.Orientation

Equations

• Time.reichenbachFrame_aspectSystem = { toDomain := Time.ReichenbachFrame.toDomain, event := Tense.Orientation.situation, reference := Tense.Orientation.topic }

Generic-predicate specializations

The generic TenseSystem/AspectSystem predicates agree with the concrete ReichenbachFrame predicates — the frame is the point-time specialization of the interval-native generic layer.

@[simp]

theorem Time.tenseSystem_isPast_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : TenseSystem.isPast f ↔ f.isPast

@[simp]

theorem Time.tenseSystem_isPresent_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : TenseSystem.isPresent f ↔ f.isPresent

@[simp]

theorem Time.tenseSystem_isFuture_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : TenseSystem.isFuture f ↔ f.isFuture

@[simp]

theorem Time.aspectSystem_isPerfect_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : AspectSystem.isPerfect f ↔ f.isPerfect

@[simp]

theorem Time.aspectSystem_isPerfective_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : AspectSystem.isPerfective f ↔ f.isPerfective

@[simp]

theorem Time.aspectSystem_isProspective_iff {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : AspectSystem.isProspective f ↔ f.isProspective

theorem Time.ReichenbachFrame.not_aspectSystem_isImperfective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : ¬AspectSystem.isImperfective f

Point frames cannot be imperfective. [Kle94]'s imperfective (TT properly inside TSit) requires a non-degenerate interval, and every ReichenbachFrame TO is a point. The audit-level claim that "the imperfective is unrepresentable in the point-frame core" is here a theorem, not a docstring.