Documentation

Linglib.Theories.Semantics.Events.Basic

Neo-Davidsonian Event Semantics — basic API #

API on top of Events/Defs.lean's foundational types: sort predicates, EventSort ↔ Aktionsart Dynamicity bridge, concrete examples on ℤ-time.

Files that only need to talk about events should import Defs.lean directly to avoid pulling in Features.Aktionsart.

Main definitions #

Sort predicates #

source
def Semantics.Events.Event.isAction {Time : Type u_1} [LinearOrder Time] (e : Event Time) :
Prop

Is this event an action (dynamic event)?

Equations
Instances For
    source
    def Semantics.Events.Event.isState {Time : Type u_1} [LinearOrder Time] (e : Event Time) :
    Prop

    Is this event a state (stative event)?

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Events.instDecidablePredEventIsAction {Time : Type u_1} [LinearOrder Time] :
      DecidablePred Event.isAction
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Events.instDecidablePredEventIsState {Time : Type u_1} [LinearOrder Time] :
      DecidablePred Event.isState
      Equations
      source
      theorem Semantics.Events.sort_exhaustive (s : EventSort) :
      s = EventSort.action ∨ s = EventSort.state

      Every event is either an action or a state (exhaustivity).

      source
      theorem Semantics.Events.sort_exclusive :
      EventSort.action ≠ EventSort.state

      No event is both an action and a state (exclusivity).

      source
      theorem Semantics.Events.isAction_iff_not_isState {Time : Type u_1} [LinearOrder Time] (e : Event Time) :
      e.isAction ↔ ¬e.isState

      isAction and isState are complementary.

      source
      theorem Semantics.Events.isState_iff_not_isAction {Time : Type u_1} [LinearOrder Time] (e : Event Time) :
      e.isState ↔ ¬e.isAction

      isState and isAction are complementary.

      Dynamicity Bridge (EventSort ↔ Aktionsart) #

      source
      def Semantics.Events.EventSort.toDynamicity :
      EventSort → Features.Dynamicity

      Map EventSort to Dynamicity (the aspectual feature).

      Equations
      Instances For
        source
        def Semantics.Events.dynamicityToEventSort :
        Features.Dynamicity → EventSort

        Map Dynamicity back to EventSort.

        Equations
        Instances For
          source
          theorem Semantics.Events.dynamicity_roundtrip (d : Features.Dynamicity) :
          (dynamicityToEventSort d).toDynamicity = d

          Roundtrip: toDynamicity ∘ dynamicityToEventSort = id.

          source
          theorem Semantics.Events.eventSort_roundtrip (s : EventSort) :
          dynamicityToEventSort s.toDynamicity = s

          Roundtrip: dynamicityToEventSort ∘ toDynamicity = id.

          source
          theorem Semantics.Events.vendlerClass_sort_agrees (c : Features.VendlerClass) :
          dynamicityToEventSort c.dynamicity = match c with | Features.VendlerClass.state => EventSort.state | Features.VendlerClass.activity => EventSort.action | Features.VendlerClass.achievement => EventSort.action | Features.VendlerClass.accomplishment => EventSort.action | Features.VendlerClass.semelfactive => EventSort.action

          VendlerClass dynamicity agrees with EventSort classification. States map to .state sort; all others map to .action sort.

          Concrete examples (ℤ-time events) #

          source
          def Semantics.Events.exampleRun :
          Event ℤ

          Example: a running event from time 1 to 5.

          Equations
          Instances For
            source
            def Semantics.Events.exampleKnow :
            Event ℤ

            Example: a knowing state from time 0 to 10.

            Equations
            Instances For
              source
              theorem Semantics.Events.exampleRun_isAction :
              exampleRun.isAction

              The run event is an action.

              source
              theorem Semantics.Events.exampleKnow_isState :
              exampleKnow.isState

              The know event is a state.

              source
              theorem Semantics.Events.exampleRun_not_state :
              ¬exampleRun.isState

              The run event is not a state.

              source
              theorem Semantics.Events.exampleKnow_not_action :
              ¬exampleKnow.isAction

              The know event is not an action.

              source
              theorem Semantics.Events.exampleRun_start :
              exampleRun.τ.start = 1

              The run event starts at 1.

              source
              theorem Semantics.Events.exampleRun_finish :
              exampleRun.τ.finish = 5

              The run event ends at 5.

              source
              theorem Semantics.Events.exampleKnow_runtime :
              exampleKnow.τ.start = 0 ∧ exampleKnow.τ.finish = 10

              The know event spans 0 to 10.