Coetzee and Pater (2011): The Place of Variation in Phonological Theory

Coetzee and Pater compare grammatical models of phonological variation on English word-final t/d-deletion (west ~ wes). Their four constraints (11) protect t/d by MAX everywhere and by MAX-PRE-V and MAX-FINAL before a vowel and phrase-finally, so every ranking that deletes anywhere deletes before a consonant, as Labov's generalization over the dialects of (10) requires. In the partially ordered constraints (POC) model of Kiparsky and Anttila a grammar draws one of its linear extensions uniformly, and the probability of deletion is the share of them that delete.

Any distribution over rankings, POC's or stochastic OT's, therefore deletes most before a consonant, and so does Noisy Harmonic Grammar with noisy weights clamped at zero; MaxEnt with negative weights does not, and variable rules fit any rates. Harmonic Grammar also expresses the cumulative devoicing of Japanese loanwords, which no distribution over rankings matches and Noisy HG matches exactly.

Implementation notes

Locators follow the ROA-946 draft of 6 October 2009, and the printed tables are read from Data/Experiments/CoetzeePater2011.json. Constraint indices follow (11): 0 is *CT, 1 MAX, 2 MAX-PRE-V and 3 MAX-FINAL, while (23) prints them in the order *CT, MAX-PRE-V, MAX-FINAL, MAX. The constraint values of stochastic OT in (14), (21) and (23) come from Praat simulations and are read as data, not derived.

TODO

• Rows (b)–(e) of (13) print counts that (9) does not give: counting the linear extensions of their grammars gives 0, 2, 4; 8, 6, 8; 2, 0, 4; and 6, 8, 8 of 12, and only the two zero cells agree (deletionProb_eq_pocRates_iff). Each printed cell is the rate of the two-stratum grammar that ranks the fixed faithfulness constraint in a stratum of its own, as if the other pairs stayed free. The published chapter has not been checked for a correction.
• §3.3 says that POC can derive only 0, .50 and 1 for pre-consonantal deletion; the grammar of row (b) derives 1/3 (deletionProb_maxPreVOverStarCT_preC_not_mem).
• p. 21 says that no ranking "yields deletion in only pre-consonantal position", which row (d) of (12) does; the argument needs deletion everywhere except pre-consonantally.
• (24) with the two-place weights of (25) gives 33/131, about .252, before a vowel in Tejano, where (25) prints 25.03: Goldvarb's expected rates use its unrounded weights.

References

• A. W. Coetzee and J. Pater, The Place of Variation in Phonological Theory (2011)
• P. Kiparsky, An OT Perspective on Phonological Variation (1993)
• A. Anttila, Deriving Variation from Grammar (1997)
• W. Labov, The Child as Linguistic Historian (1989)
• G. R. Guy, Explanation in Variable Phonology: An Exponential Model of Morphological Constraints (1991)
• H. J. Cedergren and D. Sankoff, Variable Rules: Performance as a Statistical Reflection of Competence (1974)
• P. Boersma, Functional Phonology (1998)
• P. Boersma and B. Hayes, Empirical Tests of the Gradual Learning Algorithm (2001)
• P. Smolensky and G. Legendre, The Harmonic Mind: From Neural Computation to Optimality-Theoretic Grammar (2006)
• S. Goldwater and M. Johnson, Learning OT Constraint Rankings Using a Maximum Entropy Model (2003)
• J. Itô and A. Mester, The Phonology of Voicing in Japanese (1986)
• S. Kawahara, A Faithfulness Ranking Projected from a Perceptibility Scale: The Case of [+voice] in Japanese (2006)

Deletion rates by context and by morphology ((7), (10))

def CoetzeePater2011.observedRate (d : Dialect) (ctx : Context) : ℕ

The percentage of t/d that dialect d deletes before ctx, read from (10).

Equations

• CoetzeePater2011.observedRate d ctx = (CoetzeePater2011.contextRates d ctx).percent

theorem CoetzeePater2011.observedRate_le_preC (d : Dialect) (ctx : Context) : observedRate d ctx ≤ observedRate d Context.preC

Every dialect of (10) deletes most before a consonant, Labov's cross-dialectal generalization.

theorem CoetzeePater2011.observedRate_pause_lt_preV_iff (d : Dialect) : observedRate d Context.pause < observedRate d Context.preV ↔ d = Dialect.chicano ∨ d = Dialect.philadelphia

Chicano and Philadelphia English delete more before a vowel than before a pause.

theorem CoetzeePater2011.observedRate_preV_lt_pause_iff (d : Dialect) : observedRate d Context.preV < observedRate d Context.pause ↔ d ≠ Dialect.chicano ∧ d ≠ Dialect.philadelphia

The other dialects of (10) delete more before a pause than before a vowel.

theorem CoetzeePater2011.morphRates_lt (r : MorphRate) : r ∈ morphRates → r.regularPast < r.semiWeakPast ∧ r.semiWeakPast < r.monomorpheme

In every dialect of (7) a regular past suffix deletes least and a monomorpheme most, with semi-weak pasts in between, as Guy found.

def CoetzeePater2011.tejanoPrime : Context → ℕ

Tejano′ trades the pre-vocalic and pre-consonantal rates of Tejano (p. 20–21).

Equations

• CoetzeePater2011.tejanoPrime CoetzeePater2011.Context.preV = CoetzeePater2011.observedRate CoetzeePater2011.Dialect.tejano CoetzeePater2011.Context.preC
• CoetzeePater2011.tejanoPrime CoetzeePater2011.Context.pause = CoetzeePater2011.observedRate CoetzeePater2011.Dialect.tejano CoetzeePater2011.Context.pause
• CoetzeePater2011.tejanoPrime CoetzeePater2011.Context.preC = CoetzeePater2011.observedRate CoetzeePater2011.Dialect.tejano CoetzeePater2011.Context.preV

The constraints of (11)

inductive CoetzeePater2011.Output : Type

The output retains the final t/d (west) or deletes it (wes).

• retain : Output
• delete : Output

@[instance_reducible]

instance CoetzeePater2011.instDecidableEqOutput : DecidableEq Output

Equations

• CoetzeePater2011.instDecidableEqOutput x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoetzeePater2011.instFintypeOutput : Fintype Output

Equations

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

@[reducible, inline]

abbrev CoetzeePater2011.Candidate : Type

A candidate pairs the following context with the output.

Equations

• CoetzeePater2011.Candidate = (CoetzeePater2011.Context × CoetzeePater2011.Output)

def CoetzeePater2011.starCT : OptimalityTheory.Constraint Candidate

*CT penalizes a consonant cluster ending in a coronal stop.

Equations

• CoetzeePater2011.starCT = OptimalityTheory.Constraint.binary fun (x : CoetzeePater2011.Candidate) => x.2 = CoetzeePater2011.Output.retain

def CoetzeePater2011.maxC : OptimalityTheory.Constraint Candidate

MAX penalizes an input consonant missing from the output.

Equations

• CoetzeePater2011.maxC = OptimalityTheory.Constraint.binary fun (x : CoetzeePater2011.Candidate) => x.2 = CoetzeePater2011.Output.delete

def CoetzeePater2011.maxPreV : OptimalityTheory.Constraint Candidate

MAX-PRE-V penalizes a pre-vocalic input consonant missing from the output.

Equations

• CoetzeePater2011.maxPreV = OptimalityTheory.Constraint.binary fun (c : CoetzeePater2011.Candidate) => c.2 = CoetzeePater2011.Output.delete ∧ c.1 = CoetzeePater2011.Context.preV

def CoetzeePater2011.maxFinal : OptimalityTheory.Constraint Candidate

MAX-FINAL penalizes a phrase-final input consonant missing from the output.

Equations

• CoetzeePater2011.maxFinal = OptimalityTheory.Constraint.binary fun (c : CoetzeePater2011.Candidate) => c.2 = CoetzeePater2011.Output.delete ∧ c.1 = CoetzeePater2011.Context.pause

def CoetzeePater2011.con : OptimalityTheory.ConstraintSet Candidate (Fin 4)

The constraint set (11) lists the constraints in the paper's order.

Equations

• CoetzeePater2011.con = ![CoetzeePater2011.starCT, CoetzeePater2011.maxC, CoetzeePater2011.maxPreV, CoetzeePater2011.maxFinal]

def CoetzeePater2011.cands : Context → Finset Output

Both outputs compete in every context.

Equations

• CoetzeePater2011.cands x✝ = Finset.univ

theorem CoetzeePater2011.cands_eq (ctx : Context) : cands ctx = {Output.delete, Output.retain}

Categorical systems (12)

def CoetzeePater2011.Deletes (σ : OptimalityTheory.Ranking (Fin 4) 4) (ctx : Context) : Prop

Ranking σ deletes in ctx if deletion is its unique optimum.

Equations

• CoetzeePater2011.Deletes σ ctx = OptimalityTheory.PicksAt CoetzeePater2011.cands CoetzeePater2011.con σ ctx CoetzeePater2011.Output.delete

@[instance_reducible]

instance CoetzeePater2011.instDecidableDeletes (σ : OptimalityTheory.Ranking (Fin 4) 4) (ctx : Context) : Decidable (Deletes σ ctx)

Equations

• CoetzeePater2011.instDecidableDeletes σ ctx = CoetzeePater2011.instDecidableDeletes._aux_1 σ ctx

theorem CoetzeePater2011.deletes_preC_iff (σ : OptimalityTheory.Ranking (Fin 4) 4) : Deletes σ Context.preC ↔ σ.Dominates 0 1

Pre-consonantal deletion needs only *CT ≫ MAX.

theorem CoetzeePater2011.deletes_preV_iff (σ : OptimalityTheory.Ranking (Fin 4) 4) : Deletes σ Context.preV ↔ σ.Dominates 0 1 ∧ σ.Dominates 0 2

Pre-vocalic deletion needs *CT above both MAX and MAX-PRE-V.

theorem CoetzeePater2011.deletes_pause_iff (σ : OptimalityTheory.Ranking (Fin 4) 4) : Deletes σ Context.pause ↔ σ.Dominates 0 1 ∧ σ.Dominates 0 3

Phrase-final deletion needs *CT above both MAX and MAX-FINAL.

def CoetzeePater2011.system (σ : OptimalityTheory.Ranking (Fin 4) 4) : Finset Context

The categorical system of σ is the set of contexts in which it deletes.

Equations

• CoetzeePater2011.system σ = Finset.filter (CoetzeePater2011.Deletes σ) Finset.univ

theorem CoetzeePater2011.image_system : Finset.image system Finset.univ = {∅, {Context.pause, Context.preC}, {Context.preV, Context.preC}, {Context.preC}, Finset.univ}

The five systems of (12), rows (a)–(e), from no deletion to deletion in all three contexts.

theorem CoetzeePater2011.card_system_empty : {x : OptimalityTheory.Ranking (Fin 4) 4 | system x = ∅}.card = 12

Twelve rankings, those with MAX ≫ *CT, delete nowhere.

theorem CoetzeePater2011.card_system_pause_preC : {x : OptimalityTheory.Ranking (Fin 4) 4 | system x = {Context.pause, Context.preC}}.card = 2

theorem CoetzeePater2011.card_system_preV_preC : {x : OptimalityTheory.Ranking (Fin 4) 4 | system x = {Context.preV, Context.preC}}.card = 2

theorem CoetzeePater2011.card_system_preC : {x : OptimalityTheory.Ranking (Fin 4) 4 | system x = {Context.preC}}.card = 2

theorem CoetzeePater2011.card_system_univ : {x : OptimalityTheory.Ranking (Fin 4) 4 | system x = Finset.univ}.card = 6

Six rankings, those with *CT on top, delete everywhere.

Deletion probabilities ((9), (13))

theorem CoetzeePater2011.favoring_eq (ctx : Context) : OptimalityTheory.favoring con ctx Output.delete Output.retain = {0}

Only *CT favors deletion, in every context.

theorem CoetzeePater2011.active_preC : OptimalityTheory.active con Context.preC Output.delete Output.retain = {0, 1}

MAX alone protects t/d pre-consonantally.

theorem CoetzeePater2011.active_preV : OptimalityTheory.active con Context.preV Output.delete Output.retain = {0, 1, 2}

MAX-PRE-V joins MAX pre-vocalically.

theorem CoetzeePater2011.active_pause : OptimalityTheory.active con Context.pause Output.delete Output.retain = {0, 1, 3}

MAX-FINAL joins MAX phrase-finally.

def CoetzeePater2011.extensions : ImposedRanking → Finset (OptimalityTheory.Ranking (Fin 4) 4)

The grammar of row (a) of (13) has every ranking as a linear extension, and the grammars of rows (b)–(e) the rankings that order their imposed pair as they do.

Equations

• CoetzeePater2011.extensions CoetzeePater2011.ImposedRanking.none = Finset.univ
• CoetzeePater2011.extensions CoetzeePater2011.ImposedRanking.maxPreVOverStarCT = {x : OptimalityTheory.Ranking (Fin 4) 4 | x.Dominates 2 0}
• CoetzeePater2011.extensions CoetzeePater2011.ImposedRanking.starCTOverMaxPreV = {x : OptimalityTheory.Ranking (Fin 4) 4 | x.Dominates 0 2}
• CoetzeePater2011.extensions CoetzeePater2011.ImposedRanking.maxFinalOverStarCT = {x : OptimalityTheory.Ranking (Fin 4) 4 | x.Dominates 3 0}
• CoetzeePater2011.extensions CoetzeePater2011.ImposedRanking.starCTOverMaxFinal = {x : OptimalityTheory.Ranking (Fin 4) 4 | x.Dominates 0 3}

noncomputable def CoetzeePater2011.deletionProb (g : ImposedRanking) (ctx : Context) : ℝ

The probability that a grammar of (13) deletes in ctx, the share of its linear extensions that delete (9).

Equations

• CoetzeePater2011.deletionProb g ctx = (ProbabilityTheory.uniformOn ↑(CoetzeePater2011.extensions g)).real {σ : OptimalityTheory.Ranking (Fin 4) 4 | CoetzeePater2011.Deletes σ ctx}

theorem CoetzeePater2011.deletionProb_none (ctx : Context) : deletionProb ImposedRanking.none ctx = (↑(OptimalityTheory.active con ctx Output.delete Output.retain).card)⁻¹

With no ranking imposed (row (a)), deletion needs *CT above every constraint active in the context, so its probability is one over their number: 12, 8 and 8 of the 24 rankings delete before a consonant, a vowel and a pause.

theorem CoetzeePater2011.deletionProb_none_eq_pocRates (ctx : Context) : deletionProb ImposedRanking.none ctx = ↑(pocRates ImposedRanking.none ctx).rankings / ↑(pocRates ImposedRanking.none ctx).total

Row (a) of (13) prints the counts of (9).

theorem CoetzeePater2011.card_extensions (g : ImposedRanking) (ctx : Context) : (extensions g).card = (pocRates g ctx).total

Every grammar of (13) has the printed number of linear extensions, 24 or 12.

theorem CoetzeePater2011.deletionProb_maxPreVOverStarCT : deletionProb ImposedRanking.maxPreVOverStarCT Context.preV = 0 ∧ deletionProb ImposedRanking.maxPreVOverStarCT Context.pause = 1 / 6 ∧ deletionProb ImposedRanking.maxPreVOverStarCT Context.preC = 1 / 3

Under MAX-PRE-V ≫ *CT (row (b)), 0, 2 and 4 of the 12 linear extensions delete before a vowel, a pause and a consonant.

theorem CoetzeePater2011.deletionProb_starCTOverMaxPreV : deletionProb ImposedRanking.starCTOverMaxPreV Context.preV = 2 / 3 ∧ deletionProb ImposedRanking.starCTOverMaxPreV Context.pause = 1 / 2 ∧ deletionProb ImposedRanking.starCTOverMaxPreV Context.preC = 2 / 3

Under *CT ≫ MAX-PRE-V (row (c)), 8, 6 and 8 of 12 delete.

theorem CoetzeePater2011.deletionProb_maxFinalOverStarCT : deletionProb ImposedRanking.maxFinalOverStarCT Context.preV = 1 / 6 ∧ deletionProb ImposedRanking.maxFinalOverStarCT Context.pause = 0 ∧ deletionProb ImposedRanking.maxFinalOverStarCT Context.preC = 1 / 3

Under MAX-FINAL ≫ *CT (row (d)), 2, 0 and 4 of 12 delete.

theorem CoetzeePater2011.deletionProb_starCTOverMaxFinal : deletionProb ImposedRanking.starCTOverMaxFinal Context.preV = 1 / 2 ∧ deletionProb ImposedRanking.starCTOverMaxFinal Context.pause = 2 / 3 ∧ deletionProb ImposedRanking.starCTOverMaxFinal Context.preC = 2 / 3

Under *CT ≫ MAX-FINAL (row (e)), 6, 8 and 8 of 12 delete.

theorem CoetzeePater2011.deletionProb_eq_pocRates_iff (g : ImposedRanking) (ctx : Context) : deletionProb g ctx = ↑(pocRates g ctx).rankings / ↑(pocRates g ctx).total ↔ g = ImposedRanking.none ∨ (pocRates g ctx).rankings = 0

A printed cell of (13) is the probability (9) gives exactly in row (a) and in the two cells where no linear extension deletes.

theorem CoetzeePater2011.deletionProb_maxPreVOverStarCT_preC_not_mem : deletionProb ImposedRanking.maxPreVOverStarCT Context.preC ∉ {0, 1 / 2, 1}

§3.3 says that POC can derive only 0, .50 and 1 for pre-consonantal deletion, since only MAX and *CT decide it, but the grammar of row (b) derives 1/3.

theorem CoetzeePater2011.five_le_of_real_picksAt_eq {n : ℕ} {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {cands : Input → Finset Output} {con : OptimalityTheory.ConstraintSet (Input × Output) (Fin n)} {r : Fin n → Fin n → Prop} [DecidableRel r] {i : Input} {o : Output} (h : (ProbabilityTheory.uniformOn ↑(OptimalityTheory.consistentTotalOrders r)).real {σ : OptimalityTheory.Ranking (Fin n) n | OptimalityTheory.PicksAt cands con σ i o} = 1 / 100) : 5 ≤ n

As Boersma and Hayes point out (§3.3), a POC grammar that gives an output probability .01 has at least 100 linear extensions, and so at least five constraints.

theorem CoetzeePater2011.uniformOn_univ_real_picksAt_ne {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] (cands : Input → Finset Output) (con : OptimalityTheory.ConstraintSet (Input × Output) (Fin 5)) (i : Input) (o : Output) : (ProbabilityTheory.uniformOn Set.univ).real {σ : OptimalityTheory.Ranking (Fin 5) 5 | OptimalityTheory.PicksAt cands con σ i o} ≠ 1 / 100

Five freely ranked constraints do not suffice for a probability of .01 either, since 1/100 is not a multiple of 1/120.

The restriction shared by POC and stochastic OT (§3.2, §4.4)

theorem CoetzeePater2011.deletes_preC_of_deletes {σ : OptimalityTheory.Ranking (Fin 4) 4} {ctx : Context} (h : Deletes σ ctx) : Deletes σ Context.preC

A ranking that deletes before a vowel or a pause also deletes before a consonant (rows (b), (c) and (e) of (12)).

theorem CoetzeePater2011.measure_deletes_le_preC (μ : MeasureTheory.Measure (OptimalityTheory.Ranking (Fin 4) 4)) (ctx : Context) : μ {σ : OptimalityTheory.Ranking (Fin 4) 4 | Deletes σ ctx} ≤ μ {σ : OptimalityTheory.Ranking (Fin 4) 4 | Deletes σ Context.preC}

Any distribution over rankings, a POC grammar's (p. 11) or stochastic OT's (p. 21), deletes at least as often before a consonant as in any other context.

theorem CoetzeePater2011.not_forall_real_deletes_eq_tejanoPrime (μ : MeasureTheory.Measure (OptimalityTheory.Ranking (Fin 4) 4)) [MeasureTheory.IsFiniteMeasure μ] : ¬∀ (ctx : Context), μ.real {σ : OptimalityTheory.Ranking (Fin 4) 4 | Deletes σ ctx} = ↑(tejanoPrime ctx) / 100

No distribution over rankings produces Tejano′, whose pre-consonantal rate is its lowest.

Harmonic Grammar (§4.2, §4.4)

@[simp]

theorem CoetzeePater2011.harmonyScore_retain {w : Fin 4 → ℝ} (ctx : Context) : HarmonicGrammar.harmonyScore con w (ctx, Output.retain) = -w 0

Retention violates only *CT.

@[simp]

theorem CoetzeePater2011.harmonyScore_delete_preV {w : Fin 4 → ℝ} : HarmonicGrammar.harmonyScore con w (Context.preV, Output.delete) = -(w 1 + w 2)

Pre-vocalic deletion violates MAX and MAX-PRE-V.

@[simp]

theorem CoetzeePater2011.harmonyScore_delete_pause {w : Fin 4 → ℝ} : HarmonicGrammar.harmonyScore con w (Context.pause, Output.delete) = -(w 1 + w 3)

Phrase-final deletion violates MAX and MAX-FINAL.

@[simp]

theorem CoetzeePater2011.harmonyScore_delete_preC {w : Fin 4 → ℝ} : HarmonicGrammar.harmonyScore con w (Context.preC, Output.delete) = -w 1

Pre-consonantal deletion violates MAX alone.

def CoetzeePater2011.HGDeletes (w : Fin 4 → ℝ) (ctx : Context) : Prop

Deletion in ctx has greater harmony than retention under weights w ((16)–(17)).

Equations

• CoetzeePater2011.HGDeletes w ctx = HarmonicGrammar.harmonyDominates CoetzeePater2011.con w (ctx, CoetzeePater2011.Output.delete) (ctx, CoetzeePater2011.Output.retain)

@[simp]

theorem CoetzeePater2011.hgDeletes_preC_iff {w : Fin 4 → ℝ} : HGDeletes w Context.preC ↔ w 1 < w 0

@[simp]

theorem CoetzeePater2011.hgDeletes_preV_iff {w : Fin 4 → ℝ} : HGDeletes w Context.preV ↔ w 1 + w 2 < w 0

@[simp]

theorem CoetzeePater2011.hgDeletes_pause_iff {w : Fin 4 → ℝ} : HGDeletes w Context.pause ↔ w 1 + w 3 < w 0

theorem CoetzeePater2011.hgDeletes_preC_of_hgDeletes {w : Fin 4 → ℝ} (hw : 0 ≤ w) {ctx : Context} (h : HGDeletes w ctx) : HGDeletes w Context.preC

With non-negative weights, HG shares the implication of the rankings.

theorem CoetzeePater2011.image_system_eq_filter : Finset.image system Finset.univ = {S : Finset Context | S.Nonempty → Context.preC ∈ S}

The systems of (12) are the sets of contexts in which deletion anywhere entails deletion before a consonant.

theorem CoetzeePater2011.setOf_hgDeletes_eq : {S : Finset Context | ∃ (w : Fin 4 → ℝ), 0 ≤ w ∧ ∀ (ctx : Context), HGDeletes w ctx ↔ ctx ∈ S} = ↑(Finset.image system Finset.univ)

Categorical HG with non-negative weights generates exactly the five systems of (12) (footnote 8). A system is generated by weighting *CT 1 and each faithfulness constraint 1 where the system retains and 0 where it deletes.

theorem CoetzeePater2011.weightNoise_hgDeletes_le_preC (w : Fin 4 → ℝ) (v : NNReal) (ctx : Context) : (HarmonicGrammar.weightNoise (Fin 4) v) {η : Fin 4 → ℝ | HGDeletes (w + η)⁺ ctx} ≤ (HarmonicGrammar.weightNoise (Fin 4) v) {η : Fin 4 → ℝ | HGDeletes (w + η)⁺ Context.preC}

Noisy HG as the paper's learner evaluates it, with noisy weights below zero replaced by zero (p. 19), deletes at least as often before a consonant as elsewhere, for every weighting and noise variance.

theorem CoetzeePater2011.hgDeletes_neg (ctx : Context) : HGDeletes ![0, 0, -1, 0] ctx ↔ ctx = Context.preV

A negative MAX-PRE-V weight rewards pre-vocalic deletion, giving deletion pre-vocalically alone (§4.4).

theorem CoetzeePater2011.singleton_preV_not_mem : {Context.preV} ∉ Finset.image system Finset.univ

Deletion pre-vocalically alone is not among the systems of (12).

MaxEnt Harmonic Grammar (§4.3–4.4)

@[instance_reducible]

instance CoetzeePater2011.instMeasurableSpaceOutput : MeasurableSpace Output

Equations

• CoetzeePater2011.instMeasurableSpaceOutput = ⊤

instance CoetzeePater2011.instMeasurableSingletonClassOutput : MeasurableSingletonClass Output

noncomputable def CoetzeePater2011.maxEntProb (w : Fin 4 → ℝ) (ctx : Context) : ℝ

The MaxEnt deletion probability in ctx, the probability of the deletion output under the MaxEnt distribution of the context's two outputs.

Equations

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

theorem CoetzeePater2011.maxEntProb_eq_sigmoid (w : Fin 4 → ℝ) (ctx : Context) : maxEntProb w ctx = (HarmonicGrammar.harmonyScore con w (ctx, Output.delete) - HarmonicGrammar.harmonyScore con w (ctx, Output.retain)).sigmoid

With two candidates, the deletion probability is the logistic of the harmony difference.

theorem CoetzeePater2011.maxEntProb_le_preC {w : Fin 4 → ℝ} (hw : 0 ≤ w) (ctx : Context) : maxEntProb w ctx ≤ maxEntProb w Context.preC

Non-negative contextual faithfulness keeps MaxEnt within the restriction (§4.4).

theorem CoetzeePater2011.maxEntProb_preV_lt_pause_iff (w : Fin 4 → ℝ) : maxEntProb w Context.preV < maxEntProb w Context.pause ↔ w 3 < w 2

MaxEnt deletes less before a vowel than before a pause exactly when MAX-PRE-V outweighs MAX-FINAL.

theorem CoetzeePater2011.learnedGrammars_maxFinal_lt_maxPreV_iff (d : Dialect) (m : Model) : (learnedGrammars d m).maxFinal.toRat < (learnedGrammars d m).maxPreV.toRat ↔ observedRate d Context.preV < observedRate d Context.pause

In every grammar of (23), MAX-PRE-V has the higher value when deletion is rarer before a vowel than before a pause, and MAX-FINAL otherwise (p. 20).

noncomputable def CoetzeePater2011.meWeights (d : Dialect) : Fin 4 → ℝ

The MaxEnt weights of dialect d in (23), in the order of (11).

Equations

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

theorem CoetzeePater2011.maxEntProb_meWeights_lt_iff (d : Dialect) (ctx ctx' : Context) : maxEntProb (meWeights d) ctx < maxEntProb (meWeights d) ctx' ↔ observedRate d ctx < observedRate d ctx'

The MaxEnt grammars of (23) order each dialect's three contexts as its observed rates do.

noncomputable def CoetzeePater2011.tejanoPrimeWeights : Fin 4 → ℝ

The MaxEnt weights of Tejano′ in (23), with negative contextual faithfulness.

Equations

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

theorem CoetzeePater2011.maxEntProb_tejanoPrimeWeights_lt_iff (ctx ctx' : Context) : maxEntProb tejanoPrimeWeights ctx < maxEntProb tejanoPrimeWeights ctx' ↔ tejanoPrime ctx < tejanoPrime ctx'

Negative weights reward pre-vocalic and phrase-final deletion, so the MaxEnt grammar of Tejano′ orders the contexts as Tejano′ does, pre-consonantal deletion rarest (§4.4).

Cumulativity: Japanese loanword devoicing ((18)–(22))

inductive CoetzeePater2011.Voicing : Type

A loanword keeps its voiced obstruents or devoices the geminate.

• voiced : Voicing
• devoiced : Voicing

@[instance_reducible]

instance CoetzeePater2011.instDecidableEqVoicing : DecidableEq Voicing

Equations

• CoetzeePater2011.instDecidableEqVoicing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CoetzeePater2011.instFintypeVoicing : Fintype Voicing

Equations

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

@[instance_reducible]

instance CoetzeePater2011.instMeasurableSpaceVoicing : MeasurableSpace Voicing

Equations

• CoetzeePater2011.instMeasurableSpaceVoicing = ⊤

instance CoetzeePater2011.instMeasurableSingletonClassVoicing : MeasurableSingletonClass Voicing

def CoetzeePater2011.identVoice : OptimalityTheory.Constraint (Loan × Voicing)

IDENT-VOICE is violated by the devoiced output.

Equations

• CoetzeePater2011.identVoice = OptimalityTheory.Constraint.binary fun (x : CoetzeePater2011.Loan × CoetzeePater2011.Voicing) => x.2 = CoetzeePater2011.Voicing.devoiced

def CoetzeePater2011.ocpVoice : OptimalityTheory.Constraint (Loan × Voicing)

OCP-VOICE is violated by two voiced obstruents in one root, in faithful bobu and guddo.

Equations

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

def CoetzeePater2011.voicedGeminate : OptimalityTheory.Constraint (Loan × Voicing)

*VOICED-GEMINATE is violated by a voiced geminate, in faithful webbu and guddo.

Equations

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

def CoetzeePater2011.loanwordDevoicing : HarmonicGrammar.RealizationProblem Loan Voicing (Fin 3)

The tableaux (18)–(19) form a realization problem over IDENT-VOICE, OCP-VOICE and *VOICED-GEMINATE, after Itô and Mester and Kawahara, in which only guddo devoices.

Equations

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

theorem CoetzeePater2011.loanwordDevoicing_realizedByWeighting : loanwordDevoicing.realizedByWeighting ![3 / 2, 1, 1]

The weights of (18)–(19), IDENT-VOICE 1.5 over OCP-VOICE 1 and *VOICED-GEMINATE 1, realize the pattern, since the two lower weights sum past the higher one only in guddo.

theorem CoetzeePater2011.loanwordDevoicing_not_isOTRealizable : ¬loanwordDevoicing.IsOTRealizable

No ranking realizes the pattern, the instance behind hg_strictly_contains_ot.

def CoetzeePater2011.Devoices (σ : OptimalityTheory.Ranking (Fin 3) 3) (l : Loan) : Prop

Ranking σ devoices loanword l.

Equations

• CoetzeePater2011.Devoices σ l = OptimalityTheory.PicksAt CoetzeePater2011.loanwordDevoicing.cands CoetzeePater2011.loanwordDevoicing.con σ l CoetzeePater2011.Voicing.devoiced

theorem CoetzeePater2011.setOf_devoices_guddo : {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.guddo} = {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.bobu} ∪ {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.webbu}

A ranking devoices guddo exactly when it devoices bobu or webbu, when OCP-VOICE or *VOICED-GEMINATE outranks IDENT-VOICE (p. 18).

theorem CoetzeePater2011.measure_devoices_guddo_le (μ : MeasureTheory.Measure (OptimalityTheory.Ranking (Fin 3) 3)) : μ {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.guddo} ≤ μ {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.bobu} + μ {σ : OptimalityTheory.Ranking (Fin 3) 3 | Devoices σ Loan.webbu}

No distribution over rankings devoices guddo more often than bobu and webbu together, so stochastic OT cannot learn the data of (21), where only guddo devoices (p. 18).

theorem CoetzeePater2011.weightNoiseChoiceProb_guddo (w : Fin 3 → ℝ) (hw : w 0 = w 1 + w 2) (v : NNReal) (hv : v ≠ 0) : HarmonicGrammar.weightNoiseChoiceProb (fun (k : Fin 3) (o : Voicing) => loanwordDevoicing.con k (Loan.guddo, o)) w v Voicing.devoiced = 2⁻¹

In Noisy HG, guddo devoices with probability one half, as in the learning data, whenever IDENT-VOICE weighs the sum of the other two weights (p. 18).

theorem CoetzeePater2011.guddo_maxEnt_half (o : Voicing) : (HarmonicGrammar.maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x : Voicing) => (Loan.guddo, x)) loanwordDevoicing.con).violations ![2, 1, 1]).real {o} = 2⁻¹

With IDENT-VOICE weighted 2 over 1 and 1, guddo and gutto tie at harmony −2 and MaxEnt gives each probability ½ (tableau (22)).

Variable rules (§4.5)

noncomputable def CoetzeePater2011.variableRule {ι : Type u_1} [Fintype ι] (p : ι → ℝ) : ℝ

Cedergren and Sankoff's variable-rule probability (24) combines the input probability and one factor weight for each contextual factor present, all as factors p.

Equations

• CoetzeePater2011.variableRule p = (∏ i : ι, p i) / (∏ i : ι, p i + ∏ i : ι, (1 - p i))

theorem CoetzeePater2011.variableRule_eq_sigmoid {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (hp : ∀ (i : ι), p i ∈ Set.Ioo 0 1) : variableRule p = (∑ i : ι, (p i).logit).sigmoid

The variable-rule probability is the logistic of the summed log-odds of its factors, the logistic regression Goldvarb runs (p. 21–22).

theorem CoetzeePater2011.exists_variableRule_eq (q : Context → ℝ) : ∃ (p₀ : ℝ) (p : Context → ℝ), ∀ (ctx : Context), variableRule ![p₀, p ctx] = q ctx

One factor group with input probability ½ fits any rates, so the variable rules fit Tejano′ as well as Tejano ((25)) and impose no typological restriction.

theorem CoetzeePater2011.variableRule_lt_iff {p₀ c c' s : ℝ} (h₀ : p₀ ∈ Set.Ioo 0 1) (hc : c ∈ Set.Ioo 0 1) (hc' : c' ∈ Set.Ioo 0 1) (hs : s ∈ Set.Ioo 0 1) : variableRule ![p₀, c, s] < variableRule ![p₀, c', s] ↔ c < c'

The factors of a variable rule are independent, so a register factor cannot reorder two contexts: the context with the lower factor weight deletes less in every register (p. 24–25).

theorem CoetzeePater2011.exists_styleSensitive_reorders : ∃ (w : Fin 4 → ℝ) (sens : Fin 4 → ℝ), sens 2 = 0 ∧ maxEntProb (w + 0 • sens) Context.preV < maxEntProb (w + 0 • sens) Context.pause ∧ maxEntProb (w + 1 • sens) Context.pause < maxEntProb (w + 1 • sens) Context.preV

In style-sensitive HG (28) a style sensitivity on MAX-FINAL alone lets one register delete least before a vowel and another least before a pause, which variable rules cannot (p. 25).

Lexically indexed faithfulness ((32))

def CoetzeePater2011.indexed (l : Lexeme) (c : OptimalityTheory.Constraint Candidate) : OptimalityTheory.Constraint (Lexeme × Candidate)

A constraint indexed to word l assigns its violations to the candidates of l alone.

Equations

• CoetzeePater2011.indexed l c x = if x.1 = l then c x.2 else 0

def CoetzeePater2011.indexedCon : OptimalityTheory.ConstraintSet (Lexeme × Candidate) (Option (Lexeme × Fin 3))

The constraints of (32) are those of (11) with each faithfulness constraint indexed to each word, none being *CT and some (l, k) the faithfulness constraint con k.succ indexed to l.

Equations

• CoetzeePater2011.indexedCon none = OptimalityTheory.Constraint.comap Prod.snd (CoetzeePater2011.con 0)
• CoetzeePater2011.indexedCon (some (l, k)) = CoetzeePater2011.indexed l (CoetzeePater2011.con k.succ)

noncomputable def CoetzeePater2011.indexedWeights : Option (Lexeme × Fin 3) → ℝ

The weights of (32).

Equations

• One or more equations did not get rendered due to their size.
• CoetzeePater2011.indexedWeights none = ↑CoetzeePater2011.indexedStarCT.toRat

def CoetzeePater2011.indexedTableau (l : Lexeme) (ctx : Context) : OptimalityTheory.ConstraintSet Output (Option (Lexeme × Fin 3))

The tableau of word l before ctx under the constraints of (32).

Equations

• CoetzeePater2011.indexedTableau l ctx k o = CoetzeePater2011.indexedCon k (l, ctx, o)

def CoetzeePater2011.exchange : Option (Lexeme × Fin 3) ≃ Option (Lexeme × Fin 3)

The permutation exchange swaps the two words in the indices of (32).

Equations

• CoetzeePater2011.exchange = (Equiv.prodCongr (Equiv.swap CoetzeePater2011.Lexeme.feast CoetzeePater2011.Lexeme.most) (Equiv.refl (Fin 3))).optionCongr

theorem CoetzeePater2011.indexedTableau_most (ctx : Context) : indexedTableau Lexeme.most ctx = fun (k : Option (Lexeme × Fin 3)) => indexedTableau Lexeme.feast ctx (exchange k)

The tableau of most is that of feast with the two words exchanged.

theorem CoetzeePater2011.weightNoiseChoiceProb_feast_lt_most {w : Option (Lexeme × Fin 3) → ℝ} (hw : ∀ (k : Fin 3), w (some (Lexeme.most, k)) < w (some (Lexeme.feast, k))) {v : NNReal} (hv : v ≠ 0) (ctx : Context) : HarmonicGrammar.weightNoiseChoiceProb (indexedTableau Lexeme.feast ctx) w v Output.delete < HarmonicGrammar.weightNoiseChoiceProb (indexedTableau Lexeme.most ctx) w v Output.delete

When each faithfulness weight indexed to feast exceeds the one indexed to most, Noisy HG deletes less from feast than from most in every context (p. 29).

theorem CoetzeePater2011.weightNoiseChoiceProb_indexedWeights {v : NNReal} (hv : v ≠ 0) (ctx : Context) : HarmonicGrammar.weightNoiseChoiceProb (indexedTableau Lexeme.feast ctx) indexedWeights v Output.delete < HarmonicGrammar.weightNoiseChoiceProb (indexedTableau Lexeme.most ctx) indexedWeights v Output.delete

The grammar learned in (32) deletes less from feast than from most in every context, as its learning data do.