Heinz and Lai (2013): Vowel harmony and subsequentiality

Heinz and Lai place iterative vowel harmony in the subsequential hierarchy. Over the alphabet of §3, harmonizing vowels + and −, an inert class C of consonants and transparent vowels, and opaque vowels ⊞ and ⊟, progressive harmony is computed left to right by the sequential transducer of Figure 2, and regressive harmony by the same transducer run right to left. Sour grapes harmony (8) is not left-subsequential (Theorem 5), and dominant–recessive harmony (9) is subsequential in neither direction (Theorem 6), but it is weakly deterministic in the sense of their Definition 1 (Theorem 7): progressive spreading of + alone, Figure 4, run left to right and then right to left.

Main definitions

• Seg: the alphabet of §3
• ph: progressive harmony, the transducer of Figure 2
• IsSourGrapes, IsDominantRecessive: the conditions (8) and (9)
• php: progressive spreading of + alone, the transducer of Figure 4

Main results

• not_isLeftSubsequential_of_isSourGrapes: Theorem 5
• exists_isRightSubsequential_isSourGrapes, not_isRightSubsequential_of_isSourGrapes: the right half of Theorem 5 fails for (8) alone and holds once trigger-less words are left alone
• not_isSubsequential_of_isDominantRecessive: Theorem 6
• isDominantRecessive_php, isWeaklyDeterministic_php: Theorem 7

Implementation notes

• The proof of Theorem 5 goes through the bounded delay of left-subsequential functions rather than the paper's sets of tails. The paper omits the right half as similar; it needs more than (8), since a right-to-left pass that raises every − unless the word ends in ⊟ meets (8).
• Theorem 7 is stated, as in the paper, for words over + and −.
• Not formalized: Theorem 4 (majority rules is not regular), the stem-control results (Theorems 8 and 9), and the conjecture that sour grapes is not weakly deterministic.

References

• [HL13]

inductive HeinzLai2013.Seg : Type

A symbol of the alphabet of §3 is a harmonizing vowel + or −, the inert class C, or an opaque vowel ⊞ or ⊟.

• plus : Seg
• minus : Seg
• inert : Seg
• opaquePlus : Seg
• opaqueMinus : Seg

@[instance_reducible]

instance HeinzLai2013.instDecidableEqSeg : DecidableEq Seg

Equations

• HeinzLai2013.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HeinzLai2013.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HeinzLai2013.instReprSeg.repr HeinzLai2013.Seg.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeinzLai2013.Seg.plus")).group prec✝
• HeinzLai2013.instReprSeg.repr HeinzLai2013.Seg.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeinzLai2013.Seg.minus")).group prec✝
• HeinzLai2013.instReprSeg.repr HeinzLai2013.Seg.inert prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeinzLai2013.Seg.inert")).group prec✝
• HeinzLai2013.instReprSeg.repr HeinzLai2013.Seg.opaquePlus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HeinzLai2013.Seg.opaquePlus")).group prec✝

@[instance_reducible]

instance HeinzLai2013.instReprSeg : Repr Seg

Equations

• HeinzLai2013.instReprSeg = { reprPrec := HeinzLai2013.instReprSeg.repr }

Progressive harmony

def HeinzLai2013.ph : Mealy (Option Bool) Seg Seg

Progressive harmony, Figure 2. The state is the value of the current harmonic domain, set by the first harmonizing vowel and reset by each opaque vowel; a harmonizing vowel takes that value. Run right to left, the same machine computes regressive harmony.

Equations

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

def HeinzLai2013.ofLetter : Char → Seg

ofLetter c is the class of the Turkish letter c. The vowels i and e are [−back], o and u are [+back], and everything else is inert.

Equations

• HeinzLai2013.ofLetter 'i' = HeinzLai2013.Seg.minus
• HeinzLai2013.ofLetter 'e' = HeinzLai2013.Seg.minus
• HeinzLai2013.ofLetter 'o' = HeinzLai2013.Seg.plus
• HeinzLai2013.ofLetter 'u' = HeinzLai2013.Seg.plus
• HeinzLai2013.ofLetter x✝ = HeinzLai2013.Seg.inert

def HeinzLai2013.ofAnalysis (a : Forms.Analysis) : List Seg × List Seg

ofAnalysis a is the underlying and the surface string of the word a analyses, read off its underlying form without the slashes and the morpheme boundary, and off its segments.

Equations

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

theorem HeinzLai2013.ph_forms (a : Forms.Analysis) : a ∈ Forms.analyses → ph.run (ofAnalysis a).1 = (ofAnalysis a).2

Progressive harmony takes the underlying form of each Turkish genitive of Table 2 to its surface form.

Sour grapes

def HeinzLai2013.IsSourGrapes (f : List Seg → List Seg) : Prop

f meets the sour-grapes condition (8). A trigger followed by −s spreads to all of them, and does not spread at all when an opaque ⊟ ends the word.

Equations

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

theorem HeinzLai2013.not_isLeftSubsequential_of_isSourGrapes {f : List Seg → List Seg} (hf : IsSourGrapes f) : ¬IsLeftSubsequential f

No left-subsequential function meets (8) (Theorem 5). A left scan reading + −ⁿ⁺¹ must hold back all but a bounded part of its output until it learns whether ⊟ follows.

def HeinzLai2013.raiseUnlessFinalBlocked : Mealy (Option Bool) Seg Seg

The right-to-left pass that raises every − unless the word ends in ⊟. Its state records, after the first symbol read, whether that symbol was ⊟.

Equations

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

theorem HeinzLai2013.exists_isRightSubsequential_isSourGrapes : ∃ (f : List Seg → List Seg), IsSourGrapes f ∧ IsRightSubsequential f

The right half of Theorem 5 fails for (8) alone, since a right-to-left pass meets (8).

theorem HeinzLai2013.not_isRightSubsequential_of_isSourGrapes {f : List Seg → List Seg} (hlen : ∀ (w : List Seg), (f w).length = w.length) (hf : IsSourGrapes f) (hnone : ∀ (n : ℕ), f (List.replicate n Seg.minus) = List.replicate n Seg.minus) : ¬IsRightSubsequential f

The right half of Theorem 5 holds once a word with no trigger is left alone. No length-preserving right-subsequential function meets (8) and leaves every −ⁿ unchanged.

Dominant–recessive harmony

def HeinzLai2013.IsDominantRecessive (f : List Seg → List Seg) : Prop

f meets the dominant–recessive condition (9). On words over + and −, every vowel surfaces + if some vowel is +, and − otherwise.

Equations

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

theorem HeinzLai2013.not_isSubsequential_of_isDominantRecessive {f : List Seg → List Seg} (hlen : ∀ (w : List Seg), (f w).length = w.length) (hf : IsDominantRecessive f) (d : Edge) : ¬IsSubsequential d f

No length-preserving subsequential function, in either direction, meets (9) (Theorem 6). A medial − among −s turns + under a + placed far to the left or far to the right.

def HeinzLai2013.php : Mealy Bool Seg Seg

Progressive spreading of + alone (Figure 4) turns every − after a + into +.

Equations

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

theorem HeinzLai2013.isDominantRecessive_php : IsDominantRecessive (php.runRight ∘ php.run)

Progressive spreading of +, run left to right and then right to left, meets (9) (Theorem 7).

theorem HeinzLai2013.isWeaklyDeterministic_php : IsWeaklyDeterministic (php.runRight ∘ php.run)

Dominant–recessive harmony is weakly deterministic (Theorem 7).