Slavic Verbalizer — OT Analysis @cite{stojkovic-2026}

OT evaluation connecting constraint rankings to the empirical surface forms of the Slavic verbalizer (VBLZ). Stojković (2026) argues the VBLZ has a single abstract underlying representation (a defective diphthong) across all Slavic; surface alternation is derived by OT constraint ranking.

Candidates

The VBLZ in the pre-vocalic context (before the thematic /-a-/) can surface as one of five candidates, differing in how the unspecified slot of the diphthong is resolved:

Candidate	Vowel	Mechanism
[ov]	[o] = [+back, −high]	epenthesise [+back] and [−high]
[ev]	[e] = [−back, −high]	share [−back] from palatal, epenthesise [−high]
[uv]	[u] = [+back, +high]	epenthesise [+back] and [+high]
[iv]	[i] = [−back, +high]	share [−back] from palatal, epenthesise [+high]
[u.a]	hiatus	monophthongise, delete unspecified slot

Constraints

Six constraints, of which two (NOHIATUS, SPECIFY) are undominated and four (*SHARE[−back], DEP[+back], DEP[−high], DEP[+high]) are variable:

• NOHIATUS (markedness): no adjacent vowels
• SPECIFY (markedness): every base node must be fully specified
• *SHARE[−back] (markedness): don't copy [−back] from adjacent segment
• DEP[+back] (faithfulness): don't epenthesise [+back]
• DEP[−high] (faithfulness): don't epenthesise [−high]
• DEP[+high] (faithfulness): don't epenthesise [+high]

Note: DEP[+high] is implicit in Stojković's analysis. Without it, [uv] harmonically bounds [ov] (strictly fewer violations at every constraint), making it impossible for any ranking to select [ov]. The paper derives the same effect from the markedness of [+high] vs [−high]: [−high] is the cross-linguistically unmarked epenthetic height (p. 14), while [+high] epenthesis incurs an implicit faithfulness cost. Making this explicit as DEP[+high] yields the correct factorial typology.

Factorial Typology

The 4! = 24 permutations of the four variable constraints produce exactly 4 distinct optima: {[ov]}, {[ev]}, {[uv]}, {[iv]}. Three correspond to attested groups; {[iv]} is unattested.

inductive Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate : Type

Candidate surface realisations of the VBLZ before the thematic /-a-/. Each represents a different resolution of the defective diphthong.

• ov : VBLZCandidate

  [ov]: diphthong fissions, slot 1 → [o] via epenthetic [+back, −high].

• ev : VBLZCandidate

  [ev]: diphthong fissions, slot 1 → [e] via shared [−back], epenthetic [−high].

• uv : VBLZCandidate

  [uv]: diphthong fissions, slot 1 → [u] via epenthetic [+back, +high].

• iv : VBLZCandidate

  [iv]: diphthong fissions, slot 1 → [i] via shared [−back], epenthetic [+high].

• uHiatus : VBLZCandidate

  [u.a]: monophthongisation, unspecified slot deleted, hiatus with /-a-/.

instance Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instDecidableEqVBLZCandidate : DecidableEq VBLZCandidate

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instDecidableEqVBLZCandidate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instBEqVBLZCandidate.beq : VBLZCandidate → VBLZCandidate → Bool

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instBEqVBLZCandidate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instBEqVBLZCandidate : BEq VBLZCandidate

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instBEqVBLZCandidate = { beq := Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instBEqVBLZCandidate.beq }

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instReprVBLZCandidate.repr : VBLZCandidate → Nat → Std.Format

Equations

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

instance Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instReprVBLZCandidate : Repr VBLZCandidate

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instReprVBLZCandidate = { reprPrec := Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.instReprVBLZCandidate.repr }

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.allCandidates : List VBLZCandidate

All candidates.

Equations

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

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.allCandidates_nonempty : allCandidates ≠ []

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.fissionCandidates : List VBLZCandidate

The four fission candidates (excluding hiatus), for factorial typology.

Equations

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

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.fissionCandidates_nonempty : fissionCandidates ≠ []

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.noHiatus : Core.OT.NamedConstraint VBLZCandidate

NOHIATUS: assign * for adjacent vowels.

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.specify : Core.OT.NamedConstraint VBLZCandidate

SPECIFY(•→[F]): assign * for unspecified base node. Only violated by the fully faithful candidate (not in our candidate set), so this constraint is vacuously satisfied. Included for completeness.

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.noShareBack : Core.OT.NamedConstraint VBLZCandidate

*SHARE[−back]: don't copy [−back] from an adjacent palatal. Violated by [ev] (shares [−back] for [e]) and [iv] (shares [−back] for [i]).

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.depBack : Core.OT.NamedConstraint VBLZCandidate

DEP[+back]: don't epenthesise [+back] on the unspecified slot. Violated by [ov] and [uv] (both epenthesise [+back] to get a back vowel).

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.depLowHigh : Core.OT.NamedConstraint VBLZCandidate

DEP[−high]: don't epenthesise [−high] on the unspecified slot. Violated by [ov] and [ev] (both epenthesise [−high] to get a mid vowel).

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.depHigh : Core.OT.NamedConstraint VBLZCandidate

DEP[+high]: don't epenthesise [+high] on the unspecified slot. Violated by [uv] and [iv] (both epenthesise [+high] to get a high vowel).

Implicit in Stojković's analysis. Without this constraint, [uv] harmonically bounds [ov], making it impossible for any ranking to select [ov] as optimal. Stojković derives the equivalent effect from the markedness of [+high] vs [−high] (p. 14): "The feature [−high] is cross-linguistically more likely to be unmarked compared to [+high]."

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.variableConstraints : List (Core.OT.NamedConstraint VBLZCandidate)

The four variable constraints (excluding the undominated NOHIATUS and vacuous SPECIFY). These are permuted in the factorial typology.

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.allConstraints : List (Core.OT.NamedConstraint VBLZCandidate)

All six constraints in one list.

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ovRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[ov] group ranking (Stojković 2026, (17)): NOHIATUS, SPECIFY ≫ *SHARE[−back] ≫ DEP[+high] ≫ DEP[+back] ≫ DEP[−high]

*SHARE[−back] high: sharing [−back] from palatals is banned. DEP[+high] above DEP[−high]: [+high] epenthesis is costlier than [−high], making [−high] the default → mid vowel [o] surfaces.

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ovEvRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[ov]/[ev] group ranking (Stojković 2026, (21)): NOHIATUS, SPECIFY ≫ DEP[+back] ≫ DEP[+high] ≫ *SHARE[−back] ≫ DEP[−high]

DEP[+back] high: epenthesising [+back] is banned. After palatals, sharing [−back] is the only option → [ev]. After non-palatals, [−high] epenthesis yields [ov] (in a separate non-palatal evaluation).

Equations

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

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.uvRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[uv] group ranking (Stojković 2026, (29)): NOHIATUS, SPECIFY ≫ DEP[−high] ≫ *SHARE[−back] ≫ DEP[+back] ≫ DEP[+high]

DEP[−high] high: epenthesising [−high] is banned → [+high] surfaces. *SHARE[−back] above DEP[+back]: epenthesising [+back] is cheaper than sharing [−back] → back vowel [u] surfaces.

Equations

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

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ov_optimal : (Core.OT.buildTableau allCandidates ovRanking allCandidates_nonempty).optimal = [VBLZCandidate.ov]

The [ov] group ranking selects [ov] as the unique optimal candidate.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ev_optimal : (Core.OT.buildTableau allCandidates ovEvRanking allCandidates_nonempty).optimal = [VBLZCandidate.ev]

The [ov]/[ev] ranking selects [ev] as optimal in the palatal context. (In the non-palatal context, [ev] and [iv] are unavailable because there is no palatal to share [−back]; [ov] wins trivially.)

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.uv_optimal : (Core.OT.buildTableau allCandidates uvRanking allCandidates_nonempty).optimal = [VBLZCandidate.uv]

The [uv] group ranking selects [uv] as the unique optimal candidate.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.factorial_typology_size : Core.OT.factorialTypologySize fissionCandidates variableConstraints fissionCandidates_nonempty = 4

The factorial typology over the four variable constraints and four fission candidates produces exactly 4 distinct optimal sets.

Three correspond to attested Slavic groups:

• {[ov]}: *SHARE, DEP[+high] ranked high
• {[ev]}: DEP[+back], DEP[+high] ranked high
• {[uv]}: DEP[−high], *SHARE ranked high

The fourth ({[iv]}) is unattested in Slavic.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.factorial_optima_are_singletons : Core.OT.factorialOptima fissionCandidates variableConstraints fissionCandidates_nonempty = [[VBLZCandidate.uv], [VBLZCandidate.iv], [VBLZCandidate.ov], [VBLZCandidate.ev]]

The four distinct optima are exactly the four singleton candidate sets.

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ivIsUnattested : Prop

The [iv] pattern (shared [−back] + [+high], giving a front high vowel) is the only unattested pattern among the four predicted by the factorial typology (Stojković 2026, (31f)).

Equations

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

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.iv_pattern_unattested : ivIsUnattested

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ov_matches_group : Data.VBLZGroup.ovGroup.forms.contains "ov" = true

The [ov] group's OT-predicted form matches the empirical data.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.uv_matches_group : Data.VBLZGroup.uvGroup.forms.contains "uv" = true

The [uv] group's OT-predicted form matches the empirical data.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ovEv_matches_group : Data.VBLZGroup.ovEvGroup.forms.contains "ev" = true ∧ Data.VBLZGroup.ovEvGroup.forms.contains "ov" = true

The [ov]/[ev] group's OT-predicted forms match the empirical data: [ev] in the palatal context (proved by ev_optimal), [ov] in the non-palatal context (where [ev] is unavailable).

def Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.surfaceForm : VBLZCandidate → String

The surface form of each candidate.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.ov.surfaceForm = "ov"
• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.ev.surfaceForm = "ev"
• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.uv.surfaceForm = "uv"
• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.iv.surfaceForm = "iv"
• Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.VBLZCandidate.uHiatus.surfaceForm = "u"

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ov_surface_correct : VBLZCandidate.ov.surfaceForm = "ov"

The OT-optimal candidate for the [ov] group produces the attested form.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.uv_surface_correct : VBLZCandidate.uv.surfaceForm = "uv"

The OT-optimal candidate for the [uv] group produces the attested form.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Studies.Stojkovic2026.ev_surface_correct : VBLZCandidate.ev.surfaceForm = "ev"

The OT-optimal candidate for the [ov]/[ev] palatal context produces the attested palatal-conditioned form.