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

@cite{siptar-torkenczy-2000} @cite{prince-smolensky-1993} @cite{rose-walker-2011}

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

1. Segment features (Features.lean) — Hayes binary feature inventory
2. Harmony system (Harmony.Defs) — trigger/target/transparent predicates
3. OT constraints (Harmony.OT) — SPREAD and IDENT derived from HarmonySystem
4. Tableaux (Core.Constraint.OT) — mkTableau + optimal select winner
5. Hungarian fragments (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.spreadDominant : List (Core.Constraint.OT.NamedConstraint Phonology.Harmony.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 (Core.Constraint.OT.NamedConstraint Phonology.Harmony.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 : Phonology.Harmony.VHCandidate

Faithful candidate: suffix archiphoneU surfaces unchanged.

Equations

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

def SiptarTorkenczy2000.ház_back : Phonology.Harmony.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 : Phonology.Harmony.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 Phonology.Harmony.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 : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.tűz_back : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.tűz_front : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.tűzCands : List Phonology.Harmony.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 : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.papír_back : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.papír_front : Phonology.Harmony.VHCandidate

Equations

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

def SiptarTorkenczy2000.papírCands : List Phonology.Harmony.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 : (Core.Constraint.OT.mkTableau házCands spreadDominant házCands_ne).optimal = {ház_back}

ház: SPREAD ≫ IDENT selects back-harmonized suffix as unique winner. @cite{siptar-torkenczy-2000} §3.2.2, class IA-b.

theorem SiptarTorkenczy2000.tűz_front_optimal : (Core.Constraint.OT.mkTableau tűzCands spreadDominant tűzCands_ne).optimal = {tűz_front}

tűz: SPREAD ≫ IDENT selects front-harmonized suffix as unique winner. @cite{siptar-torkenczy-2000} §3.2.2, class IA-f.

theorem SiptarTorkenczy2000.papír_transparency_optimal : (Core.Constraint.OT.mkTableau 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. @cite{siptar-torkenczy-2000} §3.2.2, class IIB-b.

theorem SiptarTorkenczy2000.faithful_wins_reversed : (Core.Constraint.OT.mkTableau 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 : Core.Constraint.OT.mkFactorialTypologySize házCands [Phonology.Harmony.mkSpread Fragments.Hungarian.VowelHarmony.hungarianPalatalHarmony, Phonology.Harmony.mkIdentHarmony Fragments.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 : (Core.Constraint.OT.mkTableau házCands spreadDominant házCands_ne).optimal = {{ stem := [Fragments.Hungarian.VowelHarmony.a_vowel], suffixIn := [Fragments.Hungarian.VowelHarmony.archiphoneU], suffixOut := Phonology.Harmony.spreadSuffix Fragments.Hungarian.VowelHarmony.hungarianPalatalHarmony true [Fragments.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 : (Core.Constraint.OT.mkTableau papírCands spreadDominant papírCands_ne).optimal = {{ stem := [Fragments.Hungarian.VowelHarmony.a_vowel, Fragments.Hungarian.VowelHarmony.i_vowel], suffixIn := [Fragments.Hungarian.VowelHarmony.archiphoneU], suffixOut := Phonology.Harmony.spreadSuffix Fragments.Hungarian.VowelHarmony.hungarianPalatalHarmony true [Fragments.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.Constraint.ConstraintSystem Phonology.Harmony.VHCandidate (Core.Constraint.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.Constraint.ConstraintSystem Phonology.Harmony.VHCandidate (Core.Constraint.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