Storme (2026): A Method to Evaluate Systemic Constraints in Probabilistic Grammars

This file formalizes [Sto26b]'s method for fitting systemic constraints, those that score several input-output mappings jointly, in probabilistic constraint-based grammars: a maximum-entropy distribution is evaluated over the joint tableau of output tuples and the probability of each mapping is recovered by marginalization. With the systemic weights at zero the marginal is the classical maximum-entropy probability of the mapping (marginal_eq_classical_of_systemic_zero). The case study is variable hiatus resolution in spoken Persian ([AJ21]): the suffix vowel of the possessive /hutʃɑ-emun/ usually deletes while that of the definite /hutʃɑ-e/ rarely does, since deleting it would make the suffixed form homophonous with the bare stem. The paradigm is two junctures over Persian segments (definite, possessive), homophony is string identity (homophonyAvoidance, starHomophony), and the joint tableau puts *HOMOPHONY beside the jointly evaluated classical constraints (jointCon), with the mapping probabilities its marginals (predicted).

On this paradigm *HOMOPHONY coincides with the jointly evaluated REALIZEMORPHEME of [Kur01] that [AJ21] use, so the marginalized model is their classical one (starHomophony_eq_joint_realizeMorpheme, predicted_eq_maxEnt). Whatever the weights, the suffix-length effect on deletion, in log-odds against faithful hiatus, is exactly the *HOMOPHONY weight (log_odds_deletion_sub), deletion is less likely for the monosegmental suffix whenever that weight is positive (deletion_lt_deletion), and without *HOMOPHONY the two suffixes receive identical distributions (classical_no_length_effect). At the paper's fitted weights the predicted orders are those of its Table 5 (mono_order, poly_order).

Implementation notes

The fitted weights are the paper's posterior means, with MAX fixed at one as in the paper; the theorems about the suffix-length effect are stated for arbitrary weights and only the preference orders use the fitted values. The base's single faithful candidate enters the tableau as the bare stem. The paper's model comparison by deviance information criterion is not formalized.

References

• [Sto26b]
• [AJ21]
• [Kur01]
• [Cas11]

Systemic constraints, joint evaluation, and marginalization

def Storme2026.homophonyAvoidance {n : ℕ} {O : Type u_1} [DecidableEq O] : OptimalityTheory.Constraint (Fin n → O)

*HOMOPHONY counts the pairs of distinct inputs that receive identical outputs. It is a systemic constraint, one that scores a whole output tuple and not a single mapping, so it is a Constraint on Fin n → O that does not decompose over the mappings.

Equations

• Storme2026.homophonyAvoidance f = {p : Fin n × Fin n | p.1 < p.2 ∧ f p.1 = f p.2}.card

theorem Storme2026.marginal_eq_classical_of_systemic_zero {ι : Type u_1} {I : Type u_2} {O : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype O] [MeasurableSpace O] [MeasurableSingletonClass O] [Nonempty O] {m k : ℕ} (inputs : ι → I) (scon : OptimalityTheory.ConstraintSet (ι → O) (Fin k)) (con : OptimalityTheory.ConstraintSet (I × O) (Fin m)) (w : Fin m → ℝ) (i : ι) : MeasureTheory.Measure.map (Function.eval i) (HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.violations (Fin.append scon (OptimalityTheory.ConstraintSet.joint inputs con))) (Fin.append 0 w)) = HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x : O) => (inputs i, x)) con).violations w

The joint MaxEnt grammar — systemic constraints scon beside the jointly evaluated classical constraints con — marginalized at input i ([Sto26b]'s marginalization equation). With the systemic weights at zero it returns the classical MaxEnt probability of each mapping: joint evaluation plus marginalization conservatively extends the classical pipeline.

The Persian paradigm

inductive Storme2026.Resolution : Type

The three candidate realizations of a suffixed input — the hiatus-resolution typology ([Cas11]) as restricted by [AJ21].

• hiatus : Resolution

  Faithful vowel hiatus, e.g. [hutʃɑe].

• epenthesis : Resolution

  Glottal-stop epenthesis, e.g. [hutʃɑʔe].

• deletion : Resolution

  Suffix-vowel deletion, e.g. [hutʃɑ], [hutʃɑmun].

@[instance_reducible]

instance Storme2026.instDecidableEqResolution : DecidableEq Resolution

Equations

• Storme2026.instDecidableEqResolution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Storme2026.instFintypeResolution : Fintype Resolution

Equations

• Storme2026.instFintypeResolution = { elems := { val := ↑Storme2026.Resolution.enumList, nodup := Storme2026.Resolution.enumList_nodup }, complete := Storme2026.instFintypeResolution._proof_1 }

@[instance_reducible]

instance Storme2026.instInhabitedResolution : Inhabited Resolution

Equations

• Storme2026.instInhabitedResolution = { default := Storme2026.instInhabitedResolution.default }

def Storme2026.instReprResolution.repr : Resolution → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Storme2026.instReprResolution : Repr Resolution

Equations

• Storme2026.instReprResolution = { reprPrec := Storme2026.instReprResolution.repr }

@[instance_reducible]

instance Storme2026.instMeasurableSpaceResolution : MeasurableSpace Resolution

Equations

• Storme2026.instMeasurableSpaceResolution = ⊤

instance Storme2026.instMeasurableSingletonClassResolution : MeasurableSingletonClass Resolution

instance Storme2026.instNontrivialResolution : Nontrivial Resolution

def Storme2026.definite : Phonology.Hiatus.Juncture

The definite-suffix juncture /hutʃɑ-e/: a monosegmental suffix.

Equations

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

def Storme2026.possessive : Phonology.Hiatus.Juncture

The possessive-suffix juncture /hutʃɑ-emun/: a polysegmental suffix.

Equations

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

def Storme2026.inputs : Fin 2 → Phonology.Hiatus.Juncture

The inputs of the joint tableau are the definite and the possessive junctures.

Equations

• Storme2026.inputs = ![Storme2026.definite, Storme2026.possessive]

def Storme2026.resolve : Resolution → Phonology.Hiatus.Juncture → List Phonology.Segment

resolve o j is the surface form of the candidate o at the juncture j, with faithful hiatus, glottal-stop epenthesis, or elision of the suffix vowel.

Equations

• Storme2026.resolve Storme2026.Resolution.hiatus = Phonology.Hiatus.Juncture.input
• Storme2026.resolve Storme2026.Resolution.epenthesis = fun (x : Phonology.Hiatus.Juncture) => x.epenthesize Farsi.glottalStop
• Storme2026.resolve Storme2026.Resolution.deletion = Phonology.Hiatus.Juncture.elideV2

The constraints and the joint tableau

def Storme2026.starHiatus : OptimalityTheory.Constraint (Phonology.Hiatus.Juncture × Resolution)

*HIATUS counts the adjacent vowel pairs that survive in the surface form.

Equations

• Storme2026.starHiatus c = Phonology.Hiatus.count (Storme2026.resolve c.2 c.1)

def Storme2026.corr : Resolution → Phonology.Hiatus.Juncture → OptimalityTheory.Correspondence OptimalityTheory.BinaryRole Phonology.Segment

corr o j is the correspondence between the unrepaired concatenation and the candidate o, which is the identity for faithful hiatus, the insertion of a glottal stop before the suffix vowel for epenthesis, and the deletion of the suffix vowel for elision.

Equations

• Storme2026.corr Storme2026.Resolution.hiatus x✝ = OptimalityTheory.Correspondence.identity x✝.input
• Storme2026.corr Storme2026.Resolution.epenthesis x✝ = OptimalityTheory.Correspondence.insertIdx x✝.input x✝.v2Idx Farsi.glottalStop
• Storme2026.corr Storme2026.Resolution.deletion x✝ = OptimalityTheory.Correspondence.eraseIdx x✝.input x✝.v2Idx

theorem Storme2026.corr_form_rhs (o : Resolution) (j : Phonology.Hiatus.Juncture) : (corr o j).form OptimalityTheory.BinaryRole.rhs = resolve o j

The output of each correspondence is the surface form of its candidate.

def Storme2026.depConstraint : OptimalityTheory.Constraint (Phonology.Hiatus.Juncture × Resolution)

DEP counts the output segments that have no correspondent in the input.

Equations

• Storme2026.depConstraint c = (Storme2026.corr c.2 c.1).depViol OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

def Storme2026.maxConstraint : OptimalityTheory.Constraint (Phonology.Hiatus.Juncture × Resolution)

MAX counts the input segments that have no correspondent in the output.

Equations

• Storme2026.maxConstraint c = (Storme2026.corr c.2 c.1).maxViol OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

theorem Storme2026.depConstraint_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : depConstraint (j, o) = if o = Resolution.epenthesis then 1 else 0

DEP is violated once by epenthesis and by no other candidate, for any juncture.

theorem Storme2026.maxConstraint_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : maxConstraint (j, o) = if o = Resolution.deletion then 1 else 0

MAX is violated once by deletion and by no other candidate, for any juncture.

theorem Storme2026.starHiatus_eq (k : Fin 2) (o : Resolution) : starHiatus (inputs k, o) = if o = Resolution.hiatus then 1 else 0

*HIATUS's string count is its binary tableau column on the paradigm's junctures — unlike DEP and MAX this depends on their segmental content, since hiatus must survive nowhere but at the juncture itself.

def Storme2026.classicalCon : OptimalityTheory.ConstraintSet (Phonology.Hiatus.Juncture × Resolution) (Fin 3)

The classical constraint set consists of DEP, *HIATUS and MAX.

Equations

• Storme2026.classicalCon = ![Storme2026.depConstraint, Storme2026.starHiatus, Storme2026.maxConstraint]

noncomputable def Storme2026.classicalW : Fin 3 → ℝ

The fitted classical weights, posterior means with MAX fixed at one.

Equations

• Storme2026.classicalW = ![2.47, 1.89, 1]

@[simp]

theorem Storme2026.classicalW_zero : classicalW 0 = 2.47

@[simp]

theorem Storme2026.classicalW_one : classicalW 1 = 1.89

@[simp]

theorem Storme2026.classicalW_two : classicalW 2 = 1

def Storme2026.starHomophony : OptimalityTheory.Constraint (Fin 2 → Resolution)

*HOMOPHONY over the paradigm counts the collisions among the surface forms of the base, which is realized faithfully as the bare stem, its only candidate, and of the two suffixed inputs. Two outputs collide when they are the same string.

Equations

• Storme2026.starHomophony f = Storme2026.homophonyAvoidance (Fin.cons Storme2026.definite.stem fun (k : Fin 2) => Storme2026.resolve (f k) (Storme2026.inputs k))

noncomputable def Storme2026.homophonyWeight : ℝ

The fitted *HOMOPHONY weight, a posterior mean.

Equations

• Storme2026.homophonyWeight = 2.27

def Storme2026.jointCon : OptimalityTheory.ConstraintSet (Fin 2 → Resolution) (Fin 4)

The constraint set of the joint tableau puts *HOMOPHONY beside the jointly evaluated classical constraints. These are the columns of the paper's Table 4, over its nine output tuples.

Equations

• Storme2026.jointCon = Fin.append ![Storme2026.starHomophony] (OptimalityTheory.ConstraintSet.joint Storme2026.inputs Storme2026.classicalCon)

def Storme2026.jointW (wh : ℝ) (w : Fin 3 → ℝ) : Fin 4 → ℝ

The weights of the joint tableau are wh for *HOMOPHONY and w for the classical constraints.

Equations

• Storme2026.jointW wh w = Fin.append ![wh] w

noncomputable def Storme2026.predicted (wh : ℝ) (w : Fin 3 → ℝ) (k : Fin 2) : MeasureTheory.Measure Resolution

predicted wh w k is the distribution of input k's realizations, the marginal of the joint MaxEnt distribution by the paper's marginalization equation, which gives its Table 5 at the fitted weights.

Equations

• Storme2026.predicted wh w k = MeasureTheory.Measure.map (Function.eval k) (HarmonicGrammar.maxEnt Storme2026.jointCon.violations (Storme2026.jointW wh w))

*HOMOPHONY against REALIZEMORPHEME

[AJ21] analyse the same data with a per-mapping constraint penalizing a null realization of the suffix ([Kur01]'s REALIZEMORPHEME) in place of *HOMOPHONY. [Sto26b] notes that the two coincide here, and that only the systemic constraint extends to homophony avoidance not involving a null morpheme.

def Storme2026.realizeMorpheme : OptimalityTheory.Constraint (Phonology.Hiatus.Juncture × Resolution)

REALIZEMORPHEME is violated when the suffix has a null realization, the suffixed form surfacing as its bare stem.

Equations

• Storme2026.realizeMorpheme = OptimalityTheory.Constraint.binary fun (c : Phonology.Hiatus.Juncture × Storme2026.Resolution) => Storme2026.resolve c.2 c.1 = c.1.stem

theorem Storme2026.realizeMorpheme_eq (j : Phonology.Hiatus.Juncture) (o : Resolution) : realizeMorpheme (j, o) = if o = Resolution.deletion ∧ j.suffixBody = [] then 1 else 0

Only deletion at a monosegmental juncture leaves the suffix unrealized — for any juncture, by the string algebra of Hiatus.Juncture.

theorem Storme2026.starHomophony_eq_joint_realizeMorpheme : starHomophony = OptimalityTheory.Constraint.joint inputs realizeMorpheme

On this paradigm *HOMOPHONY is the jointly evaluated REALIZEMORPHEME, since the suffixed forms never collide with each other, only with the base.

def Storme2026.ajCon : OptimalityTheory.ConstraintSet (Phonology.Hiatus.Juncture × Resolution) (Fin 4)

[AJ21]'s classical constraint set, REALIZEMORPHEME beside DEP, *HIATUS and MAX.

Equations

• Storme2026.ajCon = Matrix.vecCons Storme2026.realizeMorpheme Storme2026.classicalCon

def Storme2026.ajW (wh : ℝ) (w : Fin 3 → ℝ) : Fin 4 → ℝ

The weights of ajCon, REALIZEMORPHEME at the *HOMOPHONY weight.

Equations

• Storme2026.ajW wh w = Matrix.vecCons wh w

theorem Storme2026.harmonyScore_jointCon (wh : ℝ) (w : Fin 3 → ℝ) (f : Fin 2 → Resolution) : HarmonicGrammar.harmonyScore jointCon (jointW wh w) f = ∑ k : Fin 2, HarmonicGrammar.harmonyScore ajCon (ajW wh w) (inputs k, f k)

The joint harmony separates over the two inputs, each scored by [AJ21]'s grammar: the coupling *HOMOPHONY introduces folds into the per-mapping scores.

theorem Storme2026.predicted_eq_maxEnt (wh : ℝ) (w : Fin 3 → ℝ) (k : Fin 2) : predicted wh w k = HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x : Resolution) => (inputs k, x)) ajCon).violations (ajW wh w)

The marginalized model is [AJ21]'s classical one, since the joint distribution is the product of the inputs' MaxEnt distributions under their per-mapping scores.

theorem Storme2026.ajScore_eq (wh : ℝ) (w : Fin 3 → ℝ) (k : Fin 2) (o : Resolution) : HarmonicGrammar.harmonyScore ajCon (ajW wh w) (inputs k, o) = -match o with | Resolution.hiatus => w 1 | Resolution.epenthesis => w 0 | Resolution.deletion => w 2 + if k = 0 then wh else 0

The per-mapping scores: each candidate costs its constraint's weight, with the *HOMOPHONY weight landing on top of MAX exactly for deletion at the monosegmental juncture.

Predictions with the fitted weights

theorem Storme2026.mono_order : (predicted homophonyWeight classicalW 0).real {Resolution.deletion} < (predicted homophonyWeight classicalW 0).real {Resolution.epenthesis} ∧ (predicted homophonyWeight classicalW 0).real {Resolution.epenthesis} < (predicted homophonyWeight classicalW 0).real {Resolution.hiatus}

At the fitted weights the monosegmental suffix prefers hiatus over epenthesis over deletion, which would merge the suffixed form with the bare stem.

theorem Storme2026.poly_order : (predicted homophonyWeight classicalW 1).real {Resolution.epenthesis} < (predicted homophonyWeight classicalW 1).real {Resolution.hiatus} ∧ (predicted homophonyWeight classicalW 1).real {Resolution.hiatus} < (predicted homophonyWeight classicalW 1).real {Resolution.deletion}

At the fitted weights the polysegmental suffix prefers deletion over hiatus over epenthesis: the suffix stays recoverable, so *HOMOPHONY is silent.

theorem Storme2026.deletion_lt_deletion {wh : ℝ} (hwh : 0 < wh) (w : Fin 3 → ℝ) : (predicted wh w 0).real {Resolution.deletion} < (predicted wh w 1).real {Resolution.deletion}

The suffix-length effect of [AJ21]: with a positive *HOMOPHONY weight, deletion is less likely for the monosegmental suffix than for the polysegmental one.

theorem Storme2026.log_odds_deletion_sub (wh : ℝ) (w : Fin 3 → ℝ) : Real.log ((predicted wh w 1).real {Resolution.deletion} / (predicted wh w 1).real {Resolution.hiatus}) - Real.log ((predicted wh w 0).real {Resolution.deletion} / (predicted wh w 0).real {Resolution.hiatus}) = wh

In log-odds against faithful hiatus, deletion is exactly the *HOMOPHONY weight less likely under the monosegmental suffix than under the polysegmental one, whatever the weights: the whole suffix-length effect is the systemic penalty.

theorem Storme2026.harmonyScore_classicalCon_inputs (w : Fin 3 → ℝ) (k k' : Fin 2) (o : Resolution) : HarmonicGrammar.harmonyScore classicalCon w (inputs k, o) = HarmonicGrammar.harmonyScore classicalCon w (inputs k', o)

DEP, *HIATUS and MAX give the two junctures identical violation profiles.

theorem Storme2026.classical_no_length_effect (w : Fin 3 → ℝ) : HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x : Resolution) => (inputs 0, x)) classicalCon).violations w = HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x : Resolution) => (inputs 1, x)) classicalCon).violations w

Without *HOMOPHONY there is no suffix-length effect to fit: the classical grammar assigns the two suffixes the same distribution under every weighting. The paper reports the correspondingly worse fit of the model without *HOMOPHONY.