Siptár & Törkenczy (2000): The Phonology of Hungarian

[ST00] [PS93] [RW11]

End-to-end OT analysis of Hungarian vowel harmony, connecting:

1. Segment features (Feature.lean) — Hayes binary feature inventory
2. Harmony system (Subregular.Harmony) — trigger/target/transparent predicates
3. OT constraints (below) — SPREAD and IDENT derived from System (folded in from the former Harmony/OT.lean, this file's sole consumer)
4. Tableaux (Constraint) — Tableau.ofRanking + optimal select winner
5. Hungarian fragments (Hungarian.VowelHarmony) — concrete vowel segments and hungarianPalatalHarmony

Key results

• ház_back_optimal: SPREAD ≫ IDENT selects back-harmonized suffix for back-vowel stem ház 'house'. The harmonized candidate is the unique winner.
• papír_transparency_optimal: neutral /i/ in papír is transparent — triggerValue finds /a/, and SPREAD ≫ IDENT selects back harmony.
• tűz_front_optimal: front-vowel stem tűz 'fire' → front harmony.
• faithful_wins_reversed: under IDENT ≫ SPREAD, the faithful (no-change) candidate wins — demonstrating ranking-driven typology.
• factorial_two_types: the two constraints yield exactly 2 language types (harmony vs. no harmony) across all rankings.

Architecture

Unlike prior OT study files that use enum candidate types (e.g., CoetzeePater2011), this file uses VHCandidate with real Segment lists directly. This is possible because DecidableEq Segment (via exhaustive feature comparison) enables native_decide on segment-level goals. One type system, no enum wrappers.

def SiptarTorkenczy2000.spreadViolations (sys : Subregular.Harmony.System) (triggerVal : Bool) (suffix : List Phonology.Segment) : ℕ

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

Equations

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

def SiptarTorkenczy2000.identViolations (sys : Subregular.Harmony.System) (input output : List Phonology.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 (· sys.feature) and output.map (· sys.feature). This structurally identifies IDENT-[F] as IDENT-IO of [McCP95] restricted to the harmony feature.

Equations

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

structure SiptarTorkenczy2000.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 Phonology.Segment

  The stem (unchanged across candidates).

• suffixIn : List Phonology.Segment

  The underlying (input) suffix.

• suffixOut : List Phonology.Segment

  The surface (output) suffix.

@[implicit_reducible]

instance SiptarTorkenczy2000.instDecidableEqVHCandidate : DecidableEq VHCandidate

Equations

• SiptarTorkenczy2000.instDecidableEqVHCandidate = SiptarTorkenczy2000.instDecidableEqVHCandidate.decEq

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

Equations

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

def SiptarTorkenczy2000.mkSpread (sys : Subregular.Harmony.System) : Constraints.Constraint VHCandidate

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

Equations

• SiptarTorkenczy2000.mkSpread sys c = match Subregular.Harmony.triggerValue sys c.stem with | none => 0 | some val => SiptarTorkenczy2000.spreadViolations sys val c.suffixOut

def SiptarTorkenczy2000.mkIdentHarmony (sys : Subregular.Harmony.System) : Constraints.Constraint VHCandidate

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

Equations

• SiptarTorkenczy2000.mkIdentHarmony sys c = SiptarTorkenczy2000.identViolations sys c.suffixIn c.suffixOut

theorem SiptarTorkenczy2000.harmonizeOne_spec_feature (sys : Subregular.Harmony.System) (val : Bool) (s : Phonology.Segment) (ht : sys.isTarget s) : Subregular.Harmony.harmonizeOne sys val s sys.feature = some val

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

theorem SiptarTorkenczy2000.spreadSuffix_zero_spread (sys : Subregular.Harmony.System) (val : Bool) (suffix : List Phonology.Segment) (h : ∀ s ∈ suffix, sys.isBlocker s = (false = true)) : spreadViolations sys val (Subregular.Harmony.spreadSuffix sys val suffix) = 0

spreadSuffix produces zero SPREAD violations (when no blockers intervene). By induction: harmonizeOne fixes each target's feature value, so no target in the output disagrees with the trigger.

theorem SiptarTorkenczy2000.faithful_zero_ident (sys : Subregular.Harmony.System) (suffix : List Phonology.Segment) : identViolations sys suffix suffix = 0

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

theorem SiptarTorkenczy2000.identViolations_nil (sys : Subregular.Harmony.System) : identViolations sys [] [] = 0

IDENT on empty suffixes is zero.

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

The output of spreadSuffix achieves zero SPREAD violations for the harmonized candidate. With faithful_zero_ident this captures the OT trade-off: the faithful candidate has SPREAD > 0, IDENT = 0; the harmonized candidate has SPREAD = 0, IDENT ≥ 0. Under SPREAD ≫ IDENT, the harmonized output wins.

def SiptarTorkenczy2000.spreadDominant : List (Constraints.Constraint VHCandidate)

SPREAD ≫ IDENT: harmony applies. This is the ranking for Hungarian and other suffix-controlled harmony languages.

Equations

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

def SiptarTorkenczy2000.identDominant : List (Constraints.Constraint VHCandidate)

IDENT ≫ SPREAD: harmony blocked. This ranking produces a language without vowel harmony (suffixes surface faithfully).

Equations

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

def SiptarTorkenczy2000.ház_faithful : VHCandidate

Faithful candidate: suffix archiphoneU surfaces unchanged.

Equations

• SiptarTorkenczy2000.ház_faithful = { stem := [Hungarian.VowelHarmony.a_vowel], suffixIn := [Hungarian.VowelHarmony.archiphoneU], suffixOut := [Hungarian.VowelHarmony.archiphoneU] }

def SiptarTorkenczy2000.ház_back : VHCandidate

Back-harmonized candidate: suffix vowel set to [+back].

Equations

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

def SiptarTorkenczy2000.ház_front : VHCandidate

Front-harmonized candidate: suffix vowel set to [−back].

Equations

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

def SiptarTorkenczy2000.házCands : List VHCandidate

Equations

• SiptarTorkenczy2000.házCands = [SiptarTorkenczy2000.ház_faithful, SiptarTorkenczy2000.ház_back, SiptarTorkenczy2000.ház_front]

theorem SiptarTorkenczy2000.házCands_ne : házCands ≠ []

def SiptarTorkenczy2000.tűz_faithful : VHCandidate

Equations

• SiptarTorkenczy2000.tűz_faithful = { stem := [Hungarian.VowelHarmony.ü_vowel], suffixIn := [Hungarian.VowelHarmony.archiphoneU], suffixOut := [Hungarian.VowelHarmony.archiphoneU] }

def SiptarTorkenczy2000.tűz_back : VHCandidate

Equations

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

def SiptarTorkenczy2000.tűz_front : VHCandidate

Equations

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

def SiptarTorkenczy2000.tűzCands : List VHCandidate

Equations

• SiptarTorkenczy2000.tűzCands = [SiptarTorkenczy2000.tűz_faithful, SiptarTorkenczy2000.tűz_back, SiptarTorkenczy2000.tűz_front]

theorem SiptarTorkenczy2000.tűzCands_ne : tűzCands ≠ []

def SiptarTorkenczy2000.papír_faithful : VHCandidate

Equations

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

def SiptarTorkenczy2000.papír_back : VHCandidate

Equations

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

def SiptarTorkenczy2000.papír_front : VHCandidate

Equations

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

def SiptarTorkenczy2000.papírCands : List VHCandidate

Equations

• SiptarTorkenczy2000.papírCands = [SiptarTorkenczy2000.papír_faithful, SiptarTorkenczy2000.papír_back, SiptarTorkenczy2000.papír_front]

theorem SiptarTorkenczy2000.papírCands_ne : papírCands ≠ []

theorem SiptarTorkenczy2000.ház_back_optimal : (OptimalityTheory.Tableau.ofRanking házCands spreadDominant házCands_ne).optimal = {ház_back}

ház: SPREAD ≫ IDENT selects back-harmonized suffix as unique winner. [ST00] §3.2.2, class IA-b.

theorem SiptarTorkenczy2000.tűz_front_optimal : (OptimalityTheory.Tableau.ofRanking tűzCands spreadDominant tűzCands_ne).optimal = {tűz_front}

tűz: SPREAD ≫ IDENT selects front-harmonized suffix as unique winner. [ST00] §3.2.2, class IA-f.

theorem SiptarTorkenczy2000.papír_transparency_optimal : (OptimalityTheory.Tableau.ofRanking papírCands spreadDominant papírCands_ne).optimal = {papír_back}

papír: neutral /i/ is transparent — back harmony passes through. SPREAD ≫ IDENT selects back-harmonized suffix, same as ház. [ST00] §3.2.2, class IIB-b.

theorem SiptarTorkenczy2000.faithful_wins_reversed : (OptimalityTheory.Tableau.ofRanking házCands identDominant házCands_ne).optimal = {ház_faithful}

Under IDENT ≫ SPREAD, the faithful candidate wins — no harmony applies. This is the predicted grammar for a language without vowel harmony.

theorem SiptarTorkenczy2000.factorial_two_types : OptimalityTheory.factorialTypologySize házCands [mkSpread Hungarian.VowelHarmony.hungarianPalatalHarmony, mkIdentHarmony Hungarian.VowelHarmony.hungarianPalatalHarmony] házCands_ne = 2

Two constraints produce exactly 2 distinct language types across all rankings: harmony (SPREAD ≫ IDENT) vs. no harmony (IDENT ≫ SPREAD). This matches the typological prediction: suffix harmony is either present or absent, with no intermediate grammars.

theorem SiptarTorkenczy2000.ház_ot_matches_direct : (OptimalityTheory.Tableau.ofRanking házCands spreadDominant házCands_ne).optimal = {{ stem := [Hungarian.VowelHarmony.a_vowel], suffixIn := [Hungarian.VowelHarmony.archiphoneU], suffixOut := Subregular.Harmony.spreadSuffix Hungarian.VowelHarmony.hungarianPalatalHarmony true [Hungarian.VowelHarmony.archiphoneU] }}

The OT-optimal candidate for ház is identical to the output of spreadSuffix — the direct computation and the OT analysis agree.

theorem SiptarTorkenczy2000.papír_ot_matches_direct : (OptimalityTheory.Tableau.ofRanking papírCands spreadDominant papírCands_ne).optimal = {{ stem := [Hungarian.VowelHarmony.a_vowel, Hungarian.VowelHarmony.i_vowel], suffixIn := [Hungarian.VowelHarmony.archiphoneU], suffixOut := Subregular.Harmony.spreadSuffix Hungarian.VowelHarmony.hungarianPalatalHarmony true [Hungarian.VowelHarmony.archiphoneU] }}

The OT-optimal candidate for papír matches spreadSuffix with the trigger value extracted from the stem. Transparency is derived: triggerValue skips neutral /i/ and finds /a/.

Hungarian vowel harmony as a generic ConstraintSystem via tableauSystem. The same softmax-based phonology studies in this directory and the OT studies here both expose predict : Cand → ℝ; for the deterministic OT case, predict winner = 1 and predict loser = 0.

noncomputable def SiptarTorkenczy2000.házSystem : Core.Optimization.ConstraintSystem VHCandidate (Core.Optimization.LexProfile ℕ 2)

ház SPREAD ≫ IDENT tableau as a generic ConstraintSystem.

Equations

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

theorem SiptarTorkenczy2000.házSystem_predict_back : házSystem.predict ház_back = 1

The OT prediction lifts to a probability claim: under SPREAD ≫ IDENT, the back-harmonized candidate is assigned probability 1.

theorem SiptarTorkenczy2000.házSystem_predict_faithful_zero : házSystem.predict ház_faithful = 0

And the faithful loser is assigned probability 0.

noncomputable def SiptarTorkenczy2000.tűzSystem : Core.Optimization.ConstraintSystem VHCandidate (Core.Optimization.LexProfile ℕ 2)

tűz under SPREAD ≫ IDENT: front-harmonized winner gets probability 1.

Equations

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

theorem SiptarTorkenczy2000.tűzSystem_predict_front : tűzSystem.predict tűz_front = 1