Anttila 1997: deriving variation from grammar

Finnish genitive plurals come in a strong variant (heavy penult, naa.pu.rei.den) and a weak one (light penult, naa.pu.ri.en). Stems of one or two syllables choose categorically, longer CV-final stems vary, and the variation is biased by the stem-final vowel and by the weight of the antepenult. One partially ordered grammar covers all of it. Its constraints are the harmonic alignments of stress, weight, and sonority together with bans on adjacent syllables of equal stress or weight; Finnish stratifies them by promoting No Clash and the two stress–weight mismatches above the rest. Every total ranking consistent with the grammar picks a winner, and a variant's probability is the share of rankings under which it wins. The stress constraints decide short stems and stems with a heavy antepenult outright; where they tie, secondary stress being optional, the two internally unranked intermediate sets resolve the competition at rates that the corpus frequencies track.

Item and page numbers follow the ROA-63 manuscript.

Main definitions

• Syllable, Constraint: syllables as stress, weight, and nuclear sonority, and the twenty constraints of (50), with Constraint.violations counting on a syllable string.
• finnishGrammar: the strata of (50) refined by the universal rankings (28).
• Shape.cands: the candidate sets of the categorical tableaux; word: the trisyllabic candidates of (52) by motif; wins: the rankings under which a variant wins its motif.
• predicted: the result column of (52), as the paper's fraction of rankings.

References

• [Ant97]
• [PS93] — harmonic alignment
• [TS95] — stratified domination hierarchies
• [Kip93] — partial ranking as a source of quantitative predictions

Syllable prominence (25)

inductive Anttila1997.Sonority : Type

Nuclear sonority, ordered i < o < a.

• i : Sonority
• o : Sonority
• a : Sonority

@[instance_reducible]

instance Anttila1997.instDecidableEqSonority : DecidableEq Sonority

Equations

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

def Anttila1997.instReprSonority.repr : Sonority → ℕ → Std.Format

Equations

• Anttila1997.instReprSonority.repr Anttila1997.Sonority.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Sonority.i")).group prec✝
• Anttila1997.instReprSonority.repr Anttila1997.Sonority.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Sonority.o")).group prec✝
• Anttila1997.instReprSonority.repr Anttila1997.Sonority.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Sonority.a")).group prec✝

@[instance_reducible]

instance Anttila1997.instReprSonority : Repr Sonority

Equations

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

@[instance_reducible]

instance Anttila1997.instFintypeSonority : Fintype Sonority

Equations

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

def Anttila1997.Sonority.rank : Sonority → Fin 3

Position on the sonority hierarchy.

Equations

• Anttila1997.Sonority.i.rank = 0
• Anttila1997.Sonority.o.rank = 1
• Anttila1997.Sonority.a.rank = 2

@[instance_reducible]

instance Anttila1997.instLinearOrderSonority : LinearOrder Sonority

Equations

• Anttila1997.instLinearOrderSonority = LinearOrder.lift' Anttila1997.Sonority.rank Anttila1997.instLinearOrderSonority._proof_1

inductive Anttila1997.Weight : Type

Syllable weight.

• light : Weight
• heavy : Weight

@[instance_reducible]

instance Anttila1997.instDecidableEqWeight : DecidableEq Weight

Equations

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

def Anttila1997.instReprWeight.repr : Weight → ℕ → Std.Format

Equations

• Anttila1997.instReprWeight.repr Anttila1997.Weight.light prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Weight.light")).group prec✝
• Anttila1997.instReprWeight.repr Anttila1997.Weight.heavy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Weight.heavy")).group prec✝

@[instance_reducible]

instance Anttila1997.instReprWeight : Repr Weight

Equations

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

@[instance_reducible]

instance Anttila1997.instFintypeWeight : Fintype Weight

Equations

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

def Anttila1997.Weight.prominent : Weight → Bool

Whether a weight is the prominent value of its scale, the one stress aligns with.

Equations

• Anttila1997.Weight.heavy.prominent = true
• Anttila1997.Weight.light.prominent = false

structure Anttila1997.Syllable : Type

A syllable of a candidate: its stress, and its weight and nuclear sonority where the tableau specifies them (X leaves both open).

• stressed : Bool
• weight : Option Weight
• nucleus : Option Sonority

@[instance_reducible]

instance Anttila1997.instDecidableEqSyllable : DecidableEq Syllable

Equations

• Anttila1997.instDecidableEqSyllable = Anttila1997.instDecidableEqSyllable.decEq

def Anttila1997.instDecidableEqSyllable.decEq (x✝ x✝¹ : Syllable) : Decidable (x✝ = x✝¹)

Equations

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

def Anttila1997.instReprSyllable.repr : Syllable → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Anttila1997.instReprSyllable : Repr Syllable

Equations

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

inductive Anttila1997.Constraint : Type

The constraints of (50): a starred stress–weight, weight–sonority, or stress–sonority combination within a syllable (28), or a starred adjacency of equal stress or weight (29).

• stressWeight (stressed : Bool) (w : Weight) : Constraint
• weightSonority (w : Weight) (s : Sonority) : Constraint
• stressSonority (stressed : Bool) (s : Sonority) : Constraint
• clash (stressed : Bool) : Constraint
• collision (w : Weight) : Constraint

def Anttila1997.instDecidableEqConstraint.decEq (x✝ x✝¹ : Constraint) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressWeight stressed w) (Anttila1997.Constraint.weightSonority w_1 s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressWeight stressed w) (Anttila1997.Constraint.stressSonority stressed_1 s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressWeight stressed w) (Anttila1997.Constraint.clash stressed_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressWeight stressed w) (Anttila1997.Constraint.collision w_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.weightSonority w s) (Anttila1997.Constraint.stressWeight stressed w_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.weightSonority w s) (Anttila1997.Constraint.stressSonority stressed s_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.weightSonority w s) (Anttila1997.Constraint.clash stressed) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.weightSonority w s) (Anttila1997.Constraint.collision w_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressSonority stressed s) (Anttila1997.Constraint.stressWeight stressed_1 w) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressSonority stressed s) (Anttila1997.Constraint.weightSonority w s_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressSonority stressed s) (Anttila1997.Constraint.clash stressed_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.stressSonority stressed s) (Anttila1997.Constraint.collision w) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.clash stressed) (Anttila1997.Constraint.stressWeight stressed_1 w) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.clash stressed) (Anttila1997.Constraint.weightSonority w s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.clash stressed) (Anttila1997.Constraint.stressSonority stressed_1 s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.clash a) (Anttila1997.Constraint.clash b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.clash stressed) (Anttila1997.Constraint.collision w) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.collision w) (Anttila1997.Constraint.stressWeight stressed w_1) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.collision w) (Anttila1997.Constraint.weightSonority w_1 s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.collision w) (Anttila1997.Constraint.stressSonority stressed s) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.collision w) (Anttila1997.Constraint.clash stressed) = isFalse ⋯
• Anttila1997.instDecidableEqConstraint.decEq (Anttila1997.Constraint.collision a) (Anttila1997.Constraint.collision b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anttila1997.instDecidableEqConstraint : DecidableEq Constraint

Equations

• Anttila1997.instDecidableEqConstraint = Anttila1997.instDecidableEqConstraint.decEq

@[instance_reducible]

instance Anttila1997.instReprConstraint : Repr Constraint

Equations

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

def Anttila1997.instReprConstraint.repr : Constraint → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Anttila1997.instFintypeConstraint : Fintype Constraint

Equations

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

def Anttila1997.Constraint.violations : Constraint → List Syllable → ℕ

Violations on a syllable string: the syllables showing the starred combination, or the adjacent pairs sharing the starred value.

Equations

• One or more equations did not get rendered due to their size.
• (Anttila1997.Constraint.stressWeight st w).violations x✝ = List.countP (fun (σ : Anttila1997.Syllable) => decide (σ.stressed = st ∧ σ.weight = some w)) x✝
• (Anttila1997.Constraint.weightSonority w s).violations x✝ = List.countP (fun (σ : Anttila1997.Syllable) => decide (σ.weight = some w ∧ σ.nucleus = some s)) x✝
• (Anttila1997.Constraint.stressSonority st s).violations x✝ = List.countP (fun (σ : Anttila1997.Syllable) => decide (σ.stressed = st ∧ σ.nucleus = some s)) x✝
• (Anttila1997.Constraint.clash st).violations x✝ = List.countP (fun (p : Anttila1997.Syllable × Anttila1997.Syllable) => decide (p.1.stressed = st ∧ p.2.stressed = st)) (x✝.zip x✝.tail)

The grammar for Finnish (28), (50)

def Anttila1997.alignedAbove (prominent : Bool) (s s' : Sonority) : Prop

Harmonic alignment (27) of sonority with a binary scale: on the scale's prominent value the constraint against the less sonorous nucleus ranks higher; on the other value, the more.

Equations

• Anttila1997.alignedAbove prominent s s' = if prominent = true then s < s' else s' < s

@[instance_reducible]

instance Anttila1997.instDecidableAlignedAbove (p : Bool) (s s' : Sonority) : Decidable (alignedAbove p s s')

Equations

• Anttila1997.instDecidableAlignedAbove p s s' = id inferInstance

def Anttila1997.Universal : Constraint → Constraint → Prop

The universal rankings (28): the stress–weight mismatches outrank the matches, and sonority aligns with weight and with stress.

Equations

• Anttila1997.Universal (Anttila1997.Constraint.stressWeight st w) (Anttila1997.Constraint.stressWeight st' w') = (st ≠ w.prominent ∧ st' = w'.prominent)
• Anttila1997.Universal (Anttila1997.Constraint.weightSonority w s) (Anttila1997.Constraint.weightSonority w' s') = (w = w' ∧ Anttila1997.alignedAbove w.prominent s s')
• Anttila1997.Universal (Anttila1997.Constraint.stressSonority st s) (Anttila1997.Constraint.stressSonority st' s') = (st = st' ∧ Anttila1997.alignedAbove st s s')
• Anttila1997.Universal x✝¹ x✝ = False

@[instance_reducible]

instance Anttila1997.instDecidableRelConstraintUniversal : DecidableRel Universal

Equations

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

theorem Anttila1997.alignedAbove_trans {p : Bool} {s₁ s₂ s₃ : Sonority} (h : alignedAbove p s₁ s₂) (h' : alignedAbove p s₂ s₃) : alignedAbove p s₁ s₃

theorem Anttila1997.alignedAbove_asymm {p : Bool} {s s' : Sonority} (h : alignedAbove p s s') (h' : alignedAbove p s' s) : False

theorem Anttila1997.Universal.trans {a b c : Constraint} (hab : Universal a b) (hbc : Universal b c) : Universal a c

theorem Anttila1997.Universal.asymm {a b : Constraint} (hab : Universal a b) (hba : Universal b a) : False

def Anttila1997.Constraint.set : Constraint → Fin 5

The strata of (50): No Clash; the two stress–weight mismatches; the intermediary sets (49); the rest.

Equations

• (Anttila1997.Constraint.clash true).set = 0
• (Anttila1997.Constraint.stressWeight true Anttila1997.Weight.light).set = 1
• (Anttila1997.Constraint.stressWeight false Anttila1997.Weight.heavy).set = 1
• (Anttila1997.Constraint.weightSonority Anttila1997.Weight.heavy Anttila1997.Sonority.i).set = 2
• (Anttila1997.Constraint.stressSonority true Anttila1997.Sonority.i).set = 2
• (Anttila1997.Constraint.collision Anttila1997.Weight.light).set = 2
• (Anttila1997.Constraint.weightSonority Anttila1997.Weight.heavy Anttila1997.Sonority.o).set = 3
• (Anttila1997.Constraint.stressSonority true Anttila1997.Sonority.o).set = 3
• (Anttila1997.Constraint.weightSonority Anttila1997.Weight.light Anttila1997.Sonority.a).set = 3
• (Anttila1997.Constraint.collision Anttila1997.Weight.heavy).set = 3
• (Anttila1997.Constraint.stressWeight true Anttila1997.Weight.heavy).set = 3
• (Anttila1997.Constraint.clash false).set = 3
• x✝.set = 4

theorem Anttila1997.set_mono (a b : Constraint) : Universal a b → a.set ≤ b.set

Finnish only adds rankings to (28): no universal ranking is reversed across strata.

def Anttila1997.constraint : Fin 20 → Constraint

The roster in the column order of (50).

Equations

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

def Anttila1997.stratumOf (c : Fin 20) : Fin 5

Stratum of a roster position.

Equations

• Anttila1997.stratumOf c = (Anttila1997.constraint c).set

def Anttila1997.universalOn (a b : Fin 20) : Prop

The universal rankings on the roster, reflexively.

Equations

• Anttila1997.universalOn a b = (a = b ∨ Anttila1997.Universal (Anttila1997.constraint a) (Anttila1997.constraint b))

@[instance_reducible]

instance Anttila1997.instDecidableRelFinOfNatNatUniversalOn : DecidableRel universalOn

Equations

• Anttila1997.instDecidableRelFinOfNatNatUniversalOn a b = id inferInstance

instance Anttila1997.instIsPartialOrderFinOfNatNatUniversalOn : IsPartialOrder (Fin 20) universalOn

theorem Anttila1997.set_eq_of_universal (a b : Constraint) : Universal a b → a.set = b.set → a.set = 4

Only Set 5 ranks constraints internally.

theorem Anttila1997.stratum_triv {k : Fin 5} (hk : k ≠ 4) (a b : Fin 20) : stratumOf a = k → stratumOf b = k → universalOn a b → a = b

Below Set 5 the inner order is trivial.

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

The grammar for Finnish, final version (50).

Equations

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

instance Anttila1997.instIsPartialOrderFinOfNatNatFinnishGrammar : IsPartialOrder (Fin 20) finnishGrammar

@[instance_reducible]

instance Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar : DecidableRel finnishGrammar

Equations

• Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar = Anttila1997.instDecidableRelFinOfNatNatFinnishGrammar._aux_1

Categorical predictions (§5.1)

def Anttila1997.X' : Syllable

Tableau syllables: stressed or unstressed, of unspecified, heavy, or light weight.

Equations

• Anttila1997.X' = { stressed := true }

def Anttila1997.X : Syllable

Equations

• Anttila1997.X = { stressed := false }

def Anttila1997.H' : Syllable

Equations

• Anttila1997.H' = { stressed := true, weight := some Anttila1997.Weight.heavy }

def Anttila1997.H : Syllable

Equations

• Anttila1997.H = { stressed := false, weight := some Anttila1997.Weight.heavy }

def Anttila1997.L' : Syllable

Equations

• Anttila1997.L' = { stressed := true, weight := some Anttila1997.Weight.light }

def Anttila1997.L : Syllable

Equations

• Anttila1997.L = { stressed := false, weight := some Anttila1997.Weight.light }

inductive Anttila1997.Shape : Type

The stem shapes of the categorical tableaux, by their examples: (33) maa, (35) kala, (37) maailma, (39) ministeri, (40) margariini, (42) Aleksanteri, (43) koordinaatisto, (44) italiaano.

• maa : Shape
• kala : Shape
• maailma : Shape
• ministeri : Shape
• margariini : Shape
• aleksanteri : Shape
• koordinaatisto : Shape
• italiaano : Shape

@[instance_reducible]

instance Anttila1997.instDecidableEqShape : DecidableEq Shape

Equations

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

def Anttila1997.instReprShape.repr : Shape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Anttila1997.instReprShape.repr Anttila1997.Shape.maa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Shape.maa")).group prec✝
• Anttila1997.instReprShape.repr Anttila1997.Shape.kala prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Shape.kala")).group prec✝
• Anttila1997.instReprShape.repr Anttila1997.Shape.maailma prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Shape.maailma")).group prec✝
• Anttila1997.instReprShape.repr Anttila1997.Shape.ministeri prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Shape.ministeri")).group prec✝
• Anttila1997.instReprShape.repr Anttila1997.Shape.italiaano prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anttila1997.Shape.italiaano")).group prec✝

@[instance_reducible]

instance Anttila1997.instReprShape : Repr Shape

Equations

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

@[instance_reducible]

instance Anttila1997.instFintypeShape : Fintype Shape

Equations

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

def Anttila1997.Shape.cands : Shape → Finset (List Syllable)

The candidates of the tableaux (32), (34), (36), (38), (41): the weak variant, the strong one, and after a heavy antepenult the strong one with its stress shifted.

Equations

• One or more equations did not get rendered due to their size.
• Anttila1997.Shape.maa.cands = {[Anttila1997.H', Anttila1997.H], [Anttila1997.L', Anttila1997.H]}
• Anttila1997.Shape.kala.cands = {[Anttila1997.X', Anttila1997.L, Anttila1997.H], [Anttila1997.X', Anttila1997.H, Anttila1997.H]}
• Anttila1997.Shape.maailma.cands = {[Anttila1997.X', Anttila1997.X, Anttila1997.H', Anttila1997.H], [Anttila1997.X', Anttila1997.X, Anttila1997.L, Anttila1997.H]}
• Anttila1997.Shape.ministeri.cands = {[Anttila1997.X', Anttila1997.X, Anttila1997.L, Anttila1997.L, Anttila1997.H], [Anttila1997.X', Anttila1997.X, Anttila1997.L, Anttila1997.H', Anttila1997.H]}

def Anttila1997.tableauCon : OptimalityTheory.ConstraintSet (Shape × List Syllable) (Fin 20)

The roster's constraints on the candidates of a shape's tableau.

Equations

• Anttila1997.tableauCon c x = (Anttila1997.constraint c).violations x.2

def Anttila1997.rankings : Finset (OptimalityTheory.Ranking (Fin 20) 20)

The total rankings consistent with the Finnish grammar.

Equations

• Anttila1997.rankings = OptimalityTheory.consistentTotalOrders Anttila1997.finnishGrammar

def Anttila1997.Shape.Categorical (s : Shape) (cand : List Syllable) : Prop

A tableau candidate that every consistent ranking picks.

Equations

• s.Categorical cand = ∀ σ ∈ Anttila1997.rankings, OptimalityTheory.PicksAt Anttila1997.Shape.cands Anttila1997.tableauCon σ s cand

theorem Anttila1997.maa_strong : Shape.maa.Categorical [H', H]

Monosyllabic stems take the strong variant (32): mai.den, not ma.jen (33).

theorem Anttila1997.kala_weak : Shape.kala.Categorical [X', L, H]

Disyllabic CV-final stems take the weak variant (34): ka.lo.jen, not ka.loi.den (35).

theorem Anttila1997.margariini_weak : Shape.margariini.Categorical [X', X, H', L, H]

A heavy antepenult in a 4-syllabic stem is stressed and forces a light penult (38): mar.ga.rii.ni.en only (40).

theorem Anttila1997.italiaano_weak : Shape.italiaano.Categorical [X', X, L, H', L, H]

A light ante-antepenult before a heavy antepenult likewise (41): i.ta.li.aa.no.jen only (44).

theorem Anttila1997.stress_tie (s : Shape) : s ∈ [Shape.maailma, Shape.ministeri, Shape.aleksanteri, Shape.koordinaatisto] → ∀ o ∈ s.cands, ∀ o' ∈ s.cands, ∀ (c : Fin 20), stratumOf c ≤ 1 → tableauCon c (s, o) = tableauCon c (s, o')

After a light antepenult, or a heavy one following a heavy ante-antepenult, the stress constraints tie (36), (38), (41): secondary stress is optional, and both variants survive Sets 1 and 2.

Quantitative predictions (§5.3)

inductive Anttila1997.Variant : Type

The two genitive-plural variants (1).

• 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 other variant.

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}

@[reducible, inline]

abbrev Anttila1997.Motif : Type

A motif of (52): the antepenult's weight and the stem-final vowel.

Equations

• Anttila1997.Motif = (Anttila1997.Weight × Anttila1997.Sonority)

def Anttila1997.penult : Variant → Sonority → Syllable

The penult of a variant with nucleus s: stressed and heavy, or unstressed and light.

Equations

• Anttila1997.penult Anttila1997.Variant.strong x✝ = { stressed := true, weight := some Anttila1997.Weight.heavy, nucleus := some x✝ }
• Anttila1997.penult Anttila1997.Variant.weak x✝ = { stressed := false, weight := some Anttila1997.Weight.light, nucleus := some x✝ }

def Anttila1997.word : Motif → Variant → List Syllable

A trisyllabic candidate of (52): initial stress, an unstressed antepenult of the motif's weight, the variant's penult, and an unstressed heavy final.

Equations

• Anttila1997.word (w, s) x✝ = [Anttila1997.X', { stressed := false, weight := some w }, Anttila1997.penult x✝ s, Anttila1997.H]

def Anttila1997.con : OptimalityTheory.ConstraintSet (Motif × Variant) (Fin 20)

The roster's constraints on the variants of a motif.

Equations

• Anttila1997.con c x = (Anttila1997.constraint c).violations (Anttila1997.word x.1 x.2)

def Anttila1997.wins (m : Motif) (v : Variant) : Finset (OptimalityTheory.Ranking (Fin 20) 20)

The rankings under which variant v wins motif m.

Equations

• Anttila1997.wins m v = {σ ∈ Anttila1997.rankings | OptimalityTheory.PicksAt (fun (x : Anttila1997.Motif) => Finset.univ) Anttila1997.con σ m v}

theorem Anttila1997.card_wins_mul (m : Motif) (v : Variant) (k : Fin 5) (h_triv : ∀ (a b : Fin 20), stratumOf a = k → stratumOf b = k → universalOn a b → a = b) (h_tie : ∀ (c : Fin 20), stratumOf c < k → con c (m, v) = con c (m, v.other)) (h_dec : {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}.Nonempty) : (wins m v).card * {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}.card = rankings.card * (OptimalityTheory.favoring con m v v.other ∩ {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}).card

The deciding-stratum count: once the strata above k tie, the rankings won by v stand to all rankings as stratum k's constraints favoring v stand to its active ones.

theorem Anttila1997.card_wins_of_counts (m : Motif) (v : Variant) (k : Fin 5) (n t : ℕ) (h_triv : ∀ (a b : Fin 20), stratumOf a = k → stratumOf b = k → universalOn a b → a = b) (h_tie : ∀ (c : Fin 20), stratumOf c < k → con c (m, v) = con c (m, v.other)) (h_dec : {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}.Nonempty) (hn : (OptimalityTheory.favoring con m v v.other ∩ {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}).card = n) (ht : {x ∈ OptimalityTheory.active con m v v.other | stratumOf x = k}.card = t) : (wins m v).card * t = rankings.card * n

card_wins_mul with the two counts evaluated.

def Anttila1997.predictedStrong : Motif → ℕ × ℕ

The result column of (52) for the strong variant: its share of the rankings, as the paper's fraction.

Equations

• Anttila1997.predictedStrong (Anttila1997.Weight.light, Anttila1997.Sonority.i) = (1, 3)
• Anttila1997.predictedStrong (Anttila1997.Weight.light, snd) = (1, 1)
• Anttila1997.predictedStrong (Anttila1997.Weight.heavy, Anttila1997.Sonority.a) = (1, 2)
• Anttila1997.predictedStrong (Anttila1997.Weight.heavy, Anttila1997.Sonority.o) = (1, 5)
• Anttila1997.predictedStrong (Anttila1997.Weight.heavy, Anttila1997.Sonority.i) = (0, 1)

def Anttila1997.predicted (m : Motif) : Variant → ℕ × ℕ

The result column of (52).

Equations

• Anttila1997.predicted m Anttila1997.Variant.strong = Anttila1997.predictedStrong m
• Anttila1997.predicted m Anttila1997.Variant.weak = ((Anttila1997.predictedStrong m).2 - (Anttila1997.predictedStrong m).1, (Anttila1997.predictedStrong m).2)

theorem Anttila1997.card_wins_strong_of {m : Motif} {n t : ℕ} (hp : predictedStrong m = (n, t)) (h : (wins m Variant.strong).card * t = rankings.card * n) : (wins m Variant.strong).card * (predictedStrong m).2 = rankings.card * (predictedStrong m).1

A motif's strong share, from the counts behind the paper's fraction.

theorem Anttila1997.card_wins_strong (m : Motif) : (wins m Variant.strong).card * (predictedStrong m).2 = rankings.card * (predictedStrong m).1

The shares of (52): decided in Set 3 after a light antepenult and for h.tii, in Set 4 for h.taa and h.too; the strata below never matter.

theorem Anttila1997.card_wins_add (m : Motif) : (wins m Variant.strong).card + (wins m Variant.weak).card = rankings.card

Every consistent ranking picks one of the two variants.

theorem Anttila1997.predictedStrong_le (m : Motif) : (predictedStrong m).1 ≤ (predictedStrong m).2

theorem Anttila1997.card_wins_weak {m : Motif} (h : (wins m Variant.strong).card * (predictedStrong m).2 = rankings.card * (predictedStrong m).1) : (wins m Variant.weak).card * (predicted m Variant.weak).2 = rankings.card * (predicted m Variant.weak).1

The weak variant's share is the complement of the strong one's.

theorem Anttila1997.card_wins (m : Motif) (v : Variant) : (wins m v).card * (predicted m v).2 = rankings.card * (predicted m v).1

Each variant wins the share of rankings (52) predicts.

The paper's data

def Anttila1997.Weight.ofChar? : Char → Option Weight

Antepenult weight from a motif label.

Equations

• Anttila1997.Weight.ofChar? 'l' = some Anttila1997.Weight.light
• Anttila1997.Weight.ofChar? 'h' = some Anttila1997.Weight.heavy
• Anttila1997.Weight.ofChar? x✝ = none

def Anttila1997.Sonority.ofChar? : Char → Option Sonority

Stem-final vowel from a motif label.

Equations

• Anttila1997.Sonority.ofChar? 'a' = some Anttila1997.Sonority.a
• Anttila1997.Sonority.ofChar? 'o' = some Anttila1997.Sonority.o
• Anttila1997.Sonority.ofChar? 'i' = some Anttila1997.Sonority.i
• Anttila1997.Sonority.ofChar? x✝ = none

def Anttila1997.Motif.parse? (s : String) : Option (Motif × Variant)

A motif label of (52)–(53): antepenult weight, t, and the stem-final vowel, doubled for the strong variant.

Equations

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

def Anttila1997.digits (l : List Char) : ℕ

The value of a digit string.

Equations

• Anttila1997.digits l = List.foldl (fun (n : ℕ) (c : Char) => 10 * n + (c.toNat - '0'.toNat)) 0 l

def Anttila1997.percent? (s : String) : Option ℕ

A printed whole percentage.

Equations

• Anttila1997.percent? s = if s.toList.all Char.isDigit = true then some (Anttila1997.digits s.toList) else none

def Anttila1997.tenths? (s : String) : Option ℕ

A printed percentage in tenths: 99.4 as 994, 100 as 1000.

Equations

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

theorem Anttila1997.rows_predicted (r : Datum) : r ∈ Examples.all → r.feature? "syllables" = some "3" → ∀ mv ∈ (r.feature? "motif" >>= Motif.parse?).toList, ∀ p ∈ (r.feature? "pred_pct" >>= percent?).toList, 2 * p * (predicted mv.1 mv.2).2 ≤ 200 * (predicted mv.1 mv.2).1 + (predicted mv.1 mv.2).2 ∧ 200 * (predicted mv.1 mv.2).1 ≤ (2 * p + 1) * (predicted mv.1 mv.2).2

Table (53): the paper's predicted percentage is the share of (52) to the nearest percent.

theorem Anttila1997.rows_frequency (r : Datum) : r ∈ Examples.all → r.feature? "syllables" = some "3" → ∀ mv ∈ (r.feature? "motif" >>= Motif.parse?).toList, ∀ q ∈ (r.feature? "obs_pct" >>= tenths?).toList, ((predicted mv.1 mv.2).2 < 2 * (predicted mv.1 mv.2).1 → 500 < q) ∧ (2 * (predicted mv.1 mv.2).1 < (predicted mv.1 mv.2).2 → q < 500)

Tables (48) and (53): the variant the grammar favors is the more frequent one.