Grammar as Distribution

@cite{dunn-2025} @cite{bergen-levy-goodman-2016}

A grammar is a frequency profile over constructions. This generalizes lexical uncertainty: where LU varies meaning assignments, grammar uncertainty varies both meaning AND production frequency.

Architecture

Two types capture the individual–population hierarchy from @cite{dunn-2025} variationist CxG:

• GrammarDist C — frequency profile over constructions (individual grammar)
• Grammar C W — frequency + interpretation (connects to RSA Lexicon)

@cite{dunn-2025} measures variation across three dimensions — individuals, populations (dialects), and contexts (registers) — using Shannon entropy for constructional diversity and Jensen-Shannon divergence for grammar similarity.

structure ConstructionGrammar.GrammarDist (C : Type) : Type

A non-negative frequency profile over constructions.

An individual's grammar is a frequency-weighted profile over constructions — not a binary set (in/out) but a weighting reflecting how often each construction is used. Note: this does not enforce normalization (Σ freq = 1); the weights are relative frequencies, not probabilities.

• freq : C → ℚ
• freq_nonneg (c : C) : 0 ≤ self.freq c

structure ConstructionGrammar.Grammar (C W : Type) extends ConstructionGrammar.GrammarDist C : Type

A full grammar: frequency profile + interpretation function.

Extends GrammarDist with a meaning function mapping each construction to a graded truth function over worlds. This connects grammar distributions to RSA's literal semantics and to @cite{bergen-levy-goodman-2016}'s Lexicon type.

• freq : C → ℚ
• freq_nonneg (c : C) : 0 ≤ self.freq c
• meaning : C → W → ℚ

def ConstructionGrammar.GrammarDist.entropyOver {C : Type} [BEq C] (g : GrammarDist C) (inventory : List C) : ℚ

Constructional diversity: Shannon entropy of the frequency profile.

Higher entropy = more diverse construction usage. @cite{dunn-2025} uses grammar entropy to compare registers, dialects, and individual variation within L1 populations.

Equations

• g.entropyOver inventory = Core.InformationTheory.entropy (List.map (fun (c : C) => (c, g.freq c)) inventory)

def ConstructionGrammar.GrammarDist.jsd {C : Type} [BEq C] (p q : GrammarDist C) (inventory : List C) : ℚ

Jensen-Shannon divergence between two grammars over a shared inventory.

Symmetric, bounded, and a metric (after sqrt). Used by @cite{dunn-2025} to measure register distance, dialect boundaries, and L1-L2 differences.

Equations

• p.jsd q inventory = Core.InformationTheory.jsdOf inventory p.freq q.freq

def ConstructionGrammar.Grammar.toLexicon {C W : Type} (g : Grammar C W) : Lexicon C W

Project a grammar to a lexicon by forgetting frequency.

A Lexicon is a meaning assignment C → W → ℚ. A Grammar is a meaning assignment PLUS a frequency profile. The projection forgets frequency, retaining only interpretation.

Equations

• g.toLexicon = { meaning := g.meaning }

def ConstructionGrammar.grammarOfLexicon {W U : Type} (L : Lexicon U W) : Grammar U W

Embed a lexicon as a grammar with uniform frequency.

This is the key structural claim: lexical uncertainty is the special case of grammar uncertainty where only meaning varies and production frequency is uniform across constructions.

Standard LU uses a flat prior over lexicons; grammar uncertainty extends this by additionally varying production frequency.

Equations

• ConstructionGrammar.grammarOfLexicon L = { freq := fun (x : U) => 1, freq_nonneg := ⋯, meaning := L.meaning }

theorem ConstructionGrammar.toLexicon_grammarOfLexicon_meaning {W U : Type} (L : Lexicon U W) (u : U) (w : W) : (grammarOfLexicon L).toLexicon.meaning u w = L.meaning u w

Round-trip: Lexicon → Grammar → Lexicon preserves meaning.

The meaning function is unchanged by embedding into Grammar and projecting back. This makes toLexicon ∘ grammarOfLexicon the identity on meaning.

theorem ConstructionGrammar.grammar_subsumes_lexical_uncertainty {W U : Type} (L : Lexicon U W) : (grammarOfLexicon L).toLexicon.meaning = L.meaning

Lexical uncertainty embeds into grammar uncertainty (meaning preserved).

Every Lexicon embeds as a Grammar with uniform frequency, preserving the meaning function. The embedding is meaning-preserving: toLexicon after grammarOfLexicon recovers the original meaning. Grammar uncertainty extends LU by additionally varying production frequency.

def ConstructionGrammar.GrammarDist.cost {C : Type} (g : GrammarDist C) (c : C) : ℚ

Production cost derived from frequency: -log₂(freq).

Frequent constructions are cheap; rare ones are expensive. This connects @cite{dunn-2025}'s frequency-based grammar to RSA's utterance cost: setting cost(u) = -log₂(freq(u)) in S1's action-based scoring rule grounds utterance cost in production frequency rather than stipulating it.

Equations

• g.cost c = if g.freq c ≤ 0 then 10 else -Core.InformationTheory.log2Approx (g.freq c)