Documentation

Studies.BumfordRett2021

Bumford and Rett (2021): Rationalizing evaluativity #

Bumford and Rett derive the evaluativity of a degree construction, the inference that a measure lies beyond the norm of its comparison class, as an implicature drawn by a Rational Speech Act listener, and they make it graded. A world fixes the subject's height and the centre of its class, after Barker; each antonym is true relative to a threshold offset from the centre, about which the listener is uncertain as in the lexical uncertainty model of Bergen, Levy and Goodman; and the marked antonym costs the speaker more. Evaluativity is the listener's expected deviation of the measured height from the class centre.

For the positive construction and the exact equative the sign of that expectation is the antonym's, at every rationality and every cost. Reversing the height scale exchanges the antonyms, so the two antonyms of a construction differ only through their costs. How strong each inference is, and so whether the model recovers Rett's categorical classification, is a numerical matter.

Main statements #

Implementation notes #

TODO #

References #

Worlds #

def BumfordRett2021.negate (x : ↥(Finset.Icc (-4) 4)) :
↥(Finset.Icc (-4) 4)

The reflection x ↦ -x of the interval [-4, 4], in which deviations from the class centre and threshold offsets both range.

Equations
Instances For
    @[simp]
    theorem BumfordRett2021.coe_negate (x : ↥(Finset.Icc (-4) 4)) :
    ↑(negate x) = -↑x
    theorem BumfordRett2021.negate_involutive :
    Function.Involutive negate

    A world fixes the subject's height relative to the centre of its comparison class, and that centre.

    • deviation : ↥(Finset.Icc (-4) 4)

      The deviation of the subject's height from the class centre.

    • centre : ↥(Finset.Icc 5 13)

      The centre of the comparison class.

    Instances For
      def BumfordRett2021.instDecidableEqWorld.decEq (x✝ x✝¹ : World) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[instance_reducible]
        Equations
        @[instance_reducible]
        Equations

        The subject's height.

        Equations
        Instances For

          Reversing the height scale about 9, the middle of the heights 1..17, which maps the paper's worlds onto themselves.

          Equations
          Instances For
            @[simp]

            Reflecting the subject's height about the class centre.

            Equations
            Instances For

              Utterances and their interpretations #

              Keisha's height, the median height, is the standard of the equatives and the comparative, and both speaker and listener know it.

              Equations
              Instances For

                The speaker says the antonym of a polarity, tall or short, or says nothing.

                Instances For

                  The degree an antonym places relative to the threshold is the subject's height in the positive construction (none), which relates the subject to no standard, and Keisha's height in the constructions relating the subject to Keisha by =, ≥ or >.

                  Equations
                  Instances For
                    def BumfordRett2021.Holds (c : Option Degree.Comparison) :
                    Utterance → ↥(Finset.Icc (-4) 4) → World → Prop

                    Under the threshold offset σ, silence is true everywhere, and the antonym of polarity p says that the subject stands in the construction's relation to Keisha and that the measured height lies on p's side of the class centre shifted by σ. The negative antonym's relations are the order duals.

                    Equations
                    Instances For
                      @[instance_reducible]
                      instance BumfordRett2021.instDecidableHolds (c : Option Degree.Comparison) (u : Utterance) (σ : ↥(Finset.Icc (-4) 4)) (w : World) :
                      Decidable (Holds c u σ w)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      theorem BumfordRett2021.holds_reflect (c : Option Degree.Comparison) (u : Utterance) (σ : ↥(Finset.Icc (-4) 4)) (w : World) :
                      Holds c u.antonym (negate σ) w.reflect ↔ Holds c u σ w

                      Reversing the height scale about Keisha's height, and the threshold offset with it, exchanges the antonyms of every construction.

                      theorem BumfordRett2021.exists_holds (c : Option Degree.Comparison) (u : Utterance) :
                      ∃ (w : World) (σ : ↥(Finset.Icc (-4) 4)), Holds c u σ w

                      Every utterance of every construction is true at some world under some offset.

                      The listener #

                      noncomputable def BumfordRett2021.prior :
                      MeasureTheory.Measure World

                      The listener's prior weights a world by the density of its comparison class's heights, Gaussian about the centre with standard deviation 2, at the subject's height, so the centre is uniform.

                      Equations
                      Instances For
                        theorem BumfordRett2021.prior_singleton (w : World) :
                        prior {w} = ENNReal.ofReal (ProbabilityTheory.gaussianPDFReal (↑↑w.centre) 4 ↑w.height)
                        instance BumfordRett2021.instIsFiniteMeasureWorldPrior :
                        MeasureTheory.IsFiniteMeasure prior
                        theorem BumfordRett2021.prior_singleton_congr {w w' : World} (h : ↑w.deviation ^ 2 = ↑w'.deviation ^ 2) :
                        prior {w} = prior {w'}

                        The prior depends on a world through the square of its deviation alone.

                        theorem BumfordRett2021.prior_prod_count_singleton (q : World × ↥(Finset.Icc (-4) 4)) :
                        (prior.prod MeasureTheory.Measure.count) {q} = prior {q.1}
                        noncomputable def BumfordRett2021.literal (c : Option Degree.Comparison) (σ : ↥(Finset.Icc (-4) 4)) :
                        ProbabilityTheory.Kernel Utterance World

                        The literal listener under the threshold offset σ conditions the prior on the truth of the utterance.

                        Equations
                        Instances For
                          instance BumfordRett2021.instIsFiniteKernelUtteranceWorldLiteral (c : Option Degree.Comparison) (σ : ↥(Finset.Icc (-4) 4)) :
                          ProbabilityTheory.IsFiniteKernel (literal c σ)
                          noncomputable def BumfordRett2021.speaker (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) :
                          ProbabilityTheory.Kernel (World × ↥(Finset.Icc (-4) 4)) Utterance

                          The speaker at a world and a threshold offset addresses the literal listener under that offset, at rationality α with costs cost.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem BumfordRett2021.speaker_apply (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) (q : World × ↥(Finset.Icc (-4) 4)) :
                            (speaker c α cost) q = (RSA.speaker α cost (⇑(literal c q.2)) MeasureTheory.Measure.dirac) q.1
                            instance BumfordRett2021.instIsFiniteKernelProdWorldSubtypeIntMemFinsetIccNegOfNatUtteranceSpeaker (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) :
                            ProbabilityTheory.IsFiniteKernel (speaker c α cost)
                            noncomputable def BumfordRett2021.listener (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) :
                            ProbabilityTheory.Kernel Utterance (World × ↥(Finset.Icc (-4) 4))

                            The pragmatic listener at rationality α, with the speaker's costs cost, inverts the speakers indexed by the threshold offsets against the prior on worlds and uniform offsets.

                            Equations
                            Instances For
                              instance BumfordRett2021.instIsFiniteKernelUtteranceProdWorldSubtypeIntMemFinsetIccNegOfNatListener (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) :
                              ProbabilityTheory.IsFiniteKernel (listener c α cost)
                              noncomputable def BumfordRett2021.expectedDeviation (c : Option Degree.Comparison) (α : ℝ) (cost : Utterance → ℝ) (p : Polarity) :
                              ℝ

                              The listener's expected deviation of the measured height from the class centre, after the antonym of polarity p, is the statistic of evaluativity that the paper's Table 1 reports.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem BumfordRett2021.comp_speaker_ne_zero {α : ℝ} {cost : Utterance → ℝ} (hα : 0 ≤ α) (c : Option Degree.Comparison) (u : Utterance) :
                                ((prior.prod MeasureTheory.Measure.count).bind ⇑(speaker c α cost)) {u} ≠ 0

                                Every utterance of every construction has positive probability of being produced.

                                Antonym symmetry #

                                theorem BumfordRett2021.literal_antonym (c : Option Degree.Comparison) (σ : ↥(Finset.Icc (-4) 4)) (u : Utterance) (w : World) :
                                ((literal c (negate σ)) u.antonym) {w.reflect} = ((literal c σ) u) {w}
                                theorem BumfordRett2021.listener_antonym {α : ℝ} {cost : Utterance → ℝ} (c : Option Degree.Comparison) (u : Utterance) (w : World) (σ : ↥(Finset.Icc (-4) 4)) :
                                ((listener c α cost) u.antonym) {(w.reflect, negate σ)} = ((listener c α (cost ∘ Utterance.antonym)) u) {(w, σ)}

                                Reversing the height scale carries the listener after an antonym to the listener after the other antonym, with the costs of the antonyms exchanged.

                                theorem BumfordRett2021.expectedDeviation_antonym {α : ℝ} {cost : Utterance → ℝ} (c : Option Degree.Comparison) (p : Polarity) :

                                The negative antonym's expected deviation is minus the positive antonym's with the costs of the antonyms exchanged, so the antonyms of a construction differ only through their costs.

                                With equal costs the two antonyms of every construction have opposite expected deviations. The paper remarks this of the comparative, whose antonyms do not come out opposite in its simulations only because of their costs.

                                Evaluativity of the positive and the exact equative #

                                theorem BumfordRett2021.positive_evaluative {α : ℝ} {cost : Utterance → ℝ} (hα : 0 < α) (p : Polarity) :
                                0 < p • expectedDeviation none α cost p

                                The positive construction is evaluative for both antonyms, at every rationality and every cost. After tall the listener expects the subject above the centre of the class, and after short below it.

                                theorem BumfordRett2021.exactEquative_evaluative {α : ℝ} {cost : Utterance → ℝ} (hα : 0 < α) (p : Polarity) :
                                0 < p • expectedDeviation (some Degree.Comparison.eq) α cost p

                                The exact equative shifts the listener for both antonyms, at every rationality and every cost. After exactly as tall as Keisha the listener expects Keisha above the centre of the class, and after exactly as short as Keisha below it, so the unmarked antonym is evaluative in direction and its weakness in the paper is one of magnitude.

                                What the positive construction leaves open #

                                theorem BumfordRett2021.positive_centre_uniform {α : ℝ} {cost : Utterance → ℝ} (hα : 0 < α) (u : Utterance) :
                                MeasureTheory.Measure.map World.centre ((listener none α cost) u).fst = ProbabilityTheory.uniformOn Set.univ

                                Hearing the positive construction, the listener learns nothing about the class, whose centre stays uniformly distributed.

                                Evaluativity balances across the speaker's choices #

                                theorem BumfordRett2021.isMarkovKernel_speaker {α : ℝ} {cost : Utterance → ℝ} (hα : 0 ≤ α) (c : Option Degree.Comparison) :
                                ProbabilityTheory.IsMarkovKernel (speaker c α cost)

                                The speakers produce a probability distribution over the utterances at every world and offset, since silence is true everywhere.

                                theorem BumfordRett2021.evaluativity_balances {α : ℝ} {cost : Utterance → ℝ} (hα : 0 ≤ α) (c : Option Degree.Comparison) :
                                ∑ u : Utterance, ((prior.prod MeasureTheory.Measure.count).bind ⇑(speaker c α cost)).real {u} * ∫ (w : World), ↑(measured c w - ↑w.centre) ∂((listener c α cost) u).fst = 0

                                Weighted by how often the speaker makes each utterance, the listener's expected deviations sum to the prior's, which is zero. The listener's beliefs average back to the prior, so an antonym the speaker says rarely carries a more extreme inference.

                                Competition between the antonyms and Rett's classification #

                                Rett derives the evaluativity of the marked antonym from its competition with an unmarked antonym of the same truth conditions, which only the polar-invariant constructions provide. In the graded model the antonyms compete wherever both are true; where they never are, as in the comparative, each antonym's listener ignores the other antonym's cost, and markedness acts only through the antonym's own cost.

                                A simulated construction instantiates the positive construction, the equative for the comparisons = and ≥, or the comparative for >, in Rett's classification.

                                Equations
                                Instances For

                                  The antonyms of a construction exclude each other when no world verifies both under any offset.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Among the constructions relating the subject to Keisha, the antonyms exclude each other exactly where Rett's classification makes the construction polar-variant.

                                    theorem BumfordRett2021.expectedDeviation_congr_of_antonymsExclusive {α : ℝ} {cost cost' : Utterance → ℝ} (hα : 0 < α) {c : Option Degree.Comparison} (hex : AntonymsExclusive c) {p : Polarity} (hp : cost (Utterance.say p) = cost' (Utterance.say p)) (hs : cost Utterance.silence = cost' Utterance.silence) :
                                    expectedDeviation c α cost p = expectedDeviation c α cost' p

                                    Where the antonyms exclude each other, an antonym's expected deviation depends on the costs only through its own cost and silence's, since the other antonym never competes with it.

                                    The marked comparative is the unmarked comparative reflected, at the marked antonym's cost, so markedness acts on the comparative only through the antonym's own cost.