Documentation

Linglib.Comparisons.ScalarImplicatureTheories

source
theorem Comparisons.ScalarImplicatureTheories.both_derive_implicatures :
Interfaces.ImplicatureTheory.predictedBaselineRate NeoGricean.NeoGriceanTheory > 0 ∧ Interfaces.ImplicatureTheory.predictedBaselineRate RSA.RSATheory > 0

Both theories derive some implicatures (baseline > 0)

source
theorem Comparisons.ScalarImplicatureTheories.both_trigger_some_ue :
Interfaces.ImplicatureTheory.implicatureStatus NeoGricean.someStudentsSleepNG 0 = Interfaces.ImplicatureStatus.triggered ∧ Interfaces.ImplicatureTheory.implicatureStatus RSA.someRSA 0 = Interfaces.ImplicatureStatus.triggered

Both theories trigger implicature for "some" in UE context

source
theorem Comparisons.ScalarImplicatureTheories.both_triggered_not_possible :
Interfaces.derivesImplicature NeoGricean.someStudentsSleepNG 0 = true ∧ Interfaces.derivesImplicature RSA.someRSA 0 = true

Both theories derive triggered (not just possible) for "some"

source
theorem Comparisons.ScalarImplicatureTheories.both_no_implicature_all :
Interfaces.ImplicatureTheory.implicatureStatus RSA.allRSA 0 = Interfaces.ImplicatureStatus.absent

Neither theory triggers implicature for "all" (top of scale)

source
theorem Comparisons.ScalarImplicatureTheories.neogricean_predicts_de_blocking :
Interfaces.ImplicatureTheory.predictsDEBlocking NeoGricean.NeoGriceanTheory = true

NeoGricean predicts DE blocking

source
theorem Comparisons.ScalarImplicatureTheories.rsa_predicts_de_blocking :
Interfaces.ImplicatureTheory.predictsDEBlocking RSA.RSATheory = true

RSA predicts DE blocking (via @cite{potts-etal-2016} lexical uncertainty)

source
theorem Comparisons.ScalarImplicatureTheories.both_predict_de_blocking :
Interfaces.ImplicatureTheory.predictsDEBlocking NeoGricean.NeoGriceanTheory = true ∧ Interfaces.ImplicatureTheory.predictsDEBlocking RSA.RSATheory = true

Both theories now predict DE blocking

source
theorem Comparisons.ScalarImplicatureTheories.neogricean_predicts_task_effect :
Interfaces.ImplicatureTheory.predictsTaskEffect NeoGricean.NeoGriceanTheory = true

NeoGricean predicts task effect (contextualism)

source
theorem Comparisons.ScalarImplicatureTheories.rsa_task_effect_incomplete :
Interfaces.ImplicatureTheory.predictsTaskEffect RSA.RSATheory = false

RSA model incomplete: doesn't handle task effects

source
theorem Comparisons.ScalarImplicatureTheories.neogricean_task_complete_rsa_incomplete :
Interfaces.ImplicatureTheory.predictsTaskEffect NeoGricean.NeoGriceanTheory = true ∧ Interfaces.ImplicatureTheory.predictsTaskEffect RSA.RSATheory = false

NeoGricean models task effect, RSA incomplete

source
theorem Comparisons.ScalarImplicatureTheories.different_baseline_rates :
Interfaces.ImplicatureTheory.predictedBaselineRate NeoGricean.NeoGriceanTheory ≠ Interfaces.ImplicatureTheory.predictedBaselineRate RSA.RSATheory

Theories have different baseline rates

source
def Comparisons.ScalarImplicatureTheories.geurtsPouscolousVerificationRate :
ℕ

Observed verification task rate from @cite{geurts-pouscoulous-2009}

Equations
Instances For
    source
    theorem Comparisons.ScalarImplicatureTheories.neogricean_close_to_observed :
    have ng_rate := Interfaces.ImplicatureTheory.predictedBaselineRate NeoGricean.NeoGriceanTheory; have diff := if ng_rate > geurtsPouscolousVerificationRate then ng_rate - geurtsPouscolousVerificationRate else geurtsPouscolousVerificationRate - ng_rate; diff < 5

    NeoGricean baseline (35%) is close to observed (34%)

    source
    theorem Comparisons.ScalarImplicatureTheories.rsa_far_from_observed :
    have rsa_rate := Interfaces.ImplicatureTheory.predictedBaselineRate RSA.RSATheory; have diff := if rsa_rate > geurtsPouscolousVerificationRate then rsa_rate - geurtsPouscolousVerificationRate else geurtsPouscolousVerificationRate - rsa_rate; diff > 10

    RSA baseline (50%) is far from observed (34%)

    source
    theorem Comparisons.ScalarImplicatureTheories.neogricean_closer_to_geurts_data :
    have ng_rate := Interfaces.ImplicatureTheory.predictedBaselineRate NeoGricean.NeoGriceanTheory; have rsa_rate := Interfaces.ImplicatureTheory.predictedBaselineRate RSA.RSATheory; have empirical := geurtsPouscolousVerificationRate; have ng_diff := if ng_rate > empirical then ng_rate - empirical else empirical - ng_rate; have rsa_diff := if rsa_rate > empirical then rsa_rate - empirical else empirical - rsa_rate; ng_diff < rsa_diff

    NeoGricean closer to @cite{geurts-pouscoulous-2009} data than RSA

    source
    theorem Comparisons.ScalarImplicatureTheories.theories_agree_on_de :
    Interfaces.theoriesAgreeOnDEPrediction = true

    Both theories now agree on DE blocking

    source
    theorem Comparisons.ScalarImplicatureTheories.theories_disagree_on_task_effect :
    Interfaces.theoriesAgreeOnTaskEffect = false

    Agreement check on task effect

    source
    theorem Comparisons.ScalarImplicatureTheories.neogricean_matches_data :
    Interfaces.rateMatchesData (Interfaces.ImplicatureTheory.predictedBaselineRate NeoGricean.NeoGriceanTheory) geurtsPouscolousVerificationRate = true

    Rate matching using interface function

    source
    theorem Comparisons.ScalarImplicatureTheories.rsa_doesnt_match_data :
    Interfaces.rateMatchesData (Interfaces.ImplicatureTheory.predictedBaselineRate RSA.RSATheory) geurtsPouscolousVerificationRate = false

    RSA doesn't match data within tolerance

    source
    theorem Comparisons.ScalarImplicatureTheories.neogricean_closer :
    Interfaces.closerToData geurtsPouscolousVerificationRate = true

    NeoGricean is closer to data

    source
    def Comparisons.ScalarImplicatureTheories.neogriceanFullCoverage :
    Interfaces.TheoryCoverage

    NeoGricean full coverage report

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Comparisons.ScalarImplicatureTheories.rsaFullCoverage :
      Interfaces.TheoryCoverage

      RSA full coverage report

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Comparisons.ScalarImplicatureTheories.neogricean_no_incomplete :
        neogriceanFullCoverage.countByStatus Interfaces.CoverageStatus.incomplete = 0

        NeoGricean has no incomplete phenomena (but some out of scope)

        source
        theorem Comparisons.ScalarImplicatureTheories.rsa_has_incomplete :
        rsaFullCoverage.countByStatus Interfaces.CoverageStatus.incomplete > 0

        RSA has incomplete phenomena that could be extended

        source
        theorem Comparisons.ScalarImplicatureTheories.rsa_covers_reference_games :
        rsaFullCoverage.statusFor Interfaces.PragmaticPhenomenon.referenceGames = some Interfaces.CoverageStatus.complete

        RSA covers reference games (NeoGricean doesn't claim to)

        source
        theorem Comparisons.ScalarImplicatureTheories.neogricean_reference_games_out_of_scope :
        neogriceanFullCoverage.statusFor Interfaces.PragmaticPhenomenon.referenceGames = some Interfaces.CoverageStatus.outOfScope

        NeoGricean explicitly marks reference games as out of scope

        source
        def Comparisons.ScalarImplicatureTheories.neogriceanCoverage :
        Interfaces.CoverageSummary

        NeoGricean coverage summary (legacy)

        Equations
        Instances For
          source
          def Comparisons.ScalarImplicatureTheories.rsaCoverage :
          Interfaces.CoverageSummary

          RSA coverage summary (legacy)

          Equations
          Instances For
            source
            def Comparisons.ScalarImplicatureTheories.geurtsPouscolousTaskEffect :
            Interfaces.TaskEffectTestCase

            @cite{geurts-pouscoulous-2009} task effect data as a test case

            Equations
            Instances For
              source
              def Comparisons.ScalarImplicatureTheories.someAllDEBlocking :
              Interfaces.DEBlockingTestCase

              DE blocking test case from ScalarImplicatures data

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Comparisons.ScalarImplicatureTheories.neogricean_captures_de_blocking :
                (Interfaces.testDEBlocking someAllDEBlocking).isMatch = true

                Test NeoGricean against DE blocking data

                source
                theorem Comparisons.ScalarImplicatureTheories.rsa_captures_de_blocking :
                (Interfaces.testDEBlocking someAllDEBlocking).isMatch = true

                RSA captures DE blocking (via @cite{potts-etal-2016} lexical uncertainty)

                source
                theorem Comparisons.ScalarImplicatureTheories.neogricean_task_effect_result :
                have result := Interfaces.testTaskEffect geurtsPouscolousTaskEffect 5; result.theoryPredictsTaskEffect = true ∧ result.dataShowsTaskEffect = true ∧ result.rateDifference ≤ 5

                NeoGricean matches task effect pattern

                source
                theorem Comparisons.ScalarImplicatureTheories.rsa_task_effect_incomplete_test :
                have result := Interfaces.testTaskEffect geurtsPouscolousTaskEffect 5; result.theoryPredictsTaskEffect = false ∧ result.dataShowsTaskEffect = true

                RSA model incomplete for task effect (can't represent QUD manipulation)

                source
                theorem Comparisons.ScalarImplicatureTheories.neogricean_closer_using_linking :
                match Interfaces.closerToObservedRate geurtsPouscolousVerificationRate with | (ng_result, snd) => ng_result = true

                Compare both theories to observed verification rate

                source
                instance Comparisons.ScalarImplicatureTheories.instCapturesTaskEffectDataNeoGriceanTheory :
                Interfaces.CapturesTaskEffectData NeoGricean.NeoGriceanTheory

                NeoGricean captures the Geurts & Pouscoulous task effect data

                Equations
                • One or more equations did not get rendered due to their size.
                source
                instance Comparisons.ScalarImplicatureTheories.instCapturesDEBlockingPatternNeoGriceanTheory :
                Interfaces.CapturesDEBlockingPattern NeoGricean.NeoGriceanTheory

                NeoGricean captures DE blocking pattern

                Equations
                • One or more equations did not get rendered due to their size.
                source
                instance Comparisons.ScalarImplicatureTheories.instCapturesDEBlockingPatternRSATheory :
                Interfaces.CapturesDEBlockingPattern RSA.RSATheory

                RSA captures DE blocking pattern (via @cite{potts-etal-2016})

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