Documentation

Linglib.Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism

Subtype Polymorphism for Dynamic GQs #

@cite{charlow-2021}

@cite{charlow-2021}'s §4: a type system that distinguishes "complete" (T) from "incomplete" (t) dynamic meanings. Modified numerals contribute incomplete meanings (the cardinality test hasn't fired yet), and maximization expects incomplete input. The subtyping relation t ⊏ T ensures that incomplete meanings can be used where complete ones are expected, but NOT vice versa.

This blocks the pseudo-cumulative reading: the cardinality test forces completion (T) inside M_v's scope, but M_v requires its argument to be incomplete (t). The cumulative reading is well-typed because cardinality tests scope outside M_v.

source
inductive Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.Completeness :
Type

Completeness level: incomplete (t) or complete (T). Incomplete meanings await further composition (e.g., a cardinality test). Complete meanings are ready for discourse integration.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.instDecidableEqCompleteness :
    DecidableEq Completeness
    Equations
    source
    def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.instReprCompleteness.repr :
    Completeness → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.instReprCompleteness :
      Repr Completeness
      Equations
      source
      def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.subtypeOf :
      Completeness → Completeness → Prop

      Subtyping: t ⊏ T, t ⊏ t, T ⊏ T, but NOT T ⊏ t. This ensures incomplete meanings can be promoted to complete, but complete meanings cannot be demoted.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.instDecidableSubtypeOf (a b : Completeness) :
        Decidable (subtypeOf a b)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.«term_⊏_» :
        Lean.TrailingParserDescr

        Notation for subtyping

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          structure Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.TypedDRS (S : Type u_1) (c : Completeness) :
          Type u_1

          A DRS annotated with its completeness level.

          • drs : S → S → Prop

            The underlying DRS

          Instances For
            source
            def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.Evar_type :
            Completeness

            Type assignment: E^v (existential introduction) is incomplete.

            Equations
            Instances For
              source
              def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.Mvar_type :
              Completeness

              Type assignment: M_v (maximization) produces incomplete output.

              Equations
              Instances For
                source
                def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.CardTest_type :
                Completeness

                Type assignment: n_v (cardinality test) produces complete output.

                Equations
                Instances For
                  source
                  def Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.dynConj_type (c : Completeness) :
                  Completeness

                  Dynamic conjunction is polymorphic: A → A → A for any A.

                  Equations
                  Instances For
                    source
                    theorem Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.cumulative_welltyped :
                    subtypeOf (dynConj_type (dynConj_type Mvar_type)) CardTest_type

                    The cumulative formula is well-typed (equation 45): M_v(E^v; M_u(E^u; saw)) : t (incomplete), then; 5_u : T,; 3_v : T. Since t ⊏ T, the outer cardinality tests can accept incomplete input.

                    source
                    theorem Phenomena.Plurals.Studies.Charlow2021.SubtypePolymorphism.pseudo_cumulative_illtyped :
                    ¬subtypeOf CardTest_type Mvar_type

                    The pseudo-cumulative formula is ill-typed (equation 46): 5_u would need to be INSIDE M_v's scope, but 5_u forces type T (complete), and M_v requires type t (incomplete). Formalized as: CardTest_type (T) is NOT a subtype of Mvar_type (t).