Documentation

Linglib.Semantics.Probabilistic.Composition

Multiplicative composition of graded word meanings #

Graded approaches to meaning ([Erk22]'s "probabilistic turn") assign each word a graded value rather than a Boolean; an utterance meaning is then composed by multiplying the word values, treating words as independent constraints: [DHG+20]'s continuous semantics scores a referring expression as the product of per-word values, and the incremental models of [WD21] (ℚ-valued) and [SW23] (ℚ≥0-valued) apply the same composition to utterance prefixes. prodMeaning is this composition for a per-word lex function lex : U → W → R, stated over any CommMonoid R. prodMeaning_perm — the composed meaning is independent of token order — is the listener-level sanity check of [SW23].

The normalized counterpart on PMF is the Product of Experts (Core/Probability/ProductOfExperts.lean), the combination rule of [EH24]'s situation description systems.

source
def Semantics.Probabilistic.prodMeaning {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (us : List U) (w : W) :
R

Product meaning: the per-word lex composed multiplicatively over a token list, prodMeaning lex us w = (us.map (lex · w)).prod.

Equations
Instances For
    source
    @[simp]
    theorem Semantics.Probabilistic.prodMeaning_nil {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (w : W) :
    prodMeaning lex [] w = 1
    source
    @[simp]
    theorem Semantics.Probabilistic.prodMeaning_cons {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] (lex : U → W → R) (u : U) (us : List U) (w : W) :
    prodMeaning lex (u :: us) w = lex u w * prodMeaning lex us w
    source
    theorem Semantics.Probabilistic.prodMeaning_perm {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoid R] {lex : U → W → R} {us us' : List U} (h : us.Perm us') (w : W) :
    prodMeaning lex us w = prodMeaning lex us' w

    Any permutation of the token list yields the same meaning.

    source
    theorem Semantics.Probabilistic.prodMeaning_nonneg {U : Type u_1} {W : Type u_2} {R : Type u_3} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {lex : U → W → R} (h : ∀ (u : U) (w : W), 0 ≤ lex u w) (us : List U) (w : W) :
    0 ≤ prodMeaning lex us w