Documentation

Linglib.Theories.Pragmatics.RSA.Implementations.VanTielEtAl2021

source
@[reducible, inline]
abbrev RSA.VanTielEtAl2021.domainSize :
ℕ

Domain size (simplified from 432 to 10)

Equations
Instances For
    source
    @[reducible, inline]
    abbrev RSA.VanTielEtAl2021.WorldState :
    Type

    Intersection set sizes (simplified from 0-432 to 0-10)

    Equations
    Instances For
      source
      def RSA.VanTielEtAl2021.allWorlds :
      List WorldState
      Equations
      Instances For
        source
        def RSA.VanTielEtAl2021.totalSetSize :
        ℕ
        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev RSA.VanTielEtAl2021.QuantityWord :
          Type
          Equations
          Instances For
            source
            def RSA.VanTielEtAl2021.allQuantityWords :
            List QuantityWord
            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev RSA.VanTielEtAl2021.Monotonicity :
              Type
              Equations
              Instances For
                source
                def RSA.VanTielEtAl2021.monotonicity (u : VanTielQuantity.Utterance) :
                VanTielQuantity.Monotonicity
                Equations
                Instances For
                  source
                  def RSA.VanTielEtAl2021.threshold (m : QuantityWord) :
                  ℕ

                  Threshold for each quantity word (from unified entry)

                  Equations
                  Instances For
                    source
                    def RSA.VanTielEtAl2021.gqtMeaning (m : QuantityWord) (t : WorldState) :
                    Bool

                    GQT meaning: binary truth based on threshold

                    Equations
                    Instances For
                      source
                      def RSA.VanTielEtAl2021.gqtMeaningRat (m : QuantityWord) (t : WorldState) :
                      ℚ

                      GQT meaning as rational

                      Equations
                      Instances For
                        source
                        def RSA.VanTielEtAl2021.prototype (m : QuantityWord) :
                        ℕ

                        Prototype (peak truth) for each quantity word (from unified entry)

                        Equations
                        Instances For
                          source
                          def RSA.VanTielEtAl2021.spread (m : QuantityWord) :
                          ℚ

                          Spread parameter (from unified entry)

                          Equations
                          Instances For
                            source
                            def RSA.VanTielEtAl2021.ptMeaning (m : QuantityWord) (t : WorldState) :
                            ℚ

                            PT meaning: gradient truth based on distance from prototype

                            Equations
                            Instances For
                              source
                              def RSA.VanTielEtAl2021.salience :
                              QuantityWord → ℚ

                              Salience prior (uniform for simplicity)

                              Equations
                              Instances For
                                source
                                theorem RSA.VanTielEtAl2021.some_matches_montague :
                                threshold Fragments.English.Determiners.QuantityWord.some_ = 1

                                "some" threshold matches Montague's existential: count >= 1

                                source
                                theorem RSA.VanTielEtAl2021.all_matches_montague :
                                threshold Fragments.English.Determiners.QuantityWord.all = totalSetSize

                                "all" threshold matches Montague's universal: count = total

                                source
                                theorem RSA.VanTielEtAl2021.most_above_half :
                                threshold Fragments.English.Determiners.QuantityWord.most > totalSetSize / 2

                                "most" threshold > half matches Montague's most_sem

                                source
                                theorem RSA.VanTielEtAl2021.some_few_opposite_monotonicity :
                                monotonicity Fragments.English.Determiners.QuantityWord.some_ = Fragments.English.Determiners.Monotonicity.increasing ∧ monotonicity Fragments.English.Determiners.QuantityWord.few = Fragments.English.Determiners.Monotonicity.decreasing

                                "some" and "few" have opposite monotonicity (no entailment)