Harmony Systems

@cite{rose-walker-2011}

General framework for phonological harmony following @cite{rose-walker-2011}: a process by which a distinctive feature value spreads from a trigger segment to target segments, optionally skipping transparent segments and halting at blocker (opaque) segments.

Components (§1)

1. Feature: which distinctive feature spreads ([back], [round], [ATR], ...)
2. Trigger: which segments source the spreading feature value
3. Target: which segments receive the spreading feature value
4. Transparent: which segments are skipped without blocking
5. Blocker: which segments halt spreading (opaque segments)
6. Direction: rightward, leftward, or bidirectional

Operations

• harmonyDomain: extract the spreading domain (stem segments not separated from the suffix by a blocker)
• triggerValue: extract the harmony value from the domain (direction-aware)
• harmonizeOne: apply harmony to a single segment
• spreadSuffix: apply harmony through a suffix, halting at blockers

Instances

• Turkish palatal harmony: [back] from last stem vowel → all suffix vowels
• Turkish labial harmony: [round] from last stem vowel → high suffix vowels only
• Finnish palatal harmony: [back] from last harmonic stem vowel → non-neutral suffix vowels; neutral vowels (/e/, /i/) are transparent
• Hungarian palatal harmony: [back] from last harmonic stem vowel → non-neutral suffix vowels; neutral vowels (/i, í, e, é/) are transparent

inductive Theories.Phonology.Harmony.HarmonyDir : Type

Direction of harmony spreading.

• rightward : HarmonyDir
• leftward : HarmonyDir
• bidirectional : HarmonyDir

instance Theories.Phonology.Harmony.instDecidableEqHarmonyDir : DecidableEq HarmonyDir

Equations

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

def Theories.Phonology.Harmony.instBEqHarmonyDir.beq : HarmonyDir → HarmonyDir → Bool

Equations

• Theories.Phonology.Harmony.instBEqHarmonyDir.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Harmony.instBEqHarmonyDir : BEq HarmonyDir

Equations

• Theories.Phonology.Harmony.instBEqHarmonyDir = { beq := Theories.Phonology.Harmony.instBEqHarmonyDir.beq }

def Theories.Phonology.Harmony.instReprHarmonyDir.repr : HarmonyDir → Nat → Std.Format

Equations

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

instance Theories.Phonology.Harmony.instReprHarmonyDir : Repr HarmonyDir

Equations

• Theories.Phonology.Harmony.instReprHarmonyDir = { reprPrec := Theories.Phonology.Harmony.instReprHarmonyDir.repr }

structure Theories.Phonology.Harmony.HarmonySystem : Type

A parameterized harmony system.

Following @cite{rose-walker-2011}'s decomposition into trigger, target, domain, and spreading feature. Each language's vowel harmony is an instance of this type.

The isBlocker field (default: no blockers) identifies opaque segments that halt spreading. In Hungarian, low neutral vowels like /e/ sometimes block back harmony from passing through — marking /e/ as a blocker rather than transparent yields different predictions for stems like hotel.

• feature : Feature

  The distinctive feature that spreads.

• isTrigger : Segment → Bool

  Trigger predicate: which segments source the feature value.

• isTarget : Segment → Bool

  Target predicate: which segments undergo feature change.

• isTransparent : Segment → Bool

  Transparency predicate: which segments are skipped during spreading without blocking it.

• isBlocker : Segment → Bool

  Blocker predicate: which segments halt spreading (opaque). Default: no blockers.

• direction : HarmonyDir

  Direction of spreading.

def Theories.Phonology.Harmony.harmonyDomain (sys : HarmonySystem) (stem : List Segment) : List Segment

The harmony domain: the portion of the stem that governs suffix harmony. For rightward spreading, this is everything after the last blocker; for leftward, everything before the first blocker.

Without blockers, the domain is the full stem.

Example: stem = [a, BLOCKER, i] with rightward spreading → domain = [i] (only the suffix-adjacent segment governs).

Equations

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

def Theories.Phonology.Harmony.triggerValue (sys : HarmonySystem) (stem : List Segment) : Option Bool

Extract the harmony trigger value from a segment sequence.

1. Restrict to the harmony domain (respecting blockers)
2. Filter for trigger segments within the domain
3. Select the last trigger (rightward/bidirectional) or first trigger (leftward)
4. Return the trigger's value for the harmony feature

Returns none if no trigger is found in the domain (e.g., stems with only neutral vowels, or stems where a blocker separates all triggers from the suffix boundary).

Equations

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

def Theories.Phonology.Harmony.harmonizeOne (sys : HarmonySystem) (val : Bool) (s : Segment) : Segment

Apply harmony to a single segment: if the segment is a target, set the harmony feature to the given value; otherwise return unchanged.

Equations

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

def Theories.Phonology.Harmony.spreadSuffix (sys : HarmonySystem) (val : Bool) (suffix : List Segment) : List Segment

Apply harmony through a suffix segment list, respecting blockers.

Walks through segments left-to-right:

• Blocker: halts spreading — this segment and all subsequent segments are returned unchanged.
• Target: harmonized (feature value set) and spreading continues.
• Other (transparent/inert): returned unchanged and spreading continues.

Without blockers (default), this reduces to mapping harmonizeOne over the suffix.

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Harmony.spreadSuffix sys val [] = []

theorem Theories.Phonology.Harmony.harmonizeOne_nontarget {sys : HarmonySystem} {val : Bool} {s : Segment} (h : sys.isTarget s = false) : harmonizeOne sys val s = s

Non-target segments are unchanged by harmonization.

theorem Theories.Phonology.Harmony.spreadSuffix_nil (sys : HarmonySystem) (val : Bool) : spreadSuffix sys val [] = []

Spreading through an empty suffix returns an empty list.

theorem Theories.Phonology.Harmony.spreadSuffix_length (sys : HarmonySystem) (val : Bool) (suffix : List Segment) : (spreadSuffix sys val suffix).length = suffix.length

Suffix length is preserved by spreading (even with blockers — blocked segments are returned unchanged, not removed).

theorem Theories.Phonology.Harmony.harmonyDomain_no_blockers (sys : HarmonySystem) (stem : List Segment) (h : ∀ (s : Segment), s ∈ stem → sys.isBlocker s = false) : harmonyDomain sys stem = stem

The harmony domain is the full stem when there are no blockers.

theorem Theories.Phonology.Harmony.spreadSuffix_blocker (sys : HarmonySystem) (val : Bool) (s : Segment) (rest : List Segment) (hb : sys.isBlocker s = true) : spreadSuffix sys val (s :: rest) = s :: rest

Blockers in the suffix halt spreading: segments at and after the first blocker are returned unchanged.