Harmony Systems

[RW11] [Bel26]

The [RW11] 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

System is a tier-based AGREE rule (the recognizer half — a TierRule, inherited via extends) carrying the transduction discipline that turns the recognizer into a structure-changing map:

System  extends TierRule Segment          -- tier / trigger-class / side / relation
        feature   : Feature               -- which feature `transduce` writes
        isTarget  : Segment → Prop         [DecidablePred]   -- segments that undergo it
        isBlocker : Segment → Prop         [DecidablePred]   -- opaque segments

The trigger predicate is the inherited targetIsContext (not re-stored); the tier projects out transparent segments; relation is .agree (dissimilatory tier patterns use Disagree and live outside this typology).

Harmony is grounded on the subregular transducer hierarchy. The harmonized string System.transduce is an OSLRule (Subregular), so its Output-Strictly-Local class membership is a theorem by construction (System.transduce_isLeftOSL), not a post-hoc classification of a hand-rolled walk ([CEH15]).

This is the tier-based (TSL/OSL) analysis — one live account, not a settled reduction. Vowel harmony is the contested non-local boundary case: autosegmental spreading ([Gol76]), Agreement-by-Correspondence ([RW04a]), and OT SPREAD/ALIGN remain rivals with divergent predictions on transparency and opacity. The single-tier commitment is not universally adequate — Uyghur backness harmony is provably non-TSL ([MM18]). Only the identity-tier case is currently proved subsequential (TierRule's non-trivial-tier classification is deferred); a theory-neutral harmony profile consumed by rival accounts is future work.

Operations

• harmonyDomain: the stem portion governing suffix harmony (truncated at a blocker)
• triggerValue: dispatch the inherited recognizer on the harmony domain
• harmonizeOne: write the predicted value into a single target segment
• spreadSuffix: walk a suffix list (a convenience over the recognizer)
• transduce: the harmonized-string function, as a 2-OSL transducer

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 Subregular.Harmony.HarmonyDir : Type

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

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

@[implicit_reducible]

instance Subregular.Harmony.instDecidableEqHarmonyDir : DecidableEq HarmonyDir

Equations

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

@[implicit_reducible]

instance Subregular.Harmony.instReprHarmonyDir : Repr HarmonyDir

Equations

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

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

Equations

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

def Subregular.Harmony.HarmonyDir.toSide : HarmonyDir → 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

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

structure Subregular.Harmony.Systemextends Subregular.TierRule Phonology.Segment : Type

A harmony system: a tier-based AGREE rule (TierRule, the recognizer half, inherited via extends) plus the transduction discipline — which segments undergo the change (isTarget) and which are opaque blockers (isBlocker). The trigger predicate is the inherited targetIsContext; the spreading feature is feature (the inherited featureValue is fun s => s feature by construction, set by mk').

• tier : TierProjection Phonology.Segment Phonology.Segment
• side : Side
• targetIsContext : Phonology.Segment → Prop
• decTarget : DecidablePred self.targetIsContext
• relation : Relation
• featureValue : Phonology.Segment → Option Bool
• default : Option Bool
• feature : Phonology.Feature

  The distinctive feature that spreads.

• isTarget : Phonology.Segment → Prop

  Which segments undergo the feature change.

• decTarget' : DecidablePred self.isTarget
• isBlocker : Phonology.Segment → Prop

  Which segments are opaque (impose their own value, re-triggering). Default: no blockers.

• decBlocker : DecidablePred self.isBlocker

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

Smart constructor exposing the [RW11] six-way decomposition, compiling it into the inherited TierRule plus the transduction fields. Bool-lambda args stay ergonomic for fragment authors; they are stored as the decidable Prop fields. Trigger lives only in targetIsContext (no duplicate field); featureValue is derived from feature.

Equations

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

@[inline]

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

The trigger predicate (= the inherited targetIsContext). Convenience Bool accessor for the [RW11] typological decomposition; decidability is in scope via the inherited decTarget.

Equations

• Subregular.Harmony.isTrigger sys s = decide (sys.targetIsContext s)

def Subregular.Harmony.harmonyDomain (sys : System) (stem : List Phonology.Segment) : List Phonology.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 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 Subregular.Harmony.triggerValue (sys : System) (stem : List Phonology.Segment) : Option Bool

The harmony value predicted at the suffix slot: dispatch the inherited TierRule recognizer 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 — the typological decomposition was compiled into the inherited fields by the smart constructor.

Equations

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

def Subregular.Harmony.writeFeature (feature : Phonology.Feature) (v : Bool) (s : Phonology.Segment) : Phonology.Segment

Write harmonic value v into a segment's feature slot.

Equations

• Subregular.Harmony.writeFeature feature v s f = if (f == feature) = true then some v else s f

def Subregular.Harmony.harmonizeOne (sys : System) (val : Bool) (s : Phonology.Segment) : Phonology.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

• Subregular.Harmony.harmonizeOne sys val s = if sys.isTarget s then Subregular.Harmony.writeFeature sys.feature val s else s

def Subregular.Harmony.spreadSuffix (sys : System) (val : Bool) (suffix : List Phonology.Segment) : List Phonology.Segment

Apply harmony through a suffix segment list, respecting blockers. Walks left-to-right: a blocker halts (this and subsequent segments unchanged); a target is harmonized and spreading continues; anything else passes through. Without blockers this maps harmonizeOne over the suffix. For the genuine subregular semantics (blockers re-trigger), see transduce.

Equations

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

def Subregular.Harmony.System.spreadRule (sys : System) : OSLRule 2 Phonology.Segment Phonology.Segment

Harmony as a 2-Output-Strictly-Local rule ([CEH15]): scanning left-to-right, each target takes the harmonic value of the immediately preceding output segment (the propagated value); blockers and non-targets emit unchanged, and a blocker's own value enters the output window — so subsequent targets re-trigger from the blocker. This is the genuine subregular object harmony computes.

Equations

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

def Subregular.Harmony.System.transduce (sys : System) : List Phonology.Segment → List Phonology.Segment

The harmonized-string function of a harmony system: the OSL transduction.

Equations

• sys.transduce = sys.spreadRule.apply

theorem Subregular.Harmony.System.transduce_isLeftOSL (sys : System) : IsLeftOutputStrictlyLocal 2 sys.transduce

The harmonized string is a 2-OSL function by construction. Subregular class membership is a theorem about the transducer, not a post-hoc classification of a hand-rolled walk.

theorem Subregular.Harmony.harmonizeOne_nontarget {sys : System} {val : Bool} {s : Phonology.Segment} (h : ¬sys.isTarget s) : harmonizeOne sys val s = s

Non-target segments are unchanged by harmonization.

theorem Subregular.Harmony.spreadSuffix_nil (sys : System) (val : Bool) : spreadSuffix sys val [] = []

Spreading through an empty suffix returns an empty list.

theorem Subregular.Harmony.spreadSuffix_length (sys : System) (val : Bool) (suffix : List Phonology.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 Subregular.Harmony.harmonyDomain_no_blockers (sys : System) (stem : List Phonology.Segment) (h : ∀ s ∈ stem, ¬sys.isBlocker s) : harmonyDomain sys stem = stem

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

theorem Subregular.Harmony.spreadSuffix_blocker (sys : System) (val : Bool) (s : Phonology.Segment) (rest : List Phonology.Segment) (hb : sys.isBlocker s) : spreadSuffix sys val (s :: rest) = s :: rest

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