Harmony–OT Bridge

@cite{prince-smolensky-1993} @cite{rose-walker-2011}

Derives OT constraints from a HarmonySystem, connecting the direct computation in Harmony.Defs to the OT evaluation framework in Core.Logic.OT and Theories.Phonology.Constraints.

Constraints

Given a HarmonySystem sys:

• SPREAD: markedness — penalizes target segments in the suffix whose harmony feature doesn't match the trigger value. Drives harmony.
• IDENT-[F]: faithfulness — penalizes input→output changes on the harmony feature. Resists harmony.

Key result

spreadSuffix_zero_spread: the output of spreadSuffix incurs zero SPREAD violations (when no blockers intervene). This connects the algorithmic spreading in Defs.lean to its OT motivation: spreadSuffix produces the candidate that satisfies SPREAD, at the cost of IDENT violations. Under SPREAD ≫ IDENT, the harmonized output is optimal.

def Theories.Phonology.Harmony.spreadViolations (sys : HarmonySystem) (triggerVal : Bool) (suffix : List Segment) : Nat

SPREAD violations: count target segments whose harmony feature value doesn't match triggerVal.

Equations

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

def Theories.Phonology.Harmony.identViolations (sys : HarmonySystem) (input output : List Segment) : Nat

IDENT-[F] violations: count positions where the harmony feature changed between input and output.

Equations

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

structure Theories.Phonology.Harmony.VHCandidate : Type

A vowel harmony candidate for OT evaluation.

The stem is fixed across candidates; only the suffix varies. For rightward harmony, GEN produces candidates that differ only in the feature values of suffix vowels. The stem determines the trigger value; the suffix is the domain of evaluation.

• stem : List Segment

  The stem (unchanged across candidates).

• suffixIn : List Segment

  The underlying (input) suffix.

• suffixOut : List Segment

  The surface (output) suffix.

instance Theories.Phonology.Harmony.instDecidableEqVHCandidate : DecidableEq VHCandidate

Equations

• Theories.Phonology.Harmony.instDecidableEqVHCandidate = Theories.Phonology.Harmony.instDecidableEqVHCandidate.decEq

def Theories.Phonology.Harmony.instDecidableEqVHCandidate.decEq (x✝ x✝¹ : VHCandidate) : Decidable (x✝ = x✝¹)

Equations

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

instance Theories.Phonology.Harmony.instBEqVHCandidate : BEq VHCandidate

Equations

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

def Theories.Phonology.Harmony.instBEqVHCandidate.beq : VHCandidate → VHCandidate → Bool

Equations

• Theories.Phonology.Harmony.instBEqVHCandidate.beq { stem := a, suffixIn := a_1, suffixOut := a_2 } { stem := b, suffixIn := b_1, suffixOut := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Theories.Phonology.Harmony.instBEqVHCandidate.beq x✝¹ x✝ = false

def Theories.Phonology.Harmony.mkSpread (sys : HarmonySystem) : Core.OT.NamedConstraint VHCandidate

SPREAD as a NamedConstraint: penalizes unharmonized targets in the output suffix. Returns 0 when the stem has no trigger.

Equations

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

def Theories.Phonology.Harmony.mkIdentHarmony (sys : HarmonySystem) : Core.OT.NamedConstraint VHCandidate

IDENT-[F] as a NamedConstraint: penalizes feature changes from underlying to surface suffix.

Equations

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

theorem Theories.Phonology.Harmony.harmonizeOne_spec_feature (sys : HarmonySystem) (val : Bool) (s : Segment) (ht : sys.isTarget s = true) : (harmonizeOne sys val s).spec sys.feature = some val

After harmonization, a target's harmony feature is set to val.

theorem Theories.Phonology.Harmony.spreadSuffix_zero_spread (sys : HarmonySystem) (val : Bool) (suffix : List Segment) (h : ∀ (s : Segment), s ∈ suffix → sys.isBlocker s = false) : spreadViolations sys val (spreadSuffix sys val suffix) = 0

spreadSuffix produces zero SPREAD violations (when no blockers intervene).

By induction: harmonizeOne fixes each target's feature value (§4), so no target in the output disagrees with the trigger.

theorem Theories.Phonology.Harmony.faithful_zero_ident (sys : HarmonySystem) (suffix : List Segment) : identViolations sys suffix suffix = 0

The faithful candidate (no changes) has zero IDENT violations.

theorem Theories.Phonology.Harmony.identViolations_nil (sys : HarmonySystem) : identViolations sys [] [] = 0

IDENT on empty suffixes is zero.

theorem Theories.Phonology.Harmony.spreadSuffix_ot_motivation (sys : HarmonySystem) (stem suffix : List Segment) (val : Bool) (h_no_blockers : ∀ (s : Segment), s ∈ suffix → sys.isBlocker s = false) (hv : triggerValue sys stem = some val) : (mkSpread sys).eval { stem := stem, suffixIn := suffix, suffixOut := spreadSuffix sys val suffix } = 0

The output of spreadSuffix achieves zero SPREAD violations (the mkSpread constraint) for the harmonized candidate.

Combined with faithful_zero_ident, this captures the OT trade-off:

• Faithful candidate: SPREAD > 0, IDENT = 0
• Harmonized candidate: SPREAD = 0, IDENT ≥ 0

Under the ranking SPREAD ≫ IDENT, the harmonized output wins.