Hayes and Wilson (2008): A Maximum Entropy Model of Phonotactics and Phonotactic Learning

This file formalizes Hayes and Wilson's maximum-entropy model of phonotactics. A constraint is a sequence of feature matrices, one of which may be complemented, and a grammar assigns each form a score, a maxent value, and a probability. The weights are learned by maximizing the probability of the data, whose partial derivatives are differences between expected and observed violation counts (hasDerivAt_logLik), and the weights that maximize it give the distribution of greatest entropy among those that match the observed violations (isGreatest_measureEntropy_of_isMaxOn_logLik).

The grammar the learner found for English onsets (Table 4) is stated over the paper's feature chart (Table 3), and every score the paper reports is recomputed from it (rows_scores), including the ten attested onsets the grammar penalizes (attested_penalized). The predicted rating orders forms as the score does (rating_lt_iff), so the reported correlation with Scholes's ratings is a claim about the score alone.

Implementation notes

Weights are kept in hundredths over ℕ, so every score is computed by decide; the maxent value and probability then live over ℝ. Scores computed from the two-decimal weights of Table 4 can differ from the paper's reported values by one hundredth ([ð] 4.53 here against 4.54; [θw] 3.90 against 3.91; [θ] and [θr] 1.84 against 1.85), and rows_scores states the reproduction to within that rounding. Complement matrices are read against the underspecified chart, so [^+back] contains every consonant unspecified for backness, as #15 requires. The probability (6) over the infinite set of forms is realized over a finite form space, the subtype of a candidate set for the learned grammar (onsetProb); the paper's finite-state approximation of the expected counts is not modelled. The ratings of Scholes's experiment appear only as a scattergram (Figure 3), so the correlation of 0.946 and Table 5 stay in prose.

TODO

• The constraint search of §4 (accuracy O/E with the upper confidence limit, generality, the algorithm (10)) and the Gaussian prior of footnote 4.
• Projections (§6–§7), the Shona and stress simulations, and Wargamay (§8).

References

• B. Hayes and C. Wilson, A Maximum Entropy Model of Phonotactics and Phonotactic Learning (2008)
• S. Della Pietra, V. J. Della Pietra and J. D. Lafferty, Inducing Features of Random Fields (1997)
• R. J. Scholes, Phonotactic Grammaticality (1966)
• G. N. Clements and S. J. Keyser, CV Phonology: A Generative Theory of the Syllable (1983)
• S. Goldwater and M. Johnson, Learning OT Constraint Rankings Using a Maximum Entropy Model (2003)

The segments of Table 3

inductive HayesWilson2008.Seg : Type

Seg enumerates the English consonants of Table 3. Segments without an ASCII letter take their ARPAbet names, with ch for [tʃ], jh for [dʒ], th for [θ], sh for [ʃ], hh for [h], dh for [ð], zh for [ʒ], and ng for [ŋ].

• p : Seg
• t : Seg
• ch : Seg
• k : Seg
• b : Seg
• d : Seg
• jh : Seg
• g : Seg
• f : Seg
• th : Seg
• s : Seg
• sh : Seg
• hh : Seg
• v : Seg
• dh : Seg
• z : Seg
• zh : Seg
• m : Seg
• n : Seg
• ng : Seg
• l : Seg
• r : Seg
• j : Seg
• w : Seg

@[instance_reducible]

instance HayesWilson2008.instDecidableEqSeg : DecidableEq Seg

Equations

• HayesWilson2008.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HayesWilson2008.instReprSeg : Repr Seg

Equations

• HayesWilson2008.instReprSeg = { reprPrec := HayesWilson2008.instReprSeg.repr }

def HayesWilson2008.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.p")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.t")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.ch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.ch")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.k")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.b")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.d")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.jh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.jh")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.g")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.f")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.th prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.th")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.s")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.sh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.sh")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.hh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.hh")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.v")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.dh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.dh")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.z")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.zh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.zh")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.m prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.m")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.n")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.ng prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.ng")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.l")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.r")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.j")).group prec✝
• HayesWilson2008.instReprSeg.repr HayesWilson2008.Seg.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.Seg.w")).group prec✝

def HayesWilson2008.Seg.chart : Phonology.Feature → List Seg × List Seg

The chart of Table 3 lists, for each feature, the segments specified + and then those specified −. A segment in neither list is unspecified for the feature, as in the chart's blanks (privative and contrastive underspecification, §4.1.2).

Equations

• One or more equations did not get rendered due to their size.
• HayesWilson2008.Seg.chart Phonology.Feature.nasal = ([HayesWilson2008.Seg.m, HayesWilson2008.Seg.n, HayesWilson2008.Seg.ng], [])
• HayesWilson2008.Seg.chart Phonology.Feature.spreadGlottis = ([HayesWilson2008.Seg.hh], [])
• HayesWilson2008.Seg.chart Phonology.Feature.lateral = ([HayesWilson2008.Seg.l], [])
• HayesWilson2008.Seg.chart Phonology.Feature.dorsal = ([HayesWilson2008.Seg.k, HayesWilson2008.Seg.g, HayesWilson2008.Seg.ng], [])
• HayesWilson2008.Seg.chart Phonology.Feature.high = ([HayesWilson2008.Seg.j, HayesWilson2008.Seg.w], [])
• HayesWilson2008.Seg.chart Phonology.Feature.back = ([HayesWilson2008.Seg.w], [HayesWilson2008.Seg.j])
• HayesWilson2008.Seg.chart x✝ = ([], [])

def HayesWilson2008.Seg.spec (x : Seg) : Phonology.Segment

The feature specification of a segment is read off the chart.

Equations

• x.spec f = if x ∈ (HayesWilson2008.Seg.chart f).1 then ↑true else if x ∈ (HayesWilson2008.Seg.chart f).2 then ↑false else ⊥

def HayesWilson2008.Seg.ofChar : Char → Option Seg

ofChar reads the segment written by one IPA letter.

Equations

• HayesWilson2008.Seg.ofChar 'p' = some HayesWilson2008.Seg.p
• HayesWilson2008.Seg.ofChar 't' = some HayesWilson2008.Seg.t
• HayesWilson2008.Seg.ofChar 'k' = some HayesWilson2008.Seg.k
• HayesWilson2008.Seg.ofChar 'b' = some HayesWilson2008.Seg.b
• HayesWilson2008.Seg.ofChar 'd' = some HayesWilson2008.Seg.d
• HayesWilson2008.Seg.ofChar 'g' = some HayesWilson2008.Seg.g
• HayesWilson2008.Seg.ofChar 'f' = some HayesWilson2008.Seg.f
• HayesWilson2008.Seg.ofChar 'θ' = some HayesWilson2008.Seg.th
• HayesWilson2008.Seg.ofChar 's' = some HayesWilson2008.Seg.s
• HayesWilson2008.Seg.ofChar 'ʃ' = some HayesWilson2008.Seg.sh
• HayesWilson2008.Seg.ofChar 'h' = some HayesWilson2008.Seg.hh
• HayesWilson2008.Seg.ofChar 'v' = some HayesWilson2008.Seg.v
• HayesWilson2008.Seg.ofChar 'ð' = some HayesWilson2008.Seg.dh
• HayesWilson2008.Seg.ofChar 'z' = some HayesWilson2008.Seg.z
• HayesWilson2008.Seg.ofChar 'ʒ' = some HayesWilson2008.Seg.zh
• HayesWilson2008.Seg.ofChar 'm' = some HayesWilson2008.Seg.m
• HayesWilson2008.Seg.ofChar 'n' = some HayesWilson2008.Seg.n
• HayesWilson2008.Seg.ofChar 'ŋ' = some HayesWilson2008.Seg.ng
• HayesWilson2008.Seg.ofChar 'l' = some HayesWilson2008.Seg.l
• HayesWilson2008.Seg.ofChar 'r' = some HayesWilson2008.Seg.r
• HayesWilson2008.Seg.ofChar 'j' = some HayesWilson2008.Seg.j
• HayesWilson2008.Seg.ofChar 'w' = some HayesWilson2008.Seg.w
• HayesWilson2008.Seg.ofChar x✝ = none

def HayesWilson2008.Seg.parse : List Char → Option (List Seg)

parse reads an onset off a row's IPA string, with the affricates written as digraphs.

Equations

• One or more equations did not get rendered due to their size.
• HayesWilson2008.Seg.parse [] = some []
• HayesWilson2008.Seg.parse ('t' :: 'ʃ' :: cs) = Option.map (fun (x : List HayesWilson2008.Seg) => HayesWilson2008.Seg.ch :: x) (HayesWilson2008.Seg.parse cs)
• HayesWilson2008.Seg.parse ('d' :: 'ʒ' :: cs) = Option.map (fun (x : List HayesWilson2008.Seg) => HayesWilson2008.Seg.jh :: x) (HayesWilson2008.Seg.parse cs)

Constraints (§4.1.1)

inductive HayesWilson2008.Matrix : Type

A matrix of a constraint (9) is a natural class [αF, βG, …], its complement [^αF, βG, …] (the implication operator), or the word boundary #.

• cls (pat : Phonology.Segment) : Matrix
• compl (pat : Phonology.Segment) : Matrix
• boundary : Matrix

def HayesWilson2008.Matrix.Matches {α : Type u_1} (spec : α → Phonology.Segment) : Matrix → Option α → Prop

A matrix matches one symbol of a boundary-padded form, read through the segment specification spec; none is a word boundary.

Equations

• HayesWilson2008.Matrix.Matches spec (HayesWilson2008.Matrix.cls pat) (some x_2) = (pat ≤ spec x_2)
• HayesWilson2008.Matrix.Matches spec (HayesWilson2008.Matrix.compl pat) (some x_2) = ¬pat ≤ spec x_2
• HayesWilson2008.Matrix.Matches spec HayesWilson2008.Matrix.boundary none = True
• HayesWilson2008.Matrix.Matches spec x✝¹ x✝ = False

@[instance_reducible]

instance HayesWilson2008.instDecidableMatches {α : Type u_1} (spec : α → Phonology.Segment) (m : Matrix) (x : Option α) : Decidable (Matrix.Matches spec m x)

Equations

• HayesWilson2008.instDecidableMatches spec (HayesWilson2008.Matrix.cls pat) (some val) = { decide := decide (∀ (i : Phonology.Feature), pat i ≤ spec val i), reflects_decide := ⋯ }
• HayesWilson2008.instDecidableMatches spec (HayesWilson2008.Matrix.compl pat) (some val) = { decide := !decide (pat ≤ spec val), reflects_decide := ⋯ }
• HayesWilson2008.instDecidableMatches spec HayesWilson2008.Matrix.boundary none = { decide := true, reflects_decide := ⋯ }
• HayesWilson2008.instDecidableMatches spec (HayesWilson2008.Matrix.cls pat) none = { decide := false, reflects_decide := ⋯ }
• HayesWilson2008.instDecidableMatches spec (HayesWilson2008.Matrix.compl pat) none = { decide := false, reflects_decide := ⋯ }
• HayesWilson2008.instDecidableMatches spec HayesWilson2008.Matrix.boundary (some val) = { decide := false, reflects_decide := ⋯ }

@[reducible, inline]

abbrev HayesWilson2008.Cx : Type

A phonotactic constraint (9) is a sequence of matrices.

Equations

• HayesWilson2008.Cx = List HayesWilson2008.Matrix

def HayesWilson2008.Cx.prefixMatch {α : Type u_1} (spec : α → Phonology.Segment) : Cx → List (Option α) → Bool

The matrices match the padded form from its first symbol on.

Equations

• HayesWilson2008.Cx.prefixMatch spec [] x✝ = true
• HayesWilson2008.Cx.prefixMatch spec (m :: ms) (x_2 :: xs) = (decide (HayesWilson2008.Matrix.Matches spec m x_2) && HayesWilson2008.Cx.prefixMatch spec ms xs)
• HayesWilson2008.Cx.prefixMatch spec (head :: tail) [] = false

def HayesWilson2008.Cx.violations {α : Type u_1} (spec : α → Phonology.Segment) (c : Cx) (form : List α) : ℕ

A constraint's violation count on a form is the number of positions of the boundary-padded form at which its matrices match, as (9) specifies.

Equations

• HayesWilson2008.Cx.violations spec c form = (List.filter (HayesWilson2008.Cx.prefixMatch spec c) (none :: List.map some form ++ [none]).tails).length

def HayesWilson2008.M (l : List (Phonology.Feature × Bool)) : Matrix

M l is the natural class [αF, βG, …] of the specifications l.

Equations

• HayesWilson2008.M l = HayesWilson2008.Matrix.cls (Phonology.Segment.ofSpecs l)

def HayesWilson2008.M' (l : List (Phonology.Feature × Bool)) : Matrix

M' l is the complement class [^αF, βG, …] of the specifications l.

Equations

• HayesWilson2008.M' l = HayesWilson2008.Matrix.compl (Phonology.Segment.ofSpecs l)

def HayesWilson2008.any : Matrix

The empty matrix [ ] matches any segment.

Equations

• HayesWilson2008.any = HayesWilson2008.Matrix.cls (Phonology.Segment.ofSpecs [])

Score, maxent value, and probability (§3.2)

def HayesWilson2008.score {α : Type u_1} {n : ℕ} (spec : α → Phonology.Segment) (con : Fin n → Cx) (w : Fin n → ℕ) (form : List α) : ℕ

The score (4) of a form is its weighted violation count, with weights in hundredths.

Equations

• HayesWilson2008.score spec con w form = w ⬝ᵥ fun (j : Fin n) => HayesWilson2008.Cx.violations spec (con j) form

noncomputable def HayesWilson2008.maxentValue (k : ℕ) : ℝ

The maxent value (5) of a form whose score in hundredths is k is exp (−h(x)).

Equations

• HayesWilson2008.maxentValue k = Real.exp (-↑k / 100)

theorem HayesWilson2008.maxentValue_pos (k : ℕ) : 0 < maxentValue k

theorem HayesWilson2008.maxentValue_lt_iff {k₁ k₂ : ℕ} : maxentValue k₁ < maxentValue k₂ ↔ k₂ < k₁

Forms with more violations get lower values.

theorem HayesWilson2008.maxentValue_zero : maxentValue 0 = 1

A violation-free form has the highest possible maxent value, 1.

noncomputable def HayesWilson2008.rating (T : ℝ) (k : ℕ) : ℝ

The predicted rating (12) is the maxent value raised to 1 / T for a temperature T.

Equations

• HayesWilson2008.rating T k = HayesWilson2008.maxentValue k ^ (1 / T)

theorem HayesWilson2008.rating_lt_iff {T : ℝ} (hT : 0 < T) {k₁ k₂ : ℕ} : rating T k₁ < rating T k₂ ↔ k₂ < k₁

The rating orders forms exactly as the score does, so a correlation with the ratings is a claim about the score.

inductive HayesWilson2008.CV : Type

Table 1 evaluates schematic forms over consonants C and vowels V with two constraints, *#V weighted 3.0 and *C# weighted 2.0.

• C : CV
• V : CV

@[instance_reducible]

instance HayesWilson2008.instDecidableEqCV : DecidableEq CV

Equations

• HayesWilson2008.instDecidableEqCV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HayesWilson2008.instReprCV : Repr CV

Equations

• HayesWilson2008.instReprCV = { reprPrec := HayesWilson2008.instReprCV.repr }

def HayesWilson2008.instReprCV.repr : CV → ℕ → Std.Format

Equations

• HayesWilson2008.instReprCV.repr HayesWilson2008.CV.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.CV.C")).group prec✝
• HayesWilson2008.instReprCV.repr HayesWilson2008.CV.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HayesWilson2008.CV.V")).group prec✝

def HayesWilson2008.CV.spec : CV → Phonology.Segment

C is [−syllabic], V is [+syllabic] (footnote 7).

Equations

• HayesWilson2008.CV.C.spec = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, false)]
• HayesWilson2008.CV.V.spec = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, true)]

def HayesWilson2008.table1 : Fin 2 → Cx

Table 1 has the constraints *#V and *C#.

Equations

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

def HayesWilson2008.table1W : Fin 2 → ℕ

The weights of Table 1 are written in hundredths.

Equations

• HayesWilson2008.table1W = ![300, 200]

theorem HayesWilson2008.table1_scores : score CV.spec table1 table1W [CV.C, CV.V] = 0 ∧ score CV.spec table1 table1W [CV.C, CV.V, CV.C] = 200 ∧ score CV.spec table1 table1W [CV.V] = 300

Table 1 scores CV 0, CVC 2.0, and V 3.0.

theorem HayesWilson2008.table1_maxentValues : maxentValue (score CV.spec table1 table1W [CV.C, CV.V]) = 1 ∧ maxentValue (score CV.spec table1 table1W [CV.C, CV.V, CV.C]) = Real.exp (-2) ∧ maxentValue (score CV.spec table1 table1W [CV.V]) = Real.exp (-3)

Table 1 gives CV, CVC, and V the maxent values 1, exp (−2), and exp (−3).

Learning the weights (§3.3)

def HayesWilson2008.observed {Ω : Type u_2} [Fintype Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (D : Ω → ℕ) (i : Fin n) : ℕ

The observed number of violations of constraint i sums its counts over data given as counts per form.

Equations

• HayesWilson2008.observed viol D i = ∑ x : Ω, D x * viol i x

noncomputable def HayesWilson2008.logLik {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (w : Fin n → ℝ) (D : Ω → ℕ) : ℝ

The log probability of the data (7) sums the log probabilities (6) of the forms, each weighted by its count, since the forms are independent.

Equations

• HayesWilson2008.logLik viol w D = ∑ x : Ω, ↑(D x) * Real.log ((HarmonicGrammar.maxEnt viol.violations w).real {x})

noncomputable def HayesWilson2008.empirical {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] (D : Ω → ℕ) : MeasureTheory.Measure Ω

The empirical distribution of data given as counts per form.

Equations

• HayesWilson2008.empirical D = ∑ x : Ω, (↑(D x) / ∑ y : Ω, ↑(D y)) • MeasureTheory.Measure.dirac x

theorem HayesWilson2008.isProbabilityMeasure_empirical {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] (D : Ω → ℕ) (hD : ∑ x : Ω, D x ≠ 0) : MeasureTheory.IsProbabilityMeasure (empirical D)

theorem HayesWilson2008.empirical_real_singleton {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] (D : Ω → ℕ) [MeasurableSingletonClass Ω] (x : Ω) : (empirical D).real {x} = ↑(D x) / ∑ y : Ω, ↑(D y)

theorem HayesWilson2008.logLik_eq {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (w : Fin n → ℝ) (D : Ω → ℕ) [MeasurableSingletonClass Ω] (hD : ∑ x : Ω, D x ≠ 0) : logLik viol w D = ↑(∑ x : Ω, D x) * HarmonicGrammar.logLikelihood viol.violations (empirical D) w

The log probability of the data is its size times the log-likelihood of its empirical distribution.

theorem HayesWilson2008.integral_violations_empirical {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (D : Ω → ℕ) [MeasurableSingletonClass Ω] (hD : ∑ x : Ω, D x ≠ 0) (i : Fin n) : (∫ (x : Ω), viol.violations x ∂empirical D) i = ↑(observed viol D i) / ∑ x : Ω, ↑(D x)

The empirical distribution's expected violations are the observed counts over the size of the data.

theorem HayesWilson2008.hasDerivAt_logLik {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (w : Fin n → ℝ) (D : Ω → ℕ) [MeasurableSingletonClass Ω] [Nonempty Ω] (i : Fin n) : HasDerivAt (fun (t : ℝ) => logLik viol (Function.update w i t) D) (↑(∑ x : Ω, D x) * (∫ (x : Ω), viol.violations x ∂HarmonicGrammar.maxEnt viol.violations w) i - ↑(observed viol D i)) (w i)

The partial derivative of the log probability of the data in the weight of constraint i is its expected count (8), scaled by the size of the data, minus its observed count ([DPDPL97]). The paper's §3.3.2 states the two terms as O[Cᵢ] − E[Cᵢ], with the penalty direction in mind.

theorem HayesWilson2008.isGreatest_measureEntropy_of_isMaxOn_logLik {Ω : Type u_2} [Fintype Ω] [MeasurableSpace Ω] {n : ℕ} (viol : OptimalityTheory.ConstraintSet Ω (Fin n)) (w : Fin n → ℝ) (D : Ω → ℕ) [MeasurableSingletonClass Ω] [Nonempty Ω] (hD : ∑ x : Ω, D x ≠ 0) (h : IsMaxOn (fun (w : Fin n → ℝ) => logLik viol w D) Set.univ w) : IsGreatest (InformationTheory.measureEntropy '' {q : MeasureTheory.Measure Ω | MeasureTheory.IsProbabilityMeasure q ∧ ∫ (x : Ω), viol.violations x ∂q = ∫ (x : Ω), viol.violations x ∂empirical D}) (InformationTheory.measureEntropy (HarmonicGrammar.maxEnt viol.violations w))

Maximizing the probability of the data is maximizing entropy (§3.3.1, [DPDPL97]). Weights that make the data most probable give the distribution of greatest entropy among those whose expected violations average the observed ones.

The learned grammar for English onsets (Table 4)

def HayesWilson2008.table4 : Fin 23 → Cx

Table 4 lists 23 constraints in the order they were learned.

Equations

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

def HayesWilson2008.table4W : Fin 23 → ℕ

The weights of Table 4 are written in hundredths.

Equations

• HayesWilson2008.table4W = ![564, 328, 591, 517, 537, 666, 440, 131, 496, 484, 484, 317, 504, 280, 482, 269, 297, 206, 305, 206, 184, 210, 170]

def HayesWilson2008.h (o : List Seg) : ℕ

h o is the score (4) of the onset o under the learned grammar, in hundredths.

Equations

• HayesWilson2008.h o = HayesWilson2008.score HayesWilson2008.Seg.spec HayesWilson2008.table4 HayesWilson2008.table4W o

def HayesWilson2008.viol (k : Fin 23) (o : List Seg) : ℕ

viol k o counts the violations of constraint k + 1 of Table 4 on the onset o.

Equations

• HayesWilson2008.viol k o = HayesWilson2008.Cx.violations HayesWilson2008.Seg.spec (HayesWilson2008.table4 k) o

def HayesWilson2008.attested : List (List Seg)

The learning data (11) are the onsets of the nonexotic corpus, read off the rows.

Equations

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

theorem HayesWilson2008.attested_le (o : List Seg) : o ∈ attested → h o ≤ 453

Every attested onset is penalized by at most 4.53; most score 0 (§5.3.1).

theorem HayesWilson2008.attested_penalized : List.map (fun (o : List Seg) => (o, h o)) (List.filter (fun (x : List Seg) => decide (h x ≠ 0)) attested) = [([Seg.th], 184), ([Seg.z], 269), ([Seg.th, Seg.r], 184), ([Seg.t, Seg.w], 170), ([Seg.sh, Seg.r], 210), ([Seg.dh], 453), ([Seg.d, Seg.w], 297), ([Seg.g, Seg.w], 297), ([Seg.th, Seg.w], 390), ([Seg.s, Seg.k, Seg.l], 305)]

Exactly ten attested onsets receive penalties, the rarest ones, namely [θ], [z], [θr], [tw], [ʃr], [ð], [dw], [gw], [θw], and [skl] in the corpus order of (11) (§5.3.1).

def HayesWilson2008.twelve : List (List Seg)

These are the twelve unattested onsets with the best scores (§5.3.1).

Equations

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

theorem HayesWilson2008.twelve_scores : List.map h twelve = [376, 440, 482, 482, 484, 484, 484, 484, 490, 496, 496, 496]

The accidental gap [stw] scores 3.76, followed by [dl] 4.40, [hl] and [hr] 4.82, [vl], [vr], [ʃl], and [ʃw] 4.84, [sr] 4.90, and [fw], [pw], and [spw] 4.96 (§5.3.1).

theorem HayesWilson2008.h_rt : h [Seg.r, Seg.t] = 2181 ∧ viol 2 [Seg.r, Seg.t] = 1 ∧ viol 5 [Seg.r, Seg.t] = 1 ∧ viol 6 [Seg.r, Seg.t] = 1 ∧ viol 9 [Seg.r, Seg.t] = 1

Most unattested onsets score far worse, as [rt] scores 21.81 from #3, #6, #7, and #10.

theorem HayesWilson2008.stch_gang : h [Seg.s, Seg.ch] = 621 ∧ viol 7 [Seg.s, Seg.ch] = 1 ∧ viol 13 [Seg.s, Seg.ch] = 1 ∧ viol 21 [Seg.s, Seg.ch] = 1 ∧ table4W 7 < 400 ∧ table4W 13 < 400 ∧ table4W 21 < 400

In the gang of §5.2, constraints #8, #14, and #22, each weighted below the threshold of about 4, together give *[stʃ] the bad score 6.21.

theorem HayesWilson2008.zh_gang : h [Seg.zh] = 597 ∧ viol 1 [Seg.zh] = 1 ∧ viol 15 [Seg.zh] = 1

#2 ganging with #16 rules out *[ʒ].

theorem HayesWilson2008.thw_gang : h [Seg.th, Seg.w] = 390 ∧ viol 17 [Seg.th, Seg.w] = 1 ∧ viol 20 [Seg.th, Seg.w] = 1

#18 and #21 gang to penalize the especially rare attested onset [θw].

def HayesWilson2008.digits (cs : List Char) : Option ℕ

digits cs reads a decimal numeral.

Equations

• HayesWilson2008.digits cs = if cs ≠ [] ∧ cs.all Char.isDigit = true then some (List.foldl (fun (n : ℕ) (c : Char) => 10 * n + (c.toNat - '0'.toNat)) 0 cs) else none

def HayesWilson2008.hundredths (s : String) : Option ℕ

hundredths s reads a reported two-decimal score in hundredths.

Equations

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

def HayesWilson2008.Reproduced (e : Datum) : Prop

A row that reports a score is reproduced when its onset parses and the grammar's score is within one hundredth of the reported one.

Equations

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

@[instance_reducible]

instance HayesWilson2008.instDecidablePredDatumReproduced : DecidablePred Reproduced

Equations

• HayesWilson2008.instDecidablePredDatumReproduced e = id inferInstance

theorem HayesWilson2008.rows_scores (e : Datum) : e ∈ Examples.all → Reproduced e

Every score the paper reports (§5.2–5.3) is reproduced by the grammar to within one hundredth, the rounding of the printed weights.

Probability over a candidate set (§3.2, (6))

def HayesWilson2008.candidates : Finset (List Seg)

The candidate set contains the attested onsets and the unattested ones discussed.

Equations

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

instance HayesWilson2008.instNonemptySubtypeListSegMemFinsetCandidates : Nonempty ↥candidates

@[instance_reducible]

instance HayesWilson2008.instMeasurableSpaceSubtypeListSegMemFinsetCandidates : MeasurableSpace ↥candidates

Equations

• HayesWilson2008.instMeasurableSpaceSubtypeListSegMemFinsetCandidates = ⊤

instance HayesWilson2008.instMeasurableSingletonClassSubtypeListSegMemFinsetCandidates : MeasurableSingletonClass ↥candidates

def HayesWilson2008.onsetCon : OptimalityTheory.ConstraintSet (↥candidates) (Fin 23)

The constraints of Table 4 on the candidate set.

Equations

• HayesWilson2008.onsetCon k o = HayesWilson2008.viol k ↑o

noncomputable def HayesWilson2008.onsetProb (o : ↥candidates) : ℝ

onsetProb is the probability (6) of each candidate under the learned grammar, with the weights of Table 4 read as reals.

Equations

• HayesWilson2008.onsetProb o = (HarmonicGrammar.maxEnt HayesWilson2008.onsetCon.violations fun (k : Fin 23) => ↑(HayesWilson2008.table4W k) / 100).real {o}

theorem HayesWilson2008.onsetProb_eq_softmax : onsetProb = Real.softmax fun (o : ↥candidates) => -↑(h ↑o) / 100

The probability (6) is the softmax of the negated scores (4).

theorem HayesWilson2008.onsetProb_lt_iff {o₁ o₂ : ↥candidates} : onsetProb o₁ < onsetProb o₂ ↔ h ↑o₂ < h ↑o₁

On the candidate set, the probability (6) orders forms as the score does.

theorem HayesWilson2008.onsetProb_rt_lt_stw : onsetProb ⟨[Seg.r, Seg.t], onsetProb_rt_lt_stw._proof_1⟩ < onsetProb ⟨[Seg.s, Seg.t, Seg.w], onsetProb_rt_lt_stw._proof_3⟩

The accidental gap [stw] is more probable than [rt].