Harmony systems

A harmony system in the [RW11] typological decomposition: a distinctive feature value spreads from trigger segments to target segments, optionally skipping transparent segments and halting at opaque blockers ([RW11], [Bel26]). System couples the tier-based AGREE recognizer with the transduction discipline that turns it into a structure-changing map.

System is alphabet-generic; at each concrete alphabet it instantiates to a familiar finite-state object — transduce to a subsequential transducer whose only state is one lens readout (at Turkish's alphabet, the classic two-state front/back machine), the recognizer to a last-trigger-decides subsequential function. The theorems are proved once, generically; every instantiation inherits them. Finiteness is supplied at instantiation, not in the structure (mathlib's DFA convention: [Fintype α] appears only on the theorems that consume it).

Main definitions

• Subregular.Harmony.System: a Phonology.Harmony.Pattern plus the mechanism-side residue — trigger context, targets, and the feature write. The valuation and write form a lawful lens (System.lens, a Lens); blockers, the tier, and the recognizer (System.toTierRule) are derived from the pattern; System.mk' compiles the six-way decomposition.
• Subregular.Harmony.harmonyDomain, triggerValue: the stem portion governing suffix harmony, and the recognizer's prediction over it.
• System.transduce: the harmonized-string function, as a 2-OSL rule ([CEH15]).

Main results

• System.transduce_isLeftOSL: the harmonized string is 2-OSL by construction, not by post-hoc classification.
• Phonology.Harmony.Pattern.harmonic_iff_mem_tsl: a pattern's surface harmonicity is membership in a TSL₂ language ([ARGH24]).

Implementation notes

This is the tier-based (TSL/OSL) analysis — one live account, not a settled reduction: autosegmental spreading ([Gol76]), Agreement-by-Correspondence ([RW04a]), and OT SPREAD/ALIGN remain rivals with divergent predictions on transparency and opacity, and 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. The theory-neutral pattern vocabulary the rival accounts share lives in Phonology/Harmony/Basic.lean; language instances live in Fragments/{Turkish,Finnish,Hungarian}/VowelHarmony.lean.

Direction

def Phonology.Harmony.Direction.toSide : Direction → Subregular.Side

Compile a direction to the TierRule context side (bidirectional ↦ rightward).

Equations

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

System — a pattern plus its transduction discipline

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

Write harmonic value v into a segment's feature slot: the function-type lens (Lens.proj) written at feature.

Equations

• Subregular.Harmony.writeFeature feature v s = Function.update s feature (some v)

structure Subregular.Harmony.System (α : Type u_1) : Type u_1

A harmony system: the descriptive Phonology.Harmony.Pattern (valuation, blockers, transparency, direction) plus the mechanism-side residue — the trigger context, the targets, and the feature write.

• pattern : Phonology.Harmony.Pattern α Bool

  The descriptive pattern the system realizes.

• targetIsContext : α → Prop

  The natural class of triggering context segments.

• decContext : DecidablePred self.targetIsContext
• isTarget : α → Prop

  Which segments undergo the feature change.

• decTarget' : DecidablePred self.isTarget
• write : Bool → α → α

  Write the harmonic value into a segment.

• value_write (v : Bool) (s : α) : self.pattern.value (self.write v s) = some v

  Reading back a written value gives that value.

def Subregular.Harmony.System.isBlocker {α : Type u_1} (sys : System α) (s : α) : Prop

Opaque blockers, read off the pattern.

Equations

• sys.isBlocker s = (sys.pattern.participation s = Phonology.Harmony.Participation.opaque)

@[instance_reducible]

instance Subregular.Harmony.instDecidablePredIsBlocker {α : Type u_1} (sys : System α) : DecidablePred sys.isBlocker

Equations

• Subregular.Harmony.instDecidablePredIsBlocker sys s = id inferInstance

def Subregular.Harmony.System.lens {α : Type u_1} (sys : System α) : Lens α Bool

The system's lens: (pattern.value, write) with the put-get law. The slot readout is the only state the OSL transducer carries.

Equations

• sys.lens = { read := sys.pattern.value, write := sys.write, read_write := ⋯ }

def Subregular.Harmony.System.toTierRule {α : Type u_1} (sys : System α) : TierRule α

The recognizer core, derived from the pattern: an agree TierRule over the pattern's tier, reading the pattern's valuation from the pattern's side.

Equations

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

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

Compile the [RW11] six-way decomposition into a System; Bool lambdas are stored as the decidable Prop fields.

Equations

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

Recovering the Rose-Walker Typology

@[inline]

def Subregular.Harmony.isTrigger {α : Type u_1} (sys : System α) (s : α) : Bool

The trigger predicate: Bool accessor for targetIsContext.

Equations

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

Harmony Domain

def Subregular.Harmony.harmonyDomain {α : Type u_1} (sys : System α) (stem : List α) : List α

The stem portion governing suffix harmony: everything after (rightward) or before (leftward) the blocker nearest the suffix.

Equations

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

Trigger Value Extraction

def Subregular.Harmony.triggerValue {α : Type u_1} (sys : System α) (stem : List α) : Option Bool

The harmony value predicted at the suffix slot: the recognizer applied to the harmony domain.

Equations

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

Segment-Level Harmony

def Subregular.Harmony.harmonizeOne {α : Type u_1} (sys : System α) (val : Bool) (s : α) : α

Set a target's harmony feature to the given value; non-targets are unchanged.

Equations

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

Suffix Spreading (convenience over the recognizer)

def Subregular.Harmony.spreadSuffix {α : Type u_1} (sys : System α) (val : Bool) (suffix : List α) : List α

Walk a suffix: blockers halt spreading, targets harmonize, all else passes through. For the re-triggering subregular semantics, 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

Transducer grounding — harmony as an OSL function

def Subregular.Harmony.System.spreadRule {α : Type u_1} (sys : System α) : OSLRule 2 α α

Harmony as a 2-OSL rule ([CEH15]): each target copies the harmonic value of the preceding output segment; blockers re-trigger.

Equations

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

def Subregular.Harmony.System.transduce {α : Type u_1} (sys : System α) : List α → List α

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

Equations

• sys.transduce = sys.spreadRule.apply

theorem Subregular.Harmony.System.transduce_isLeftOSL {α : Type u_1} (sys : System α) : IsLeftOutputStrictlyLocal 2 sys.transduce

The harmonized string is 2-OSL by construction.

Properties

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

Non-target segments are unchanged by harmonization.

theorem Subregular.Harmony.spreadSuffix_nil {α : Type u_1} {sys : System α} {val : Bool} : spreadSuffix sys val [] = []

Spreading through an empty suffix returns an empty list.

theorem Subregular.Harmony.spreadSuffix_length {α : Type u_1} {sys : System α} {val : Bool} (suffix : List α) : (spreadSuffix sys val suffix).length = suffix.length

Spreading preserves length: blocked segments are kept, not removed.

theorem Subregular.Harmony.harmonyDomain_no_blockers {α : Type u_1} {sys : System α} {stem : List α} (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 {α : Type u_1} {sys : System α} {val : Bool} {s : α} {rest : List α} (hb : sys.isBlocker s) : spreadSuffix sys val (s :: rest) = s :: rest

A leading blocker halts spreading: the suffix is returned unchanged.

theorem Phonology.Harmony.Pattern.harmonic_iff_mem_tsl {α : Type u_1} {V : Type u_2} (p : Pattern α V) (w : List α) : p.Harmonic w ↔ w ∈ (Subregular.TSLGrammar.ofForbiddenPairs (fun (x1 x2 : α) => ¬p.Compatible x1 x2) p.OnTier).lang

Harmony is TSL₂ by construction: the tier supplies both the unbounded distance strictly local grammars lack and the blocking strictly piecewise grammars lack ([ARGH24]; for the latter, McMullin2016.blockingLang_not_isStrictlyPiecewise).