Reichenbach's Temporal Framework

@cite{kiparsky-2002} @cite{klein-1994} @cite{reichenbach-1947}

@cite{reichenbach-1947} / @cite{klein-1994} tense–aspect parameters, extended with @cite{kiparsky-2002}'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 Core.Time.Domain (central = S, sub-TOs = [P, R, E], all as point intervals via TO.point). The *_iff_relatedByName bridge theorems re-express each Boolean 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 (Interval.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 Core.Time.Reichenbach.ReichenbachFrame (Time : Type u_1) : Type u_1

Reichenbach's temporal parameters for tense/aspect analysis, extended with @cite{kiparsky-2002}'s perspective time P.

• speechTime: When the utterance is made (S)
• perspectiveTime: Origin of temporal deixis (P, @cite{kiparsky-2002})
• 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 : Time

  Speech time (S): when the utterance occurs

• perspectiveTime : Time

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

• referenceTime : Time

  Reference time (R): the time under discussion

• eventTime : Time

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

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

PAST: R < P (reference time precedes perspective time). @cite{kiparsky-2002}: tense locates R relative to P, not S.

Equations

• f.isPast = (f.referenceTime < f.perspectiveTime)

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

PRESENT: R = P (reference time equals perspective time).

Equations

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

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

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

Equations

• f.isFuture = (f.perspectiveTime < f.referenceTime)

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

def Core.Time.Reichenbach.ReichenbachFrame.isPerfective {Time : Type u_1} (f : ReichenbachFrame Time) : 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 Theories/Semantics/Lexical/Verb/ViewpointAspect.lean.

Equations

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

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

Perfect: E < R (event precedes reference)

Equations

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

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

Prospective: R < E (reference precedes event)

Equations

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

def Core.Time.Reichenbach.ReichenbachFrame.toDomain {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Domain Time 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.point). 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 = Core.Time.Domain.ofReichenbachPoints f.speechTime f.perspectiveTime f.referenceTime f.eventTime

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Core.Time.Reichenbach.ReichenbachFrame.isPast_iff_relatedByName {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : f.isPast ↔ f.toDomain.relatedByName AllenRelation.precedesSet Orientation.topic 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 Core.Time.Reichenbach.ReichenbachFrame.isFuture_iff_relatedByName {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : f.isFuture ↔ f.toDomain.relatedByName AllenRelation.precedesSet Orientation.perspective Orientation.topic

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

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

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

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

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

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

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

theorem Core.Time.Reichenbach.ReichenbachFrame.isPerfective_iff_relatedByName {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : f.isPerfective ↔ f.toDomain.relatedByName AllenRelation.equalSet Orientation.situation 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 Theories/Semantics/Lexical/Verb/ViewpointAspect.lean.)

Reichenbach as a Core.Time.TenseSystem (anchor = P, situation = R) and Core.Time.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 Core.Time.Reichenbach.reichenbachFrame_tenseSystem {Time : Type u_1} [LinearOrder Time] : TenseSystem (ReichenbachFrame Time) Time Orientation

Equations

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

@[implicit_reducible]

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

Equations

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