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.Constraint.OT and 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. Defined as Corr.identViol on the (input, output) edge of a binary parallel-pair correspondence between feature-projected tiers, i.e., IDENT-IO of @cite{mccarthy-prince-1995} specialized to the harmony feature.

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 Phonology.Harmony.spreadViolations (sys : HarmonySystem) (triggerVal : Bool) (suffix : List Segment) : ℕ

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

Equations

• Phonology.Harmony.spreadViolations sys triggerVal suffix = (List.filter (fun (s : Phonology.Segment) => sys.isTarget s && !s.spec sys.feature == some triggerVal) suffix).length

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

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

Derived from Corr.identViol on the (false, true) edge of a binary parallel-pair correspondence between the feature-projected tiers input.map (·.spec sys.feature) and output.map (·.spec sys.feature). This structurally identifies IDENT-[F] as IDENT-IO of @cite{mccarthy-prince-1995} restricted to the harmony feature.

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Phonology.Harmony.instDecidableEqVHCandidate : DecidableEq VHCandidate

Equations

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

def Phonology.Harmony.mkSpread (sys : HarmonySystem) : Core.Constraint.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 Phonology.Harmony.mkIdentHarmony (sys : HarmonySystem) : Core.Constraint.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 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 Phonology.Harmony.spreadSuffix_zero_spread (sys : HarmonySystem) (val : Bool) (suffix : List Segment) (h : ∀ 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 Phonology.Harmony.faithful_zero_ident (sys : HarmonySystem) (suffix : List Segment) : identViolations sys suffix suffix = 0

The faithful candidate (no changes) has zero IDENT violations. Derived from Corr.identity_ident_zero.

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

IDENT on empty suffixes is zero.

theorem Phonology.Harmony.spreadSuffix_ot_motivation (sys : HarmonySystem) (stem suffix : List Segment) (val : Bool) (h_no_blockers : ∀ 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.