Documentation

Linglib.Theories.Semantics.Events.DegreeEvents

Degree Events @cite{zhao-2025} #

Gradable predicates introduce events with degree traces τ_d parallel to temporal traces τ_i. Comparison involves thematic roles [STD], [TAR], [DIFF] that relate events to degree intervals.

This extends the neo-Davidsonian event ontology (Ev) with a degree dimension, following Zhao's cross-domain parallel:

Temporal domainDegree domain
τ_i : Event → Interval Tτ_d : Event → Interval D
AGENT, THEME rolesSTD, TAR, DIFF roles
States: ATOM-DIST_tBare comp: ATOM-DIST_d
source
structure Semantics.Events.DegreeEvents.DegreeEv (Time : Type u_1) (Deg : Type u_2) [LE Time] [LE Deg] :
Type (max u_1 u_2)

A degree event: an event with both temporal and degree traces. Extends the standard Ev (which has temporal trace τ_i = runtime) with a degree trace τ_d.

  • base : Ev Time

    The underlying temporal event

  • degTrace : Core.Time.Interval Deg

    Degree trace: the interval on the degree scale spanned by this event

Instances For
    source
    def Semantics.Events.DegreeEvents.DegreeEv.τ_i {Time : Type u_1} {Deg : Type u_2} [LE Time] [LE Deg] (e : DegreeEv Time Deg) :
    Core.Time.Interval Time

    Temporal trace τ_i of a degree event (inherited from base).

    Equations
    Instances For
      source
      def Semantics.Events.DegreeEvents.DegreeEv.τ_d {Time : Type u_1} {Deg : Type u_2} [LE Time] [LE Deg] (e : DegreeEv Time Deg) :
      Core.Time.Interval Deg

      Degree trace τ_d of a degree event.

      Equations
      Instances For
        source
        inductive Semantics.Events.DegreeEvents.ComparisonRole :
        Type

        Comparison thematic roles. In comparative constructions, events have participants playing degree-related roles analogous to standard thematic roles.

        Instances For
          source
          instance Semantics.Events.DegreeEvents.instDecidableEqComparisonRole :
          DecidableEq ComparisonRole
          Equations
          source
          instance Semantics.Events.DegreeEvents.instReprComparisonRole :
          Repr ComparisonRole
          Equations
          source
          def Semantics.Events.DegreeEvents.instReprComparisonRole.repr :
          ComparisonRole → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance Semantics.Events.DegreeEvents.instBEqComparisonRole :
            BEq ComparisonRole
            Equations
            source
            def Semantics.Events.DegreeEvents.instBEqComparisonRole.beq :
            ComparisonRole → ComparisonRole → Bool
            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Semantics.Events.DegreeEvents.DegEvPred (Time : Type u_1) (Deg : Type u_2) [LE Time] [LE Deg] :
              Type (max u_2 u_1)

              A predicate over degree events (not world-indexed).

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Semantics.Events.DegreeEvents.DegEvPredW (W : Type u_1) (Time : Type u_2) (Deg : Type u_3) [LE Time] [LE Deg] :
                Type (max (max u_1 u_3) u_2)

                A world-indexed predicate over degree events.

                Equations
                Instances For
                  source
                  def Semantics.Events.DegreeEvents.degExistsClosure {Time : Type u_1} {Deg : Type u_2} [LE Time] [LE Deg] (P : DegEvPred Time Deg) :
                  Prop

                  Existential closure for degree events.

                  Equations
                  Instances For