structure Semantics.Lexical.Verb.ViewpointAspect.Eventuality (Time : Type u_1) [LE Time] : Type u_1

An eventuality with interval-valued runtime. @cite{pancheva-2003} Unlike Situation (point-valued τ), eventualities occupy temporal intervals.

• runtime : Core.Time.Interval Time

  The temporal extent of this eventuality

def Semantics.Lexical.Verb.ViewpointAspect.Eventuality.τ {Time : Type u_1} [LE Time] (e : Eventuality Time) : Core.Time.Interval Time

Temporal trace: the runtime interval of an eventuality.

Equations

• e.τ = e.runtime

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.EventPred (W : Type u_1) (Time : Type u_2) [LE Time] : Type (max u_1 u_2)

Predicate over eventualities (VP denotations).

Equations

• Semantics.Lexical.Verb.ViewpointAspect.EventPred W Time = (W → Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time → Prop)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.IntervalPred (W : Type u_1) (Time : Type u_2) [LE Time] : Type (max u_1 u_2)

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

Equations

• Semantics.Lexical.Verb.ViewpointAspect.IntervalPred W Time = (W → Core.Time.Interval Time → Prop)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.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 Situation W Time → Prop to make the situation structure explicit in the tense-aspect pipeline, connecting directly to situation semantics (Elbourne, Percus, Kratzer).

Equations

• Semantics.Lexical.Verb.ViewpointAspect.PointPred W Time = (Situation W Time → Prop)

inductive Semantics.Lexical.Verb.ViewpointAspect.ViewpointType : Type

@cite{klein-1994} viewpoint aspect types.

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

instance Semantics.Lexical.Verb.ViewpointAspect.instDecidableEqViewpointType : DecidableEq ViewpointType

Equations

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

def Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointType.repr : ViewpointType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointType : Repr ViewpointType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointType = { reprPrec := Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointType.repr }

def Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointType.beq : ViewpointType → ViewpointType → Bool

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointType : BEq ViewpointType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointType = { beq := Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointType.beq }

def Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointType.default : ViewpointType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointType.default = Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.imperfective

instance Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointType : Inhabited ViewpointType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointType = { default := Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointType.default }

inductive Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB : Type

Bool-level viewpoint aspect, capturing the perfective/imperfective distinction without the full interval-based EventPred/IntervalPred machinery.

Used by Modal/Ability.lean (actuality inferences) and Phenomena/ActualityInferences/Data.lean where the key insight is simply "perfective requires actualization, imperfective doesn't."

• perfective : ViewpointAspectB
• imperfective : ViewpointAspectB

instance Semantics.Lexical.Verb.ViewpointAspect.instDecidableEqViewpointAspectB : DecidableEq ViewpointAspectB

Equations

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

def Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointAspectB.repr : ViewpointAspectB → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointAspectB : Repr ViewpointAspectB

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointAspectB = { reprPrec := Semantics.Lexical.Verb.ViewpointAspect.instReprViewpointAspectB.repr }

def Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointAspectB.beq : ViewpointAspectB → ViewpointAspectB → Bool

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointAspectB.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointAspectB : BEq ViewpointAspectB

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointAspectB = { beq := Semantics.Lexical.Verb.ViewpointAspect.instBEqViewpointAspectB.beq }

def Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointAspectB.default : ViewpointAspectB

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointAspectB.default = Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.perfective

instance Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointAspectB : Inhabited ViewpointAspectB

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointAspectB = { default := Semantics.Lexical.Verb.ViewpointAspect.instInhabitedViewpointAspectB.default }

def Semantics.Lexical.Verb.ViewpointAspect.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.Lexical.Verb.ViewpointAspect.ViewpointType.perfective.toBoolAspect = some Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.perfective
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.imperfective.toBoolAspect = some Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.imperfective
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.perfect.toBoolAspect = none
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.prospective.toBoolAspect = none

def Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.toKleinViewpoint : ViewpointAspectB → ViewpointType

Embed ViewpointAspectB back into Klein's full classification.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.perfective.toKleinViewpoint = Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.perfective
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointAspectB.imperfective.toKleinViewpoint = Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.imperfective

theorem Semantics.Lexical.Verb.ViewpointAspect.toBoolAspect_toKleinViewpoint (a : ViewpointAspectB) : a.toKleinViewpoint.toBoolAspect = some a

Roundtrip: embedding then projecting is the identity.

def Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.ttTSitRelation {Time : Type u_1} [LinearOrder Time] (v : ViewpointType) (tt tsit : Core.Time.Interval Time) : Prop

The TT↔TSit interval relation for each viewpoint (@cite{klein-1994}: 108).

Equations

• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.imperfective.ttTSitRelation tt tsit = tt.properSubinterval tsit
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.perfective.ttTSitRelation tt tsit = tsit.subinterval tt
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.perfect.ttTSitRelation tt tsit = tt.isAfter tsit
• Semantics.Lexical.Verb.ViewpointAspect.ViewpointType.prospective.ttTSitRelation tt tsit = tt.isBefore tsit

def Semantics.Lexical.Verb.ViewpointAspect.IMPF {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

IMPERFECTIVE: reference time properly contained in event runtime. @cite{klein-1994}: TT INCL TSit. @cite{knick-sharf-2026} eq. 25.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.IMPF P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), t.properSubinterval e.τ ∧ P w e

def Semantics.Lexical.Verb.ViewpointAspect.PRFV {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

PERFECTIVE: event runtime contained in reference time. @cite{klein-1994}: TT AT TSit (simplified to TSit ⊆ TT, following @cite{smith-1991}). @cite{knick-sharf-2026} eq. 28.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.PRFV P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), e.τ.subinterval t ∧ P w e

def Semantics.Lexical.Verb.ViewpointAspect.PROSP {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

PROSPECTIVE: reference time before situation time. @cite{klein-1994}: TT BEFORE TSit.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.PROSP P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), t.isBefore e.τ ∧ P w e

def Semantics.Lexical.Verb.ViewpointAspect.NEUTRAL {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

NEUTRAL: initial overlap between reference time and event runtime. @cite{pancheva-2003} 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.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.NEUTRAL P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), t.initialOverlap e.τ ∧ P w e

def Semantics.Lexical.Verb.ViewpointAspect.RB {Time : Type u_1} [LinearOrder Time] (pts : Core.Time.Interval Time) (t : Time) : Prop

Right Boundary: PTS finishes at reference time point t.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.RB pts t = (pts.finish = t)

def Semantics.Lexical.Verb.ViewpointAspect.LB {Time : Type u_1} [LinearOrder Time] (tLB : Time) (pts : Core.Time.Interval Time) : Prop

Left Boundary: PTS starts at time tLB.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.LB tLB pts = (pts.start = tLB)

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

PERFECT: introduces Perfect Time Span. @cite{knick-sharf-2026} eq. 22b.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.PERF p s = ∃ (pts : Core.Time.Interval Time), Semantics.Lexical.Verb.ViewpointAspect.RB pts s.time ∧ p s.world pts

def Semantics.Lexical.Verb.ViewpointAspect.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 (domain-restricted left boundary). @cite{knick-sharf-2026} eq. 23b. The domain restriction tᵣ constrains where the LB can be placed. Narrow focus on BEEN generates alternatives over tᵣ.

Equations

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

theorem Semantics.Lexical.Verb.ViewpointAspect.impf_is_klein_imperfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t ↔ ∃ (e : Eventuality Time), ViewpointType.imperfective.ttTSitRelation t e.τ ∧ P w e

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

theorem Semantics.Lexical.Verb.ViewpointAspect.prfv_is_klein_perfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : PRFV P w t ↔ ∃ (e : Eventuality Time), ViewpointType.perfective.ttTSitRelation t e.τ ∧ P w e

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

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.perfProg {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : PointPred W Time

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

Equations

• Semantics.Lexical.Verb.ViewpointAspect.perfProg P = Semantics.Lexical.Verb.ViewpointAspect.PERF (Semantics.Lexical.Verb.ViewpointAspect.IMPF P)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.perfSimple {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : PointPred W Time

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

Equations

• Semantics.Lexical.Verb.ViewpointAspect.perfSimple P = Semantics.Lexical.Verb.ViewpointAspect.PERF (Semantics.Lexical.Verb.ViewpointAspect.PRFV P)

theorem Semantics.Lexical.Verb.ViewpointAspect.perf_impf_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Time) : perfProg P { world := w, time := t } ↔ ∃ (pts : Core.Time.Interval Time) (e : Eventuality Time), RB pts t ∧ pts.properSubinterval 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.Lexical.Verb.ViewpointAspect.perf_prfv_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Time) : perfSimple P { world := w, time := t } ↔ ∃ (pts : Core.Time.Interval Time) (e : Eventuality Time), RB pts t ∧ e.τ.subinterval 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.Lexical.Verb.ViewpointAspect.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.Lexical.Verb.ViewpointAspect.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.Lexical.Verb.ViewpointAspect.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ᵣ).

def Semantics.Lexical.Verb.Aspect.VendlerClass.naturallyImperfective : VendlerClass → Bool

States and activities naturally pair with IMPF (homogeneous).

Equations

• Semantics.Lexical.Verb.Aspect.VendlerClass.state.naturallyImperfective = true
• Semantics.Lexical.Verb.Aspect.VendlerClass.activity.naturallyImperfective = true
• Semantics.Lexical.Verb.Aspect.VendlerClass.achievement.naturallyImperfective = false
• Semantics.Lexical.Verb.Aspect.VendlerClass.accomplishment.naturallyImperfective = false

def Semantics.Lexical.Verb.Aspect.VendlerClass.naturallyPerfective : VendlerClass → Bool

Achievements and accomplishments naturally pair with PRFV (telic).

Equations

• Semantics.Lexical.Verb.Aspect.VendlerClass.state.naturallyPerfective = false
• Semantics.Lexical.Verb.Aspect.VendlerClass.activity.naturallyPerfective = false
• Semantics.Lexical.Verb.Aspect.VendlerClass.achievement.naturallyPerfective = true
• Semantics.Lexical.Verb.Aspect.VendlerClass.accomplishment.naturallyPerfective = true

theorem Semantics.Lexical.Verb.ViewpointAspect.naturally_imperfective_iff_homogeneous (c : Aspect.VendlerClass) : c.naturallyImperfective = c.toProfile.isHomogeneous

Natural imperfectivity = homogeneity (subinterval property).

theorem Semantics.Lexical.Verb.ViewpointAspect.naturally_perfective_iff_telic (c : Aspect.VendlerClass) : c.naturallyPerfective = (c.telicity == Aspect.Telicity.telic)

Natural perfectivity = telicity.

theorem Semantics.Lexical.Verb.ViewpointAspect.impf_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t → ∃ (e : Eventuality Time), P w e

IMPF entails an event exists.

theorem Semantics.Lexical.Verb.ViewpointAspect.prfv_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : PRFV P w t → ∃ (e : Eventuality Time), P w e

PRFV entails an event exists.

theorem Semantics.Lexical.Verb.ViewpointAspect.perf_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : Core.Time.Interval 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.Lexical.Verb.ViewpointAspect.impf_prfv_opposite_containment {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : (IMPF P w t → ∃ (e : Eventuality Time), P w e ∧ t.properSubinterval e.τ) ∧ (PRFV P w t → ∃ (e : Eventuality Time), P w e ∧ e.τ.subinterval t)

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

@cite{pancheva-2003} decomposes perfect participles into two aspect heads: [T [Asp₁=PERFECT [Asp₂=VIEWPOINT [vP]]]]. The inner Asp₂ (UNBOUNDED, NEUTRAL, 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.Lexical.Verb.ViewpointAspect.UNBOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

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

Equations

• Semantics.Lexical.Verb.ViewpointAspect.UNBOUNDED P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), t.subinterval e.τ ∧ P w e

def Semantics.Lexical.Verb.ViewpointAspect.BOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

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

Equations

• Semantics.Lexical.Verb.ViewpointAspect.BOUNDED P w t = ∃ (e : Semantics.Lexical.Verb.ViewpointAspect.Eventuality Time), e.τ.properSubinterval t ∧ P w e

theorem Semantics.Lexical.Verb.ViewpointAspect.impf_entails_unbounded {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t → UNBOUNDED P w t

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

theorem Semantics.Lexical.Verb.ViewpointAspect.bounded_entails_prfv {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : BOUNDED P w t → PRFV P w t

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

def Semantics.Lexical.Verb.ViewpointAspect.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')] (@cite{pancheva-2003}: 284, eq. 9b). PTS(i', i) iff i is a final subinterval of i': i ⊆ i' ∧ i.finish = i'.finish.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.PERF_P p w i = ∃ (pts : Core.Time.Interval Time), i.finalSubinterval pts ∧ p w pts

theorem Semantics.Lexical.Verb.ViewpointAspect.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 (Core.Time.Interval.point 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.Lexical.Verb.ViewpointAspect.perf_p_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : Core.Time.Interval Time), p w t → q w t) (w : W) (i : Core.Time.Interval 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.Lexical.Verb.ViewpointAspect.PerfectType : Type

@cite{pancheva-2003} 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

instance Semantics.Lexical.Verb.ViewpointAspect.instDecidableEqPerfectType : DecidableEq PerfectType

Equations

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

def Semantics.Lexical.Verb.ViewpointAspect.instReprPerfectType.repr : PerfectType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.ViewpointAspect.instReprPerfectType : Repr PerfectType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instReprPerfectType = { reprPrec := Semantics.Lexical.Verb.ViewpointAspect.instReprPerfectType.repr }

def Semantics.Lexical.Verb.ViewpointAspect.instBEqPerfectType.beq : PerfectType → PerfectType → Bool

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqPerfectType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.ViewpointAspect.instBEqPerfectType : BEq PerfectType

Equations

• Semantics.Lexical.Verb.ViewpointAspect.instBEqPerfectType = { beq := Semantics.Lexical.Verb.ViewpointAspect.instBEqPerfectType.beq }

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.universalPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

Universal perfect: PERF_P(UNBOUNDED(V)). "has been running" — event ongoing throughout PTS. @cite{pancheva-2003}: explains why universal reading requires imperfective.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.universalPerfect P = Semantics.Lexical.Verb.ViewpointAspect.PERF_P (Semantics.Lexical.Verb.ViewpointAspect.UNBOUNDED P)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.experientialPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

Experiential perfect: PERF_P(NEUTRAL(V)). "has visited Paris" — event began within PTS. @cite{pancheva-2003}: neutral aspect allows event to extend beyond PTS.

Equations

• Semantics.Lexical.Verb.ViewpointAspect.experientialPerfect P = Semantics.Lexical.Verb.ViewpointAspect.PERF_P (Semantics.Lexical.Verb.ViewpointAspect.NEUTRAL P)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.resultativePerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) : IntervalPred W Time

Resultative perfect: PERF_P(BOUNDED(V)). "has broken the vase" — event completed within PTS. Simplified: properly involves result state (@cite{pancheva-2003}: 288).

Equations

• Semantics.Lexical.Verb.ViewpointAspect.resultativePerfect P = Semantics.Lexical.Verb.ViewpointAspect.PERF_P (Semantics.Lexical.Verb.ViewpointAspect.BOUNDED P)

theorem Semantics.Lexical.Verb.ViewpointAspect.perf_prog_entails_universal_at_point {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : EventPred W Time) (w : W) (t : Time) : perfProg P { world := w, time := t } → universalPerfect P w (Core.Time.Interval.point 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.Lexical.Verb.ViewpointAspect.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 (Core.Time.Interval.point s.time)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.ViewpointAspect.PointPred.toSitProp {Time : Type u_1} {W : Type u_2} (p : PointPred W Time) : Situation W Time → Prop

PointPred is now Situation W Time → Prop, so toSitProp is the identity. Retained as an abbreviation for backward compatibility at call sites.

Equations

• p.toSitProp = p