Dunn (2025): Syntactic Variation from Individuals to Populations

[Dun25] (Cambridge Elements in Construction Grammar) models syntactic variation across individuals, populations (dialects), and contexts (registers) in a computational CxG: constructions are sequences of slot-constraints at the LEX/SYN/SEM levels (the SlotFiller levels of ConstructionGrammar), and an individual's grammar is a frequency profile over constructions. Formalized here: the frequency-profile grammar (Grammar), the Element's centrality strata (central = more than one standard deviation above the mean frequency; peripheral = below the mean), and the cosine similarity underlying its grammar-distance pipeline. The corpus case studies — classifier-based variation detection, feature weighting, z-standardization of distances, and the induced first- to fourth-order construction hierarchy — are empirical pipeline, not formalized.

Slot-constraints at three levels

def Dunn2025.example3 : ConstructionGrammar.TypedForm String

The Element's example (3): a late-stage noun-phrase construction whose slot-constraints draw on all three sources — [ SEM:141 ⟨which–whereas⟩ – SYN:66 ⟨shadiest–silliest⟩ – LEX: "person" ] — producing definite noun phrases like "the worst person" and "the happiest person". The induced SYN category, glossed by its superlative-adjective exemplars, is rendered ADJ.

Equations

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

theorem Dunn2025.example3_specificity : ConstructionGrammar.derivedSpecificity example3 = ConstructionGrammar.Specificity.partiallyOpen

Example (3) mixes open (SEM, SYN) and fixed (LEX) slots.

Grammars as frequency profiles

structure Dunn2025.Grammar (C : Type u_1) : Type u_1

An individual's grammar: a nonnegative frequency profile over constructions. The weights are relative frequencies, not probabilities — no normalization is imposed.

• freq : C → ℚ

  Usage frequency of each construction.

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

  Frequencies are nonnegative.

def Dunn2025.Grammar.meanFreq {C : Type u_1} (g : Grammar C) (inv : Finset C) : ℚ

Mean frequency across an inventory of constructions.

Equations

• g.meanFreq inv = (∑ c ∈ inv, g.freq c) / ↑inv.card

def Dunn2025.Grammar.varFreq {C : Type u_1} (g : Grammar C) (inv : Finset C) : ℚ

Frequency variance across an inventory.

Equations

• g.varFreq inv = (∑ c ∈ inv, (g.freq c - g.meanFreq inv) ^ 2) / ↑inv.card

def Dunn2025.Grammar.IsCentral {C : Type u_1} (g : Grammar C) (inv : Finset C) (c : C) : Prop

A construction is central when its frequency is more than one standard deviation above the inventory mean — the Element's operationalization of the centrality strata.

Equations

• g.IsCentral inv c = (↑(g.meanFreq inv) + √↑(g.varFreq inv) < ↑(g.freq c))

def Dunn2025.Grammar.IsPeripheral {C : Type u_1} (g : Grammar C) (inv : Finset C) (c : C) : Prop

A construction is peripheral when its frequency is below the inventory mean.

Equations

• g.IsPeripheral inv c = (g.freq c < g.meanFreq inv)

theorem Dunn2025.Grammar.isCentral_iff {C : Type u_1} (g : Grammar C) (inv : Finset C) (c : C) : g.IsCentral inv c ↔ g.meanFreq inv < g.freq c ∧ g.varFreq inv < (g.freq c - g.meanFreq inv) ^ 2

Squared characterization of centrality: above the mean, with squared deviation exceeding the variance. Keeps centrality decidable in ℚ.

@[instance_reducible]

instance Dunn2025.Grammar.instDecidableIsCentral {C : Type u_1} (g : Grammar C) (inv : Finset C) (c : C) : Decidable (g.IsCentral inv c)

Equations

• g.instDecidableIsCentral inv c = decidable_of_iff' (g.meanFreq inv < g.freq c ∧ g.varFreq inv < (g.freq c - g.meanFreq inv) ^ 2) ⋯

@[instance_reducible]

instance Dunn2025.Grammar.instDecidableIsPeripheral {C : Type u_1} (g : Grammar C) (inv : Finset C) (c : C) : Decidable (g.IsPeripheral inv c)

Equations

• g.instDecidableIsPeripheral inv c = Dunn2025.Grammar.instDecidableIsPeripheral._aux_1 g inv c

theorem Dunn2025.Grammar.IsCentral.not_isPeripheral {C : Type u_1} {g : Grammar C} {inv : Finset C} {c : C} (h : g.IsCentral inv c) : ¬g.IsPeripheral inv c

The strata are disjoint: no construction is both central and peripheral.

Similarity between grammars

noncomputable def Dunn2025.Grammar.cosineSim {C : Type u_1} (p q : Grammar C) (inv : Finset C) : ℝ

Cosine similarity of two frequency profiles over a shared inventory — the inner-product measure underlying the Element's standardized cosine-distance pipeline.

Equations

• p.cosineSim q inv = (∑ c ∈ inv, ↑(p.freq c) * ↑(q.freq c)) / (√(∑ c ∈ inv, ↑(p.freq c) ^ 2) * √(∑ c ∈ inv, ↑(q.freq c) ^ 2))

theorem Dunn2025.Grammar.cosineSim_comm {C : Type u_1} (p q : Grammar C) (inv : Finset C) : p.cosineSim q inv = q.cosineSim p inv

theorem Dunn2025.Grammar.cosineSim_nonneg {C : Type u_1} (p q : Grammar C) (inv : Finset C) : 0 ≤ p.cosineSim q inv

theorem Dunn2025.Grammar.cosineSim_le_one {C : Type u_1} (p q : Grammar C) (inv : Finset C) : p.cosineSim q inv ≤ 1

theorem Dunn2025.Grammar.cosineSim_self {C : Type u_1} (p : Grammar C) (inv : Finset C) (h : ∑ c ∈ inv, ↑(p.freq c) ^ 2 ≠ 0) : p.cosineSim p inv = 1

A nonzero profile has cosine similarity 1 with itself.

noncomputable def Dunn2025.Grammar.cosineDist {C : Type u_1} (p q : Grammar C) (inv : Finset C) : ℝ

Cosine distance: the dissimilarity the Element's pipeline standardizes and ranks.

Equations

• p.cosineDist q inv = 1 - p.cosineSim q inv

theorem Dunn2025.Grammar.cosineDist_self {C : Type u_1} (p : Grammar C) (inv : Finset C) (h : ∑ c ∈ inv, ↑(p.freq c) ^ 2 ≠ 0) : p.cosineDist p inv = 0

A nonzero profile is at distance 0 from itself.

theorem Dunn2025.Grammar.cosineDist_nonneg {C : Type u_1} (p q : Grammar C) (inv : Finset C) : 0 ≤ p.cosineDist q inv

theorem Dunn2025.Grammar.cosineDist_le_one {C : Type u_1} (p q : Grammar C) (inv : Finset C) : p.cosineDist q inv ≤ 1