@cite{hayes-wilson-2008}: A Maximum Entropy Model of Phonotactics

@cite{hayes-wilson-2008}

@cite{hayes-wilson-2008} propose that phonotactic well-formedness is probability: a MaxEnt grammar assigns each surface form a score h(x) = Σ wⱼ · Cⱼ(x), and well-formedness is P(x) = exp(−h(x)) / Z.

Hayes & Wilson's "score" is the negation of harmonyScore: h(x) = −harmonyScore(x), so P(x) ∝ exp(harmonyScore(x)). Higher harmony = higher probability = better well-formedness. This is exactly softmax(harmonyScoreR, 1) on a finite candidate set.

Key contribution: ganging

The central empirical prediction distinguishing MaxEnt from OT is ganging: two individually weak constraints can jointly override a stronger one. This is impossible with OT's strict ranking, which corresponds to exponentially separated weights (OTLimit.lean).

The Ganging definition and anti-ganging theorems live in OTLimit.lean alongside ExponentiallySeparated, since they are two sides of the same coin.

English onset data

We encode a subset of the learned grammar (Table (4)) and verify that the model assigns higher harmony (= higher MaxEnt probability via exp_lt_exp) to attested onsets than to unattested ones (§2).

@[reducible, inline]

abbrev HayesWilson2008.Onset : Type

An English onset: a list of consonants preceding the nucleus.

Equations

• HayesWilson2008.Onset = List Phonology.Segment

def HayesWilson2008.c1_star_son_dors : Core.Constraint.WeightedConstraint Onset

Constraint #1 from Table (4): *[+sonorant, +dorsal]. Weight 5.64.

Equations

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

def HayesWilson2008.c4_star_blank_cont : Core.Constraint.WeightedConstraint Onset

Constraint #4 from Table (4): *[ ][+continuant]. Weight 5.17.

Equations

• HayesWilson2008.c4_star_blank_cont = Phonology.Constraints.mkMarkW "*[ ][+cont]" (fun (o : HayesWilson2008.Onset) => HayesWilson2008.c4_violated✝ o = true) (517 / 100)

def HayesWilson2008.c5_star_blank_voice : Core.Constraint.WeightedConstraint Onset

Constraint #5 from Table (4): *[ ][+voice, −sonorant]. Weight 5.37.

Equations

• HayesWilson2008.c5_star_blank_voice = Phonology.Constraints.mkMarkW "*[ ][+voice]" (fun (o : HayesWilson2008.Onset) => HayesWilson2008.c5_violated✝ o = true) (537 / 100)

def HayesWilson2008.c6_star_son_blank : Core.Constraint.WeightedConstraint Onset

Constraint #6 from Table (4): *[+sonorant][ ]. Weight 6.66.

Equations

• HayesWilson2008.c6_star_son_blank = Phonology.Constraints.mkMarkW "*[+son][ ]" (fun (o : HayesWilson2008.Onset) => HayesWilson2008.c6_violated✝ o = true) (666 / 100)

def HayesWilson2008.onsetGrammar : List (Core.Constraint.WeightedConstraint Onset)

The subset grammar: 4 constraints from Table (4).

Equations

• HayesWilson2008.onsetGrammar = [HayesWilson2008.c1_star_son_dors, HayesWilson2008.c4_star_blank_cont, HayesWilson2008.c5_star_blank_voice, HayesWilson2008.c6_star_son_blank]

theorem HayesWilson2008.k_harmony : Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.k] = 0

Attested onset [k]: harmony = 0 (no violations).

theorem HayesWilson2008.ŋ_harmony : Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.ŋ] = -(564 / 100)

Unattested onset *[ŋ]: harmony = −5.64 (violates *[+son,+dors]).

theorem HayesWilson2008.rk_harmony : Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.r, Fragments.English.Phonology.k] = -(666 / 100)

Unattested onset *[rk]: harmony = −6.66 (violates *[+son][ ]).

theorem HayesWilson2008.attested_higher_harmony_k_ŋ : Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.ŋ] < Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.k]

Attested [k] has higher harmony than unattested *[ŋ].

theorem HayesWilson2008.attested_higher_harmony_br_rk : Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.r, Fragments.English.Phonology.k] < Core.Constraint.harmonyScore onsetGrammar [Fragments.English.Phonology.b, Fragments.English.Phonology.r]

Attested [br] has higher harmony than unattested *[rk].

theorem HayesWilson2008.maxent_prob_k_gt_ŋ : Real.exp (Core.Constraint.harmonyScoreR onsetGrammar [Fragments.English.Phonology.ŋ]) < Real.exp (Core.Constraint.harmonyScoreR onsetGrammar [Fragments.English.Phonology.k])

MaxEnt probability ordering: higher harmony ⟹ higher exp(harmonyScore) ⟹ higher MaxEnt probability.

Applies exp_lt_exp (Mathlib) to harmonyScoreR (Core.Constraint.Weighted).

theorem HayesWilson2008.gradient_prob_ŋ_gt_rk : Real.exp (Core.Constraint.harmonyScoreR onsetGrammar [Fragments.English.Phonology.r, Fragments.English.Phonology.k]) < Real.exp (Core.Constraint.harmonyScoreR onsetGrammar [Fragments.English.Phonology.ŋ])

Gradient well-formedness: among unattested forms, *[ŋ] has higher MaxEnt probability than *[rk]. Uses exp_lt_exp.

Phonological MaxEnt is one instance of the framework-agnostic ConstraintSystem abstraction in Core.Constraint.System. The same maxEntSystem constructor that scores phonological onsets here also scores syntactic candidates in HG/MaxEnt syntax models, RSA utterances in soft-max pragmatic listeners, etc. The decoder (softmaxDecoder 1) is what makes this MaxEnt rather than HG (argmaxDecoder) or OT (argminDecoder over a LexProfile).

This section eats the dog food: rather than comparing exp(harmonyScoreR ...) directly (as in §3), we go through ConstraintSystem.predict.

def HayesWilson2008.candidateOnsets : Finset Onset

The four onsets used as MaxEnt candidates: two attested ([k], [b,r]) and two unattested (*[ŋ], *[r,k]).

Equations

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

noncomputable def HayesWilson2008.onsetSystem : Core.Constraint.ConstraintSystem Onset ℝ

@cite{hayes-wilson-2008}'s grammar realised as a generic ConstraintSystem over candidateOnsets, decoded by softmax at temperature 1. The score component is harmonyScoreR onsetGrammar (the canonical MaxEnt harmony function).

Equations

• HayesWilson2008.onsetSystem = Core.Constraint.maxEntSystem HayesWilson2008.candidateOnsets HayesWilson2008.onsetGrammar

theorem HayesWilson2008.predict_k_gt_ŋ : onsetSystem.predict [Fragments.English.Phonology.ŋ] < onsetSystem.predict [Fragments.English.Phonology.k]

The system literally predicts a higher MaxEnt probability for [k] than for *[ŋ]. Unlike maxent_prob_k_gt_ŋ, this is a comparison of actual softmax probabilities (numerator / partition function), not just exponentiated harmony scores — so the partition function over candidateOnsets is part of the claim.

theorem HayesWilson2008.predict_ŋ_gt_rk : onsetSystem.predict [Fragments.English.Phonology.r, Fragments.English.Phonology.k] < onsetSystem.predict [Fragments.English.Phonology.ŋ]

The system also predicts a higher MaxEnt probability for *[ŋ] than for *[rk] — gradient well-formedness among unattested forms.

theorem HayesWilson2008.onsetSystem_isProb : ∑ c ∈ candidateOnsets, onsetSystem.predict c = 1

The MaxEnt softmax decoder is a probability decoder, so the system's predictions are non-negative and sum to 1 over the candidate set. Follows from Decoder.IsProb.sum_eq_one for softmaxDecoder.