Zuraw and Hayes (2017): Intersecting Constraint Families

This file formalizes the Tagalog case of Zuraw and Hayes's argument for Harmonic Grammar. Nasal substitution is conditioned by two families of constraints (§2.4): the consonant-sensitive markedness constraints (3), (4), (6), and the Uniformity constraints (5), one for each of the six prefix constructions. Every square crossing two prefixes with two stems is independent in the sense of the substrate: each constraint is insensitive to the prefix or to the stem (independent). The rates of application show across-the-board effects in both dimensions, restrained by floor and ceiling effects (§2.3); Harmonic Grammar predicts the pattern because constraint effects add.

In MaxEnt the probability of substitution is logistic in the harmony difference (13) (maxEntSubst_eq), the logit rates have constant differences on every square (maxEnt_interaction_logOdds_eq_zero), and so the effects of prefixes and of stems are across the board on every square, for every weighting (maxEnt_acrossTheBoard). In Noisy Harmonic Grammar the noise on a comparison grows with the number of constraints that distinguish the candidates, four for /p/ as in (15) (dotProduct_violationDiff_self_p); since that number depends on the stem alone, the effects of the prefixes are across the board on every square, for every weighting and noise (weightNoise_acrossTheBoard). A decision-tree model instead multiplies a prefix probability by a stem probability, so the stem differences grow with the prefix probability, the paper's claws (decision_tree_monotonic_diff).

Stochastic OT fails differently (§3.8). When a lone constraint opposes two synergistic families that each apply through one constraint, as in the French liaison and elision data, generation is a race: the opposing constraint's candidate wins when that constraint outruns the other two (raceRate). By a theorem of Magri's that the paper reports, the difference that a stronger constraint of one family makes then grows monotonically as the constraint of the other family weakens (raceRate_add_le, antitone_raceRate_sub) and vanishes as it strengthens (tendsto_raceRate_atTop): the rates converge in one direction and diverge in the other. In Harmonic Grammar's tug-of-war the difference vanishes in both directions (not_antitone_not_monotone_sigmoid_sub).

Implementation notes

• The inputs are the thirty-six crossings of the six prefix constructions of Figure 3 with the six stem-initial consonants of Zuraw (2010); its /t/ stands for the paper's t/s class.
• The constraints are those of Table 1, in its order, the consonant-sensitive ones pulled back from Zuraw (2010) along the projection of a candidate onto its stem and decision.
• Magri's theorem is proved for noise of any law, stochastic OT's Gaussian noise among them: the opposing candidate's rate integrates, against the law of its constraint, the product of the other two constraints' distribution functions (choiceProb_pi_eq_lintegral), and that product has increasing differences in the two ranking values.
• The paper's fitted weights and ranking values, their log likelihoods, the empirical rates, the French and Hungarian data, and the partial-ordering model are not represented.

References

• [ZH17]
• [Zur10]
• [Pat99]
• [McCP95]

Inputs and candidates

inductive ZurawHayes2017.Prefix : Type

The six most type-frequent prefix constructions of Figure 3, in the order of Table 1.

• mangOther : Prefix

  maŋ- OTHER, nonadversative verbs.

• pangRed : Prefix

  paŋ- RED-, mainly gerunds.

• mangAdv : Prefix

  maŋ- ADV, adversative verbs.

• mangRed : Prefix

  maŋ- RED-, professional or habitual nouns.

• pangNoun : Prefix

  paŋ- NOUN, various nominalizations.

• pangRes : Prefix

  paŋ- RES, reservational adjectives.

@[instance_reducible]

instance ZurawHayes2017.instDecidableEqPrefix : DecidableEq Prefix

Equations

• ZurawHayes2017.instDecidableEqPrefix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ZurawHayes2017.instReprPrefix : Repr Prefix

Equations

• ZurawHayes2017.instReprPrefix = { reprPrec := ZurawHayes2017.instReprPrefix.repr }

def ZurawHayes2017.instReprPrefix.repr : Prefix → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZurawHayes2017.instFintypePrefix : Fintype Prefix

Equations

• ZurawHayes2017.instFintypePrefix = { elems := { val := ↑ZurawHayes2017.Prefix.enumList, nodup := ZurawHayes2017.Prefix.enumList_nodup }, complete := ZurawHayes2017.instFintypePrefix._proof_1 }

@[reducible, inline]

abbrev ZurawHayes2017.Candidate : Type

A candidate is a prefix construction and a stem-initial consonant, with or without substitution.

Equations

• ZurawHayes2017.Candidate = ((ZurawHayes2017.Prefix × Zuraw2010.StemC) × Zuraw2010.SubSt)

def ZurawHayes2017.project (c : Candidate) : Zuraw2010.NSCand

The projection of a candidate onto the stem and decision of a Zuraw2010 candidate.

Equations

• ZurawHayes2017.project c = (c.1.2, c.2)

def ZurawHayes2017.square (p p' : Prefix) (c c' : Zuraw2010.StemC) : HarmonicGrammar.Square (Prefix × Zuraw2010.StemC)

The square crossing the prefixes p and p' (rows) with the stems c and c' (columns).

Equations

• ZurawHayes2017.square p p' c c' = { tl := (p, c), tr := (p, c'), bl := (p', c), br := (p', c') }

The constraints

def ZurawHayes2017.nasSub : OptimalityTheory.Constraint Candidate

NasSub (3) assigns one violation to a nasal followed by an obstruent across a morpheme boundary.

Equations

• ZurawHayes2017.nasSub = OptimalityTheory.Constraint.comap ZurawHayes2017.project Zuraw2010.nasSub

def ZurawHayes2017.starNC : OptimalityTheory.Constraint Candidate

*NC̥ (4) assigns one violation to a nasal followed by a voiceless obstruent.

Equations

• ZurawHayes2017.starNC = OptimalityTheory.Constraint.comap ZurawHayes2017.project Zuraw2010.starNC

def ZurawHayes2017.starRootNasal : OptimalityTheory.Constraint Candidate

*[root m/n/ŋ (6a) forbids a root to begin with a nasal.

Equations

• ZurawHayes2017.starRootNasal = OptimalityTheory.Constraint.comap ZurawHayes2017.project Zuraw2010.starInitAll

def ZurawHayes2017.starRootCorVel : OptimalityTheory.Constraint Candidate

*[root n/ŋ (6b) forbids a root to begin with a coronal or velar nasal.

Equations

• ZurawHayes2017.starRootCorVel = OptimalityTheory.Constraint.comap ZurawHayes2017.project Zuraw2010.starInitCorVel

def ZurawHayes2017.starRootVelar : OptimalityTheory.Constraint Candidate

*[root ŋ (6c) forbids a root to begin with a velar nasal.

Equations

• ZurawHayes2017.starRootVelar = OptimalityTheory.Constraint.comap ZurawHayes2017.project Zuraw2010.starInitVelar

def ZurawHayes2017.unif (q : Prefix) : OptimalityTheory.Constraint Candidate

The Uniformity constraint of (5) indexed to prefix construction q, which forbids a segment of the prefix and a distinct input segment to correspond to one output segment.

Equations

• ZurawHayes2017.unif q = OptimalityTheory.Constraint.binary fun (c : ZurawHayes2017.Candidate) => c.1.1 = q ∧ c.2 = Zuraw2010.SubSt.yes

def ZurawHayes2017.constraints : OptimalityTheory.ConstraintSet Candidate (Fin 11)

The eleven constraints, in the order of Table 1.

Equations

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

theorem ZurawHayes2017.independent (p p' : Prefix) (c c' : Zuraw2010.StemC) : (square p p' c c').Independent constraints

The two families intersect, since on every square the consonant-sensitive constraints are insensitive to the prefix and the Uniformity constraints to the stem.

theorem ZurawHayes2017.sum_unif_eq_starRootNasal (c : Candidate) : ∑ q : Prefix, unif q c = starRootNasal c

The Uniformity family sums to *[root m/n/ŋ, since a substituted candidate violates exactly the Uniformity constraint of its prefix.

Across-the-board effects

def ZurawHayes2017.AcrossTheBoard {X : Type u_1} (sq : HarmonicGrammar.Square X) (r : X → ℝ) : Prop

The effect of the rows of a square is across the board (§2.3) when it has the same direction in both columns, so that the lines of Figure 4 do not cross.

Equations

• ZurawHayes2017.AcrossTheBoard sq r = (0 ≤ (r sq.tl - r sq.bl) * (r sq.tr - r sq.br))

theorem ZurawHayes2017.acrossTheBoard_of_interaction_eq_zero {X : Type u_1} {S : Type u_2} {sq : HarmonicGrammar.Square X} {d : X → ℝ} {s : X → S} {F : S → ℝ → ℝ} (hF : ∀ (x : X), Monotone (F (s x))) (hd : sq.interaction d = 0) (hs : sq.InsensitiveToRow s) : AcrossTheBoard sq fun (x : X) => F (s x) (d x)

A score with zero interaction, passed through a monotone link whose other argument (a noise scale, say) is insensitive to the rows, has across-the-board row effects.

Maximum entropy

@[instance_reducible]

instance ZurawHayes2017.instMeasurableSpaceSubSt : MeasurableSpace Zuraw2010.SubSt

Equations

• ZurawHayes2017.instMeasurableSpaceSubSt = ⊤

instance ZurawHayes2017.instMeasurableSingletonClassSubSt : MeasurableSingletonClass Zuraw2010.SubSt

noncomputable def ZurawHayes2017.maxEntSubst (w : Fin 11 → ℝ) (x : Prefix × Zuraw2010.StemC) : ℝ

The MaxEnt probability of substitution for an input.

Equations

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

theorem ZurawHayes2017.maxEntSubst_eq (w : Fin 11 → ℝ) (x : Prefix × Zuraw2010.StemC) : maxEntSubst w x = (HarmonicGrammar.harmonyScore constraints w (x, Zuraw2010.SubSt.yes) - HarmonicGrammar.harmonyScore constraints w (x, Zuraw2010.SubSt.no)).sigmoid

The MaxEnt probability of substitution is logistic in the harmony difference between the substituted and unsubstituted candidates (13).

theorem ZurawHayes2017.maxEnt_interaction_logOdds_eq_zero (w : Fin 11 → ℝ) (p p' : Prefix) (c c' : Zuraw2010.StemC) : ((square p p' c c').interaction fun (x : Prefix × Zuraw2010.StemC) => Real.log ((HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x_1 : Zuraw2010.SubSt) => (x, x_1)) constraints).violations w).real {Zuraw2010.SubSt.yes} / (HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x_1 : Zuraw2010.SubSt) => (x, x_1)) constraints).violations w).real {Zuraw2010.SubSt.no})) = 0

Any MaxEnt weighting has constant logit differences on every square, whatever the other candidates.

theorem ZurawHayes2017.harmony_b_sub_harmony_k (w : Fin 11 → ℝ) (p : Prefix) : HarmonicGrammar.harmonyScore constraints w ((p, Zuraw2010.StemC.b), Zuraw2010.SubSt.yes) - HarmonicGrammar.harmonyScore constraints w ((p, Zuraw2010.StemC.b), Zuraw2010.SubSt.no) - (HarmonicGrammar.harmonyScore constraints w ((p, Zuraw2010.StemC.k), Zuraw2010.SubSt.yes) - HarmonicGrammar.harmonyScore constraints w ((p, Zuraw2010.StemC.k), Zuraw2010.SubSt.no)) = w 3 + w 4 - w 1

The logit of substitution for /b/ exceeds that for /k/ by the weights of *[root n/ŋ and *[root ŋ less that of *NC̥, whatever the prefix.

theorem ZurawHayes2017.maxEnt_acrossTheBoard (w : Fin 11 → ℝ) (p p' : Prefix) (c c' : Zuraw2010.StemC) : AcrossTheBoard (square p p' c c') (maxEntSubst w) ∧ AcrossTheBoard (square p p' c c').transpose (maxEntSubst w)

For every weighting, MaxEnt's prefix effects are across the board at every pair of stems, and its stem effects at every pair of prefixes.

Noisy Harmonic Grammar

noncomputable def ZurawHayes2017.weightNoiseSubst (w : Fin 11 → ℝ) (v : NNReal) (x : Prefix × Zuraw2010.StemC) : ℝ

The NHG probability of substitution for an input under noise of variance v on the weights.

Equations

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

theorem ZurawHayes2017.dotProduct_violationDiff_self_p (q : Prefix) : constraints.violationDiff ((q, Zuraw2010.StemC.p), Zuraw2010.SubSt.yes) ((q, Zuraw2010.StemC.p), Zuraw2010.SubSt.no) ⬝ᵥ constraints.violationDiff ((q, Zuraw2010.StemC.p), Zuraw2010.SubSt.yes) ((q, Zuraw2010.StemC.p), Zuraw2010.SubSt.no) = 4

The Noisy HG noise on /p/ is the sum of four Gaussians, one for each constraint that distinguishes substitution from its absence, whatever the prefix (15).

theorem ZurawHayes2017.weightNoise_acrossTheBoard (w : Fin 11 → ℝ) {v : NNReal} (hv : v ≠ 0) (p p' : Prefix) (c c' : Zuraw2010.StemC) : AcrossTheBoard (square p p' c c') (weightNoiseSubst w v)

Noisy Harmonic Grammar's prefix effects are across the board on every square, for every weighting and noise: its noise depends on the stem alone.

Stochastic OT with synergistic families (§3.8)

noncomputable def ZurawHayes2017.raceRate (η : MeasureTheory.Measure ℝ) (n a u : ℝ) : ENNReal

In stochastic OT every ranking value is perturbed by independent noise of law η, and an evaluation is decided by the highest-ranked constraint that distinguishes the candidates. When a lone opposing constraint, with ranking value n, faces two synergistic families, each applying through one constraint, with ranking values a and u, the candidate it favors wins exactly when it outruns the other two (§3.8). raceRate η n a u is the rate of that candidate.

Equations

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

theorem ZurawHayes2017.raceRate_eq (η : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure η] (n a u : ℝ) : raceRate η n a u = ∫⁻ (x : ℝ), η (Set.Iio (x - a)) * η (Set.Iio (x - u)) ∂MeasureTheory.Measure.map (fun (x : ℝ) => n + x) η

The rate of the first candidate integrates, against the law of its constraint, the product of the distribution functions of the other two.

theorem ZurawHayes2017.raceRate_le_one (η : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure η] (n a u : ℝ) : raceRate η n a u ≤ 1

theorem ZurawHayes2017.raceRate_add_le (η : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure η] {n a a' u u' : ℝ} (ha : a' ≤ a) (hu : u ≤ u') : raceRate η n a u + raceRate η n a' u' ≤ raceRate η n a' u + raceRate η n a u'

Magri's theorem (§3.8). The difference that a stronger constraint of one family makes to the opposing candidate's rate is larger the weaker the constraint of the other family, for noise of any law.

theorem ZurawHayes2017.antitone_raceRate_sub (η : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure η] (n : ℝ) {u u' : ℝ} (hu : u ≤ u') : Antitone fun (a : ℝ) => (raceRate η n a u).toReal - (raceRate η n a u').toReal

The difference that a stronger constraint of one family makes grows monotonically as the constraint of the other family weakens: the rates diverge uniformly (§3.8, Figure 20).

theorem ZurawHayes2017.tendsto_raceRate_atTop (η : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure η] (n u : ℝ) : Filter.Tendsto (fun (a : ℝ) => raceRate η n a u) Filter.atTop (nhds 0)

As a constraint of one family strengthens, the opposing candidate's rate vanishes whatever the other: the rates converge (§3.8).

theorem ZurawHayes2017.not_antitone_not_monotone_sigmoid_sub (n : ℝ) {u u' : ℝ} (hu : u < u') : (¬Antitone fun (a : ℝ) => (n - a - u).sigmoid - (n - a - u').sigmoid) ∧ ¬Monotone fun (a : ℝ) => (n - a - u).sigmoid - (n - a - u').sigmoid

In Harmonic Grammar the three constraints pull against each other as in a tug-of-war: with two candidates MaxEnt gives the first the rate sigmoid (n - a - u) (13). A stronger constraint of one family then makes no difference at either extreme of the other, so the difference it makes is neither antitone nor monotone.

The decision-tree model

theorem ZurawHayes2017.decision_tree_monotonic_diff (g₁ g₂ h₁ h₂ : ℚ) (hg : g₁ < g₂) (hh : h₁ < h₂) : g₁ * h₂ - g₁ * h₁ < g₂ * h₂ - g₂ * h₁

In a multiplicative model p(x, y) = g(x) · h(y), the difference between two h-values grows with g: it vanishes at the floor and is largest at the ceiling, the paper's claws.

theorem ZurawHayes2017.decision_tree_diff_proportional (g₁ g₂ h₁ h₂ : ℚ) : (g₂ * h₂ - g₂ * h₁) * g₁ = (g₁ * h₂ - g₁ * h₁) * g₂

In a multiplicative model the ratio of h-differences across two g-values is the ratio of the g-values.