Harmony Systems

@cite{rose-walker-2011} @cite{belth-2026}

The @cite{rose-walker-2011} typological lens — 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.

Architecture

A HarmonySystem is a thin typological wrapper around a tier-based agreement rule (the formal core, à la @cite{belth-2026} / Heinz-style TSL phonology):

HarmonySystem  =  rule      : Phonology.Alternation.TierRule Segment   -- value prediction
                 isTarget   : Segment → Bool                           -- spreading discipline
                 isBlocker  : Segment → Bool                           -- iteration halt
                 feature    : Phonology.Feature                        -- which Feature for harmonizeOne

The rule field IS the formal pattern. Its tier projects out transparent segments; its context class is the trigger predicate; its relation is .agree (harmony is by definition assimilatory — dissimilatory tier patterns like Latin liquid dissimilation use Disagree and live outside this typology). isTarget/isBlocker are the spreading discipline — which segments accept the predicted value and where iteration halts.

Why this shape: in the modern computational/learnability framing (@cite{belth-2026} and the TSL literature), the tier projection plus a local rule on it is the central object; the Rose-Walker typological decomposition (trigger / target / transparent / blocker / direction) is the descriptive lens for cataloguing what languages do, not a separate formal primitive. So harmony systems contain tier rules rather than reducing to them via a bridge theorem — the relationship is true-by-construction.

Components (§1) of @cite{rose-walker-2011}

The smart constructor HarmonySystem.mk' exposes exactly Rose-Walker's six-way decomposition:

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

It compiles these into the underlying TierRule plus the application fields. After construction, the typology is recoverable: trigger = rule.targetIsContext, transparency is encoded in rule.tier, etc.

Operations

• harmonyDomain: extract the spreading domain (stem segments not separated from the harmonic edge by a blocker)
• triggerValue: dispatch the rule on the harmony domain (true-by-construction equivalent to "find the trigger and read off its feature value")
• harmonizeOne: apply the predicted value to a single segment
• spreadSuffix: walk a suffix list, 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 Phonology.Harmony.HarmonyDir : Type

Direction of harmony spreading (Rose-Walker typological label).

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

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqHarmonyDir : DecidableEq HarmonyDir

Equations

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

def Phonology.Harmony.instReprHarmonyDir.repr : HarmonyDir → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instReprHarmonyDir : Repr HarmonyDir

Equations

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

def Phonology.Harmony.HarmonyDir.toSide : HarmonyDir → Alternation.Side

Compile a typological direction to the side at which the underlying TierRule reads its triggering context. Bidirectional collapses to rightward operationally (the same harmonyDomain/triggerValue computation handles both); the typological distinction lives only at the smart-constructor argument site.

Equations

• Phonology.Harmony.HarmonyDir.rightward.toSide = Core.Direction.left
• Phonology.Harmony.HarmonyDir.bidirectional.toSide = Core.Direction.left
• Phonology.Harmony.HarmonyDir.leftward.toSide = Core.Direction.right

structure Phonology.Harmony.HarmonySystem : Type

A harmony system in the @cite{rose-walker-2011} typological sense.

Structurally a TierRule (the value-prediction half — @cite{belth-2026}'s tier-based AGREE rule) bundled with an application policy (which segments accept the change, which halt iteration). The feature field is the Phonology.Feature whose value harmonizeOne/spreadSuffix write into target segments; by convention rule.featureValue s = s.spec feature (enforced by the mk' smart constructor; not a typed invariant — direct record construction can break it).

• feature : Feature

  The distinctive feature that spreads.

• rule : Alternation.TierRule Segment

  The underlying tier-based AGREE rule (the formal core).

• isTarget : Segment → Bool

  Target predicate: which segments undergo feature change.

• isBlocker : Segment → Bool

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

def Phonology.Harmony.HarmonySystem.mk' (feature : Feature) (isTrigger isTarget isTransparent : Segment → Bool) (direction : HarmonyDir := HarmonyDir.rightward) (isBlocker : Segment → Bool := fun (x : Segment) => false) : HarmonySystem

Smart constructor exposing Rose-Walker's six-way decomposition.

Compiles directly into the underlying TierRule:

• tier projects out transparent segments
• side is determined by direction (rightward/bidirectional ↦ left context; leftward ↦ right context)
• context class is the trigger predicate
• relation is .agree (harmony is assimilatory by definition)
• feature value extraction reads s.spec feature
• default is none (no Elsewhere fallback)

Equations

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

@[inline]

def Phonology.Harmony.isTrigger (sys : HarmonySystem) (s : Segment) : Bool

The trigger predicate (= the rule's context class). Convenience accessor for the @cite{rose-walker-2011} typological decomposition. Returns Bool via decide since the underlying TierRule predicate is Prop-valued; the smart constructor HarmonySystem.mk' ensures decidability is in scope.

Equations

• Phonology.Harmony.isTrigger sys s = decide (sys.rule.targetIsContext s)

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

The harmony domain: the portion of the stem that governs suffix harmony. For left-context (rightward / bidirectional) rules, this is everything after the last blocker; for right-context (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 Phonology.Harmony.triggerValue (sys : HarmonySystem) (stem : List Segment) : Option Bool

The harmony value predicted at the suffix slot: dispatch the underlying TierRule on the harmony domain.

True by construction: this IS the rule's prediction at the suffix-adjacent position, after truncating the stem at the first blocker. No bridge theorem is needed (and none exists) — the typological decomposition was just compiled into the rule's fields by the smart constructor.

Equations

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

def 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

• Phonology.Harmony.harmonizeOne sys val s = if sys.isTarget s = true then { spec := fun (f : Phonology.Feature) => if (f == sys.feature) = true then some val else s.spec f } else s

def 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

• Phonology.Harmony.spreadSuffix sys val [] = []
• Phonology.Harmony.spreadSuffix sys val (s :: rest) = if sys.isBlocker s = true then s :: rest else Phonology.Harmony.harmonizeOne sys val s :: Phonology.Harmony.spreadSuffix sys val rest

theorem 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 Phonology.Harmony.spreadSuffix_nil (sys : HarmonySystem) (val : Bool) : spreadSuffix sys val [] = []

Spreading through an empty suffix returns an empty list.

theorem 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 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 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.