Dunn (2025): Syntactic Variation from Individuals to Populations: Language as a Complex System

Dunn measures syntactic variation as differences in how individuals, populations and registers use one umbrella construction grammar. A construction is a contiguous sequence of slot-constraints, each drawn from one of three ontologies, lexical, syntactic or semantic. The grammar emerges in stages: two early grammars each draw on one ontology, lexical or syntactic, and the late grammar on all three. First-order constructions are bundled into third-order constructions and these into fourth-order ones, and a construction is central or peripheral by its frequency in a reference corpus. Two samples of usage are compared by the pipeline of Figure 3: token frequencies are standardized across the samples, weighted by how much the classifiers rely on each construction, compared by cosine distance, and the distances standardized across the sampled comparisons.

The two standardizations do what the book says they are for. Standardizing frequencies makes the distances blind to how frequent a construction is overall, standardizing distances keeps their ranking, and the sign of a set of comparisons' mean standardized distance says whether its samples are more or less similar than the average pair.

Main statements

• Stage.eq_semPlus_of_admits_of_ne: a construction that mixes ontologies emerges only in the late grammar.
• standardizedDistance_const_mul_add_const: rescaling a construction's frequencies across the samples changes no standardized distance.
• standardizedDistance_le_standardizedDistance_iff: the standardized distances rank the comparisons as the cosine distances do.
• sign_integral_standardizedDistance: the sign of a set of comparisons' mean standardized distance says whether its samples are more or less similar than average.

Implementation notes

• Learned syntactic categories are rendered by the part of speech of their exemplars, noun phrase slots as phrasal slots, and semantic constraints by their human-readable labels.
• The book does not say how the frequency of a higher-order construction is counted, so the pipeline is stated for any type of constructions and the network carries no frequencies.
• The sampled comparisons are a finite type mapped to pairs of samples, so a pair may be drawn twice.
• Grammar induction, the classifiers, the Bayesian confidence intervals, Figure 1's counts and the accuracy tables are not represented; the classifiers enter only through their weights.

TODO

• The accuracy tables, such as Table 6, belong in Data/Experiments.

References

• [Dun25]

Constructions and the stages of emergence

def Dunn2025.example1a : ConstructionGrammar.TypedForm String

(1a) is a ditransitive, with a semantic constraint on the verb and two noun phrases, as in send me the bill.

Equations

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

def Dunn2025.example1c : ConstructionGrammar.TypedForm String

(1c) puts lexical constraints in place of the semantic one and of the second noun phrase, as in give me a hand.

Equations

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

def Dunn2025.example2 : ConstructionGrammar.TypedForm String

(2) is an early noun phrase with two syntactic constraints, as in peanut butter cup.

Equations

• Dunn2025.example2 = [{ filler := ConstructionGrammar.SlotFiller.open_ UD.UPOS.NOUN }, { filler := ConstructionGrammar.SlotFiller.open_ UD.UPOS.NOUN }]

def Dunn2025.example3 : ConstructionGrammar.TypedForm String

(3) is a late noun phrase drawing on all three ontologies, as in the happiest person.

Equations

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

def Dunn2025.example5 : ConstructionGrammar.TypedForm String

(5) is a late construction with semantic constraints only, as in i know i'm.

Equations

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

inductive Dunn2025.Stage : Type

The stages of emergence are the columns of Figure 1, two early grammars and a late one.

• lexOnly : Stage

  LEX-Only is an early grammar with lexical constraints only.

• synOnly : Stage

  SYN-Only is an early grammar with syntactic constraints only.

• semPlus : Stage

  SEM+ is the late grammar, with constraints from all three ontologies.

@[instance_reducible]

instance Dunn2025.instDecidableEqStage : DecidableEq Stage

Equations

• Dunn2025.instDecidableEqStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dunn2025.instFintypeStage : Fintype Stage

Equations

• Dunn2025.instFintypeStage = { elems := { val := ↑Dunn2025.Stage.enumList, nodup := Dunn2025.Stage.enumList_nodup }, complete := Dunn2025.instFintypeStage._proof_1 }

def Dunn2025.Stage.levels : Stage → Finset ConstructionGrammar.RepresentationLevel

st.levels are the representation levels the grammar of stage st draws on.

Equations

• Dunn2025.Stage.lexOnly.levels = {ConstructionGrammar.RepresentationLevel.lex}
• Dunn2025.Stage.synOnly.levels = {ConstructionGrammar.RepresentationLevel.syn}
• Dunn2025.Stage.semPlus.levels = Finset.univ

def Dunn2025.Stage.Admits {Lex : Type u_1} (st : Stage) (form : ConstructionGrammar.TypedForm Lex) : Prop

The grammar of a stage can contain a construction when it draws on the level of each of the construction's slot-constraints.

Equations

• st.Admits form = ∀ s ∈ form, s.filler.level ∈ st.levels

@[instance_reducible]

instance Dunn2025.instDecidableAdmits {Lex : Type u_1} (st : Stage) (form : ConstructionGrammar.TypedForm Lex) : Decidable (st.Admits form)

Equations

• Dunn2025.instDecidableAdmits st form = Dunn2025.instDecidableAdmits._aux_1 st form

theorem Dunn2025.Stage.eq_semPlus_of_admits_of_ne {Lex : Type u_1} {st : Stage} {form : ConstructionGrammar.TypedForm Lex} {s t : ConstructionGrammar.Slot Lex} (h : st.Admits form) (hs : s ∈ form) (ht : t ∈ form) (hst : s.filler.level ≠ t.filler.level) : st = semPlus

A construction whose slot-constraints come from two ontologies emerges only in the late grammar.

theorem Dunn2025.Stage.eq_semPlus_of_admits_of_sem {Lex : Type u_1} {st : Stage} {form : ConstructionGrammar.TypedForm Lex} {s : ConstructionGrammar.Slot Lex} (h : st.Admits form) (hs : s ∈ form) (hsem : s.filler.level = ConstructionGrammar.RepresentationLevel.sem) : st = semPlus

A construction with a semantic constraint emerges only in the late grammar.

The network

structure Dunn2025.Network (C₁ : Type u_1) (C₃ : Type u_2) (C₄ : Type u_3) : Type (max (max u_1 u_2) u_3)

A network bundles every first-order construction into a third-order construction and every third-order construction into a fourth-order one.

• thirdOrder : C₁ → C₃

  thirdOrder c is the third-order construction bundling c.

• fourthOrder : C₃ → C₄

  fourthOrder d is the fourth-order construction bundling d.

def Dunn2025.Network.siblings {C₁ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_3} (n : Network C₁ C₃ C₄) : Setoid C₁

Two first-order constructions are siblings when they belong to one third-order construction.

Equations

• n.siblings = Setoid.ker n.thirdOrder

def Dunn2025.Network.cousins {C₁ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_3} (n : Network C₁ C₃ C₄) : Setoid C₁

Two first-order constructions are cousins when they belong to one fourth-order construction.

Equations

• n.cousins = Setoid.ker (n.fourthOrder ∘ n.thirdOrder)

@[instance_reducible]

instance Dunn2025.Network.instDecidableRelROfDecidableEq {C₁ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_3} (n : Network C₁ C₃ C₄) [DecidableEq C₃] : DecidableRel ⇑n.siblings

Equations

• n.instDecidableRelROfDecidableEq = Setoid.ker.decidableRel n.thirdOrder

@[instance_reducible]

instance Dunn2025.Network.instDecidableRelROfDecidableEq_1 {C₁ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_3} (n : Network C₁ C₃ C₄) [DecidableEq C₄] : DecidableRel ⇑n.cousins

Equations

• n.instDecidableRelROfDecidableEq_1 = Setoid.ker.decidableRel (n.fourthOrder ∘ n.thirdOrder)

theorem Dunn2025.Network.siblings_le_cousins {C₁ : Type u_1} {C₃ : Type u_2} {C₄ : Type u_3} (n : Network C₁ C₃ C₄) : n.siblings ≤ n.cousins

def Dunn2025.network6to11 : Network (Fin 6) (Fin 4) Unit

This network places (6) to (11), indexed in order. (6), (7) and (8) are siblings, and (9), (10) and (11) belong to other third-order constructions of the same fourth-order construction, here each to its own.

Equations

• Dunn2025.network6to11 = { thirdOrder := ![0, 0, 0, 1, 2, 3], fourthOrder := fun (x : Fin 4) => () }

Centrality, footnote 2

def Dunn2025.IsCentral {C : Type u_1} [MeasurableSpace C] (ref : C → ℝ) (c : C) : Prop

A construction is central when its frequency in the reference corpus is more than one standard deviation above the mean over the grammar's constructions.

Equations

• Dunn2025.IsCentral ref c = (1 < ProbabilityTheory.standardize ref (ProbabilityTheory.uniformOn Set.univ) c)

def Dunn2025.IsPeripheral {C : Type u_1} [MeasurableSpace C] (ref : C → ℝ) (c : C) : Prop

A construction is peripheral when its frequency in the reference corpus is below the mean; the constructions neither central nor peripheral are mid-frequency.

Equations

• Dunn2025.IsPeripheral ref c = (ProbabilityTheory.standardize ref (ProbabilityTheory.uniformOn Set.univ) c < 0)

theorem Dunn2025.IsCentral.not_isPeripheral {C : Type u_1} [MeasurableSpace C] {ref : C → ℝ} {c : C} (h : IsCentral ref c) : ¬IsPeripheral ref c

theorem Dunn2025.isCentral_iff {C : Type u_1} [MeasurableSpace C] {ref : C → ℝ} {c : C} (h : 0 < ProbabilityTheory.variance ref (ProbabilityTheory.uniformOn Set.univ)) : IsCentral ref c ↔ ∫ (x : C), ref x ∂ProbabilityTheory.uniformOn Set.univ + √(ProbabilityTheory.variance ref (ProbabilityTheory.uniformOn Set.univ)) < ref c

theorem Dunn2025.isPeripheral_iff {C : Type u_1} [MeasurableSpace C] {ref : C → ℝ} {c : C} (h : 0 < ProbabilityTheory.variance ref (ProbabilityTheory.uniformOn Set.univ)) : IsPeripheral ref c ↔ ref c < ∫ (x : C), ref x ∂ProbabilityTheory.uniformOn Set.univ

The similarity pipeline, Figure 3

noncomputable def Dunn2025.saliency {C : Type u_2} {K : Type u_3} [Fintype K] (W : K → C → ℝ) (c : C) : ℝ

The saliency of a construction is the mean absolute weight the classifiers give it across their classes.

Equations

• Dunn2025.saliency W c = Finset.univ.expect fun (k : K) => |W k c|

noncomputable def Dunn2025.standardizedUsage {S : Type u_1} {C : Type u_2} {K : Type u_3} [MeasurableSpace S] [Fintype K] (freq : S → C → ℝ) (W : K → C → ℝ) (s : S) : EuclideanSpace ℝ C

The standardized usage of a sample, steps 1 to 3, weights each construction's token frequency, standardized across the samples, by the construction's saliency.

Equations

• Dunn2025.standardizedUsage freq W s = WithLp.toLp 2 fun (c : C) => Dunn2025.saliency W c * ProbabilityTheory.standardize (fun (x : S) => freq x c) (ProbabilityTheory.uniformOn Set.univ) s

theorem Dunn2025.standardizedUsage_const_mul_add_const {S : Type u_1} {C : Type u_2} {K : Type u_3} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} [Finite S] [Nonempty S] [MeasurableSingletonClass S] {a : C → ℝ} (ha : ∀ (c : C), 0 < a c) (b : C → ℝ) : standardizedUsage (fun (s : S) (c : C) => a c * freq s c + b c) W = standardizedUsage freq W

Rescaling and shifting a construction's frequencies across all the samples changes no sample's standardized usage.

noncomputable def Dunn2025.cosineDistance {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) : ℝ

The cosine distance of two vectors is one minus the cosine of the angle between them.

Equations

• Dunn2025.cosineDistance x y = 1 - Real.cos (InnerProductGeometry.angle x y)

theorem Dunn2025.cosineDistance_comm {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x y : V) : cosineDistance x y = cosineDistance y x

noncomputable def Dunn2025.sampleDistance {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] [Fintype C] (freq : S → C → ℝ) (W : K → C → ℝ) (pair : P → S × S) (p : P) : ℝ

The distance of a sampled comparison, step 4, is the cosine distance between the standardized usage of its two samples.

Equations

• Dunn2025.sampleDistance freq W pair p = Dunn2025.cosineDistance (Dunn2025.standardizedUsage freq W (pair p).1) (Dunn2025.standardizedUsage freq W (pair p).2)

theorem Dunn2025.sampleDistance_swap {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} {pair : P → S × S} [Fintype C] : sampleDistance freq W (Prod.swap ∘ pair) = sampleDistance freq W pair

Distances are symmetric, so a comparison does not depend on the order of its samples.

noncomputable def Dunn2025.standardizedDistance {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] [Fintype C] [MeasurableSpace P] (freq : S → C → ℝ) (W : K → C → ℝ) (pair : P → S × S) : P → ℝ

The standardized distances, step 5, are the sample distances standardized across the comparisons.

Equations

• Dunn2025.standardizedDistance freq W pair = ProbabilityTheory.standardize (Dunn2025.sampleDistance freq W pair) (ProbabilityTheory.uniformOn Set.univ)

theorem Dunn2025.standardizedDistance_const_mul_add_const {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} {pair : P → S × S} [Fintype C] [MeasurableSpace P] [Finite S] [Nonempty S] [MeasurableSingletonClass S] {a : C → ℝ} (ha : ∀ (c : C), 0 < a c) (b : C → ℝ) : standardizedDistance (fun (s : S) (c : C) => a c * freq s c + b c) W pair = standardizedDistance freq W pair

How frequent a construction is overall does not affect any standardized distance.

theorem Dunn2025.standardizedDistance_le_standardizedDistance_iff {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} {pair : P → S × S} [Fintype C] [MeasurableSpace P] (h : 0 < ProbabilityTheory.variance (sampleDistance freq W pair) (ProbabilityTheory.uniformOn Set.univ)) {p q : P} : standardizedDistance freq W pair p ≤ standardizedDistance freq W pair q ↔ sampleDistance freq W pair p ≤ sampleDistance freq W pair q

Standardizing the distances keeps their ranking, from the most to the least similar pair.

theorem Dunn2025.integral_standardizedDistance {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} {pair : P → S × S} [Fintype C] [MeasurableSpace P] [Finite P] [MeasurableSingletonClass P] [Nonempty P] : ∫ (x : P), standardizedDistance freq W pair x ∂ProbabilityTheory.uniformOn Set.univ = 0

A standardized distance of 0 is the average distance.

theorem Dunn2025.sign_integral_standardizedDistance {S : Type u_1} {C : Type u_2} {K : Type u_3} {P : Type u_4} [MeasurableSpace S] [Fintype K] {freq : S → C → ℝ} {W : K → C → ℝ} {pair : P → S × S} [Fintype C] [MeasurableSpace P] [Finite P] [MeasurableSingletonClass P] {T : Finset P} (hT : T.Nonempty) : SignType.sign (∫ (x : P), standardizedDistance freq W pair x ∂ProbabilityTheory.uniformOn ↑T) = SignType.sign (∫ (x : P), sampleDistance freq W pair x ∂ProbabilityTheory.uniformOn ↑T - ∫ (x : P), sampleDistance freq W pair x ∂ProbabilityTheory.uniformOn Set.univ)

Comparisons within T are more similar than average exactly when their mean standardized distance is negative, and more different exactly when it is positive.