diff --git a/Linglib.lean b/Linglib.lean index 108374d9e..6afde3385 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -2398,7 +2398,6 @@ import Linglib.Semantics.Aspect.ChangeOfState -- Theories: Semantics.Iconic (Iconological Semantics for sign language) import Linglib.Semantics.Iconic.Basic -- Theories: Semantics.Events (neo-Davidsonian) -import Linglib.Semantics.Events.Defs import Linglib.Semantics.Events.Basic import Linglib.Semantics.ArgumentStructure.Defs import Linglib.Semantics.Events.CEM diff --git a/Linglib/Semantics/ArgumentStructure/Defs.lean b/Linglib/Semantics/ArgumentStructure/Defs.lean index 3edf683f5..440cfd74a 100644 --- a/Linglib/Semantics/ArgumentStructure/Defs.lean +++ b/Linglib/Semantics/ArgumentStructure/Defs.lean @@ -1,4 +1,4 @@ -import Linglib.Semantics.Events.Defs +import Linglib.Semantics.Events.Basic import Linglib.Core.Word import Linglib.Semantics.ArgumentStructure.Linking diff --git a/Linglib/Semantics/Events/Basic.lean b/Linglib/Semantics/Events/Basic.lean index 81b5e4b25..954a7505f 100644 --- a/Linglib/Semantics/Events/Basic.lean +++ b/Linglib/Semantics/Events/Basic.lean @@ -1,51 +1,95 @@ -import Linglib.Semantics.Events.Defs +import Mathlib.Order.Basic +import Linglib.Core.Time.Interval.Basic +import Linglib.Tactics.OntSort import Linglib.Features.Aktionsart /-! -# Neo-Davidsonian Event Semantics — basic API +# Neo-Davidsonian Event Semantics -API on top of `Events/Defs.lean`'s foundational types: sort predicates over -the `Features.Dynamicity` event sort, and concrete examples on `ℤ`-time. - -Files that only need to *talk about* events should import `Defs.lean` -directly. +Foundational types and basic API for neo-Davidsonian event semantics +(@cite{davidson-1967}, @cite{parsons-1990}). Verbs denote predicates of +events; thematic roles are independent two-place predicates +(`Semantics.ArgumentStructure.ThematicRel`). ## Main definitions +* `Event` — the unified event type: a runtime interval + `Features.Dynamicity` sort +* `Event.τ` — temporal trace function * `Event.isAction` / `Event.isState` — decidable `Prop` sort predicates (the `dynamic` / `stative` poles of `Features.Dynamicity`) +* `Event.isPunctual` / `Event.isDurative` — decidable `Prop` duration predicates +* `Event.existsClosure` — Davidsonian existential closure +* `Event.Mereology` — part-of typeclass with τ-monotonicity + sort-preservation +* `Event.preorder` — Preorder instance derived from `Event.Mereology` +* `Event.Manner` — manner ontology (@cite{liefke-2024} §4.3) * `exampleRun` / `exampleKnow` — concrete `Event ℤ` instances + +## Naming note + +`Event` is the unified type for linguistic events. The Bach 1981/1986 +distinction between "eventuality" (genus, sortless) and "event" (narrow +sense, non-state) has largely collapsed in current practice — +@cite{champollion-2017} and @cite{zhao-2025} both use "event" +generically with sort/aktionsart as an inherent attribute. Tense-aspect +code that doesn't care about sort simply doesn't reference `.sort`; +sortless construction sites default to `.dynamic`. + +## References + +* @cite{davidson-1967}, @cite{parsons-1990} (neo-Davidsonian foundations) +* @cite{bach-1986} (action/state ontology) +* @cite{krifka-1989} (interval-valued runtimes) +* @cite{champollion-2017}, @cite{zhao-2025} (event-as-generic) +* @cite{liefke-2024} §4.3 (manner ontology) -/ open Core.Time open Features +/-- An event: a temporal individual with ontological sort. -/ +@[ont_sort] structure Event (Time : Type*) [LinearOrder Time] where + /-- The temporal extent of this event -/ + runtime : Interval Time + /-- Ontological sort (aktionsart): `dynamic` or `stative` (@cite{bach-1986}). + This is the `Features.Dynamicity` feature — the action/state distinction + at the event-token level. -/ + sort : Features.Dynamicity + +namespace Event + +variable {Time : Type*} [LinearOrder Time] + +/-! ### Temporal trace -/ + +/-- Temporal trace function τ(e) = the runtime interval of event e. -/ +@[simp] +def τ (e : Event Time) : Interval Time := + e.runtime + /-! ### Sort predicates -/ /-- Is this event an action (dynamic event)? -/ -def Event.isAction {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := +def isAction (e : Event Time) : Prop := e.sort = .dynamic /-- Is this event a state (stative event)? -/ -def Event.isState {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := +def isState (e : Event Time) : Prop := e.sort = .stative -instance {Time : Type*} [LinearOrder Time] : - DecidablePred (Event.isAction (Time := Time)) := +instance : DecidablePred (isAction (Time := Time)) := fun e => decEq e.sort .dynamic -instance {Time : Type*} [LinearOrder Time] : - DecidablePred (Event.isState (Time := Time)) := +instance : DecidablePred (isState (Time := Time)) := fun e => decEq e.sort .stative /-- `isAction` and `isState` are complementary. -/ -theorem isAction_iff_not_isState {Time : Type*} [LinearOrder Time] (e : Event Time) : +theorem isAction_iff_not_isState (e : Event Time) : e.isAction ↔ ¬ e.isState := by simp only [Event.isAction, Event.isState] cases e.sort <;> decide /-- `isState` and `isAction` are complementary. -/ -theorem isState_iff_not_isAction {Time : Type*} [LinearOrder Time] (e : Event Time) : +theorem isState_iff_not_isAction (e : Event Time) : e.isState ↔ ¬ e.isAction := by simp only [Event.isAction, Event.isState] cases e.sort <;> decide @@ -55,25 +99,77 @@ theorem isState_iff_not_isAction {Time : Type*} [LinearOrder Time] (e : Event Ti /-- Is this event punctual (instantaneous)? Its runtime is a single point. The temporal-extent counterpart of the dynamicity sort; derived from the runtime via `Interval.IsPoint`. -/ -def Event.isPunctual {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := +def isPunctual (e : Event Time) : Prop := e.τ.IsPoint /-- Is this event durative (temporally extended)? -/ -def Event.isDurative {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := +def isDurative (e : Event Time) : Prop := ¬ e.isPunctual -instance {Time : Type*} [LinearOrder Time] : - DecidablePred (Event.isPunctual (Time := Time)) := +instance : DecidablePred (isPunctual (Time := Time)) := fun e => by unfold Event.isPunctual Interval.IsPoint; infer_instance -instance {Time : Type*} [LinearOrder Time] : - DecidablePred (Event.isDurative (Time := Time)) := +instance : DecidablePred (isDurative (Time := Time)) := fun e => by unfold Event.isDurative; infer_instance /-- `isDurative` and `isPunctual` are complementary. -/ -theorem isDurative_iff_not_isPunctual {Time : Type*} [LinearOrder Time] (e : Event Time) : +theorem isDurative_iff_not_isPunctual (e : Event Time) : e.isDurative ↔ ¬ e.isPunctual := Iff.rfl +/-! ### Existential closure -/ + +/-- Existential closure: ∃e. P(e). The fundamental step from event + semantics to truth conditions. -/ +def existsClosure (P : Event Time → Prop) : Prop := + ∃ e : Event Time, P e + +/-! ### Mereology -/ + +/-- Axioms for event part-of structure. Part-of is a partial order on + events with temporal and sort constraints. -/ +class Mereology (Time : Type*) [LinearOrder Time] where + /-- e₁ is a part of e₂ -/ + partOf : Event Time → Event Time → Prop + /-- Part-of is reflexive -/ + refl : ∀ e, partOf e e + /-- Part-of is antisymmetric -/ + antisymm : ∀ e₁ e₂, partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂ + /-- Part-of is transitive -/ + trans : ∀ e₁ e₂ e₃, partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃ + /-- τ is monotone: if e₁ ⊑ e₂ then τ(e₁) ⊆ τ(e₂) -/ + τ_monotone : ∀ e₁ e₂, partOf e₁ e₂ → + e₁.runtime.subinterval e₂.runtime + /-- Sort is preserved under part-of: parts of actions are actions, + parts of states are states -/ + sort_preserved : ∀ e₁ e₂, partOf e₁ e₂ → e₁.sort = e₂.sort + +/-- Event mereology induces a Preorder. -/ +instance preorder (Time : Type*) [LinearOrder Time] + [m : Mereology Time] : Preorder (Event Time) where + le := m.partOf + le_refl := m.refl + le_trans := m.trans + +/-! ### Manner -/ + +/-- A manner: the "how" of an event, individuated as an equivalence class + of events under a similarity relation (@cite{liefke-2024} §4.3). + Manners are to events what properties are to individuals. -/ +@[ont_sort] structure Manner (Time : Type*) [LinearOrder Time] where + /-- The characteristic predicate: which events exhibit this manner -/ + exhibits : Event Time → Prop + +/-- The manner of an event under a similarity criterion. + `e.manner sim` gives the manner class of `e` under `sim`. -/ +def manner (e : Event Time) (sim : Event Time → Event Time → Prop) : Manner Time := + ⟨sim e⟩ + +/-- Two events share a manner iff both satisfy the manner predicate. -/ +def Manner.sharedBy (m : Manner Time) (e₁ e₂ : Event Time) : Prop := + m.exhibits e₁ ∧ m.exhibits e₂ + +end Event + /-! ### Concrete examples (ℤ-time events) -/ /-- Example: a running event from time 1 to 5. -/ @@ -96,6 +192,9 @@ theorem exampleRun_not_state : ¬ exampleRun.isState := by decide /-- The know event is not an action. -/ theorem exampleKnow_not_action : ¬ exampleKnow.isAction := by decide +/-- The run event is durative. -/ +theorem exampleRun_isDurative : exampleRun.isDurative := by decide + /-- The run event starts at 1. -/ theorem exampleRun_start : exampleRun.τ.start = 1 := rfl diff --git a/Linglib/Semantics/Events/Defs.lean b/Linglib/Semantics/Events/Defs.lean deleted file mode 100644 index 86586db58..000000000 --- a/Linglib/Semantics/Events/Defs.lean +++ /dev/null @@ -1,115 +0,0 @@ -import Mathlib.Order.Basic -import Linglib.Core.Time.Interval.Basic -import Linglib.Tactics.OntSort -import Linglib.Features.Aktionsart - -/-! -# Neo-Davidsonian Event Semantics — type definitions - -Foundational types for neo-Davidsonian event semantics -(@cite{davidson-1967}, @cite{parsons-1990}). Verbs denote predicates of -events; thematic roles are independent two-place predicates -(`Semantics.ArgumentStructure.ThematicRel`). - -This file is the `Defs` partner to `Basic.lean`: pure type/structure -declarations and one foundational typeclass + instance, no API. Files -that only need to *talk about* events (taking `Event Time` as an -argument, parameterizing by `[Event.Mereology Time]`) can import this -file alone; files that need sort predicates, dynamicity bridges, or -Davidsonian existential closure import `Basic.lean`. - -## Main definitions - -* `Event` — the unified event type: a runtime interval + `Features.Dynamicity` sort -* `Event.τ` — temporal trace function -* `Event.Mereology` — part-of typeclass with τ-monotonicity + sort-preservation -* `Event.preorder` — Preorder instance derived from `Event.Mereology` -* `Event.existsClosure` — Davidsonian existential closure -* `Event.Manner` — manner ontology (@cite{liefke-2024} §4.3) - -## Naming note - -`Event` is the unified type for linguistic events. The Bach 1981/1986 -distinction between "eventuality" (genus, sortless) and "event" (narrow -sense, non-state) has largely collapsed in current practice — -@cite{champollion-2017} and @cite{zhao-2025} both use "event" -generically with sort/aktionsart as an inherent attribute. Tense-aspect -code that doesn't care about sort simply doesn't reference `.sort`; -sortless construction sites default to `.dynamic`. - -## References - -* @cite{davidson-1967}, @cite{parsons-1990} (neo-Davidsonian foundations) -* @cite{bach-1986} (action/state ontology) -* @cite{krifka-1989} (interval-valued runtimes) -* @cite{champollion-2017}, @cite{zhao-2025} (event-as-generic) -* @cite{liefke-2024} §4.3 (manner ontology) --/ - -open Core.Time - -/-- An event: a temporal individual with ontological sort. -/ -@[ont_sort] structure Event (Time : Type*) [LinearOrder Time] where - /-- The temporal extent of this event -/ - runtime : Interval Time - /-- Ontological sort (aktionsart): `dynamic` or `stative` (@cite{bach-1986}). - This is the `Features.Dynamicity` feature — the action/state distinction - at the event-token level. -/ - sort : Features.Dynamicity - -namespace Event - -variable {Time : Type*} [LinearOrder Time] - -/-- Temporal trace function τ(e) = the runtime interval of event e. -/ -@[simp] -def τ (e : Event Time) : Interval Time := - e.runtime - -/-- Existential closure: ∃e. P(e). The fundamental step from event - semantics to truth conditions. -/ -def existsClosure (P : Event Time → Prop) : Prop := - ∃ e : Event Time, P e - -/-- Axioms for event part-of structure. Part-of is a partial order on - events with temporal and sort constraints. -/ -class Mereology (Time : Type*) [LinearOrder Time] where - /-- e₁ is a part of e₂ -/ - partOf : Event Time → Event Time → Prop - /-- Part-of is reflexive -/ - refl : ∀ e, partOf e e - /-- Part-of is antisymmetric -/ - antisymm : ∀ e₁ e₂, partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂ - /-- Part-of is transitive -/ - trans : ∀ e₁ e₂ e₃, partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃ - /-- τ is monotone: if e₁ ⊑ e₂ then τ(e₁) ⊆ τ(e₂) -/ - τ_monotone : ∀ e₁ e₂, partOf e₁ e₂ → - e₁.runtime.subinterval e₂.runtime - /-- Sort is preserved under part-of: parts of actions are actions, - parts of states are states -/ - sort_preserved : ∀ e₁ e₂, partOf e₁ e₂ → e₁.sort = e₂.sort - -/-- Event mereology induces a Preorder. -/ -instance preorder (Time : Type*) [LinearOrder Time] - [m : Mereology Time] : Preorder (Event Time) where - le := m.partOf - le_refl := m.refl - le_trans := m.trans - -/-- A manner: the "how" of an event, individuated as an equivalence class - of events under a similarity relation (@cite{liefke-2024} §4.3). - Manners are to events what properties are to individuals. -/ -@[ont_sort] structure Manner (Time : Type*) [LinearOrder Time] where - /-- The characteristic predicate: which events exhibit this manner -/ - exhibits : Event Time → Prop - -/-- The manner of an event under a similarity criterion. - `e.manner sim` gives the manner class of `e` under `sim`. -/ -def manner (e : Event Time) (sim : Event Time → Event Time → Prop) : Manner Time := - ⟨sim e⟩ - -/-- Two events share a manner iff both satisfy the manner predicate. -/ -def Manner.sharedBy (m : Manner Time) (e₁ e₂ : Event Time) : Prop := - m.exhibits e₁ ∧ m.exhibits e₂ - -end Event