Vowel harmony: pattern-level vocabulary

The theory-neutral vocabulary of vowel harmony, anchored on [RvdH24b]: the typological enums and Pattern, the descriptive object mechanisms derive. At a finite alphabet a pattern presents a TSL₂ grammar (Pattern.harmonic_iff_mem_tsl). Segment-level participation cannot express parasitic harmony ((8b)) or configuration-dependent blocking (Yakut); those need the general forbidden-pairs machinery.

Main definitions

• Participation, Direction, ControlType, Domain, HarmonyType: the typological enums.
• Pattern: valuation, participation, descriptors; Pattern.Harmonic is the surface semantics — tier-adjacent compatibility with blocker imposition and icy absorption.

Main results

• Pattern.harmonic_insert_transparent: transparency interrupts harmlessly.
• Pattern.harmonic_iff_agreeOn: with all segments participating, the chain and pairwise formulations coincide.

inductive Phonology.Harmony.Participation : Type

How a segment participates in harmony ([RvdH24b] §1.3).

• participating : Participation

  Alternates and propagates.

• transparent : Participation

  Skipped harmlessly (neutral).

• opaque : Participation

  Does not undergo; imposes its value on what follows ((8c)).

• icyTarget : Participation

  Undergoes without passing on ([jurgec-2011]'s absorbing vowels).

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqParticipation : DecidableEq Participation

Equations

• Phonology.Harmony.instDecidableEqParticipation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Harmony.instReprParticipation.repr : Participation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instReprParticipation : Repr Participation

Equations

• Phonology.Harmony.instReprParticipation = { reprPrec := Phonology.Harmony.instReprParticipation.repr }

inductive Phonology.Harmony.Direction : Type

Direction of the agreement relation ([RvdH24b] §1.2.3).

• rightward : Direction
• leftward : Direction
• bidirectional : Direction

  The prototype: outward from the root, no stipulated direction.

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqDirection : DecidableEq Direction

Equations

• Phonology.Harmony.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Harmony.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instReprDirection : Repr Direction

Equations

• Phonology.Harmony.instReprDirection = { reprPrec := Phonology.Harmony.instReprDirection.repr }

inductive Phonology.Harmony.ControlType (V : Type u) : Type u

Who determines the harmonic value ([RvdH24b] §1.2.4).

• rootControlled {V : Type u} : ControlType V

  Roots do not alternate; affixes harmonize to them (morphologically determined).

• dominantRecessive {V : Type u} (dominant : V) : ControlType V

  A designated value wins regardless of position (phonologically determined).

• affixControlled {V : Type u} : ControlType V

  Posed as an open question by the chapter: metaphony and umlaut, where stress attracts the harmonic value.

def Phonology.Harmony.instDecidableEqControlType.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : ControlType V✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.rootControlled Phonology.Harmony.ControlType.rootControlled = isTrue ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.rootControlled (Phonology.Harmony.ControlType.dominantRecessive dominant) = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.rootControlled Phonology.Harmony.ControlType.affixControlled = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq (Phonology.Harmony.ControlType.dominantRecessive dominant) Phonology.Harmony.ControlType.rootControlled = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq (Phonology.Harmony.ControlType.dominantRecessive dominant) Phonology.Harmony.ControlType.affixControlled = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.affixControlled Phonology.Harmony.ControlType.rootControlled = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.affixControlled (Phonology.Harmony.ControlType.dominantRecessive dominant) = isFalse ⋯
• Phonology.Harmony.instDecidableEqControlType.decEq Phonology.Harmony.ControlType.affixControlled Phonology.Harmony.ControlType.affixControlled = isTrue ⋯

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqControlType {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (ControlType V✝)

Equations

• Phonology.Harmony.instDecidableEqControlType = Phonology.Harmony.instDecidableEqControlType.decEq

def Phonology.Harmony.instReprControlType.repr {V✝ : Type u_1} [Repr V✝] : ControlType V✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instReprControlType {V✝ : Type u_1} [Repr V✝] : Repr (ControlType V✝)

Equations

• Phonology.Harmony.instReprControlType = { reprPrec := Phonology.Harmony.instReprControlType.repr }

inductive Phonology.Harmony.Domain : Type

The domain delimiting harmony ([RvdH24b] §1.2.2).

• root : Domain
• stem : Domain
• stemAndFirstAffix : Domain

  Bounded bisyllabic agreement: the stem-final vowel and first suffix vowel only.

• word : Domain
• foot : Domain

  As in metaphony and umlaut.

• phrase : Domain

  Post-lexical harmony.

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqDomain : DecidableEq Domain

Equations

• Phonology.Harmony.instDecidableEqDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Harmony.instReprDomain.repr : Domain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instReprDomain : Repr Domain

Equations

• Phonology.Harmony.instReprDomain = { reprPrec := Phonology.Harmony.instReprDomain.repr }

inductive Phonology.Harmony.HarmonyType : Type

The feature types of [RvdH24b] §1.5; tonal harmony is unattested.

• palatal : HarmonyType
• labial : HarmonyType
• height : HarmonyType
• tongueRoot : HarmonyType

  [ATR]/[RTR]; see Phonology/Harmony/TongueRoot.lean.

• tenseLax : HarmonyType
• nasal : HarmonyType
• emphasis : HarmonyType

  Post-velar harmony.

• retroflex : HarmonyType
• total : HarmonyType

  Echo/copy harmony: all features.

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqHarmonyType : DecidableEq HarmonyType

Equations

• Phonology.Harmony.instDecidableEqHarmonyType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.Harmony.instReprHarmonyType : Repr HarmonyType

Equations

• Phonology.Harmony.instReprHarmonyType = { reprPrec := Phonology.Harmony.instReprHarmonyType.repr }

def Phonology.Harmony.instReprHarmonyType.repr : HarmonyType → ℕ → Std.Format

Equations

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

Patterns and their surface semantics

The descriptive object every mechanism must derive: harmony creates likeness among the participating vowels of a domain ((2) of [RvdH24b]). The undergoer/blocker/transparent decomposition follows [ARGH24]: transparent segments are skipped; opaque blockers do not undergo but impose their transmitted value on what follows ((8c)); icy targets undergo without passing on ([jurgec-2011]).

structure Phonology.Harmony.Pattern (α : Type u) (V : Type v) : Type (max u v)

A harmony pattern over segment type α with harmonic values in V.

• value : α → Option V

  The valuation; none = no harmonic counterpart. For opaque and icy segments, the value transmitted (not necessarily the phonetic one).

• participation : α → Participation

  Stored independently of the valuation: neutral vowels' transparent-vs-opaque behavior is not predictable (§1.3.2). Discipline: value s = none → participation s ≠ .participating.

• direction : Direction
• domain : Domain
• control : ControlType V

def Phonology.Harmony.Pattern.AgreeOn {α : Type u} {V : Type v} (p : Pattern α V) (w : List α) : Prop

Pairwise agreement in harmonic value.

Equations

• p.AgreeOn w = List.Pairwise (fun (a b : α) => p.value a = p.value b) w

def Phonology.Harmony.Pattern.OnTier {α : Type u} {V : Type v} (p : Pattern α V) (s : α) : Prop

Tier membership: everything but transparent segments.

Equations

• p.OnTier s = (p.participation s ≠ Phonology.Harmony.Participation.transparent)

@[implicit_reducible]

instance Phonology.Harmony.instDecidablePredOnTier {α : Type u} {V : Type v} (p : Pattern α V) : DecidablePred p.OnTier

Equations

• Phonology.Harmony.instDecidablePredOnTier p s = id inferInstance

def Phonology.Harmony.Pattern.tier {α : Type u} {V : Type v} (p : Pattern α V) (w : List α) : List α

The harmonic tier of a string.

Equations

• p.tier w = List.filter (fun (s : α) => decide (p.OnTier s)) w

def Phonology.Harmony.Pattern.Compatible {α : Type u} {V : Type v} (p : Pattern α V) (a b : α) : Prop

Adjacent compatibility, left to right: an opaque right member is exempt (blockers do not undergo), an icy left member is exempt (no passing on); otherwise the values agree. Deliberately asymmetric.

Equations

• p.Compatible a b = (p.participation a = Phonology.Harmony.Participation.icyTarget ∨ p.participation b = Phonology.Harmony.Participation.opaque ∨ p.value a = p.value b)

@[implicit_reducible]

instance Phonology.Harmony.instDecidableRelCompatibleOfDecidableEq {α : Type u} {V : Type v} [DecidableEq V] (p : Pattern α V) : DecidableRel p.Compatible

Equations

• Phonology.Harmony.instDecidableRelCompatibleOfDecidableEq p a b = id inferInstance

def Phonology.Harmony.Pattern.Harmonic {α : Type u} {V : Type v} (p : Pattern α V) (w : List α) : Prop

Surface harmonicity: the tier is a chain of compatible segments.

Equations

• p.Harmonic w = List.IsChain p.Compatible (p.tier w)

@[implicit_reducible]

instance Phonology.Harmony.instDecidableHarmonicOfDecidableEq {α : Type u} {V : Type v} [DecidableEq V] (p : Pattern α V) (w : List α) : Decidable (p.Harmonic w)

Equations

• Phonology.Harmony.instDecidableHarmonicOfDecidableEq p w = id inferInstance

theorem Phonology.Harmony.Pattern.harmonic_insert_transparent {α : Type u} {V : Type v} {p : Pattern α V} {t : α} (w₁ w₂ : List α) (ht : p.participation t = Participation.transparent) : p.Harmonic (w₁ ++ t :: w₂) ↔ p.Harmonic (w₁ ++ w₂)

Transparency interrupts harmlessly ([RvdH24b] §1.3.2).

theorem Phonology.Harmony.Pattern.harmonic_iff_agreeOn {α : Type u} {V : Type v} {p : Pattern α V} {w : List α} (h : ∀ (s : α), s ∈ w → p.participation s = Participation.participating) : p.Harmonic w ↔ p.AgreeOn (p.tier w)

With all segments participating, the chain and pairwise formulations coincide (value-agreement is transitive).