Temporal Decomposition of Events

@cite{kiparsky-2002}

Bridges the gap between EventStructure.Template (predicate-role decomposition, no temporal information) and ViewpointAspect (temporal operators on opaque predicates, no subevent structure).

Accomplishments and achievements have internal temporal structure: an activity phase and a result phase with ordering constraints. States and activities are temporally simple. This module makes that structure explicit via TemporalDecomposition, enabling the perfect polysemy analysis in PerfectPolysemy.lean.

Key Definitions

• SubeventPhases: activity trace + result trace with ordering constraint
• TemporalDecomposition: .simple (single runtime) or .complex (phased)
• hasComplexDecomposition: telic classes have complex decomposition
• DecomposedEv: event enriched with decomposition
• phasePred: converts an interval (event phase) into an EventPred for ViewpointAspect operators
• MoensSteedmanClass: five-way event classification
• Nucleus: tripartite event structure (prep process → culmination → cons state)
• WhenTarget: what when accesses in each event type

ViewpointAspect Bridge (§ 6–7)

phasePred converts temporal phases into EventPred Unit Time, making them consumable by IMPF/PRFV/PERF. Key results:

• impf_phasePred / prfv_phasePred: reduce operator applications to interval containment
• progressive_before_result: the imperfective paradox — IMPF on the activity phase can hold at times entirely before the result
• perfective_full_entails_result: PRFV on the full event entails the result trace is within the reference time
• impf_activity_prfv_full_incompatible: progressive and perfective are mutually exclusive at the same reference time

structure Semantics.Events.SubeventPhases (Time : Type u_1) [LinearOrder Time] : Type u_1

The two temporal phases of a complex event (accomplishment/achievement): an activity trace (the process) and a result trace (the outcome state). The activity phase must precede or meet the result phase.

• activityTrace : Core.Time.Interval Time

  Temporal extent of the activity/process phase

• resultTrace : Core.Time.Interval Time

  Temporal extent of the result state phase

• activity_precedes_result : self.activityTrace.finish ≤ self.resultTrace.start

  Activity precedes or meets result: activity ends ≤ result starts

inductive Semantics.Events.TemporalDecomposition (Time : Type u_1) [LinearOrder Time] : Type u_1

Temporal decomposition of an event: either simple (single runtime) or complex (runtime with internal activity + result phases).

• States and activities are .simple: one homogeneous interval.
• Accomplishments and achievements are .complex: the overall runtime decomposes into an activity phase and a result phase.

• simple {Time : Type u_1} [LinearOrder Time] (runtime : Core.Time.Interval Time) : TemporalDecomposition Time

  Simple event: a single runtime interval with no internal structure.

• complex {Time : Type u_1} [LinearOrder Time] (runtime : Core.Time.Interval Time) (phases : SubeventPhases Time) (activity_in_runtime : phases.activityTrace.subinterval runtime) (result_in_runtime : phases.resultTrace.subinterval runtime) : TemporalDecomposition Time

  Complex event: overall runtime with activity and result subphases. Both subphases are contained within the overall runtime.

def Semantics.Events.TemporalDecomposition.runtime {Time : Type u_1} [LinearOrder Time] : TemporalDecomposition Time → Core.Time.Interval Time

Extract the overall runtime from any decomposition.

Equations

• (Semantics.Events.TemporalDecomposition.simple r).runtime = r
• (Semantics.Events.TemporalDecomposition.complex r phases activity_in_runtime result_in_runtime).runtime = r

def Semantics.Events.TemporalDecomposition.activityPhase {Time : Type u_1} [LinearOrder Time] : TemporalDecomposition Time → Option (Core.Time.Interval Time)

Extract the activity phase (only available for complex events).

Equations

• (Semantics.Events.TemporalDecomposition.simple r).activityPhase = none
• (Semantics.Events.TemporalDecomposition.complex r phases activity_in_runtime result_in_runtime).activityPhase = some phases.activityTrace

def Semantics.Events.TemporalDecomposition.resultPhase {Time : Type u_1} [LinearOrder Time] : TemporalDecomposition Time → Option (Core.Time.Interval Time)

Extract the result phase (only available for complex events).

Equations

• (Semantics.Events.TemporalDecomposition.simple r).resultPhase = none
• (Semantics.Events.TemporalDecomposition.complex r phases activity_in_runtime result_in_runtime).resultPhase = some phases.resultTrace

def Semantics.Events.TemporalDecomposition.isComplex {Time : Type u_1} [LinearOrder Time] : TemporalDecomposition Time → Bool

Is this a complex (phased) decomposition?

Equations

• (Semantics.Events.TemporalDecomposition.simple r).isComplex = false
• (Semantics.Events.TemporalDecomposition.complex r phases activity_in_runtime result_in_runtime).isComplex = true

def Semantics.Events.hasComplexDecomposition : Tense.Aspect.LexicalAspect.VendlerClass → Bool

Telic Vendler classes (accomplishment, achievement) have complex temporal structure with distinguishable activity and result phases. Atelic classes (state, activity) are temporally simple.

Equations

• Semantics.Events.hasComplexDecomposition Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = true
• Semantics.Events.hasComplexDecomposition Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = true
• Semantics.Events.hasComplexDecomposition Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = false
• Semantics.Events.hasComplexDecomposition Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = false

theorem Semantics.Events.hasComplexDecomposition_iff_telic (c : Tense.Aspect.LexicalAspect.VendlerClass) : hasComplexDecomposition c = (c.telicity == Tense.Aspect.LexicalAspect.Telicity.telic)

Complex decomposition ↔ telicity.

structure Semantics.Events.DecomposedEv (Time : Type u_1) [LinearOrder Time] : Type u_1

An event enriched with temporal decomposition information. Extends Ev (which has runtime + sort) with subevent phase structure.

• event : Ev Time

  The underlying event

• decomposition : TemporalDecomposition Time

  Temporal decomposition of the event

• runtime_consistent : self.decomposition.runtime = self.event.runtime

  The decomposition's runtime matches the event's runtime

def Semantics.Events.Ev.withSimpleDecomposition {Time : Type u_1} [LinearOrder Time] (e : Ev Time) : DecomposedEv Time

Attach a simple decomposition to an event (for states/activities).

Equations

• e.withSimpleDecomposition = { event := e, decomposition := Semantics.Events.TemporalDecomposition.simple e.runtime, runtime_consistent := ⋯ }

def Semantics.Events.Ev.withComplexDecomposition {Time : Type u_1} [LinearOrder Time] (e : Ev Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval e.runtime) (h_res : phases.resultTrace.subinterval e.runtime) : DecomposedEv Time

Attach a complex decomposition to an event (for accomplishments/achievements).

Equations

• e.withComplexDecomposition phases h_act h_res = { event := e, decomposition := Semantics.Events.TemporalDecomposition.complex e.runtime phases h_act h_res, runtime_consistent := ⋯ }

theorem Semantics.Events.SubeventPhases.ordering {Time : Type u_1} [LinearOrder Time] (p : SubeventPhases Time) : p.activityTrace.finish ≤ p.resultTrace.start

Activity precedes result in any SubeventPhases (direct accessor).

theorem Semantics.Events.complex_phases_in_runtime {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval rt) (h_res : phases.resultTrace.subinterval rt) : phases.activityTrace.subinterval rt ∧ phases.resultTrace.subinterval rt

Both subevent phases are contained in the overall runtime of a complex decomposition (by construction).

theorem Semantics.Events.simple_no_result {Time : Type u_1} [LinearOrder Time] (r : Core.Time.Interval Time) : (TemporalDecomposition.simple r).resultPhase = none

A simple decomposition has no result phase.

theorem Semantics.Events.simple_no_activity {Time : Type u_1} [LinearOrder Time] (r : Core.Time.Interval Time) : (TemporalDecomposition.simple r).activityPhase = none

A simple decomposition has no activity phase.

def Semantics.Events.phasePred {Time : Type u_1} [LinearOrder Time] (phase : Core.Time.Interval Time) : Tense.Aspect.Core.EventPred Unit Time

Event predicate localized to an interval: holds of eventualities whose runtime equals the given interval. Converts temporal phases of a DecomposedEv into predicates consumable by ViewpointAspect operators (IMPF, PRFV, PERF).

The world parameter is fixed to Unit since temporal decomposition is world-independent (following the same convention as Giannakidou.lean).

Equations

• Semantics.Events.phasePred phase x✝ ev = (ev.runtime = phase)

theorem Semantics.Events.impf_phasePred {Time : Type u_1} [LinearOrder Time] (phase t : Core.Time.Interval Time) : Tense.Aspect.Core.IMPF (phasePred phase) () t ↔ t.properSubinterval phase

IMPF applied to a phase predicate reduces to the reference time being properly inside that phase interval.

theorem Semantics.Events.prfv_phasePred {Time : Type u_1} [LinearOrder Time] (phase t : Core.Time.Interval Time) : Tense.Aspect.Core.PRFV (phasePred phase) () t ↔ phase.subinterval t

PRFV applied to a phase predicate reduces to the phase interval being contained in the reference time.

theorem Semantics.Events.progressive_before_result : ∃ (phases : SubeventPhases ℤ) (t : Core.Time.Interval ℤ), Tense.Aspect.Core.IMPF (phasePred phases.activityTrace) () t ∧ t.isBefore phases.resultTrace

The imperfective paradox via temporal decomposition: IMPF on the activity phase can hold at reference times entirely before the result phase. "Was building a house" doesn't entail a house was built.

Counterexample: activity = [0, 10], result = [15, 20], ref = [3, 7]. The reference [3, 7] is properly inside the activity [0, 10], but entirely before the result [15, 20].

theorem Semantics.Events.perfective_full_entails_result {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : SubeventPhases Time) (h_res : phases.resultTrace.subinterval rt) (t : Core.Time.Interval Time) (h_prfv : Tense.Aspect.Core.PRFV (phasePred rt) () t) : phases.resultTrace.subinterval t

PRFV on the full event entails the result trace is within the reference time. "Built a house" entails the building was completed: the result phase is contained in any reference time that contains the whole event.

Proof: result ⊆ runtime (by h_res) and runtime ⊆ ref (by PRFV), so result ⊆ ref by transitivity.

theorem Semantics.Events.perfective_full_entails_activity {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval rt) (t : Core.Time.Interval Time) (h_prfv : Tense.Aspect.Core.PRFV (phasePred rt) () t) : phases.activityTrace.subinterval t

PRFV on the full event entails the activity trace is within the reference time. The process phase is also covered.

theorem Semantics.Events.perfective_full_covers_phases {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval rt) (h_res : phases.resultTrace.subinterval rt) (t : Core.Time.Interval Time) (h_prfv : Tense.Aspect.Core.PRFV (phasePred rt) () t) : phases.activityTrace.subinterval t ∧ phases.resultTrace.subinterval t

For complex events, PRFV on the full event entails both subevent phases are within the reference time. This is the compositional account of why perfective aspect entails completion for accomplishments.

theorem Semantics.Events.impf_activity_prfv_full_incompatible {Time : Type u_1} [LinearOrder Time] (rt : Core.Time.Interval Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval rt) (t : Core.Time.Interval Time) : Tense.Aspect.Core.IMPF (phasePred phases.activityTrace) () t → ¬Tense.Aspect.Core.PRFV (phasePred rt) () t

IMPF on the activity phase is incompatible with PRFV on the full event at the same reference time: the progressive and perfective can't simultaneously hold for the same temporal window.

Proof: IMPF requires ref ⊂ activity (proper subset). PRFV requires runtime ⊆ ref. Since activity ⊆ runtime (by h_act), we get activity ⊆ ref. Combined with ref ⊆ activity (from IMPF), this forces ref = activity, contradicting the strict inequality in properSubinterval.

structure Semantics.Events.MoensSteedmanProfileextends Semantics.Tense.Aspect.LexicalAspect.AspectualProfile : Type

@cite{moens-steedman-1988} aspectual profile. Extends Vendler's three-feature AspectualProfile with ±consequent state, so the Vendler classification is inherited rather than stipulated. @cite{moens-steedman-1988}

• telicity : Telicity
• duration : Duration
• dynamicity : Dynamicity
• hasConsequentState : Bool

  Whether the event has a persistent result after culmination

instance Semantics.Events.instDecidableEqMoensSteedmanProfile : DecidableEq MoensSteedmanProfile

Equations

• Semantics.Events.instDecidableEqMoensSteedmanProfile = Semantics.Events.instDecidableEqMoensSteedmanProfile.decEq

def Semantics.Events.instDecidableEqMoensSteedmanProfile.decEq (x✝ x✝¹ : MoensSteedmanProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Events.instReprMoensSteedmanProfile : Repr MoensSteedmanProfile

Equations

• Semantics.Events.instReprMoensSteedmanProfile = { reprPrec := Semantics.Events.instReprMoensSteedmanProfile.repr }

def Semantics.Events.instReprMoensSteedmanProfile.repr : MoensSteedmanProfile → ℕ → Std.Format

Equations

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

def Semantics.Events.instBEqMoensSteedmanProfile.beq : MoensSteedmanProfile → MoensSteedmanProfile → Bool

Equations

• Semantics.Events.instBEqMoensSteedmanProfile.beq { toAspectualProfile := a, hasConsequentState := a_1 } { toAspectualProfile := b, hasConsequentState := b_1 } = (a == b && a_1 == b_1)
• Semantics.Events.instBEqMoensSteedmanProfile.beq x✝¹ x✝ = false

instance Semantics.Events.instBEqMoensSteedmanProfile : BEq MoensSteedmanProfile

Equations

• Semantics.Events.instBEqMoensSteedmanProfile = { beq := Semantics.Events.instBEqMoensSteedmanProfile.beq }

inductive Semantics.Events.MoensSteedmanClass : Type

@cite{moens-steedman-1988} five-way event classification. Refines Vendler by splitting achievement along ±consequent state:

Class	Atomic?	+ConsState?	Vendler
state	no	—	state
process	no	no	activity
culminatedProcess	no	yes	accomplishment
culmination	yes	yes	achievement
point	yes	no	(none)

@cite{moens-steedman-1988}

• state : MoensSteedmanClass
• process : MoensSteedmanClass
• culminatedProcess : MoensSteedmanClass
• culmination : MoensSteedmanClass
• point : MoensSteedmanClass

instance Semantics.Events.instDecidableEqMoensSteedmanClass : DecidableEq MoensSteedmanClass

Equations

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

instance Semantics.Events.instReprMoensSteedmanClass : Repr MoensSteedmanClass

Equations

• Semantics.Events.instReprMoensSteedmanClass = { reprPrec := Semantics.Events.instReprMoensSteedmanClass.repr }

def Semantics.Events.instReprMoensSteedmanClass.repr : MoensSteedmanClass → ℕ → Std.Format

Equations

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

instance Semantics.Events.instBEqMoensSteedmanClass : BEq MoensSteedmanClass

Equations

• Semantics.Events.instBEqMoensSteedmanClass = { beq := Semantics.Events.instBEqMoensSteedmanClass.beq }

def Semantics.Events.instBEqMoensSteedmanClass.beq : MoensSteedmanClass → MoensSteedmanClass → Bool

Equations

• Semantics.Events.instBEqMoensSteedmanClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Events.MoensSteedmanClass.toProfile : MoensSteedmanClass → MoensSteedmanProfile

Canonical profile for each M&S event type. The VendlerClass is inherited from AspectualProfile via extends — accessible as c.toProfile.toVendlerClass without a separate mapping function.

Equations

• Semantics.Events.MoensSteedmanClass.state.toProfile = { toAspectualProfile := Semantics.Tense.Aspect.LexicalAspect.stateProfile, hasConsequentState := false }
• Semantics.Events.MoensSteedmanClass.process.toProfile = { toAspectualProfile := Semantics.Tense.Aspect.LexicalAspect.activityProfile, hasConsequentState := false }
• Semantics.Events.MoensSteedmanClass.culminatedProcess.toProfile = { toAspectualProfile := Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile, hasConsequentState := true }
• Semantics.Events.MoensSteedmanClass.culmination.toProfile = { toAspectualProfile := Semantics.Tense.Aspect.LexicalAspect.achievementProfile, hasConsequentState := true }
• Semantics.Events.MoensSteedmanClass.point.toProfile = { toAspectualProfile := Semantics.Tense.Aspect.LexicalAspect.achievementProfile, hasConsequentState := false }

def Semantics.Events.MoensSteedmanClass.isAtomic : MoensSteedmanClass → Bool

Whether the event is atomic (instantaneous).

Equations

• Semantics.Events.MoensSteedmanClass.culmination.isAtomic = true
• Semantics.Events.MoensSteedmanClass.point.isAtomic = true
• Semantics.Events.MoensSteedmanClass.state.isAtomic = false
• Semantics.Events.MoensSteedmanClass.process.isAtomic = false
• Semantics.Events.MoensSteedmanClass.culminatedProcess.isAtomic = false

theorem Semantics.Events.MoensSteedmanClass.point_culmination_vendler_collapse : point.toProfile.toVendlerClass = culmination.toProfile.toVendlerClass ∧ point.toProfile.hasConsequentState ≠ culmination.toProfile.hasConsequentState

Points and culminations share a Vendler class (achievement) but differ in ±consequent state — exactly the conflation Moens & Steedman identify.

theorem Semantics.Events.MoensSteedmanClass.point_telic_without_consState : point.toProfile.telicity = Tense.Aspect.LexicalAspect.Telicity.telic ∧ point.toProfile.hasConsequentState = false

Points are telic (achievements) but lack consequent states — the reason Vendler's classification is too coarse for the perfect.

theorem Semantics.Events.MoensSteedmanClass.isAtomic_iff_punctual (c : MoensSteedmanClass) (h : c ≠ state) : c.isAtomic = (c.toProfile.duration == Tense.Aspect.LexicalAspect.Duration.punctual)

Atomicity matches Vendler's punctuality for dynamic classes.

inductive Semantics.Events.WhenTarget : Type

What when accesses in each event type. M&S's key claim: when has a single meaning (locate the main clause at the culmination), with apparent ambiguity arising from different nucleus structures. @cite{moens-steedman-1988}

• directCulmination : WhenTarget
• completionCoercion : WhenTarget
• inceptionCoercion : WhenTarget
• homogeneousOverlap : WhenTarget

instance Semantics.Events.instDecidableEqWhenTarget : DecidableEq WhenTarget

Equations

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

instance Semantics.Events.instReprWhenTarget : Repr WhenTarget

Equations

• Semantics.Events.instReprWhenTarget = { reprPrec := Semantics.Events.instReprWhenTarget.repr }

def Semantics.Events.instReprWhenTarget.repr : WhenTarget → ℕ → Std.Format

Equations

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

instance Semantics.Events.instBEqWhenTarget : BEq WhenTarget

Equations

• Semantics.Events.instBEqWhenTarget = { beq := Semantics.Events.instBEqWhenTarget.beq }

def Semantics.Events.instBEqWhenTarget.beq : WhenTarget → WhenTarget → Bool

Equations

• Semantics.Events.instBEqWhenTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Events.MoensSteedmanClass.whenTarget : MoensSteedmanClass → WhenTarget

M&S's unified when semantics: one meaning, four behaviors derived from event type.

Equations

• Semantics.Events.MoensSteedmanClass.culmination.whenTarget = Semantics.Events.WhenTarget.directCulmination
• Semantics.Events.MoensSteedmanClass.point.whenTarget = Semantics.Events.WhenTarget.directCulmination
• Semantics.Events.MoensSteedmanClass.culminatedProcess.whenTarget = Semantics.Events.WhenTarget.completionCoercion
• Semantics.Events.MoensSteedmanClass.process.whenTarget = Semantics.Events.WhenTarget.inceptionCoercion
• Semantics.Events.MoensSteedmanClass.state.whenTarget = Semantics.Events.WhenTarget.homogeneousOverlap

theorem Semantics.Events.MoensSteedmanClass.when_needs_coercion_iff (c : MoensSteedmanClass) : c.whenTarget = WhenTarget.completionCoercion ∨ c.whenTarget = WhenTarget.inceptionCoercion ↔ c = culminatedProcess ∨ c = process

Coercion is needed iff the event type is process or culminated process.

structure Semantics.Events.Nucleus (Time : Type u_1) [LinearOrder Time] : Type u_1

The @cite{moens-steedman-1988} nucleus: tripartite event structure for events with a culmination point. Makes the culmination explicit — it is implicit in SubeventPhases as the boundary between activityTrace and resultTrace.

SubeventPhases: |---activity---| |---result---|
Nucleus: |---prep-------|•c |---cons-----|
                                 ↑
                         explicit culmination

@cite{moens-steedman-1988}

• prepProcess : Option (Core.Time.Interval Time)

  Preparatory process leading to culmination

• culmination : Time

  The culmination point: instantaneous transition

• consState : Option (Core.Time.Interval Time)

  Consequent state persisting after culmination

• prep_le_culm (i : Core.Time.Interval Time) : self.prepProcess = some i → i.finish ≤ self.culmination

  Prep process ends at or before culmination

• culm_le_cons (i : Core.Time.Interval Time) : self.consState = some i → self.culmination ≤ i.start

  Consequent state starts at or after culmination

def Semantics.Events.Nucleus.eventType {Time : Type u_1} [LinearOrder Time] (n : Nucleus Time) : MoensSteedmanClass

The M&S event type determined by which components are present.

Equations

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

def Semantics.Events.Nucleus.toSubeventPhases {Time : Type u_1} [LinearOrder Time] (n : Nucleus Time) (prep cons : Core.Time.Interval Time) (h_prep : n.prepProcess = some prep) (h_cons : n.consState = some cons) : SubeventPhases Time

A full nucleus (both prep and cons present) yields SubeventPhases. The ordering proof follows from transitivity through the culmination.

Equations

• n.toSubeventPhases prep cons h_prep h_cons = { activityTrace := prep, resultTrace := cons, activity_precedes_result := ⋯ }

theorem Semantics.Events.Nucleus.full_is_culminatedProcess {Time : Type u_1} [LinearOrder Time] (n : Nucleus Time) {p c : Core.Time.Interval Time} (hp : n.prepProcess = some p) (hc : n.consState = some c) : n.eventType = MoensSteedmanClass.culminatedProcess

A full nucleus has event type culminatedProcess.

theorem Semantics.Events.Nucleus.hasConsState_of_consState {Time : Type u_1} [LinearOrder Time] (n : Nucleus Time) {c : Core.Time.Interval Time} (hc : n.consState = some c) : n.eventType.toProfile.hasConsequentState = true

A nucleus with consequent state has M&S's consequent state feature.