Documentation

Linglib.Theories.Semantics.Dynamic.Systems.DynamicGQ.HigherOrder

Higher-Order Dynamic Generalized Quantifiers #

@cite{barker-shan-2014} @cite{charlow-2021}

@cite{charlow-2021}'s first solution to cumulative readings: higher-order dynamic GQs using a "tower" continuation type. A modified numeral like "exactly 3" denotes a scope-taking dynamic meaning — type ((DRS S → DRS S) → DRS S) → DRS S — rather than a flat DRS S.

The key insight: the tower structure allows the nuclear scope (VP body) to be placed INSIDE maximization while the cardinality test escapes OUTSIDE, producing genuine cumulative readings via LOWER.

The simpler HODGQ type (DRS S → DRS S) → DRS S (= Cont (DRS S) (DRS S)) cannot achieve this because its continuation receives an already-maximized flat DRS — the nuclear scope can only be placed outside maximization.

source
@[reducible, inline]
abbrev Semantics.Dynamic.DynamicGQ.HigherOrder.HODGQ (S : Type u_3) :
Type u_3

Higher-order dynamic GQ: a continuized DRS. Type: (DRS S → DRS S) → DRS S. This is Cont (DRS S) (DRS S), useful for scope-taking in general but insufficient for cumulative readings (see TowerGQ below).

Equations
Instances For
    source
    def Semantics.Dynamic.DynamicGQ.HigherOrder.liftGQ {S : Type u_1} (D : Core.DynamicTy2.DRS S) :
    HODGQ S

    Lift a flat DRS to higher-order (trivially scope-taking). This is Cont.pure specialized to DRS.

    Equations
    Instances For
      source
      def Semantics.Dynamic.DynamicGQ.HigherOrder.lowerGQ {S : Type u_1} (m : HODGQ S) :
      Core.DynamicTy2.DRS S

      Lower a higher-order GQ back to flat DRS. Applies the identity continuation.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Semantics.Dynamic.DynamicGQ.HigherOrder.TowerGQ (S : Type u_3) :
        Type u_3

        Tower-type dynamic GQ (@cite{charlow-2021} §3, equation 24).

        The continuation receives a scope-taking function DRS S → DRS S rather than a flat DRS. This allows the nuclear scope (VP body) to be placed INSIDE maximization while the cardinality test escapes outside.

        In Barker & Shan's tower notation, this is [DRS S | DRS S → DRS S], the type of an expression that contributes a DRS S → DRS S at the local level but produces a DRS S at the top level.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Dynamic.DynamicGQ.HigherOrder.exactlyN_tower {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v : Core.DynamicTy2.Dref S E) (P : E → Prop) (n : ℕ) :
          TowerGQ S

          "Exactly N" as tower GQ (equation 24): λk. k(λbody. M_v(E^v P; body)); n_v

          The continuation k receives a scope-taker λbody. M_v(E^v P; body), allowing the nuclear scope to be threaded inside maximization. The cardinality test n_v is placed OUTSIDE the continuation, ensuring it scopes over any embedded operators.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Semantics.Dynamic.DynamicGQ.HigherOrder.cumulativeTower {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Core.DynamicTy2.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) :
            Core.DynamicTy2.DRS S

            The cumulative derivation (equation 27) via tower composition.

            For "exactly 3 boys saw exactly 5 movies" (cumulative reading):

            • The outer tower (boys) receives the inner tower's result as its body
            • The inner tower (movies) receives the relation saw' as its body
            • Both cardinality tests end up OUTSIDE both maximizations

            This is the derivation that ONLY the tower system can produce; the pointwise system from Basic.lean is limited to pseudo-cumulative.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Semantics.Dynamic.DynamicGQ.HigherOrder.ho_cumulative_derivation {S : Type u_1} {E : Type u_2} [Core.DynamicTy2.AssignmentStructure S E] [PartialOrder E] [Fintype E] (v u : Core.DynamicTy2.Dref S E) (boys movies : E → Prop) (saw' : E → E → Prop) :
              cumulativeTower v u boys movies saw' = Basic.cumulative v u boys movies saw'

              The tower derivation produces exactly the cumulative logical form.

              The higher-order derivation threads the saw' relation through both maximization operators, placing both cardinality tests OUTSIDE: M_v(E^v boys; M_u(E^u movies; saw')); 5_u; 3_v

              This matches cumulative from Basic.lean and is what distinguishes the cumulative reading from the pseudo-cumulative reading, where at least one cardinality test is trapped inside a maximization operator.