Stojković (2026): Same Form, Different Grammars: The Slavic [ov]~[u] Alternation

This file formalizes Stojković's account of the Slavic verbalizer, the suffix of verbs derived from nouns and adjectives. The suffix is [u] before the theme /-je-/ and a vowel followed by [v] before the theme /-a-/, where the languages fall into three groups: [ov] throughout, [ov] alternating with [ev] after a palatal, and [uv] throughout.

Stojković gives the suffix one underlying form in every language, a defective diphthong whose first base node has no features and whose second is high and back but neither vowel nor consonant. A candidate leaves that form as it is, deletes the empty node and makes the second a vowel, or fills the empty node and makes the second [v]. A candidate here is its string of segments with its correspondence to the input, and every constraint is computed from the two. One ranking per group then gives [u] before /-je-/ and the group's vowel before /-a-/ (optimal_eq), and for every variety of the paper's Tables 1 and 2 exactly one of the three rankings generates all of its forms (existsUnique_generates), the Bulgarian and Macedonian present in [uv] included, since its theme is /-a-/.

Main results

• optimal_eq: the winner of each group's ranking in each context.
• image_pattern: the factorial typology of the variable constraints, the paper's (31).
• existsUnique_generates: each variety's forms single out its group.
• uv_bounds_ov: over the paper's own constraints [uv] harmonically bounds [ov].

Implementation notes

The paper states MAX and DEP over the morphemic and phonetic structures of Containment Theory. They are rendered as the correspondence constraints that count input nodes without a correspondent and corresponding pairs whose output has a feature value its input lacks. The candidates are the paper's; a deleted node with [v], which it sets aside, is not among them. A front vowel shares the [−back] of a palatal and so is a candidate only after one.

TODO

The paper's tableaux never penalize the epenthesis of [+high], so that over its constraints [uv] does at least as well as [ov] everywhere and better on DEP[−high] (uv_bounds_ov), and its typology (31) cannot be derived from them (image_pattern_of_paperFamilies). The paper attributes the [o] of the first two groups to the markedness of [+high]; that preference is made a constraint here, DEP[+high], ranked where each group needs it. The paper's tableau (28) also marks [iv] for DEP[+back], which its representation of [iv] with a shared [−back] does not support and which changes no outcome.

References

• [Sto26a]
• [McCP95]

Segments

def Stojkovic2026.node₀ : Phonology.Segment

The first base node of the verbalizer, which has no features.

Equations

• Stojkovic2026.node₀ = ⊥

def Stojkovic2026.glide₀ : Phonology.Segment

The second base node of the verbalizer, high and back but neither vowel nor consonant.

Equations

• Stojkovic2026.glide₀ = Phonology.Segment.ofSpecs [(Phonology.Feature.high, true), (Phonology.Feature.back, true)]

def Stojkovic2026.v : Phonology.Segment

The consonant [v], the second node as a consonant.

Equations

• Stojkovic2026.v = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, false), (Phonology.Feature.consonantal, true), (Phonology.Feature.high, true), (Phonology.Feature.back, true)]

def Stojkovic2026.vowel (back high : Bool) : Phonology.Segment

vowel back high is the vowel with the given backness and height, one of [o], [u], [e] and [i].

Equations

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

Contexts and candidates

inductive Stojkovic2026.StemFinal : Type

The stem-final consonant before the verbalizer is plain or palatal.

• plain : StemFinal
• palatal : StemFinal

@[instance_reducible]

instance Stojkovic2026.instDecidableEqStemFinal : DecidableEq StemFinal

Equations

• Stojkovic2026.instDecidableEqStemFinal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stojkovic2026.instFintypeStemFinal : Fintype StemFinal

Equations

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

@[instance_reducible]

instance Stojkovic2026.instReprStemFinal : Repr StemFinal

Equations

• Stojkovic2026.instReprStemFinal = { reprPrec := Stojkovic2026.instReprStemFinal.repr }

def Stojkovic2026.instReprStemFinal.repr : StemFinal → ℕ → Std.Format

Equations

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

inductive Stojkovic2026.Theme : Type

The theme after the verbalizer is /-a-/ or /-je-/.

• a : Theme
• je : Theme

@[instance_reducible]

instance Stojkovic2026.instDecidableEqTheme : DecidableEq Theme

Equations

• Stojkovic2026.instDecidableEqTheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stojkovic2026.instFintypeTheme : Fintype Theme

Equations

• Stojkovic2026.instFintypeTheme = { elems := { val := ↑Stojkovic2026.Theme.enumList, nodup := Stojkovic2026.Theme.enumList_nodup }, complete := Stojkovic2026.instFintypeTheme._proof_1 }

@[instance_reducible]

instance Stojkovic2026.instReprTheme : Repr Theme

Equations

• Stojkovic2026.instReprTheme = { reprPrec := Stojkovic2026.instReprTheme.repr }

def Stojkovic2026.instReprTheme.repr : Theme → ℕ → Std.Format

Equations

• Stojkovic2026.instReprTheme.repr Stojkovic2026.Theme.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stojkovic2026.Theme.a")).group prec✝
• Stojkovic2026.instReprTheme.repr Stojkovic2026.Theme.je prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stojkovic2026.Theme.je")).group prec✝

def Stojkovic2026.StemFinal.segment : StemFinal → Phonology.Segment

A plain consonant has no backness, and a palatal is [−back].

Equations

• One or more equations did not get rendered due to their size.
• Stojkovic2026.StemFinal.plain.segment = Phonology.Segment.ofSpecs [(Phonology.Feature.syllabic, false), (Phonology.Feature.consonantal, true), (Phonology.Feature.high, false)]

def Stojkovic2026.Theme.segment : Theme → Phonology.Segment

The first segment of a theme, the vowel [a] or the glide [j].

Equations

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

structure Stojkovic2026.Context : Type

A context is the stem-final consonant before the verbalizer and the theme after it.

• stemFinal : StemFinal
• theme : Theme

def Stojkovic2026.instDecidableEqContext.decEq (x✝ x✝¹ : Context) : Decidable (x✝ = x✝¹)

Equations

• Stojkovic2026.instDecidableEqContext.decEq { stemFinal := a, theme := a_1 } { stemFinal := b, theme := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Stojkovic2026.instDecidableEqContext : DecidableEq Context

Equations

• Stojkovic2026.instDecidableEqContext = Stojkovic2026.instDecidableEqContext.decEq

@[instance_reducible]

instance Stojkovic2026.instFintypeContext : Fintype Context

Equations

• Stojkovic2026.instFintypeContext = Fintype.ofEquiv ((_ : Stojkovic2026.StemFinal) × Stojkovic2026.Theme) Stojkovic2026.Context.proxyTypeEquiv

@[instance_reducible]

instance Stojkovic2026.instReprContext : Repr Context

Equations

• Stojkovic2026.instReprContext = { reprPrec := Stojkovic2026.instReprContext.repr }

def Stojkovic2026.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

inductive Stojkovic2026.Candidate : Type

A candidate realization of the verbalizer.

• faithful : Candidate

  The underlying form unchanged.

• delete : Candidate

  The empty node deleted and the second node a vowel, [u].

• fill (back high : Bool) : Candidate

  The empty node filled with a backness and a height and the second node [v].

def Stojkovic2026.instDecidableEqCandidate.decEq (x✝ x✝¹ : Candidate) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.faithful Stojkovic2026.Candidate.faithful = isTrue ⋯
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.faithful Stojkovic2026.Candidate.delete = isFalse Stojkovic2026.instDecidableEqCandidate.decEq._proof_3
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.faithful (Stojkovic2026.Candidate.fill back high) = isFalse ⋯
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.delete Stojkovic2026.Candidate.faithful = isFalse Stojkovic2026.instDecidableEqCandidate.decEq._proof_5
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.delete Stojkovic2026.Candidate.delete = isTrue ⋯
• Stojkovic2026.instDecidableEqCandidate.decEq Stojkovic2026.Candidate.delete (Stojkovic2026.Candidate.fill back high) = isFalse ⋯
• Stojkovic2026.instDecidableEqCandidate.decEq (Stojkovic2026.Candidate.fill back high) Stojkovic2026.Candidate.faithful = isFalse ⋯
• Stojkovic2026.instDecidableEqCandidate.decEq (Stojkovic2026.Candidate.fill back high) Stojkovic2026.Candidate.delete = isFalse ⋯

@[instance_reducible]

instance Stojkovic2026.instDecidableEqCandidate : DecidableEq Candidate

Equations

• Stojkovic2026.instDecidableEqCandidate = Stojkovic2026.instDecidableEqCandidate.decEq

@[instance_reducible]

instance Stojkovic2026.instFintypeCandidate : Fintype Candidate

Equations

• Stojkovic2026.instFintypeCandidate = Fintype.ofEquiv (Unit ⊕ Unit ⊕ (_ : Bool) × Bool) Stojkovic2026.Candidate.proxyTypeEquiv

@[instance_reducible]

instance Stojkovic2026.instReprCandidate : Repr Candidate

Equations

• Stojkovic2026.instReprCandidate = { reprPrec := Stojkovic2026.instReprCandidate.repr }

def Stojkovic2026.instReprCandidate.repr : Candidate → ℕ → Std.Format

Equations

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

def Stojkovic2026.input (c : Context) : List Phonology.Segment

The input is the stem-final consonant, the two nodes of the verbalizer, and the theme.

Equations

• Stojkovic2026.input c = [c.stemFinal.segment, Stojkovic2026.node₀, Stojkovic2026.glide₀, c.theme.segment]

def Stojkovic2026.output (c : Context) : Candidate → List Phonology.Segment

output c k is the string of segments of the candidate k.

Equations

• Stojkovic2026.output c Stojkovic2026.Candidate.faithful = Stojkovic2026.input c
• Stojkovic2026.output c Stojkovic2026.Candidate.delete = [c.stemFinal.segment, Stojkovic2026.vowel true true, c.theme.segment]
• Stojkovic2026.output c (Stojkovic2026.Candidate.fill a a_1) = [c.stemFinal.segment, Stojkovic2026.vowel a a_1, Stojkovic2026.v, c.theme.segment]

def Stojkovic2026.corr (c : Context) : Candidate → OptimalityTheory.Correspondence OptimalityTheory.BinaryRole Phonology.Segment

corr c k is the correspondence of the candidate k to the input, a deletion of the empty node for delete and position by position for the others.

Equations

• Stojkovic2026.corr c Stojkovic2026.Candidate.delete = OptimalityTheory.Correspondence.deletion (Stojkovic2026.input c) (Stojkovic2026.output c Stojkovic2026.Candidate.delete) 1
• Stojkovic2026.corr c x✝ = OptimalityTheory.Correspondence.parallel (Stojkovic2026.input c) (Stojkovic2026.output c x✝)

def Stojkovic2026.candidates (c : Context) : List Candidate

The candidates of a context. A front vowel is a candidate only after a palatal.

Equations

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

Constraints

def Stojkovic2026.noHiatus (c : Context) : OptimalityTheory.Constraint Candidate

NOHIATUS counts the adjacent vowels of the output.

Equations

• Stojkovic2026.noHiatus c k = Phonology.Hiatus.count (Stojkovic2026.output c k)

def Stojkovic2026.specify (c : Context) : OptimalityTheory.Constraint Candidate

SPECIFY counts the output nodes that have no features.

Equations

• Stojkovic2026.specify c k = List.count Stojkovic2026.node₀ (Stojkovic2026.output c k)

def Stojkovic2026.maxNode (c : Context) : OptimalityTheory.Constraint Candidate

MAX counts the input nodes that have no correspondent in the output.

Equations

• Stojkovic2026.maxNode c k = (Stojkovic2026.corr c k).maxViol OptimalityTheory.BinaryRole.lhs OptimalityTheory.BinaryRole.rhs

def Stojkovic2026.dep (c : Context) (f : Phonology.Feature) (val : Bool) : OptimalityTheory.Constraint Candidate

dep f val counts the corresponding pairs whose output has the value val of the feature f and whose input lacks it, the epenthesis of that value.

Equations

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

def Stojkovic2026.noShare (c : Context) : OptimalityTheory.Constraint Candidate

*SHARE[−back] counts the adjacent output segments that are both [−back] and whose first is a segment of the input, a palatal sharing its frontness with the vowel after it.

Equations

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

@[reducible, inline]

abbrev Stojkovic2026.depBack (c : Context) : OptimalityTheory.Constraint Candidate

DEP[+back].

Equations

• Stojkovic2026.depBack c = Stojkovic2026.dep c Phonology.Feature.back true

@[reducible, inline]

abbrev Stojkovic2026.depNonhigh (c : Context) : OptimalityTheory.Constraint Candidate

DEP[−high].

Equations

• Stojkovic2026.depNonhigh c = Stojkovic2026.dep c Phonology.Feature.high false

@[reducible, inline]

abbrev Stojkovic2026.depHigh (c : Context) : OptimalityTheory.Constraint Candidate

DEP[+high].

Equations

• Stojkovic2026.depHigh c = Stojkovic2026.dep c Phonology.Feature.high true

def Stojkovic2026.ranking (c : Context) (vs : List (Context → OptimalityTheory.Constraint Candidate)) : List (OptimalityTheory.Constraint Candidate)

A ranking of constraints that vary across the groups, completed by the undominated NOHIATUS and SPECIFY above them and MAX below.

Equations

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

def Stojkovic2026.optimal (c : Context) (vs : List (Context → OptimalityTheory.Constraint Candidate)) : Finset Candidate

optimal c vs is the set of winners in the context c under the ranking vs.

Equations

• Stojkovic2026.optimal c vs = (OptimalityTheory.Tableau.ofRanking (Stojkovic2026.candidates c) (Stojkovic2026.ranking c vs) ⋯).optimal

The three groups

inductive Stojkovic2026.Group : Type

The three groups of languages.

• ov : Group
• ovEv : Group
• uv : Group

@[instance_reducible]

instance Stojkovic2026.instDecidableEqGroup : DecidableEq Group

Equations

• Stojkovic2026.instDecidableEqGroup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stojkovic2026.instFintypeGroup : Fintype Group

Equations

• Stojkovic2026.instFintypeGroup = { elems := { val := ↑Stojkovic2026.Group.enumList, nodup := Stojkovic2026.Group.enumList_nodup }, complete := Stojkovic2026.instFintypeGroup._proof_1 }

@[instance_reducible]

instance Stojkovic2026.instReprGroup : Repr Group

Equations

• Stojkovic2026.instReprGroup = { reprPrec := Stojkovic2026.instReprGroup.repr }

def Stojkovic2026.instReprGroup.repr : Group → ℕ → Std.Format

Equations

• Stojkovic2026.instReprGroup.repr Stojkovic2026.Group.ov prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stojkovic2026.Group.ov")).group prec✝
• Stojkovic2026.instReprGroup.repr Stojkovic2026.Group.ovEv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stojkovic2026.Group.ovEv")).group prec✝
• Stojkovic2026.instReprGroup.repr Stojkovic2026.Group.uv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stojkovic2026.Group.uv")).group prec✝

def Stojkovic2026.Group.ranking : Group → List (Context → OptimalityTheory.Constraint Candidate)

The rankings of the paper's (17), (21) and (29), with DEP[+high] added.

Equations

• Stojkovic2026.Group.ov.ranking = [Stojkovic2026.noShare, Stojkovic2026.depHigh, Stojkovic2026.depBack, Stojkovic2026.depNonhigh]
• Stojkovic2026.Group.ovEv.ranking = [Stojkovic2026.depBack, Stojkovic2026.depHigh, Stojkovic2026.noShare, Stojkovic2026.depNonhigh]
• Stojkovic2026.Group.uv.ranking = [Stojkovic2026.depNonhigh, Stojkovic2026.noShare, Stojkovic2026.depBack, Stojkovic2026.depHigh]

def Stojkovic2026.Group.form (g : Group) : Context → Candidate

g.form c is the verbalizer of the group g in the context c. It is [u] before /-je-/, and before /-a-/ the group's vowel with [v], the vowel of the middle group being front after a palatal.

Equations

• One or more equations did not get rendered due to their size.
• g.form { stemFinal := stemFinal, theme := Stojkovic2026.Theme.je } = Stojkovic2026.Candidate.delete

theorem Stojkovic2026.optimal_eq (g : Group) (c : Context) : optimal c g.ranking = {g.form c}

Each group's ranking gives its verbalizer in every context.

The paper's constraints

def Stojkovic2026.paperConstraints (c : Context) : List (OptimalityTheory.Constraint Candidate)

The paper's constraints, without DEP[+high].

Equations

• Stojkovic2026.paperConstraints c = [Stojkovic2026.noHiatus c, Stojkovic2026.specify c, Stojkovic2026.noShare c, Stojkovic2026.depBack c, Stojkovic2026.depNonhigh c, Stojkovic2026.maxNode c]

theorem Stojkovic2026.uv_le_ov (s : StemFinal) : (∀ con ∈ paperConstraints { stemFinal := s, theme := Theme.a }, con (Candidate.fill true true) ≤ con (Candidate.fill true false)) ∧ depNonhigh { stemFinal := s, theme := Theme.a } (Candidate.fill true true) < depNonhigh { stemFinal := s, theme := Theme.a } (Candidate.fill true false)

Over the paper's constraints [uv] does at least as well as [ov] on every constraint and better on DEP[−high], before /-a-/.

theorem Stojkovic2026.uv_bounds_ov (s : StemFinal) {rk : List (OptimalityTheory.Constraint Candidate)} (hrk : rk.Perm (paperConstraints { stemFinal := s, theme := Theme.a })) : Candidate.fill true false ∉ (OptimalityTheory.Tableau.ofRanking (candidates { stemFinal := s, theme := Theme.a }) rk ⋯).optimal

No ranking of the paper's constraints gives [ov], since [uv] harmonically bounds it.

Factorial typology

def Stojkovic2026.pattern (vs : List (Context → OptimalityTheory.Constraint Candidate)) : Finset Candidate × Finset Candidate

pattern vs is the pair of winners before /-a-/ under the ranking vs, after a plain consonant and after a palatal.

Equations

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

theorem Stojkovic2026.image_pattern : (List.map pattern [noShare, depBack, depNonhigh, depHigh].permutations').toFinset = {({Candidate.fill true false}, {Candidate.fill true false}), ({Candidate.fill true false}, {Candidate.fill false false}), ({Candidate.fill true true}, {Candidate.fill true true}), ({Candidate.fill true true}, {Candidate.fill false true})}

The rankings of the four variable constraints derive exactly the four patterns of the paper's (31): [ov] throughout, [ov] with [ev], [uv] throughout, and [uv] with [iv], which no Slavic language is known to show.

theorem Stojkovic2026.image_pattern_of_paperFamilies : (List.map pattern [noShare, depBack, depNonhigh].permutations').toFinset = {({Candidate.fill true true}, {Candidate.fill true true}), ({Candidate.fill true true}, {Candidate.fill false true})}

The rankings of the paper's three variable constraints derive only the two patterns with [uv].

The forms of Tables 1 and 2

def Stojkovic2026.letter? (s : Phonology.Segment) : Option Char

The letter that writes a vowel of the verbalizer or its [v].

Equations

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

def Stojkovic2026.spelling (c : Context) (k : Candidate) : String

spelling c k writes the segments of the verbalizer in the candidate k.

Equations

• Stojkovic2026.spelling c k = String.ofList (List.filterMap Stojkovic2026.letter? (List.drop 1 (Stojkovic2026.output c k)).dropLast)

def Stojkovic2026.context? (a : Forms.Analysis) : Option Context

context? a is the context of the verbalizer in the form a analyses. The root is plain or palatal by the table the form comes from, and the theme is the morph after the verbalizer.

Equations

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

def Stojkovic2026.verbalizer? (f : Data.Forms.Form Forms.Cell) : Option String

The verbalizer a form is written with. Belarusian writes the reduced vowel of [ov] as a, and the paper takes it to be /o/.

Equations

• Stojkovic2026.verbalizer? f = Option.map (fun (s : String) => if f.lexeme.variety = "Belarusian" ∧ s = "av" then "ov" else s) f.morphs[1]?

def Stojkovic2026.Generates (g : Group) (a : Forms.Analysis) : Prop

A group generates a form when the form is written with the group's verbalizer for its context.

Equations

• Stojkovic2026.Generates g a = ∃ c ∈ Stojkovic2026.context? a, Stojkovic2026.verbalizer? a.form = some (Stojkovic2026.spelling c (g.form c))

@[instance_reducible]

instance Stojkovic2026.instDecidableGenerates (g : Group) (a : Forms.Analysis) : Decidable (Generates g a)

Equations

• Stojkovic2026.instDecidableGenerates g a = Stojkovic2026.instDecidableGenerates._aux_1 g a

def Stojkovic2026.varieties : List String

The varieties of the two tables.

Equations

• Stojkovic2026.varieties = (List.map (fun (x : Data.Forms.Lexeme) => x.variety) Stojkovic2026.Forms.lexemes).dedup

def Stojkovic2026.formsOf (variety : String) : List Forms.Analysis

The analysed forms of a variety.

Equations

• Stojkovic2026.formsOf variety = List.filter (fun (x : Stojkovic2026.Forms.Analysis) => decide (x.form.lexeme.variety = variety)) Stojkovic2026.Forms.analyses

theorem Stojkovic2026.existsUnique_generates (variety : String) : variety ∈ varieties → ∃ (g : Group), (∀ a ∈ formsOf variety, Generates g a) ∧ ∀ (g' : Group), (∀ a ∈ formsOf variety, Generates g' a) → g' = g

For every variety exactly one group generates all of its forms, the infinitive-stem forms after a plain and after a palatal root and the present forms alike. The Bulgarian and Macedonian present in [uv] needs no separate statement, since its theme is /-a-/.