[Ant97]: Deriving Variation from Grammar

Formalizes the Finnish genitive-plural predictions of [Ant97]: free variation — including its statistical biases — follows from a single partially-ranked OT grammar, a variant's probability being the fraction of total rankings under which it wins. Categorical outputs are the limiting case where every ranking converges on the same winner (probability 1 or 0), so categorical and variable motifs fall out of the same grammar.

Page and item numbers cite the ROA-63 manuscript version (May 1995); the published chapter [Ant97] paginates 35–68.

The grammar

finnishGrammar is "the grammar for Finnish, final version" (eq. (50), page 21) in full: 20 constraints in 5 mutually-ranked sets, as a single stratified partial order on Fin 20:

• Set 1: *X́.X́ (No Clash)
• Set 2: *Ĺ (Peak Prominence: no stressed lights), *H (Weight-to-Stress: no unstressed heavies)
• Set 3: *H/I, *Í, *L.L
• Set 4: *H/O, *Ó, *L/A, *H.H, *H́, *X.X
• Set 5: *H/A, *Á, *L/O, *L/I, *A, *O, *I, *L, with internal rankings *L/O ≫ *L/I and *A ≫ *O ≫ *I (setFiveInner)

Sets 3 and 4 — the "intermediary constraint sets" of eq. (49) — are internally unranked: "While mutually ranked, the sets are internally random" (page 21), so each evaluation samples a total order.

Substrate consumption

Each motif's probability is winProb over finnishGrammar — uniform sampling of the total rankings consistent with the whole grammar, not a per-stratum sub-grammar. The substrate's deciding-stratum theorem (winProb_stratified_binary_rate) reduces each competition to the closed form |favoring ∩ Dₖ| / |Dₖ| over the deciding stratum's active set — the paper's own shortcut ("Drawing the tableaux was in fact unnecessary … knowing that the weak variant violates one constraint (*L.L) while the strong variant violates two (*H/I, *Í) gives us the result directly", page 22) — with the irrelevance of the lower strata a theorem rather than an aside.

Violation profiles are stipulated from table (52) rather than derived from Constraint instances: the paper's quantitative section works directly at violation-profile granularity. True Constraint formalisations would need a Finnish syllable substrate (stress / weight / sonority features feeding syllable structure) which doesn't yet exist in linglib. Sets 1–2 tie on every motif (the stress constraints are inactive on these long-stem competitions, witnessed by table (52) carrying only Set 3 and Set 4 columns); Set-5 cells are set to 0 — the deciding-stratum theorem makes them provably irrelevant, so no Set-5 profile fidelity is claimed.

Predictions formalized

All six motif competitions of table (52) (page 22); observed 3-syllabic-stem frequencies from table (53) (page 23):

• 1ab (L.TÁA ∼ L.TA, ká.me.ròi.den ∼ ká.me.ro.jen): strong wins in all rankings. Observed: 99.4% / 0.6% (720 / 4 corpus tokens).
• 2ab (L.TÓO ∼ L.TO, hé.te.ròi.den ∼ hé.te.ro.jen): strong wins in all rankings. Observed: 99.5% / 0.5% (389 / 2).
• 3ab (L.TÍI ∼ L.TI, náa.pu.rèi.den ∼ náa.pu.ri.en): strong wins 1/3, weak 2/3. Observed: 36.9% / 63.1% (215 / 368).
• 4ab (H.TÁA ∼ H.TA, máa.il.mòi.den ∼ máa.il.mo.jen): each wins 1/2. Observed: 50.5% / 49.5% (46 / 45).
• 5ab (H.TÓO ∼ H.TO, kór.jaa.mòi.den ∼ kór.jaa.mo.jen): strong wins 1/5, weak 4/5. Observed: 17.8% / 82.2% (76 / 350).
• 6ab (H.TÍI ∼ H.TI, pó.lii.sèi.den ∼ pó.lii.si.en): strong loses in all rankings. Observed: 1.6% / 98.4% (13 / 806).

winProb_strong_add_weak verifies the two variants partition the probability mass for every motif (sum_winProb_eq_one substrate instance).

Out of scope

• The categorical short-stem patterns decided by the stress constraints of Sets 1–2 (mono- and disyllabic stems, the paper's §2.1 and §5.1–5.2).
• Observed-vs-predicted comparison theorems. Table (53)'s small gap between predicted and observed is empirical noise around the discrete prediction ("as the quantitative predictions of our model are discrete probabilities (1/2, 1/3, 1/5 etc.) it would be difficult to get any closer", page 23).

Variants and motifs

inductive Anttila1997.Variant : Type

The two genitive-plural variants: strong (heavy penult, final-syllable onset /t/ or /d/) vs weak (light penult, onset /j/ or absent) ([Ant97] ex. (1), page 3).

• strong : Variant
• weak : Variant

@[instance_reducible]

instance Anttila1997.instDecidableEqVariant : DecidableEq Variant

Equations

• Anttila1997.instDecidableEqVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anttila1997.instReprVariant : Repr Variant

Equations

• Anttila1997.instReprVariant = { reprPrec := Anttila1997.instReprVariant.repr }

def Anttila1997.instReprVariant.repr : Variant → ℕ → Std.Format

Equations

• Anttila1997.instReprVariant.repr Anttila1997.Variant.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Variant.strong")).group prec✝
• Anttila1997.instReprVariant.repr Anttila1997.Variant.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Variant.weak")).group prec✝

@[instance_reducible]

instance Anttila1997.instFintypeVariant : Fintype Variant

Equations

• Anttila1997.instFintypeVariant = { elems := { val := ↑Anttila1997.Variant.enumList, nodup := Anttila1997.Variant.enumList_nodup }, complete := Anttila1997.instFintypeVariant._proof_1 }

def Anttila1997.Variant.other : Variant → Variant

The opposite variant: strong ↔ weak.

Equations

• Anttila1997.Variant.strong.other = Anttila1997.Variant.weak
• Anttila1997.Variant.weak.other = Anttila1997.Variant.strong

theorem Anttila1997.Variant.ne_other (v : Variant) : v ≠ v.other

theorem Anttila1997.Variant.univ_eq_pair (v : Variant) : Finset.univ = {v, v.other}

Both variants compete for every input: the candidate set is the pair {v, v.other} for either choice of v.

inductive Anttila1997.Motif : Type

The six motif competitions of [Ant97] table (52): 1ab (L.TÁA ∼ L.TA), 2ab (L.TÓO ∼ L.TO), 3ab (L.TÍI ∼ L.TI), 4ab (H.TÁA ∼ H.TA), 5ab (H.TÓO ∼ H.TO), 6ab (H.TÍI ∼ H.TI).

• one : Motif
• two : Motif
• three : Motif
• four : Motif
• five : Motif
• six : Motif

@[instance_reducible]

instance Anttila1997.instDecidableEqMotif : DecidableEq Motif

Equations

• Anttila1997.instDecidableEqMotif x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anttila1997.instReprMotif : Repr Motif

Equations

• Anttila1997.instReprMotif = { reprPrec := Anttila1997.instReprMotif.repr }

def Anttila1997.instReprMotif.repr : Motif → ℕ → Std.Format

Equations

• Anttila1997.instReprMotif.repr Anttila1997.Motif.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.one")).group prec✝
• Anttila1997.instReprMotif.repr Anttila1997.Motif.two prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.two")).group prec✝
• Anttila1997.instReprMotif.repr Anttila1997.Motif.three prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.three")).group prec✝
• Anttila1997.instReprMotif.repr Anttila1997.Motif.four prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.four")).group prec✝
• Anttila1997.instReprMotif.repr Anttila1997.Motif.five prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.five")).group prec✝
• Anttila1997.instReprMotif.repr Anttila1997.Motif.six prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Motif.six")).group prec✝

@[instance_reducible]

instance Anttila1997.instFintypeMotif : Fintype Motif

Equations

• Anttila1997.instFintypeMotif = { elems := { val := ↑Anttila1997.Motif.enumList, nodup := Anttila1997.Motif.enumList_nodup }, complete := Anttila1997.instFintypeMotif._proof_1 }

The grammar for Finnish, final version

Constraint roster, in eq. (50)'s column order: 0 = *X́.X́ (Set 1); 1 = *Ĺ, 2 = *H (Set 2); 3 = *H/I, 4 = *Í, 5 = *L.L (Set 3); 6 = *H/O, 7 = *Ó, 8 = *L/A, 9 = *H.H, 10 = *H́, 11 = *X.X (Set 4); 12 = *H/A, 13 = *Á, 14 = *L/O, 15 = *L/I, 16 = *A, 17 = *O, 18 = *I, 19 = *L (Set 5).

def Anttila1997.stratumOf : Fin 20 → Fin 5

Stratum assignment: constraint c belongs to Set stratumOf c + 1 of [Ant97] eq. (50).

Equations

• Anttila1997.stratumOf = ![0, 1, 1, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4]

def Anttila1997.setFiveInner : Fin 20 → Fin 20 → Prop

The Set-5-internal rankings of [Ant97] eq. (50): *L/O ≫ *L/I (14 ≫ 15) and *A ≫ *O ≫ *I (16 ≫ 17 ≫ 18), transitively closed.

Equations

• Anttila1997.setFiveInner a b = (a = b ∨ (a, b) ∈ [(14, 15), (16, 17), (17, 18), (16, 18)])

@[instance_reducible]

instance Anttila1997.instDecidableRelFinOfNatNatSetFiveInner : DecidableRel setFiveInner

Equations

• Anttila1997.instDecidableRelFinOfNatNatSetFiveInner = id inferInstance

instance Anttila1997.instIsPartialOrderFinOfNatNatSetFiveInner : IsPartialOrder (Fin 20) setFiveInner

def Anttila1997.finnishGrammar : Fin 20 → Fin 20 → Prop

The grammar for Finnish, final version ([Ant97] eq. (50), page 21): five mutually-ranked strata, internally free except for setFiveInner's Set-5 rankings.

Equations

• Anttila1997.finnishGrammar = OptimalityTheory.stratified Anttila1997.stratumOf Anttila1997.setFiveInner

instance Anttila1997.instIsPartialOrderFinOfNatNatFinnishGrammar : IsPartialOrder (Fin 20) finnishGrammar

@[instance_reducible]

instance Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar : DecidableRel finnishGrammar

Equations

• Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar = Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar._aux_1

def Anttila1997.vp : Motif → Variant → Fin 20 → ℕ

Violation profile over the full constraint roster, from [Ant97] table (52). Sets 1–2 tie on every motif and Set-5 cells are 0 (provably irrelevant; see module docstring).

Equations

• Anttila1997.vp Anttila1997.Motif.one Anttila1997.Variant.weak ⟨5, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.two Anttila1997.Variant.weak ⟨5, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.three Anttila1997.Variant.strong ⟨3, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.three Anttila1997.Variant.strong ⟨4, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.three Anttila1997.Variant.weak ⟨5, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.four Anttila1997.Variant.strong ⟨9, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.four Anttila1997.Variant.strong ⟨10, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.four Anttila1997.Variant.weak ⟨8, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.four Anttila1997.Variant.weak ⟨11, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.five Anttila1997.Variant.strong ⟨6, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.five Anttila1997.Variant.strong ⟨7, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.five Anttila1997.Variant.strong ⟨9, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.five Anttila1997.Variant.strong ⟨10, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.five Anttila1997.Variant.weak ⟨11, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.six Anttila1997.Variant.strong ⟨3, isLt⟩ = 1
• Anttila1997.vp Anttila1997.Motif.six Anttila1997.Variant.strong ⟨4, isLt⟩ = 1
• Anttila1997.vp x✝² x✝¹ x✝ = 0

def Anttila1997.winProb (m : Motif) (v : Variant) : ℚ

Probability that variant v wins motif m under uniform sampling of the total rankings consistent with finnishGrammar.

Equations

• Anttila1997.winProb m v = OptimalityTheory.winProb (fun (x : Anttila1997.Motif) => Finset.univ) Anttila1997.vp Anttila1997.finnishGrammar m v

Rate theorems — table (52), all six motifs

theorem Anttila1997.strongProb_1ab : winProb Motif.one Variant.strong = 1

Motif 1ab strong L.TÁA wins in all rankings — only the weak variant violates a deciding-stratum constraint (*L.L), so D = Y = {5} and the rate is 1: the categorical limiting case.

theorem Anttila1997.weakProb_1ab : winProb Motif.one Variant.weak = 0

Motif 1ab weak L.TA loses in all rankings ([Ant97] table (53): observed 0.6%, an artefact of the spelling of /kollega/).

theorem Anttila1997.strongProb_2ab : winProb Motif.two Variant.strong = 1

Motif 2ab strong L.TÓO wins in all rankings — same Set-3 profile as motif 1ab.

theorem Anttila1997.weakProb_2ab : winProb Motif.two Variant.weak = 0

Motif 2ab weak L.TO loses in all rankings.

theorem Anttila1997.strongProb_3ab : winProb Motif.three Variant.strong = 1 / 3

Motif 3ab strong L.TÍI wins 1/3 of rankings: decided in Set 3 with D = {*H/I, *Í, *L.L}, Y = {*L.L} (violated by weak alone). Observed 36.9% for náa.pu.rèi.den ([Ant97] table (53), row 3a).

theorem Anttila1997.weakProb_3ab : winProb Motif.three Variant.weak = 2 / 3

Motif 3ab weak L.TI wins 2/3 of rankings: Y = {*H/I, *Í} (violated by strong alone). Observed 63.1% for náa.pu.ri.en ([Ant97] table (53), row 3b).

theorem Anttila1997.strongProb_4ab : winProb Motif.four Variant.strong = 1 / 2

Motif 4ab strong H.TÁA wins 1/2 of rankings: decided in Set 4 with D = {*L/A, *H.H, *H́, *X.X}, Y = {*L/A, *X.X} (violated by weak alone). Observed 50.5% for máa.il.mòi.den ([Ant97] table (53), row 4a).

theorem Anttila1997.weakProb_4ab : winProb Motif.four Variant.weak = 1 / 2

Motif 4ab weak H.TA wins 1/2 of rankings: Y = {*H.H, *H́}. Observed 49.5% for máa.il.mo.jen ([Ant97] table (53), row 4b).

theorem Anttila1997.strongProb_5ab : winProb Motif.five Variant.strong = 1 / 5

Motif 5ab strong H.TÓO wins 1/5 of rankings: decided in Set 4 with D = {*H/O, *Ó, *H.H, *H́, *X.X}, Y = {*X.X} (violated by weak alone). Observed 17.8% for kór.jaa.mòi.den ([Ant97] table (53), row 5a).

theorem Anttila1997.weakProb_5ab : winProb Motif.five Variant.weak = 4 / 5

Motif 5ab weak H.TO wins 4/5 of rankings: Y = {*H/O, *Ó, *H.H, *H́}. Observed 82.2% for kór.jaa.mo.jen ([Ant97] table (53), row 5b).

theorem Anttila1997.strongProb_6ab : winProb Motif.six Variant.strong = 0

Motif 6ab strong H.TÍI loses in all rankings — only the strong variant violates deciding-stratum constraints (*H/I, *Í), so Y = ∅.

theorem Anttila1997.weakProb_6ab : winProb Motif.six Variant.weak = 1

Motif 6ab weak H.TI wins in all rankings ([Ant97] table (53): observed 98.4%).

Completeness

theorem Anttila1997.winProb_strong_add_weak (m : Motif) : winProb m Variant.strong + winProb m Variant.weak = 1

Every ranking of finnishGrammar picks a winner for every motif: the two variants' probabilities sum to 1 (sum_winProb_eq_one instance).