O'Donnell (2015): Productivity and Reuse in Language

This file formalizes the central empirical contrast of the seventh chapter of [OD15] on English derivational morphology: the nominalizer -ness is productive while -ion and the verb-forming -ate are not, and of the competing models only the fragment grammar recovers this, the Dirichlet-multinomial probabilistic context-free grammar ranking the token-frequent -ion first. The three suffixes carry a productivity ordering (Suffix.productivityIndex, moreProductiveThan) grounded in the hapax-based statistics of Baayen that the book correlates with its models (ness_hapax_richer, ness_higher_type_token_ratio, ion_token_frequency_dominates), the book's adaptor and fragment grammars are built over the Dirichlet PCFG of DirichletPCFG (AdaptorGrammar, FragmentGrammar), the suffixes are rules of a toy grammar (suffixGrammar), and a Dirichlet prior whose pseudo-counts track the empirical productivity is exhibited (suffixPrior, suffixPrior_pseudo_respects_productivity).

Implementation notes

The -ate rule produces verbs from bound stems, so the three suffixes are grouped by the book's contrast rather than by output category; the ordering of -ion above -ate is a tie-break between two unproductive suffixes, not part of the book's claim. The pseudo-counts are stipulated to track productivity, not learned from a corpus, which is the book's point against the token-frequency model.

References

• [OD15]
• [Kip73]
• [Pit06]

The three suffixes

[OD15] Chapter 7's central productivity contrast (pp. 261–263). The terms "productive" and "unproductive" are pre-theoretic descriptions consistent with the literature the book reviews; the data below commits to nothing about why one suffix is productive and another is not.

inductive ODonnell2015.Suffix : Type

The three English derivational suffixes of the Chapter 7 contrast.

• -ness (Adj>N): "perhaps the most commonly-discussed productive suffix in English" (p. 261); pine-scented → pine-scentedness.
• -ion (V>N): high type and token frequency but unproductive on novel verbs — the competing models' "obviously absurd prediction" is that it attaches to arbitrary verbs, producing *meetion "a MEETING event" (pp. 261–262).
• -ate (BND>V): a verb-forming suffix "restricted, by its categorial definition, from attaching to anything besides bound stems" (p. 263), e.g. segregate from bound segregat-.

• ness : Suffix
• ion : Suffix
• ate : Suffix

@[instance_reducible]

instance ODonnell2015.instDecidableEqSuffix : DecidableEq Suffix

Equations

• ODonnell2015.instDecidableEqSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ODonnell2015.instReprSuffix : Repr Suffix

Equations

• ODonnell2015.instReprSuffix = { reprPrec := ODonnell2015.instReprSuffix.repr }

def ODonnell2015.instReprSuffix.repr : Suffix → ℕ → Std.Format

Equations

• ODonnell2015.instReprSuffix.repr ODonnell2015.Suffix.ness prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Suffix.ness")).group prec✝
• ODonnell2015.instReprSuffix.repr ODonnell2015.Suffix.ion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Suffix.ion")).group prec✝
• ODonnell2015.instReprSuffix.repr ODonnell2015.Suffix.ate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Suffix.ate")).group prec✝

def ODonnell2015.Suffix.productivityIndex : Suffix → ℕ

A pre-theoretic productivity index for the three suffixes — higher is more productive. Coding ness > ion > ate reproduces the ordering implied by [OD15] Chapter 7 (Fig 7.3 and the §7.3.1.1 discussion). The ion > ate direction is a tie-break: both are unproductive on novel forms, but ate is structurally more restricted (bound stems only), so we rank it strictly lower.

Equations

• ODonnell2015.Suffix.ness.productivityIndex = 2
• ODonnell2015.Suffix.ion.productivityIndex = 1
• ODonnell2015.Suffix.ate.productivityIndex = 0

def ODonnell2015.moreProductiveThan (a b : Suffix) : Prop

The pre-theoretic strict ordering on the three suffixes by productivity. Any theory of productivity that purports to account for the [OD15] Chapter 7 data must reproduce this ordering; failure to do so falsifies the theory against the data (this is exactly the discriminator deployed against the Dirichlet PCFG, MAG, DOP1 and ENDOP in Fig 7.3, all of which place -ion in their top 5).

Equations

• ODonnell2015.moreProductiveThan a b = (a.productivityIndex > b.productivityIndex)

@[instance_reducible]

instance ODonnell2015.instDecidableRelSuffixMoreProductiveThan : DecidableRel moreProductiveThan

Equations

• ODonnell2015.instDecidableRelSuffixMoreProductiveThan a b = { decide := b.productivityIndex.succ.ble a.productivityIndex, reflects_decide := ⋯ }

Frequency-spectrum statistics (Fig 7.4, pp. 267–268)

The book's distributional evidence: -ness has the "large number of rare events" (LNRE) shape characteristic of a productive process — a spectrum "sharply peaked at low-frequency forms"; -ion's spectrum has few hapaxes and spreads its mass through higher frequency ranges (cf. §1.2.6 and Fig 1.1 on unproductive -ity/-th). Fig 7.4 reports spectra for -ness and -ion only; the book gives no spectrum for -ate, whose unproductivity is categorial (bound stems only).

structure ODonnell2015.SpectrumStats : Type

Corpus statistics for a suffix in the Chapter 7 training corpus (CELEX-derived): word types, word tokens, hapax legomena.

• wordTypes : ℕ
• wordTokens : ℕ
• hapaxes : ℕ

def ODonnell2015.instDecidableEqSpectrumStats.decEq (x✝ x✝¹ : SpectrumStats) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ODonnell2015.instDecidableEqSpectrumStats : DecidableEq SpectrumStats

Equations

• ODonnell2015.instDecidableEqSpectrumStats = ODonnell2015.instDecidableEqSpectrumStats.decEq

@[instance_reducible]

instance ODonnell2015.instReprSpectrumStats : Repr SpectrumStats

Equations

• ODonnell2015.instReprSpectrumStats = { reprPrec := ODonnell2015.instReprSpectrumStats.repr }

def ODonnell2015.instReprSpectrumStats.repr : SpectrumStats → ℕ → Std.Format

Equations

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

def ODonnell2015.nessStats : SpectrumStats

-ness has 1024 word types, 15,568 tokens and 350 hapaxes ([OD15] pp. 267–268). Its spectrum is LNRE-shaped, hapax-rich and peaked at frequency 1 (Fig 7.4, left).

Equations

• ODonnell2015.nessStats = { wordTypes := 1024, wordTokens := 15568, hapaxes := 350 }

def ODonnell2015.ionStats : SpectrumStats

-ion has 1117 word types, 162,573 tokens and 83 hapaxes ([OD15] pp. 267–268). Its spectrum is not LNRE-shaped, being hapax-poor with its mass spread toward higher frequencies (Fig 7.4, right).

Equations

• ODonnell2015.ionStats = { wordTypes := 1117, wordTokens := 162573, hapaxes := 83 }

theorem ODonnell2015.ness_hapax_richer : nessStats.hapaxes * ionStats.wordTypes > ionStats.hapaxes * nessStats.wordTypes

-ness is hapax-richer than -ion (350/1024 vs 83/1117) — the distributional fingerprint of productivity that Baayen's hapax-based estimators measure and that the FG model exploits (p. 268). Stated by cross-multiplication to stay in Nat.

theorem ODonnell2015.ness_higher_type_token_ratio : nessStats.wordTypes * ionStats.wordTokens > ionStats.wordTypes * nessStats.wordTokens

-ness has the higher type–token ratio (1024/15,568 vs 1117/162,573): -ion's distribution is dominated by reuse of high-frequency existing words, not novel coinage.

theorem ODonnell2015.ion_token_frequency_dominates : ionStats.wordTokens > 10 * nessStats.wordTokens

-ion has more than an order of magnitude more tokens than -ness — the token-frequency gap that misleads the Dirichlet PCFG, which "bases productivity inferences purely on the token frequency of suffixes" (p. 268).

Adaptor and fragment grammars (§3.1.7, §3.1.8)

An adaptor grammar in the book's maximum-a-posteriori variant is a Dirichlet PCFG with a Pitman–Yor process at each nonterminal memoising the subtrees computed there. The corpus probability is stated given the latent table assignment Y, per nonterminal a set partition of the uses of that nonterminal by the table they sat at, since marginalising over Y is the inference problem of §3.2. A table assignment at a nonterminal is a set partition of Fin n, a Finpartition, and its Pitman–Yor factor is its probability under the seating plan, pitmanYor, which depends only on the block sizes ([Pit06]).

structure ODonnell2015.AdaptorGrammar {T : Type} [DecidableEq T] (G : ContextFreeGrammar T) [DecidableEq G.NT] extends DirichletPCFG G : Type

The book's adaptor grammar over G is a Dirichlet PCFG with a Pitman–Yor process memoising the subtrees rooted at each nonterminal.

• pseudo : ContextFreeRule T G.NT → ℝ
• pseudo_pos (r : ContextFreeRule T G.NT) : r ∈ G.rules → 0 < self.pseudo r
• discount : G.NT → ℝ

  The discount of the Pitman–Yor process memoising expansions of each nonterminal.

• concentration : G.NT → ℝ

  The concentration of the Pitman–Yor process memoising expansions of each nonterminal.

• discount_nonneg (a : G.NT) : 0 ≤ self.discount a

  The discount is nonnegative.

• discount_le_one (a : G.NT) : self.discount a ≤ 1

  The discount is at most 1.

• neg_discount_lt_concentration (a : G.NT) : -self.discount a < self.concentration a

  The concentration exceeds minus the discount. With the bounds on the discount, this is the constraint under which the seating plan is a probability ([Pit06] (3.5)).

theorem ODonnell2015.AdaptorGrammar.ext {T : Type} {inst✝ : DecidableEq T} {G : ContextFreeGrammar T} {inst✝¹ : DecidableEq G.NT} {x y : AdaptorGrammar G} (pseudo : x.pseudo = y.pseudo) (discount : x.discount = y.discount) (concentration : x.concentration = y.concentration) : x = y

theorem ODonnell2015.AdaptorGrammar.ext_iff {T : Type} {inst✝ : DecidableEq T} {G : ContextFreeGrammar T} {inst✝¹ : DecidableEq G.NT} {x y : AdaptorGrammar G} : x = y ↔ x.pseudo = y.pseudo ∧ x.discount = y.discount ∧ x.concentration = y.concentration

@[reducible, inline]

abbrev ODonnell2015.AdaptorGrammar.TableAssignment {T : Type} (G : ContextFreeGrammar T) : Type

The latent table assignment Y gives, for each nonterminal, a set partition of its uses in the corpus by the table they sat at. Consistency with the corpus is the caller's hypothesis.

Equations

• ODonnell2015.AdaptorGrammar.TableAssignment G = (G.NT → (n : ℕ) × Finpartition Finset.univ)

noncomputable def ODonnell2015.AdaptorGrammar.pypFactor {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (a : G.NT) (Y : TableAssignment G) : ℝ

The Pitman–Yor probability of the table assignment at nonterminal a.

Equations

• M.pypFactor a Y = (ProbabilityTheory.pitmanYor (M.discount a) (M.concentration a) (Y a).fst).real {(Y a).snd}

theorem ODonnell2015.AdaptorGrammar.pypFactor_eq {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (a : G.NT) (Y : TableAssignment G) : M.pypFactor a Y = ProbabilityTheory.pitmanYorEPPF (M.discount a) (M.concentration a) (Y a).snd.partSizes

The Pitman–Yor factor is the EPPF of the table sizes ([Pit06] Theorem 3.2).

noncomputable def ODonnell2015.AdaptorGrammar.corpusProbGivenTables {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) (Y : TableAssignment G) : ℝ

The corpus probability given a table assignment is the product, over the nonterminals the grammar expands, of the Dirichlet PCFG factor and the Pitman–Yor factor.

Equations

• M.corpusProbGivenTables D Y = ∏ a ∈ Finset.image (fun (x : ContextFreeRule T G.NT) => x.input) G.rules, M.lhsFactor a D * M.pypFactor a Y

theorem ODonnell2015.AdaptorGrammar.corpusProbGivenTables_nonneg {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) (Y : TableAssignment G) : 0 ≤ M.corpusProbGivenTables D Y

def ODonnell2015.AdaptorGrammar.emptyTables {T : Type} (G : ContextFreeGrammar T) : TableAssignment G

The table assignment with no customers at any nonterminal.

Equations

• ODonnell2015.AdaptorGrammar.emptyTables G x✝ = ⟨0, ⊥⟩

@[simp]

theorem ODonnell2015.AdaptorGrammar.pypFactor_emptyTables {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (a : G.NT) : M.pypFactor a (emptyTables G) = 1

@[simp]

theorem ODonnell2015.AdaptorGrammar.corpusProbGivenTables_empty {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) : M.corpusProbGivenTables 0 (emptyTables G) = 1

noncomputable def ODonnell2015.AdaptorGrammar.posterior {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) : AdaptorGrammar G

The conjugate update of the Dirichlet component by a corpus; the Pitman–Yor hyperparameters are unchanged.

Equations

• M.posterior D = { toDirichletPCFG := M.posterior D, discount := M.discount, concentration := M.concentration, discount_nonneg := ⋯, discount_le_one := ⋯, neg_discount_lt_concentration := ⋯ }

@[simp]

theorem ODonnell2015.AdaptorGrammar.posterior_zero {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) : M.posterior 0 = M

theorem ODonnell2015.AdaptorGrammar.posterior_add {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : AdaptorGrammar G) (D₁ D₂ : Multiset (RoseTree (Symbol T G.NT))) : M.posterior (D₁ + D₂) = (M.posterior D₁).posterior D₂

Expanding a rule r, a fragment grammar decides at each right-hand-side nonterminal B whether to expand B productively or to halt and leave B an open slot of the fragment being stored. The decision is a biased coin whose weight has a beta prior with pseudo-counts ψ_{r,B}; integrating the weight out turns the decisions at that slot into a two-colour Pólya urn, which is the representation the book computes with. The halt count Z is latent like Y; the book writes the halt count at a slot of r as x_r - z_{r,B}, so a Z consistent with the corpus has Z r i .recurse + Z r i .halt equal to the corpus count of r.

inductive ODonnell2015.FragmentGrammar.Decision : Type

The outcome of the lazy coin at a nonterminal slot is recurse, which expands the slot productively, or halt, which leaves it open in the stored fragment.

• recurse : Decision
• halt : Decision

@[instance_reducible]

instance ODonnell2015.FragmentGrammar.instDecidableEqDecision : DecidableEq Decision

Equations

• ODonnell2015.FragmentGrammar.instDecidableEqDecision x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ODonnell2015.FragmentGrammar.instFintypeDecision : Fintype Decision

Equations

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

@[instance_reducible]

instance ODonnell2015.FragmentGrammar.instInhabitedDecision : Inhabited Decision

Equations

• ODonnell2015.FragmentGrammar.instInhabitedDecision = { default := ODonnell2015.FragmentGrammar.instInhabitedDecision.default }

structure ODonnell2015.FragmentGrammar {T : Type} [DecidableEq T] (G : ContextFreeGrammar T) [DecidableEq G.NT] extends ODonnell2015.AdaptorGrammar G : Type

A fragment grammar over G is an adaptor grammar with, at each nonterminal position of each rule, a Pólya urn over recurse/halt decisions whose pseudo-counts are the beta parameters ψ_{r,B}.

• pseudo : ContextFreeRule T G.NT → ℝ
• pseudo_pos (r : ContextFreeRule T G.NT) : r ∈ G.rules → 0 < self.pseudo r
• discount : G.NT → ℝ
• concentration : G.NT → ℝ
• discount_nonneg (a : G.NT) : 0 ≤ self.discount a
• discount_le_one (a : G.NT) : self.discount a ≤ 1
• neg_discount_lt_concentration (a : G.NT) : -self.discount a < self.concentration a
• halt (r : ContextFreeRule T G.NT) : r.NonterminalPos → Decision → ℝ

  The pseudo-counts of the urn over recurse/halt decisions at nonterminal position i of rule r.

• halt_pos (r : ContextFreeRule T G.NT) (i : r.NonterminalPos) (d : Decision) : 0 < self.halt r i d

  The pseudo-counts are positive.

theorem ODonnell2015.FragmentGrammar.ext_iff {T : Type} {inst✝ : DecidableEq T} {G : ContextFreeGrammar T} {inst✝¹ : DecidableEq G.NT} {x y : FragmentGrammar G} : x = y ↔ x.pseudo = y.pseudo ∧ x.discount = y.discount ∧ x.concentration = y.concentration ∧ x.halt = y.halt

theorem ODonnell2015.FragmentGrammar.ext {T : Type} {inst✝ : DecidableEq T} {G : ContextFreeGrammar T} {inst✝¹ : DecidableEq G.NT} {x y : FragmentGrammar G} (pseudo : x.pseudo = y.pseudo) (discount : x.discount = y.discount) (concentration : x.concentration = y.concentration) (halt : x.halt = y.halt) : x = y

@[reducible, inline]

abbrev ODonnell2015.FragmentGrammar.HaltCounts {T : Type} (G : ContextFreeGrammar T) : Type

The latent variable Z counts, at each nonterminal position of each rule, the recurse and the halt decisions taken there across the corpus.

Equations

• ODonnell2015.FragmentGrammar.HaltCounts G = ((r : ContextFreeRule T G.NT) → r.NonterminalPos → ODonnell2015.FragmentGrammar.Decision → ℕ)

noncomputable def ODonnell2015.FragmentGrammar.corpusProbGivenStorage {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) (Y : AdaptorGrammar.TableAssignment G) (Z : HaltCounts G) : ℝ

The corpus probability given a table assignment Y and halt counts Z is the adaptor-grammar factor times, at each nonterminal slot, the urn likelihood of the decisions taken there.

Equations

• M.corpusProbGivenStorage D Y Z = M.corpusProbGivenTables D Y * ∏ r ∈ G.rules, ∏ i : r.NonterminalPos, ProbabilityTheory.polyaUrnProb (M.halt r i) (Z r i)

theorem ODonnell2015.FragmentGrammar.corpusProbGivenStorage_nonneg {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) (Y : AdaptorGrammar.TableAssignment G) (Z : HaltCounts G) : 0 ≤ M.corpusProbGivenStorage D Y Z

@[simp]

theorem ODonnell2015.FragmentGrammar.corpusProbGivenStorage_empty {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) : M.corpusProbGivenStorage 0 (AdaptorGrammar.emptyTables G) 0 = 1

noncomputable def ODonnell2015.FragmentGrammar.posterior {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) (D : Multiset (RoseTree (Symbol T G.NT))) (Z : HaltCounts G) : FragmentGrammar G

In the conjugate update by a corpus D and its halt counts Z, the adaptor-grammar component absorbs the rule counts of D, and the urn at each slot absorbs the decisions taken there.

Equations

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

@[simp]

theorem ODonnell2015.FragmentGrammar.posterior_zero {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) : M.posterior 0 0 = M

theorem ODonnell2015.FragmentGrammar.posterior_add {T : Type} [DecidableEq T] {G : ContextFreeGrammar T} [DecidableEq G.NT] (M : FragmentGrammar G) (D₁ D₂ : Multiset (RoseTree (Symbol T G.NT))) (Z₁ Z₂ : HaltCounts G) : M.posterior (D₁ + D₂) (Z₁ + Z₂) = (M.posterior D₁ Z₁).posterior D₂ Z₂

Toy CFG

inductive ODonnell2015.Sym : Type

The six terminal symbols of the toy derivational grammar: sentinels adj/v/bnd for adjective, verb and bound-stem bases, plus the three derivational suffixes -ness, -ion, -ate.

• adj : Sym
• v : Sym
• bnd : Sym
• ness : Sym
• ion : Sym
• ate : Sym

@[instance_reducible]

instance ODonnell2015.instDecidableEqSym : DecidableEq Sym

Equations

• ODonnell2015.instDecidableEqSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ODonnell2015.instReprSym.repr : Sym → ℕ → Std.Format

Equations

• ODonnell2015.instReprSym.repr ODonnell2015.Sym.adj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.adj")).group prec✝
• ODonnell2015.instReprSym.repr ODonnell2015.Sym.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.v")).group prec✝
• ODonnell2015.instReprSym.repr ODonnell2015.Sym.bnd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.bnd")).group prec✝
• ODonnell2015.instReprSym.repr ODonnell2015.Sym.ness prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.ness")).group prec✝
• ODonnell2015.instReprSym.repr ODonnell2015.Sym.ion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.ion")).group prec✝
• ODonnell2015.instReprSym.repr ODonnell2015.Sym.ate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.Sym.ate")).group prec✝

@[instance_reducible]

instance ODonnell2015.instReprSym : Repr Sym

Equations

• ODonnell2015.instReprSym = { reprPrec := ODonnell2015.instReprSym.repr }

inductive ODonnell2015.SuffixNT : Type

The four nonterminals of the toy derivational grammar. BND represents a bound stem — the selectional restriction of -ate (cf. segregat-, demonstrat-).

• N : SuffixNT
• A : SuffixNT
• V : SuffixNT
• BND : SuffixNT

@[instance_reducible]

instance ODonnell2015.instDecidableEqSuffixNT : DecidableEq SuffixNT

Equations

• ODonnell2015.instDecidableEqSuffixNT x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ODonnell2015.instReprSuffixNT.repr : SuffixNT → ℕ → Std.Format

Equations

• ODonnell2015.instReprSuffixNT.repr ODonnell2015.SuffixNT.N prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.SuffixNT.N")).group prec✝
• ODonnell2015.instReprSuffixNT.repr ODonnell2015.SuffixNT.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.SuffixNT.A")).group prec✝
• ODonnell2015.instReprSuffixNT.repr ODonnell2015.SuffixNT.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.SuffixNT.V")).group prec✝
• ODonnell2015.instReprSuffixNT.repr ODonnell2015.SuffixNT.BND prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ODonnell2015.SuffixNT.BND")).group prec✝

@[instance_reducible]

instance ODonnell2015.instReprSuffixNT : Repr SuffixNT

Equations

• ODonnell2015.instReprSuffixNT = { reprPrec := ODonnell2015.instReprSuffixNT.repr }

def ODonnell2015.rNess : ContextFreeRule Sym SuffixNT

Rule N → A · ness.

Equations

• ODonnell2015.rNess = { input := ODonnell2015.SuffixNT.N, output := [Symbol.nonterminal ODonnell2015.SuffixNT.A, Symbol.terminal ODonnell2015.Sym.ness] }

def ODonnell2015.rIon : ContextFreeRule Sym SuffixNT

Rule N → V · ion.

Equations

• ODonnell2015.rIon = { input := ODonnell2015.SuffixNT.N, output := [Symbol.nonterminal ODonnell2015.SuffixNT.V, Symbol.terminal ODonnell2015.Sym.ion] }

def ODonnell2015.rAte : ContextFreeRule Sym SuffixNT

Rule V → BND · ate. Reflects [OD15]'s -ate:BND>V classification (p. 261): -ate is a verb-forming suffix that selects bound stems, not a noun-forming suffix.

Equations

• ODonnell2015.rAte = { input := ODonnell2015.SuffixNT.V, output := [Symbol.nonterminal ODonnell2015.SuffixNT.BND, Symbol.terminal ODonnell2015.Sym.ate] }

def ODonnell2015.rAdj : ContextFreeRule Sym SuffixNT

Rule A → adj.

Equations

• ODonnell2015.rAdj = { input := ODonnell2015.SuffixNT.A, output := [Symbol.terminal ODonnell2015.Sym.adj] }

def ODonnell2015.rV : ContextFreeRule Sym SuffixNT

Rule V → v.

Equations

• ODonnell2015.rV = { input := ODonnell2015.SuffixNT.V, output := [Symbol.terminal ODonnell2015.Sym.v] }

def ODonnell2015.rBnd : ContextFreeRule Sym SuffixNT

Rule BND → bnd.

Equations

• ODonnell2015.rBnd = { input := ODonnell2015.SuffixNT.BND, output := [Symbol.terminal ODonnell2015.Sym.bnd] }

def ODonnell2015.suffixGrammar : ContextFreeGrammar Sym

The toy CFG has nominalisation via -ness (from adjective) or -ion (from verb), and verb formation via -ate (from bound stem).

Equations

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

@[instance_reducible]

instance ODonnell2015.instDecidableEqNTSymSuffixGrammar : DecidableEq suffixGrammar.NT

DecidableEq for the grammar's NT projection — needed by DirichletPCFG's typeclass arguments. Not synthesised automatically because suffixGrammar.NT is a structure projection that the typeclass solver does not reduce to SuffixNT.

Equations

• ODonnell2015.instDecidableEqNTSymSuffixGrammar = ODonnell2015.instDecidableEqNTSymSuffixGrammar._aux_1

The Dirichlet prior over the toy grammar

def ODonnell2015.suffixToRule : Suffix → ContextFreeRule Sym SuffixNT

Bridge from Suffix to the rules of this grammar.

Equations

• ODonnell2015.suffixToRule ODonnell2015.Suffix.ness = ODonnell2015.rNess
• ODonnell2015.suffixToRule ODonnell2015.Suffix.ion = ODonnell2015.rIon
• ODonnell2015.suffixToRule ODonnell2015.Suffix.ate = ODonnell2015.rAte

def ODonnell2015.pseudoVal (r : ContextFreeRule Sym SuffixNT) : ℝ

Per-rule pseudo-count for the toy grammar. The three productivity-bearing rules get productivityIndex + 1 (so ness ↦ 3, ion ↦ 2, ate ↦ 1), inheriting both the strict ordering and any future revision of Suffix.productivityIndex. The three structural selectional rules get a neutral 1.

Equations

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

def ODonnell2015.suffixPrior : DirichletPCFG suffixGrammar

The Dirichlet prior over suffixGrammar whose pseudo-counts derive from Suffix.productivityIndex, so revising the ranking changes the prior in lockstep.

Equations

• ODonnell2015.suffixPrior = { pseudo := ODonnell2015.pseudoVal, pseudo_pos := ⋯ }

Theorems

theorem ODonnell2015.corpusProb_pos_for_empty (M : DirichletPCFG suffixGrammar) : 0 < M.corpusProb 0

Any Dirichlet PCFG over suffixGrammar assigns probability 1, hence positive probability, to the empty corpus.

theorem ODonnell2015.suffixPrior_pseudo_respects_productivity {a b : Suffix} (h : moreProductiveThan a b) : suffixPrior.pseudo (suffixToRule a) > suffixPrior.pseudo (suffixToRule b)

A stronger productivity ranking (moreProductiveThan) implies a larger pseudo-count for the corresponding rule, so a revision of Suffix.productivityIndex that contradicts the rule-level encoding breaks here.

theorem ODonnell2015.suffixPrior_predictive_lt_of_count_gap (D : Multiset (RoseTree (Symbol Sym SuffixNT))) (h : RoseTree.corpusRuleCount rNess D + 1 < RoseTree.corpusRuleCount rIon D) : suffixPrior.predictive rNess D < suffixPrior.predictive rIon D

The failure mode of the Dirichlet PCFG the book documents in Chapter 7 (p. 268, with the CELEX evidence of Fig 7.4 on p. 267): its posterior predictive tracks pseudo-count plus corpus count, so any corpus in which rIon derivations exceed rNess derivations by more than the pseudo-count gap of 1 ranks rIon above rNess, against moreProductiveThan ness ion. The CELEX token gap is an order of magnitude larger than the hypothesis requires.

theorem ODonnell2015.suffixPrior_predictive_prior_lt : suffixPrior.predictive rIon 0 < suffixPrior.predictive rNess 0

With no data the Dirichlet PCFG orders the nominalising rules correctly, since the prior predictive is the normalised pseudo-count and pseudoVal rNess > pseudoVal rIon. The model's failure is data-driven, not prior-driven.

theorem ODonnell2015.suffixPrior_predictivePCFG_prior_lt : (suffixPrior.predictivePCFG 0).weight rIon < (suffixPrior.predictivePCFG 0).weight rNess

The same prior comparison as a fact about the predictive PCFG, the point estimate the Dirichlet prior induces.

theorem ODonnell2015.suffixPrior_prior_and_posterior_disagree (D : Multiset (RoseTree (Symbol Sym SuffixNT))) (h : RoseTree.corpusRuleCount rNess D + 1 < RoseTree.corpusRuleCount rIon D) : suffixPrior.predictive rIon 0 < suffixPrior.predictive rNess 0 ∧ suffixPrior.predictive rNess D < suffixPrior.predictive rIon D

The Chapter 7 critique of the Dirichlet PCFG in one theorem is that it is right without data and wrong once -ion tokens dominate. The fix the book proposes, the fragment grammar, gives a posterior that does not collapse productivity into raw frequency.

The Probabilistic Elsewhere Condition (§5.5.3)

[OD15] §5.5.3 (pp. 189–191) derives the Elsewhere Condition — "also known as Pāṇini's principle, pre-emption, the subset principle, or the blocking principle" — from probabilistic inference alone: rules define distributions over the forms they generate, so a rule whose support properly includes another's "must assign lower probability to each of those forms, on average" (conservation of belief), and conditioning preserves the preference. The book quotes [Kip73]'s formulation — prefer r₂ when Inputs(r₂) ⊂ Inputs(r₁) — which is Morphology.Exponence.Rule's specificity order (applicability-set inclusion, Exponence.toPreorder).

Formalized over Exponence.DomainRule, a rule's support being its domain, in the uniform-generation case, where the preference is pointwise rather than on average: nested supports give the narrower rule a strictly higher generation probability at every shared form (genProb_lt_of_ssubset), and a likelihood-maximal rule among a vocabulary's generators is an Elsewhere winner (maxGenProb_isElsewhereWinner) — no nesting or comparability assumption needed, because card-minimality forces ⊆-minimality. Since higher probability is smaller support (genProb_le_iff_card_le), this is the size principle as a specificity score in the shared core: selectByCard_isElsewhereWinner runs Exponence.RuleSet.selectBy on the dualized support cardinality, discharging the core's conditional soundness law via Finset.eq_of_subset_of_card_le.

def ODonnell2015.genProb {Ctx : Type u_1} [DecidableEq Ctx] (s : Finset Ctx) (c : Ctx) : ℚ

Uniform generation probability over a finite support — the uniform case of [OD15] §5.5.3's rules-as-distributions.

Equations

• ODonnell2015.genProb s c = if c ∈ s then (↑s.card)⁻¹ else 0

theorem ODonnell2015.genProb_lt_of_ssubset {Ctx : Type u_1} [DecidableEq Ctx] {s₁ s₂ : Finset Ctx} (h : s₂ ⊂ s₁) {c : Ctx} (hc : c ∈ s₂) : genProb s₁ c < genProb s₂ c

By the pointwise probabilistic Elsewhere Condition, at every shared form a properly narrower rule assigns strictly higher probability.

theorem ODonnell2015.genProb_le_iff_card_le {Ctx : Type u_1} [DecidableEq Ctx] {s₁ s₂ : Finset Ctx} {c : Ctx} (h₁ : c ∈ s₁) (h₂ : c ∈ s₂) : genProb s₁ c ≤ genProb s₂ c ↔ s₂.card ≤ s₁.card

Uniform generation probability ranks supports by cardinality at a shared form: a rule assigns at least as much probability iff its support is no larger. The monotone bridge from maximum-likelihood selection to the support-cardinality specificity score — maximizing probability is minimizing support cardinality.

theorem ODonnell2015.selectByCard_isElsewhereWinner {Ctx : Type u_1} {F : Type u_2} [DecidableEq Ctx] {v : Morphology.Exponence.RuleSet (Morphology.Exponence.DomainRule Ctx F)} {c : Ctx} {r : Morphology.Exponence.DomainRule Ctx F} (h : v.selectBy (fun (s : Morphology.Exponence.DomainRule Ctx F) => OrderDual.toDual s.dom.card) c = some r) : v.IsElsewhereWinner c r

The size principle as a specificity score ([OD15] §5.5.3): selecting the finitely supported rule of least support cardinality — dualized so smaller supports win the argmax — through the shared core's Exponence.RuleSet.selectBy yields an Elsewhere winner. Minimizing support cardinality is maximizing uniform generation probability (genProb_le_iff_card_le), so this is Elsewhere selection as maximum-likelihood inference, on record as a score.

theorem ODonnell2015.maxGenProb_isElsewhereWinner {Ctx : Type u_1} {F : Type u_2} [DecidableEq Ctx] {v : Morphology.Exponence.RuleSet (Morphology.Exponence.DomainRule Ctx F)} {c : Ctx} {r : Morphology.Exponence.DomainRule Ctx F} (hrv : r ∈ v) (hrc : c ∈ r.dom) (hmax : ∀ s ∈ v, c ∈ s.dom → genProb s.dom c ≤ genProb r.dom c) : v.IsElsewhereWinner c r

Elsewhere selection is maximum-likelihood inference ([OD15] §5.5.3): a rule maximizing uniform generation probability at c among a vocabulary's generators is an Elsewhere winner of the corresponding vocabulary. Maximizing probability is minimizing support cardinality (genProb_le_iff_card_le), whence card-minimality forces ⊆-minimality — the same reasoning selectByCard_isElsewhereWinner routes through the core's score.