Documentation

Linglib.Phenomena.Negation.Studies.TesslerFranke2020PMF

@cite{tessler-franke-2019} on mathlib PMF (Shape B + cost-factor migration) #

@cite{tessler-franke-2019}

PMF-shaped formalisation of the paper's 6 findings. The first PMF migration with a cost factor in the S1 score: S1(u | w) ∝ L0(w | u)^α · exp(−C(u)). Validates that RSA.S1Belief's costFactor : U → ℝ≥0∞ argument handles the canonical exp(-cost) shape.

Friction surfaced (informs API direction) #

§0. Domain types #

source
@[reducible, inline]
abbrev TesslerFranke2020.PMF.HappinessDeg :
Type

Happiness degree: 0 (miserable) to 4 (ecstatic).

Equations
Instances For
    source
    instance TesslerFranke2020.PMF.instNeZeroNatOfNat_linglib :
    NeZero 4
    source
    @[reducible, inline]
    abbrev TesslerFranke2020.PMF.HThreshold :
    Type

    Threshold values 0–3, used for both θ₁ (positive) and θ₂ (contrary).

    Equations
    Instances For
      source
      inductive TesslerFranke2020.PMF.Utterance :
      Type
      Instances For
        source
        def TesslerFranke2020.PMF.instReprUtterance.repr :
        Utterance → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance TesslerFranke2020.PMF.instReprUtterance :
          Repr Utterance
          Equations
          source
          @[implicit_reducible]
          instance TesslerFranke2020.PMF.instDecidableEqUtterance :
          DecidableEq Utterance
          Equations
          source
          @[implicit_reducible]
          instance TesslerFranke2020.PMF.instFintypeUtterance :
          Fintype Utterance
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[reducible, inline]
          abbrev TesslerFranke2020.PMF.NegLexicon :
          Type

          Lexicon for morphological negation "un-": contrary (polar opposite with gap) vs contradictory (complement). Aliased to Features.NegationType.

          Equations
          Instances For
            source
            @[reducible]
            def TesslerFranke2020.PMF.LatentState :
            Type

            Joint latent state: (θ₁, θ₂, L) — 4 × 4 × 2 = 32 latent states.

            Equations
            Instances For
              source
              def TesslerFranke2020.PMF.utteranceMeaning (θ₁ θ₂ : HThreshold) (L : NegLexicon) (u : Utterance) (d : HappinessDeg) :
              Bool

              Utterance meaning parameterized by thresholds and lexicon, grounded in shared Semantics.Degree predicates.

              Equations
              Instances For
                source
                def TesslerFranke2020.PMF.utteranceCost (u : Utterance) :
                ℚ

                Utterance cost (morphological complexity): C(un-) = 2, C(not) = 3, combined additively.

                Equations
                Instances For
                  source
                  instance TesslerFranke2020.PMF.instNonemptyHappinessDeg :
                  Nonempty HappinessDeg
                  source
                  instance TesslerFranke2020.PMF.instNonemptyUtterance :
                  Nonempty Utterance
                  source
                  instance TesslerFranke2020.PMF.instNonemptyLatentState :
                  Nonempty LatentState

                  §1. L0 — uniform on extension via RSA.L0OfBoolMeaning #

                  source
                  @[reducible, inline]
                  abbrev TesslerFranke2020.PMF.meaningAt (l : LatentState) :
                  Utterance → HappinessDeg → Bool

                  Lexicon as a function from latent state.

                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev TesslerFranke2020.PMF.extension (l : LatentState) (u : Utterance) :
                    Finset HappinessDeg

                    Extension of meaningAt l u.

                    Equations
                    Instances For

                      §2. S1Belief — cost-bearing speaker via RSA.S1Belief #

                      The cost factor: exp (-utteranceCost u). Cast to ℝ≥0∞.

                      source
                      noncomputable def TesslerFranke2020.PMF.costFactor (u : Utterance) :
                      ENNReal
                      Equations
                      Instances For
                        source
                        theorem TesslerFranke2020.PMF.costFactor_pos (u : Utterance) :
                        costFactor u ≠ 0
                        source
                        theorem TesslerFranke2020.PMF.costFactor_finite (u : Utterance) :
                        costFactor u ≠ ⊤

                        §3. Per-latent L0 + S1g + marginalSpeaker — sketch only #

                        The per-latent S1g would be RSA.S1Belief (L0_at l) costFactor 1, marginalized over LatentState via RSA.marginalizeKernel against a uniform latent prior. Then L1 = PMF.posterior against uniform world prior.

                        The structural shell follows the ScontrasPearl template exactly. The leaves (per-latent comparisons across 32 states) are well beyond hand-discharge without the pmf_score_compare tactic.

                        This file is a placeholder + friction documentation. Full migration deferred pending tactic infrastructure.