Event predicates and the Event type are imported from Semantics/Events/Basic.lean — the unified event ontology. Tense-aspect code uses Event Time and W → Event Time → Prop without referencing .sort (the field exists for Krifka-style consumers but is irrelevant for Klein-style tense composition).

@[reducible, inline]

abbrev Semantics.Aspect.IntervalPred (W : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

Predicate over time intervals (output of IMPF/PRFV).

Equations

• Semantics.Aspect.IntervalPred W Time = (W → NonemptyInterval Time → Prop)

@[reducible, inline]

abbrev Semantics.Aspect.PointPred (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Predicate over time points (output of PERF, input to TENSE). Defined as WorldTimeIndex W Time → Prop to make the situation structure explicit in the tense-aspect pipeline, connecting directly to situation semantics (Elbourne, Percus, Kratzer).

Equations

• Semantics.Aspect.PointPred W Time = (Intensional.WorldTimeIndex W Time → Prop)

inductive Semantics.Aspect.ViewpointType : Type

Viewpoint aspect types. [Kle94] identified imperfective, perfective, perfect, and prospective. [Smi97] added the neutral viewpoint (default in the absence of overt aspect morphology).

• imperfective : ViewpointType
• perfective : ViewpointType
• perfect : ViewpointType
• prospective : ViewpointType
• neutral : ViewpointType

@[implicit_reducible]

instance Semantics.Aspect.instDecidableEqViewpointType : DecidableEq ViewpointType

Equations

• Semantics.Aspect.instDecidableEqViewpointType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.instReprViewpointType : Repr ViewpointType

Equations

• Semantics.Aspect.instReprViewpointType = { reprPrec := Semantics.Aspect.instReprViewpointType.repr }

def Semantics.Aspect.instReprViewpointType.repr : ViewpointType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Aspect.instInhabitedViewpointType : Inhabited ViewpointType

Equations

• Semantics.Aspect.instInhabitedViewpointType = { default := Semantics.Aspect.instInhabitedViewpointType.default }

inductive Semantics.Aspect.ViewpointAspectB : Type

Bool-level viewpoint aspect, capturing the perfective/imperfective distinction without the full interval-based Event Time → Prop/IntervalPred machinery.

Used by Modal/Ability.lean and the actuality-inference consumers (Modality/ActualityEntailments.lean, Studies/Hacquard2006.lean) where the key insight is simply "perfective requires actualization, imperfective doesn't."

• perfective : ViewpointAspectB
• imperfective : ViewpointAspectB

@[implicit_reducible]

instance Semantics.Aspect.instDecidableEqViewpointAspectB : DecidableEq ViewpointAspectB

Equations

• Semantics.Aspect.instDecidableEqViewpointAspectB x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.instReprViewpointAspectB : Repr ViewpointAspectB

Equations

• Semantics.Aspect.instReprViewpointAspectB = { reprPrec := Semantics.Aspect.instReprViewpointAspectB.repr }

def Semantics.Aspect.instReprViewpointAspectB.repr : ViewpointAspectB → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Aspect.instInhabitedViewpointAspectB : Inhabited ViewpointAspectB

Equations

• Semantics.Aspect.instInhabitedViewpointAspectB = { default := Semantics.Aspect.instInhabitedViewpointAspectB.default }

def Semantics.Aspect.ViewpointType.toBoolAspect : ViewpointType → Option ViewpointAspectB

Project ViewpointType to the coarser perfective/imperfective distinction. Returns none for perfect and prospective (neither is simply perf/impf).

Equations

• Semantics.Aspect.ViewpointType.perfective.toBoolAspect = some Semantics.Aspect.ViewpointAspectB.perfective
• Semantics.Aspect.ViewpointType.imperfective.toBoolAspect = some Semantics.Aspect.ViewpointAspectB.imperfective
• Semantics.Aspect.ViewpointType.perfect.toBoolAspect = none
• Semantics.Aspect.ViewpointType.prospective.toBoolAspect = none
• Semantics.Aspect.ViewpointType.neutral.toBoolAspect = none

def Semantics.Aspect.ViewpointAspectB.toKleinViewpoint : ViewpointAspectB → ViewpointType

Embed ViewpointAspectB back into Klein's full classification.

Equations

• Semantics.Aspect.ViewpointAspectB.perfective.toKleinViewpoint = Semantics.Aspect.ViewpointType.perfective
• Semantics.Aspect.ViewpointAspectB.imperfective.toKleinViewpoint = Semantics.Aspect.ViewpointType.imperfective

theorem Semantics.Aspect.toBoolAspect_toKleinViewpoint (a : ViewpointAspectB) : a.toKleinViewpoint.toBoolAspect = some a

Roundtrip: embedding then projecting is the identity.

def Semantics.Aspect.ViewpointType.ttTSitRelation {Time : Type u_1} [LinearOrder Time] (v : ViewpointType) (tt tsit : NonemptyInterval Time) : Prop

The TT↔TSit interval relation for each viewpoint ([Kle94]: 108).

Equations

• Semantics.Aspect.ViewpointType.imperfective.ttTSitRelation tt tsit = (tt < tsit)
• Semantics.Aspect.ViewpointType.perfective.ttTSitRelation tt tsit = (tsit ≤ tt)
• Semantics.Aspect.ViewpointType.perfect.ttTSitRelation tt tsit = tt.isAfter tsit
• Semantics.Aspect.ViewpointType.prospective.ttTSitRelation tt tsit = tt.isBefore tsit
• Semantics.Aspect.ViewpointType.neutral.ttTSitRelation tt tsit = tt.initialOverlap tsit

@[implicit_reducible]

instance Semantics.Aspect.instDecidableTtTSitRelation {Time : Type u_1} [LinearOrder Time] (v : ViewpointType) (tt tsit : NonemptyInterval Time) : Decidable (v.ttTSitRelation tt tsit)

Equations

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

Visibility properties of viewpoints

[Smi97] §4.1 tabulates four visibility properties per viewpoint: whether the initial point of the situation is asserted, whether the final point is asserted, whether the viewpoint presents the situation as informationally closed, and whether the viewpoint can focus an interval strictly inside the situation (the structural source of the imperfective's "preliminary stages" reading for punctuals, §4.2.2). Each property derives from ttTSitRelation: visibility is interval geometry, and Smith's Table 1 re-emerges below as iff theorems, not as a stipulated lookup.

def Semantics.Aspect.ViewpointType.ShowsInitialPoint (v : ViewpointType) : Prop

The viewpoint asserts the situation's initial point: every licensed (tt, tsit) pair has tt containing tsit.fst.

Equations

• v.ShowsInitialPoint = ∀ {Time : Type} [inst : LinearOrder Time] {tt tsit : NonemptyInterval Time}, v.ttTSitRelation tt tsit → tsit.toProd.1 ∈ tt

def Semantics.Aspect.ViewpointType.ShowsFinalPoint (v : ViewpointType) : Prop

The viewpoint asserts the situation's final point.

Equations

• v.ShowsFinalPoint = ∀ {Time : Type} [inst : LinearOrder Time] {tt tsit : NonemptyInterval Time}, v.ttTSitRelation tt tsit → tsit.toProd.2 ∈ tt

def Semantics.Aspect.ViewpointType.IsClosed (v : ViewpointType) : Prop

The viewpoint presents the situation as informationally closed: the topic time reaches at least the situation time's right endpoint.

Equations

• v.IsClosed = ∀ {Time : Type} [inst : LinearOrder Time] {tt tsit : NonemptyInterval Time}, v.ttTSitRelation tt tsit → tsit.toProd.2 ≤ tt.toProd.2

def Semantics.Aspect.ViewpointType.FocusesPreliminaryStages (v : ViewpointType) : Prop

The viewpoint focuses a topic time strictly inside the situation, the structural source of the imperfective's "preliminary stages" reading for punctual events ([Smi97] §4.2.2).

Equations

• v.FocusesPreliminaryStages = ∀ {Time : Type} [inst : LinearOrder Time] {tt tsit : NonemptyInterval Time}, v.ttTSitRelation tt tsit → tt < tsit

theorem Semantics.Aspect.ViewpointType.showsInitialPoint_iff (v : ViewpointType) : v.ShowsInitialPoint ↔ v = perfective ∨ v = neutral

[Smi97] Table 1, IP column: only perfective and neutral assert the initial point.

theorem Semantics.Aspect.ViewpointType.showsFinalPoint_iff (v : ViewpointType) : v.ShowsFinalPoint ↔ v = perfective

[Smi97] Table 1, FP column: only perfective asserts the final point.

theorem Semantics.Aspect.ViewpointType.isClosed_iff (v : ViewpointType) : v.IsClosed ↔ v = perfective ∨ v = perfect

[Smi97] Table 1, Closed column: only perfective and perfect are closed.

theorem Semantics.Aspect.ViewpointType.focusesPreliminaryStages_iff (v : ViewpointType) : v.FocusesPreliminaryStages ↔ v = imperfective

[Smi97] Table 1, Preliminaries column: only the imperfective places the topic time strictly inside the situation.

def Semantics.Aspect.IMPF {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

IMPERFECTIVE: reference time properly contained in event runtime. [Kle94]: TT INCL TSit. [KS26] eq. 25.

Equations

• Semantics.Aspect.IMPF P w t = ∃ (e : Event Time), t < e.τ ∧ P w e

def Semantics.Aspect.PRFV {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

PERFECTIVE: event runtime contained in reference time. [Kle94]: TT AT TSit (simplified to TSit ⊆ TT, following [Smi97]). [KS26] eq. 28.

Equations

• Semantics.Aspect.PRFV P w t = ∃ (e : Event Time), e.τ ≤ t ∧ P w e

def Semantics.Aspect.PROSP {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

PROSPECTIVE: reference time before situation time. [Kle94]: TT BEFORE TSit.

Equations

• Semantics.Aspect.PROSP P w t = ∃ (e : Event Time), t.isBefore e.τ ∧ P w e

def Semantics.Aspect.INIT_OVERLAP {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

INIT_OVERLAP: initial overlap between reference time and event runtime. [Pan03] eq. 7b: ⟦NEUTRAL⟧ = λP.λi.∃e[i ∂τ(e) & P(e)] The beginning of the eventuality is in the reference interval, but the end may extend beyond. Derives experiential perfect readings.

Renamed from NEUTRAL to avoid collision with [Smi97]'s neutral viewpoint (ViewpointType.neutral), which is a different concept. Pancheva's operator is an inner Asp₂ head; Smith's neutral viewpoint is a default viewpoint type.

Equations

• Semantics.Aspect.INIT_OVERLAP P w t = ∃ (e : Event Time), t.initialOverlap e.τ ∧ P w e

def Semantics.Aspect.RB {Time : Type u_1} [LinearOrder Time] (pts : NonemptyInterval Time) (t : Time) : Prop

Right Boundary: PTS finishes at reference time point t.

Equations

• Semantics.Aspect.RB pts t = (pts.toProd.2 = t)

def Semantics.Aspect.LB {Time : Type u_1} [LinearOrder Time] (tLB : Time) (pts : NonemptyInterval Time) : Prop

Left Boundary: PTS starts at time tLB.

Equations

• Semantics.Aspect.LB tLB pts = (pts.toProd.1 = tLB)

def Semantics.Aspect.PERF {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : PointPred W Time

PERFECT: introduces Perfect Time Span. [KS26] eq. 22b — the standard XN-theoretic entry that K&S start from. Verified against the proceedings PDF.

K&S notation: λp_it.λt.∃t_PTS.[RB(t_PTS, t) ∧ p(t)]. The p(t) is written by K&S as application to the outer reference time, with the composition convention that t is bound to t_PTS when IMPF appears below PERF (paper §4.2.1, sentence after eq. 25). The implementation here applies p to pts directly (the post-composition meaning), which matches K&S's worked composition in their (26).

Equations

• Semantics.Aspect.PERF p s = ∃ (pts : NonemptyInterval Time), Semantics.Aspect.RB pts s.time ∧ p s.world pts

def Semantics.Aspect.PERF_XN {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ : Set Time) : PointPred W Time

PERFECT with Extended Now (K&S's revision: domain-restricted left boundary). [KS26] eq. 23b. Verified against the proceedings PDF.

K&S notation: λp_it.λt.∃t_PTS.∃t_LB ⊆ tᵣ. [LB(t_LB, t_PTS) ∧ RB(t_PTS, t) ∧ p(t)]. The domain restriction tᵣ constrains where the LB can be placed; narrow focus on BEEN generates alternatives over tᵣ.

K&S's (23b) is not the standard XN entry — that's their (22b), realized here as PERF. (23b) is K&S's own revision adding an LB existential bounded by the domain restriction. The legacy name PERF_XN predates this clarification; both PERF and PERF_XN are XN-theoretic, the difference being the LB+domain-restriction.

Type-level simplification: K&S's t_LB is an initial subinterval of t_PTS (per their 23a), and t_LB ⊆ t_r compares two interval-sets. The implementation here uses tLB : Time (a single point) with ∃ tLB ∈ tᵣ (membership), simplifying K&S's set-theoretic LB to a single time witness inside the domain-restriction set. The simpler typing is sufficient for the empirical predictions K&S draw and avoids carrying intervals at every level.

Equations

• Semantics.Aspect.PERF_XN p tᵣ s = ∃ (pts : NonemptyInterval Time), ∃ tLB ∈ tᵣ, Semantics.Aspect.LB tLB pts ∧ Semantics.Aspect.RB pts s.time ∧ p s.world pts

theorem Semantics.Aspect.impf_is_klein_imperfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : IMPF P w t ↔ ∃ (e : Event Time), ViewpointType.imperfective.ttTSitRelation t e.τ ∧ P w e

IMPF matches Klein's IMPERFECTIVE: ∃e where TT ⊂ TSit.

theorem Semantics.Aspect.prfv_is_klein_perfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : PRFV P w t ↔ ∃ (e : Event Time), ViewpointType.perfective.ttTSitRelation t e.τ ∧ P w e

PRFV matches Klein's PERFECTIVE: ∃e where TSit ⊆ TT.

@[reducible, inline]

abbrev Semantics.Aspect.perfProg {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : PointPred W Time

"has been V-ing" = PERF(IMPF(V)).

Equations

• Semantics.Aspect.perfProg P = Semantics.Aspect.PERF (Semantics.Aspect.IMPF P)

@[reducible, inline]

abbrev Semantics.Aspect.perfSimple {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : PointPred W Time

"has V-ed" = PERF(PRFV(V)).

Equations

• Semantics.Aspect.perfSimple P = Semantics.Aspect.PERF (Semantics.Aspect.PRFV P)

theorem Semantics.Aspect.perf_impf_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : Time) : perfProg P { world := w, time := t } ↔ ∃ (pts : NonemptyInterval Time) (e : Event Time), RB pts t ∧ pts < e.τ ∧ P w e

PERF(IMPF(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the PTS properly inside the event, and P holds of the event.

theorem Semantics.Aspect.perf_prfv_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : Time) : perfSimple P { world := w, time := t } ↔ ∃ (pts : NonemptyInterval Time) (e : Event Time), RB pts t ∧ e.τ ≤ pts ∧ P w e

PERF(PRFV(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the event inside the PTS, and P holds of the event.

theorem Semantics.Aspect.perf_xn_entails_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ : Set Time) (w : W) (t : Time) : PERF_XN p tᵣ { world := w, time := t } → PERF p { world := w, time := t }

Extended Now entails basic perfect (PERF_XN is stronger).

theorem Semantics.Aspect.perf_xn_univ_iff_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (w : W) (t : Time) : PERF_XN p Set.univ { world := w, time := t } ↔ PERF p { world := w, time := t }

With maximal domain (Set.univ), PERF_XN collapses to PERF.

theorem Semantics.Aspect.perf_xn_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ₁ tᵣ₂ : Set Time) (hSub : tᵣ₁ ⊆ tᵣ₂) (w : W) (t : Time) : PERF_XN p tᵣ₁ { world := w, time := t } → PERF_XN p tᵣ₂ { world := w, time := t }

Narrower domain restriction is stronger (monotone in tᵣ).

theorem Semantics.Aspect.impf_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : IMPF P w t → ∃ (e : Event Time), P w e

IMPF entails an event exists.

theorem Semantics.Aspect.prfv_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : PRFV P w t → ∃ (e : Event Time), P w e

PRFV entails an event exists.

theorem Semantics.Aspect.perf_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : NonemptyInterval Time), p w t → q w t) (w : W) (t : Time) : PERF p { world := w, time := t } → PERF q { world := w, time := t }

PERF is monotone: p ⊆ q → PERF(p) ⊆ PERF(q).

theorem Semantics.Aspect.impf_prfv_opposite_containment {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : (IMPF P w t → ∃ (e : Event Time), P w e ∧ t < e.τ) ∧ (PRFV P w t → ∃ (e : Event Time), P w e ∧ e.τ ≤ t)

IMPF and PRFV impose opposite containment directions. IMPF: reference ⊂ event runtime. PRFV: event runtime ⊆ reference.

[Pan03] decomposes perfect participles into two aspect heads: [T [Asp₁=PERFECT [Asp₂=VIEWPOINT [vP]]]]. The inner Asp₂ (UNBOUNDED, INIT_OVERLAP, or BOUNDED) determines the perfect type (universal, experiential, or resultative). The outer Asp₁ = PERFECT introduces the PTS via a final subinterval relation rather than a point-based right boundary.

def Semantics.Aspect.UNBOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

Pancheva's UNBOUNDED (Asp₂): non-strict ⊆ variant of IMPF. ⟦UNBOUNDED⟧ = λP.λi.∃e[i ⊆ τ(e) & P(e)] ([Pan03]: 282, eq. 7b). Differs from IMPF in using non-strict ⊆ rather than strict ⊂.

Equations

• Semantics.Aspect.UNBOUNDED P w t = ∃ (e : Event Time), t ≤ e.τ ∧ P w e

def Semantics.Aspect.BOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

Pancheva's BOUNDED (Asp₂): strict ⊂ variant of PRFV. ⟦BOUNDED⟧ = λP.λi.∃e[τ(e) ⊂ i & P(e)] ([Pan03]: 282, eq. 7b). Differs from PRFV in using strict ⊂ rather than non-strict ⊆.

Equations

• Semantics.Aspect.BOUNDED P w t = ∃ (e : Event Time), e.τ < t ∧ P w e

theorem Semantics.Aspect.impf_entails_unbounded {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : IMPF P w t → UNBOUNDED P w t

IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆).

theorem Semantics.Aspect.bounded_entails_prfv {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : BOUNDED P w t → PRFV P w t

BOUNDED (strict ⊂) entails PRFV (non-strict ⊆).

def Semantics.Aspect.PERF_P {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : IntervalPred W Time

Pancheva-style interval-level PERFECT (Asp₁). ⟦PERFECT⟧ = λp.λi.∃i'[PTS(i', i) & p(i')] ([Pan03]: 284, eq. 9b). PTS(i', i) iff i is a final subinterval of i': i ⊆ i' ∧ i.snd = i'.snd.

Equations

• Semantics.Aspect.PERF_P p w i = ∃ (pts : NonemptyInterval Time), i.finalSubinterval pts ∧ p w pts

theorem Semantics.Aspect.perf_p_at_point_iff_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (w : W) (t : Time) : PERF_P p w (NonemptyInterval.pure t) ↔ PERF p { world := w, time := t }

Point-based PERF is the special case of interval-based PERF_P where the reference interval degenerates to a point [t, t].

theorem Semantics.Aspect.perf_p_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : NonemptyInterval Time), p w t → q w t) (w : W) (i : NonemptyInterval Time) : PERF_P p w i → PERF_P q w i

PERF_P is monotone: if p entails q, then PERF_P(p) entails PERF_P(q).

inductive Semantics.Aspect.PerfectType : Type

[Pan03] perfect type classification. The embedded Asp₂ determines the perfect reading:

• universal = PERFECT(UNBOUNDED): event ongoing throughout PTS
• experiential = PERFECT(NEUTRAL): event began within PTS
• resultative = PERFECT(BOUNDED): event completed within PTS Note: Pancheva's resultative properly involves a result state relation; BOUNDED is a simplification sufficient for the temporal structure.

• universal : PerfectType
• experiential : PerfectType
• resultative : PerfectType

@[implicit_reducible]

instance Semantics.Aspect.instDecidableEqPerfectType : DecidableEq PerfectType

Equations

• Semantics.Aspect.instDecidableEqPerfectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.instReprPerfectType : Repr PerfectType

Equations

• Semantics.Aspect.instReprPerfectType = { reprPrec := Semantics.Aspect.instReprPerfectType.repr }

def Semantics.Aspect.instReprPerfectType.repr : PerfectType → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Semantics.Aspect.universalPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

Universal perfect: PERF_P(UNBOUNDED(V)). "has been running" — event ongoing throughout PTS. [Pan03]: explains why universal reading requires imperfective.

Equations

• Semantics.Aspect.universalPerfect P = Semantics.Aspect.PERF_P (Semantics.Aspect.UNBOUNDED P)

@[reducible, inline]

abbrev Semantics.Aspect.experientialPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

Experiential perfect: PERF_P(INIT_OVERLAP(V)). "has visited Paris" — event began within PTS. [Pan03]: initial-overlap aspect allows event to extend beyond PTS.

Equations

• Semantics.Aspect.experientialPerfect P = Semantics.Aspect.PERF_P (Semantics.Aspect.INIT_OVERLAP P)

@[reducible, inline]

abbrev Semantics.Aspect.resultativePerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) : IntervalPred W Time

Resultative perfect: PERF_P(BOUNDED(V)). "has broken the vase" — event completed within PTS. Simplified: properly involves result state ([Pan03]: 288).

Equations

• Semantics.Aspect.resultativePerfect P = Semantics.Aspect.PERF_P (Semantics.Aspect.BOUNDED P)

theorem Semantics.Aspect.perf_prog_entails_universal_at_point {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : W → Event Time → Prop) (w : W) (t : Time) : perfProg P { world := w, time := t } → universalPerfect P w (NonemptyInterval.pure t)

perfProg at a point entails universalPerfect at that point. Since IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆), PERF(IMPF(V)) entails PERF(UNBOUNDED(V)) = universalPerfect.

def Semantics.Aspect.IntervalPred.atPoint {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : PointPred W Time

Evaluate an interval predicate at a point (trivial interval [t, t]). Bridge for non-perfect forms.

Equations

• p.atPoint s = p s.world (NonemptyInterval.pure s.time)