Documentation

Linglib.Theories.Semantics.Tense.TemporalAdverbials

source
@[reducible, inline]
abbrev Semantics.Montague.Sentence.TemporalAdverbials.PTSConstraint (Time : Type u_3) [LE Time] :
Type u_3

A constraint on the Perfect Time Span. Adverbials restrict which PTS intervals are admissible.

Equations
Instances For
    source
    inductive Semantics.Montague.Sentence.TemporalAdverbials.AdverbialType :
    Type

    @cite{iatridou-anagnostopoulou-izvorski-2001} adverbial type classification.

    • durative: specifies the left boundary (e.g., "since Monday")
    • inclusive: does not specify the left boundary (e.g., "before Monday")
    Instances For
      source
      instance Semantics.Montague.Sentence.TemporalAdverbials.instDecidableEqAdverbialType :
      DecidableEq AdverbialType
      Equations
      source
      instance Semantics.Montague.Sentence.TemporalAdverbials.instReprAdverbialType :
      Repr AdverbialType
      Equations
      source
      def Semantics.Montague.Sentence.TemporalAdverbials.instReprAdverbialType.repr :
      AdverbialType → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Semantics.Montague.Sentence.TemporalAdverbials.instBEqAdverbialType :
        BEq AdverbialType
        Equations
        source
        def Semantics.Montague.Sentence.TemporalAdverbials.instBEqAdverbialType.beq :
        AdverbialType → AdverbialType → Bool
        Equations
        Instances For
          source
          def Semantics.Montague.Sentence.TemporalAdverbials.everSince {Time : Type u_2} [LinearOrder Time] (t₀ : Time) :
          PTSConstraint Time

          "ever since t₀": PTS must start at t₀. E.g., "has been running since Monday" → PTS.start = Monday.

          Equations
          Instances For
            source
            def Semantics.Montague.Sentence.TemporalAdverbials.forDurationFrom {Time : Type u_2} [LinearOrder Time] (tStart : Time) :
            PTSConstraint Time

            "for (duration) from tStart": PTS must start at tStart. Simplified duration adverbial — the duration is implicit in the interval length [tStart, RB].

            Equations
            Instances For
              source
              def Semantics.Montague.Sentence.TemporalAdverbials.always {Time : Type u_2} [LinearOrder Time] :
              PTSConstraint Time

              "always" / no temporal adverbial: no constraint on PTS.

              Equations
              Instances For
                source
                def Semantics.Montague.Sentence.TemporalAdverbials.before {Time : Type u_2} [LinearOrder Time] :
                PTSConstraint Time

                "before t" (inclusive adverbial): no constraint on PTS start. The adverbial constrains the event location, not the PTS boundary.

                Equations
                Instances For
                  source
                  def Semantics.Montague.Sentence.TemporalAdverbials.PTSConstraint.toLBDomain {Time : Type u_2} [LinearOrder Time] (adv : PTSConstraint Time) (tc : Time) :
                  Set Time

                  Convert a PTS constraint to a domain of compatible LB values, given that the right boundary is fixed at tc.

                  For a constraint C, the compatible LBs are those tLB ≤ tc such that C holds of the interval [tLB, tc].

                  Equations
                  Instances For
                    source
                    def Semantics.Montague.Sentence.TemporalAdverbials.PERF_ADV {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Tense.Aspect.Core.IntervalPred W Time) (adv : PTSConstraint Time) :
                    Tense.Aspect.Core.PointPred W Time

                    Perfect with adverbial constraint: PERF_ADV(p, adv). Combines PERF with an adverbial constraint on the PTS. Equivalent to PERF_XN with the adverbial's derived LB domain.

                    Equations
                    Instances For
                      source
                      def Semantics.Montague.Sentence.TemporalAdverbials.AdverbialType.specifiesLB :
                      AdverbialType → Bool

                      Does this adverbial type specify the left boundary? Durative adverbials pin the LB; inclusive adverbials leave it free.

                      Equations
                      Instances For
                        source
                        theorem Semantics.Montague.Sentence.TemporalAdverbials.perf_adv_eq_perf_xn {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Tense.Aspect.Core.IntervalPred W Time) (adv : PTSConstraint Time) (tc : Time) (w : W) :
                        PERF_ADV p adv { world := w, time := tc } ↔ Tense.Aspect.Core.PERF_XN p (adv.toLBDomain tc) { world := w, time := tc }

                        PERF_ADV is equivalent to PERF_XN with the adverbial's derived LB domain.

                        Proof sketch: Both existentially quantify over a PTS with RB = tc. PERF_ADV requires adv(PTS); PERF_XN requires LB(tLB, PTS) with tLB ∈ toLBDomain(adv, tc). These are equivalent by definition of toLBDomain: tLB ∈ toLBDomain ↔ tLB ≤ tc ∧ adv([tLB, tc]).

                        source
                        theorem Semantics.Montague.Sentence.TemporalAdverbials.everSince_specifies_lb {Time : Type u_2} [LinearOrder Time] (t₀ tc : Time) (h : t₀ ≤ tc) :
                        (everSince t₀).toLBDomain tc = {t₀}

                        "ever since t₀" specifies the LB domain to exactly {t₀} (assuming t₀ ≤ tc).

                        Proof sketch: toLBDomain(everSince t₀, tc) = {tLB | tLB ≤ tc ∧ tLB = t₀} = {t₀} when t₀ ≤ tc.

                        source
                        theorem Semantics.Montague.Sentence.TemporalAdverbials.before_no_lb_constraint {Time : Type u_2} [LinearOrder Time] (tc : Time) :
                        before.toLBDomain tc = {tLB : Time | tLB ≤ tc}

                        "before" imposes no LB constraint: all tLB ≤ tc are compatible.

                        Proof sketch: toLBDomain(before, tc) = {tLB | tLB ≤ tc ∧ True} = {tLB | tLB ≤ tc}.

                        source
                        theorem Semantics.Montague.Sentence.TemporalAdverbials.durative_licenses_u_perfect {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Tense.Aspect.Core.EventPred W Time) (t₀ tc : Time) (w : W) (_h : t₀ ≤ tc) :
                        TenseAspectComposition.presPerfProgXN V {t₀} tc w → TenseAspectComposition.simplePresent V tc w

                        Durative adverbials (specified LB) license U-perf → simple present.

                        When the LB is pinned (durative adverbial), the U-perf reading entails the simple present via u_perf_entails_simple_present.

                        source
                        theorem Semantics.Montague.Sentence.TemporalAdverbials.inclusive_no_u_license {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Tense.Aspect.Core.EventPred W Time) (tc : Time) (w : W) :
                        TenseAspectComposition.presPerfProgXN V Set.univ tc w ↔ TenseAspectComposition.simplePresent V tc w

                        Inclusive adverbials (unspecified LB) yield U-perf ↔ simple present when the LB domain is maximal.

                        With no LB constraint, the domain is {tLB | tLB ≤ tc}. Under IMPF (subinterval property), this is close to Set.univ for the relevant range, so U-perf ↔ simple present by broad_focus_equiv's argument.