Zuraw (2010): A Model of Lexical Variation and the Grammar

This file formalizes Zuraw's factorial typology of Tagalog nasal substitution. When a nasal-final prefix such as maŋ- attaches to an obstruent-initial stem, the nasal and the obstruent may coalesce into a single nasal at the obstruent's place, as in maŋ+bigáj → mamigáj 'to distribute', or the cluster may survive, as in paŋ+tabój → pantabój 'to goad'. Six constraints decide the outcome. DEP-C and *NC favour substitution, while *ASSOCIATE and the stringent hierarchy of stem-initial nasals after Prince and de Lacy oppose it.

With the six constraints freely ranked, the share of the rankings that substitute for each stem-initial stop follows in closed form from uniform sampling of total orders (factorial_rates). Substitution is therefore more likely on voiceless than on voiced stems (voicing_monotonicity) and on fronter than on backer stems (place_monotonicity). Newman's implicational universals, which the paper's Table 5 organizes, hold ranking by ranking, so that substitution on voiced velar g entails substitution on every stop (g_implies_all).

Implementation notes

• The candidate space is the stem-initial stop paired with the substitution decision; the constraints the paper holds fixed above the six do not distinguish the two candidates.
• The rates are model quantities of the free-ranking idealization. The paper's dictionary counts, corpus rates and acceptability results are not represented; the place effect among voiceless stems is not significant in its judgment data.

References

• K. Zuraw, A Model of Lexical Variation and the Grammar with Application to Tagalog Nasal Substitution (2010)
• K. Zuraw and B. Hayes, Intersecting Constraint Families: An Argument for Harmonic Grammar (2017)
• J. Pater, Austronesian nasal substitution and other NC effects (1999)
• A. Prince, Stringency and anti-Paninian hierarchies (1997)
• P. de Lacy, The formal expression of markedness (2002)
• J. Newman, Nasal replacement in Western Austronesian: an overview (1984)
• R. Blust, Austronesian nasal substitution: a survey (2004)

Stems and substitution decisions

inductive Zuraw2010.StemC : Type

The six stem-initial stops; coalescence maps each to its homorganic nasal.

• p : StemC
• t : StemC
• k : StemC
• b : StemC
• d : StemC
• g : StemC

@[instance_reducible]

instance Zuraw2010.instDecidableEqStemC : DecidableEq StemC

Equations

• Zuraw2010.instDecidableEqStemC x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Zuraw2010.instReprStemC : Repr StemC

Equations

• Zuraw2010.instReprStemC = { reprPrec := Zuraw2010.instReprStemC.repr }

def Zuraw2010.instReprStemC.repr : StemC → ℕ → Std.Format

Equations

• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.p")).group prec✝
• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.t")).group prec✝
• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.k")).group prec✝
• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.b")).group prec✝
• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.d")).group prec✝
• Zuraw2010.instReprStemC.repr Zuraw2010.StemC.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.StemC.g")).group prec✝

@[instance_reducible]

instance Zuraw2010.instFintypeStemC : Fintype StemC

Equations

• Zuraw2010.instFintypeStemC = { elems := { val := ↑Zuraw2010.StemC.enumList, nodup := Zuraw2010.StemC.enumList_nodup }, complete := Zuraw2010.instFintypeStemC._proof_1 }

inductive Zuraw2010.SubSt : Type

Nasal substitution either applies, giving the coalesced nasal, or does not, leaving the faithful cluster.

• yes : SubSt
• no : SubSt

@[instance_reducible]

instance Zuraw2010.instDecidableEqSubSt : DecidableEq SubSt

Equations

• Zuraw2010.instDecidableEqSubSt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Zuraw2010.instReprSubSt : Repr SubSt

Equations

• Zuraw2010.instReprSubSt = { reprPrec := Zuraw2010.instReprSubSt.repr }

def Zuraw2010.instReprSubSt.repr : SubSt → ℕ → Std.Format

Equations

• Zuraw2010.instReprSubSt.repr Zuraw2010.SubSt.yes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.SubSt.yes")).group prec✝
• Zuraw2010.instReprSubSt.repr Zuraw2010.SubSt.no prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zuraw2010.SubSt.no")).group prec✝

@[instance_reducible]

instance Zuraw2010.instFintypeSubSt : Fintype SubSt

Equations

• Zuraw2010.instFintypeSubSt = { elems := { val := ↑Zuraw2010.SubSt.enumList, nodup := Zuraw2010.SubSt.enumList_nodup }, complete := Zuraw2010.instFintypeSubSt._proof_1 }

@[reducible, inline]

abbrev Zuraw2010.NSCand : Type

A candidate is a stem-initial stop paired with a substitution decision.

Equations

• Zuraw2010.NSCand = (Zuraw2010.StemC × Zuraw2010.SubSt)

def Zuraw2010.StemC.segment : StemC → Phonology.Segment

c.segment is the stem-initial stop c as a segment of Fragments/Tagalog/Phonology.lean.

Equations

• Zuraw2010.StemC.p.segment = Tagalog.p
• Zuraw2010.StemC.t.segment = Tagalog.t
• Zuraw2010.StemC.k.segment = Tagalog.k
• Zuraw2010.StemC.b.segment = Tagalog.b
• Zuraw2010.StemC.d.segment = Tagalog.d
• Zuraw2010.StemC.g.segment = Tagalog.g

theorem Zuraw2010.mem_iff_segment (c : StemC) : (c ∈ [StemC.p, StemC.t, StemC.k] ↔ Phonology.Segment.ofSpecs [(Phonology.Feature.voice, false)] ≤ c.segment) ∧ (c ∈ [StemC.k, StemC.g] ↔ Phonology.Segment.ofSpecs [(Phonology.Feature.dorsal, true)] ≤ c.segment) ∧ (c ∈ [StemC.t, StemC.d, StemC.k, StemC.g] ↔ Phonology.Segment.ofSpecs [(Phonology.Feature.labial, false)] ≤ c.segment)

The stem classes that the constraints below list are natural classes, since the stems of *NC are the voiceless ones, those of *[ŋ the dorsal ones, and those of *[n the ones that are not labial.

def Zuraw2010.StemC.nasal : StemC → Phonology.Segment

c.nasal is the nasal at the place of the stop c.

Equations

• Zuraw2010.StemC.p.nasal = Tagalog.m
• Zuraw2010.StemC.b.nasal = Tagalog.m
• Zuraw2010.StemC.t.nasal = Tagalog.n
• Zuraw2010.StemC.d.nasal = Tagalog.n
• Zuraw2010.StemC.k.nasal = Tagalog.ŋ
• Zuraw2010.StemC.g.nasal = Tagalog.ŋ

theorem Zuraw2010.substitute_segment (c : StemC) : Tagalog.substitute c.segment = [c.nasal]

Coalescence gives the nasal of the stop's place, by the fragment's substitution.

The six constraints

def Zuraw2010.nasSub : OptimalityTheory.Constraint NSCand

DEP-C of (6) penalizes inserting a segmental host for the floating nasal, so the faithful cluster violates it for every stem. It is named after [ZH17]'s markedness NasSub, which has the same violation profile on this candidate space.

Equations

• Zuraw2010.nasSub = OptimalityTheory.Constraint.binary fun (c : Zuraw2010.NSCand) => c.2 = Zuraw2010.SubSt.no

def Zuraw2010.starNC : OptimalityTheory.Constraint NSCand

*NC of (17), after [Pat99], forbids a nasal followed by a voiceless obstruent, so the faithful cluster violates it for voiceless stems.

Equations

• Zuraw2010.starNC = OptimalityTheory.Constraint.binary fun (c : Zuraw2010.NSCand) => c.1 ∈ [Zuraw2010.StemC.p, Zuraw2010.StemC.t, Zuraw2010.StemC.k] ∧ c.2 = Zuraw2010.SubSt.no

def Zuraw2010.starAssoc : OptimalityTheory.Constraint NSCand

*ASSOCIATE of (7) forbids new association lines across a morpheme boundary, so coalescence violates it for every stem.

Equations

• Zuraw2010.starAssoc = OptimalityTheory.Constraint.binary fun (c : Zuraw2010.NSCand) => c.2 = Zuraw2010.SubSt.yes

def Zuraw2010.starInitVelar : OptimalityTheory.Constraint NSCand

*[ŋ of (19) forbids a stem to begin with ŋ, so coalescence violates it on velar stems.

Equations

• Zuraw2010.starInitVelar = OptimalityTheory.Constraint.binary fun (c : Zuraw2010.NSCand) => c.1 ∈ [Zuraw2010.StemC.k, Zuraw2010.StemC.g] ∧ c.2 = Zuraw2010.SubSt.yes

def Zuraw2010.starInitCorVel : OptimalityTheory.Constraint NSCand

*[n of (19) forbids a stem to begin with n or a backer nasal, so coalescence violates it on coronal and velar stems.

Equations

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

def Zuraw2010.starInitAll : OptimalityTheory.Constraint NSCand

*[m of (19) forbids a stem to begin with m or a backer nasal, so coalescence violates it on every stem.

Equations

• Zuraw2010.starInitAll = OptimalityTheory.Constraint.binary fun (c : Zuraw2010.NSCand) => c.2 = Zuraw2010.SubSt.yes

def Zuraw2010.con : OptimalityTheory.ConstraintSet NSCand (Fin 6)

The six constraints are listed in the order of the paper's footnote on free ranking.

Equations

• Zuraw2010.con 0 = Zuraw2010.nasSub
• Zuraw2010.con 1 = Zuraw2010.starNC
• Zuraw2010.con 2 = Zuraw2010.starAssoc
• Zuraw2010.con 3 = Zuraw2010.starInitVelar
• Zuraw2010.con 4 = Zuraw2010.starInitCorVel
• Zuraw2010.con 5 = Zuraw2010.starInitAll

theorem Zuraw2010.stringency_violations : starInitAll (StemC.p, SubSt.yes) + starInitCorVel (StemC.p, SubSt.yes) + starInitVelar (StemC.p, SubSt.yes) = 1 ∧ starInitAll (StemC.t, SubSt.yes) + starInitCorVel (StemC.t, SubSt.yes) + starInitVelar (StemC.t, SubSt.yes) = 2 ∧ starInitAll (StemC.k, SubSt.yes) + starInitCorVel (StemC.k, SubSt.yes) + starInitVelar (StemC.k, SubSt.yes) = 3

The stringent hierarchy assigns one, two and three violations to coalesced labial, coronal and velar stems.

theorem Zuraw2010.assoc_eq_initAll (c : StemC) (s : SubSt) : starAssoc (c, s) = starInitAll (c, s)

*ASSOCIATE and *[m have the same violation profile on this candidate space.

The free-ranking rates

def Zuraw2010.nsCands : StemC → Finset SubSt

Both decisions are available for every stem.

Equations

• Zuraw2010.nsCands x✝ = Finset.univ

noncomputable def Zuraw2010.subProb (c : StemC) : ℝ

subProb c is the share of the 720 total orders on which stem c substitutes.

Equations

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

theorem Zuraw2010.subProb_p : subProb StemC.p = 1 / 2

theorem Zuraw2010.subProb_t : subProb StemC.t = 2 / 5

theorem Zuraw2010.subProb_k : subProb StemC.k = 1 / 3

theorem Zuraw2010.subProb_b : subProb StemC.b = 1 / 3

theorem Zuraw2010.subProb_d : subProb StemC.d = 1 / 4

theorem Zuraw2010.subProb_g : subProb StemC.g = 1 / 5

theorem Zuraw2010.factorial_rates : subProb StemC.p = 1 / 2 ∧ subProb StemC.t = 2 / 5 ∧ subProb StemC.k = 1 / 3 ∧ subProb StemC.b = 1 / 3 ∧ subProb StemC.d = 1 / 4 ∧ subProb StemC.g = 1 / 5

The six free-ranking shares of the paper's footnote are a half, two fifths and a third for the voiceless stops and a third, a quarter and a fifth for the voiced ones.

theorem Zuraw2010.place_monotonicity : subProb StemC.p > subProb StemC.t ∧ subProb StemC.t > subProb StemC.k ∧ subProb StemC.b > subProb StemC.d ∧ subProb StemC.d > subProb StemC.g

Within each voicing class the share falls from labial to coronal to velar.

theorem Zuraw2010.voicing_monotonicity : subProb StemC.p ≥ subProb StemC.b ∧ subProb StemC.t ≥ subProb StemC.d ∧ subProb StemC.k ≥ subProb StemC.g

At each place the voiceless share is at least the voiced one.

The implicational universals, ranking by ranking

theorem Zuraw2010.PicksAt_extends_smaller_D {σ : Equiv.Perm (Fin 6)} {c c' : StemC} (h_D : OptimalityTheory.active con c' SubSt.yes SubSt.no ⊆ OptimalityTheory.active con c SubSt.yes SubSt.no) (h_Y : OptimalityTheory.favoring con c' SubSt.yes SubSt.no ⊆ OptimalityTheory.favoring con c SubSt.yes SubSt.no) (h_extra : ∀ x ∈ OptimalityTheory.active con c SubSt.yes SubSt.no, x ∉ OptimalityTheory.active con c' SubSt.yes SubSt.no → x ∈ OptimalityTheory.favoring con c SubSt.yes SubSt.no) (h_c' : OptimalityTheory.PicksAt nsCands con σ c' SubSt.yes) : OptimalityTheory.PicksAt nsCands con σ c SubSt.yes

If c' has a smaller distinguishing set than c and every extra constraint of c favours substitution, then substitution on c' entails substitution on c.

theorem Zuraw2010.PicksAt_extends_larger_D {σ : Equiv.Perm (Fin 6)} {c c' : StemC} (h_D : OptimalityTheory.active con c SubSt.yes SubSt.no ⊆ OptimalityTheory.active con c' SubSt.yes SubSt.no) (h_Y : OptimalityTheory.favoring con c' SubSt.yes SubSt.no ⊆ OptimalityTheory.favoring con c SubSt.yes SubSt.no) (h_subset : OptimalityTheory.favoring con c' SubSt.yes SubSt.no ⊆ OptimalityTheory.active con c SubSt.yes SubSt.no) (h_c' : OptimalityTheory.PicksAt nsCands con σ c' SubSt.yes) : OptimalityTheory.PicksAt nsCands con σ c SubSt.yes

If c' has a larger distinguishing set than c and its substitution-favouring constraints all distinguish the candidates for c, then substitution on c' entails substitution on c.

theorem Zuraw2010.voicing_b_implies_p (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.b SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.p SubSt.yes

Substitution on voiced b entails substitution on voiceless p.

theorem Zuraw2010.voicing_d_implies_t (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.d SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.t SubSt.yes

Substitution on voiced d entails substitution on voiceless t.

theorem Zuraw2010.voicing_g_implies_k (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.g SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.k SubSt.yes

Substitution on voiced g entails substitution on voiceless k.

theorem Zuraw2010.place_k_implies_t (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.k SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.t SubSt.yes

Substitution on velar k entails substitution on coronal t.

theorem Zuraw2010.place_t_implies_p (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.t SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.p SubSt.yes

Substitution on coronal t entails substitution on labial p.

theorem Zuraw2010.place_g_implies_d (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.g SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.d SubSt.yes

Substitution on velar g entails substitution on coronal d.

theorem Zuraw2010.place_d_implies_b (σ : Equiv.Perm (Fin 6)) : OptimalityTheory.PicksAt nsCands con σ StemC.d SubSt.yes → OptimalityTheory.PicksAt nsCands con σ StemC.b SubSt.yes

Substitution on coronal d entails substitution on labial b.

theorem Zuraw2010.g_implies_all (σ : Equiv.Perm (Fin 6)) (h : OptimalityTheory.PicksAt nsCands con σ StemC.g SubSt.yes) : OptimalityTheory.PicksAt nsCands con σ StemC.p SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.t SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.k SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.b SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.d SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.g SubSt.yes

Substitution on voiced velar g entails substitution on every stop, the top of the implicational hierarchy of Table 5.

theorem Zuraw2010.pattern_j_witness : ∃ (σ : Equiv.Perm (Fin 6)), OptimalityTheory.PicksAt nsCands con σ StemC.p SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.t SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.k SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.b SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.d SubSt.yes ∧ OptimalityTheory.PicksAt nsCands con σ StemC.g SubSt.yes

Some ranking substitutes on every stop, which is pattern (j) of Table 5, that of Kalinga and Sarangani Manobo. The identity ranking, with DEP-C on top, is one.