Cavirani and Vanden Wyngaerd (2026): A representational analysis of Czech palatalisation

Czech suffixes palatalise the consonant before them in three patterns, small, medium and big, which the vowel of the suffix does not tell apart: -ě, -ěj and -ěn begin alike and palatalise differently. Cavirani and Vanden Wyngaerd give each suffix floating elements that dock onto the base-final consonant, |I| for the small pattern, |H| and |I| for the medium one, |H| and a headed |I| for the big one. What is built is pronounced by lookup in a phonetic lexicon, so several structures may share a phone. A labial and /l/ have |U| at the place node, which repels |I|. After a labial the |I| is then heard as a segment of its own, unless the vowel of the suffix floats, and after /l/ it is not heard.

The rows are the word pairs of the paper's tables, and the Czech fragment reads the alternating consonant off their spelling.

Main statements

• derive_eq_sup: on a velar or a coronal the palataliser docks whole, whatever the suffix.
• associate_of_mem: a consonant with |U| at its place keeps its place and leaves |I| afloat.
• interpret_roots: outside /ɦ/, the root nodes built for a row are pronounced as the phonemes of its attested alternant.
• derive_comparative, derive_h: a fricative builds one structure under small and medium palatalisation, where /ɦ/ has two reflexes.

Implementation notes

• The skeleton is reduced to what the outcome depends on: the root node of the base-final consonant, whether the vowel of the suffix floats, and what a sonorant spreads. Government, licensing and the reduction of empty slots are not modelled.
• The melodies are those of the paper's tables of plain and palatalised consonants. Its closing summary table prints /s/ without |I| and /n/ without |A|.
• Union is taken in the structure, so small and medium palatalisation of /x/ build one structure where the paper counts two.
• The palatal segment after a labial is a root node under a V slot, a vowel for the paper. The fragment follows Short in writing it /j/.

TODO

The paper derives a voiced obstruent as its voiceless counterpart with a headed |L| at the laryngeal node, and pairs /ɦ/ with /x/. Since /x/ has |H| at its manner node, /ɦ/ then has one structure under small and medium palatalisation, where the forms have [z] and [ʒ] (derive_h). The reflexes of /ɦ/ pattern as those of /k/ do, small against medium and big.

References

• [CVW26]
• [Bac11]
• [Bac17]
• [Sho93a]
• [Low96]
• [Sch04a]

The plain consonants

def CaviraniVandenWyngaerd2026.k : ElementTheory.Segment

The stop /k/ is |ʔ|, with no place.

Equations

• CaviraniVandenWyngaerd2026.k = { manner := ElementTheory.MR.simplex ElementTheory.Element.glottal }

def CaviraniVandenWyngaerd2026.x : ElementTheory.Segment

The fricative /x/ is |H|, with no place.

Equations

• CaviraniVandenWyngaerd2026.x = { manner := ElementTheory.MR.simplex ElementTheory.Element.H }

def CaviraniVandenWyngaerd2026.t : ElementTheory.Segment

The stop /t/ is |ʔ.A|.

Equations

• CaviraniVandenWyngaerd2026.t = { manner := ElementTheory.MR.simplex ElementTheory.Element.glottal, place := ElementTheory.MR.simplex ElementTheory.Element.A }

def CaviraniVandenWyngaerd2026.s : ElementTheory.Segment

The fricative /s/ is |H.AI|.

Equations

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

def CaviraniVandenWyngaerd2026.n : ElementTheory.Segment

The nasal /n/ is |L.A|.

Equations

• CaviraniVandenWyngaerd2026.n = { manner := ElementTheory.MR.simplex ElementTheory.Element.L, place := ElementTheory.MR.simplex ElementTheory.Element.A }

def CaviraniVandenWyngaerd2026.r : ElementTheory.Segment

The rhotic /r/ is |A| at the manner node, where /s/ has |A| at the place node.

Equations

• CaviraniVandenWyngaerd2026.r = { manner := ElementTheory.MR.simplex ElementTheory.Element.A }

def CaviraniVandenWyngaerd2026.p : ElementTheory.Segment

The stop /p/ is |ʔ.U|.

Equations

• CaviraniVandenWyngaerd2026.p = { manner := ElementTheory.MR.simplex ElementTheory.Element.glottal, place := ElementTheory.MR.simplex ElementTheory.Element.U }

def CaviraniVandenWyngaerd2026.f : ElementTheory.Segment

The fricative /f/ is |H.U|.

Equations

• CaviraniVandenWyngaerd2026.f = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.simplex ElementTheory.Element.U }

def CaviraniVandenWyngaerd2026.m : ElementTheory.Segment

The nasal /m/ is |L.U|.

Equations

• CaviraniVandenWyngaerd2026.m = { manner := ElementTheory.MR.simplex ElementTheory.Element.L, place := ElementTheory.MR.simplex ElementTheory.Element.U }

def CaviraniVandenWyngaerd2026.l : ElementTheory.Segment

The lateral /l/ is |A.U|, a liquid with the place of the labials.

Equations

• CaviraniVandenWyngaerd2026.l = { manner := ElementTheory.MR.simplex ElementTheory.Element.A, place := ElementTheory.MR.simplex ElementTheory.Element.U }

def CaviraniVandenWyngaerd2026.voice : ElementTheory.Segment

Voicing is a headed |L| at the laryngeal node.

Equations

• CaviraniVandenWyngaerd2026.voice = { laryngeal := ElementTheory.MR.headedSimplex ElementTheory.Element.L }

def CaviraniVandenWyngaerd2026.consonants : List (String × Phonology.Segment × Option ElementTheory.Segment)

The consonants of the paper's tables by the letters that write them, each with its phoneme in the fragment and with its melody if the paper analyses it. A voiced obstruent is its voiceless counterpart with voicing. The paper sets /g/ and /ʦ/ aside.

Equations

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

theorem CaviraniVandenWyngaerd2026.ofString?_consonants (a : String × Phonology.Segment × Option ElementTheory.Segment) : a ∈ consonants → Czech.Phonology.ofString? a.1 = some [a.2.1]

Each letter writes its phoneme.

theorem CaviraniVandenWyngaerd2026.wellFormed_consonants (a : String × Phonology.Segment × Option ElementTheory.Segment) : a ∈ consonants → ∀ c ∈ a.2.2, c.WellFormed

Each node of a melody holds only elements that it hosts.

The palatalisers and their suffixes

def CaviraniVandenWyngaerd2026.PAL₁ : ElementTheory.Segment

The small palataliser is a floating |I|.

Equations

• CaviraniVandenWyngaerd2026.PAL₁ = { place := ElementTheory.MR.simplex ElementTheory.Element.I }

def CaviraniVandenWyngaerd2026.PAL₂ : ElementTheory.Segment

The medium palataliser is a floating |H| and |I|.

Equations

• CaviraniVandenWyngaerd2026.PAL₂ = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.simplex ElementTheory.Element.I }

def CaviraniVandenWyngaerd2026.PAL₃ : ElementTheory.Segment

The big palataliser is a floating |H| and a headed |I|.

Equations

• CaviraniVandenWyngaerd2026.PAL₃ = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.headedSimplex ElementTheory.Element.I }

theorem CaviraniVandenWyngaerd2026.PAL₁_lt_PAL₂ : PAL₁ < PAL₂

theorem CaviraniVandenWyngaerd2026.PAL₂_lt_PAL₃ : PAL₂ < PAL₃

theorem CaviraniVandenWyngaerd2026.wellFormed_PAL : PAL₁.WellFormed ∧ PAL₂.WellFormed ∧ PAL₃.WellFormed

inductive CaviraniVandenWyngaerd2026.Link : Type

How the vowel of a suffix sits on the skeleton.

• linked : Link

  The vowel is linked to a V slot of the suffix, which begins with an empty C slot.

• floating : Link

  The vowel is on a root node that floats.

@[instance_reducible]

instance CaviraniVandenWyngaerd2026.instDecidableEqLink : DecidableEq Link

Equations

• CaviraniVandenWyngaerd2026.instDecidableEqLink x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CaviraniVandenWyngaerd2026.instReprLink : Repr Link

Equations

• CaviraniVandenWyngaerd2026.instReprLink = { reprPrec := CaviraniVandenWyngaerd2026.instReprLink.repr }

def CaviraniVandenWyngaerd2026.instReprLink.repr : Link → ℕ → Std.Format

Equations

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

structure CaviraniVandenWyngaerd2026.Suffix : Type

A palatalising suffix has a floating palataliser before its vowel.

• palataliser : ElementTheory.Segment

  The floating elements.

• vowel : ElementTheory.MR

  The melody of the vowel.

• link : Link

  How the vowel sits on the skeleton.

@[instance_reducible]

instance CaviraniVandenWyngaerd2026.instDecidableEqSuffix : DecidableEq Suffix

Equations

• CaviraniVandenWyngaerd2026.instDecidableEqSuffix = CaviraniVandenWyngaerd2026.instDecidableEqSuffix.decEq

def CaviraniVandenWyngaerd2026.instDecidableEqSuffix.decEq (x✝ x✝¹ : Suffix) : Decidable (x✝ = x✝¹)

Equations

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

def CaviraniVandenWyngaerd2026.locDat : Suffix

The locative and dative singular feminine -ě has the small palataliser and a linked /ɛ/ (14).

Equations

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

def CaviraniVandenWyngaerd2026.comparative : Suffix

The comparative -ěj has the medium palataliser and a linked /ɛ/ (15).

Equations

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

def CaviraniVandenWyngaerd2026.causative : Suffix

The causative -i has the medium palataliser and a floating /i/ (16).

Equations

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

def CaviraniVandenWyngaerd2026.passPtcp : Suffix

The passive participle -ěn has the big palataliser and a floating /ɛ/ (17).

Equations

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

Docking

theorem CaviraniVandenWyngaerd2026.sup_PAL_mono (b : ElementTheory.Segment) : b ≤ b ⊔ PAL₁ ∧ b ⊔ PAL₁ ≤ b ⊔ PAL₂ ∧ b ⊔ PAL₂ ≤ b ⊔ PAL₃

A stronger palataliser builds a larger structure on any base.

theorem CaviraniVandenWyngaerd2026.s_sup_PAL : s ⊔ PAL₁ = s ∧ s ⊔ PAL₂ = s

/s/ contains the small and the medium palataliser, so neither changes it.

theorem CaviraniVandenWyngaerd2026.heads_d_sup_PAL₃ : (t ⊔ voice ⊔ PAL₃).place.heads ∪ (t ⊔ voice ⊔ PAL₃).laryngeal.heads = {ElementTheory.Element.I, ElementTheory.Element.L} ∧ ElementTheory.Element.AntagonismFree {ElementTheory.Element.I, ElementTheory.Element.L}

Big-palatalised /d/ has two heads, |I| at its place node and |L| at its laryngeal node, one for each of two fundamentals.

Association

def CaviraniVandenWyngaerd2026.associate (root floating : ElementTheory.Segment) : ElementTheory.Segment × ElementTheory.Segment

The association of floating elements with a root node (13). They join its nodes, except that floating place elements stay afloat where the place node would come to hold both |I| and |U|, which Czech has on one tier. The result is the root node and the elements left afloat.

Equations

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

theorem CaviraniVandenWyngaerd2026.associate_eq_sup {b a : ElementTheory.Segment} (hb : b.place.elements ⊆ {ElementTheory.Element.A, ElementTheory.Element.I}) (ha : a.place.elements ⊆ {ElementTheory.Element.A, ElementTheory.Element.I}) : associate b a = (b ⊔ a, ⊥)

Floating elements associate whole with a root node whose place holds at most |A| and |I|, as that of a velar or a coronal does.

theorem CaviraniVandenWyngaerd2026.associate_of_mem {b a : ElementTheory.Segment} (hU : ElementTheory.Element.U ∈ b.place.elements) (hI : ElementTheory.Element.I ∈ a.place.elements) : associate b a = (b ⊔ { manner := a.manner, laryngeal := a.laryngeal }, { place := a.place })

A root node with |U| at its place repels a floating |I|. The root node keeps its place and the floating place elements stay afloat, while the other floating elements associate.

theorem CaviraniVandenWyngaerd2026.associate_sup {c : ElementTheory.Segment} (hc : c.place = ⊥) (b a : ElementTheory.Segment) : associate (b ⊔ c) a = ((associate b a).1 ⊔ c, (associate b a).2)

Elements away from the place node commute with association, so a voiced base is derived as its voiceless counterpart is, with voicing added.

theorem CaviraniVandenWyngaerd2026.associate_PAL₂ {b : ElementTheory.Segment} (h : ElementTheory.Element.H ∈ b.manner.elements) : associate b PAL₂ = associate b PAL₁

A base with |H| at its manner node associates with the medium palataliser as with the small one.

Derivations

def CaviraniVandenWyngaerd2026.spread (c : ElementTheory.Segment) : Option ElementTheory.Segment

What a sonorant spreads to a following C slot, a nasal its manner node (29) and a liquid its root node (34). An obstruent spreads nothing.

Equations

• CaviraniVandenWyngaerd2026.spread c = if ElementTheory.Element.L ∈ c.manner.elements then some { manner := c.manner } else if ElementTheory.Element.A ∈ c.manner.elements then some c else none

def CaviraniVandenWyngaerd2026.derive (b : ElementTheory.Segment) (σ : Suffix) : List (Morphology.CVSlot × ElementTheory.Segment)

The root nodes on which a base-final consonant and the palataliser of a suffix are pronounced, each with the slot of the skeleton it is linked to. The palataliser associates with the consonant. Elements left afloat join a floating vowel on the base-final V slot, and so have no root node of their own (31), (33). Before a linked vowel they take the base-final V slot (28), unless the consonant spreads to the C slot of the suffix and so bars the way, when they associate with that slot if it does not repel them (29) and otherwise stay afloat (34).

Equations

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

theorem CaviraniVandenWyngaerd2026.derive_eq_sup {b : ElementTheory.Segment} {σ : Suffix} (hb : b.place.elements ⊆ {ElementTheory.Element.A, ElementTheory.Element.I}) (hσ : σ.palataliser.place.elements ⊆ {ElementTheory.Element.A, ElementTheory.Element.I}) : derive b σ = [(Morphology.CVSlot.C, b ⊔ σ.palataliser)]

On a velar or a coronal the palataliser docks whole, whatever the suffix.

theorem CaviraniVandenWyngaerd2026.derive_of_floating {b : ElementTheory.Segment} {σ : Suffix} (h : σ.link = Link.floating) : derive b σ = [(Morphology.CVSlot.C, (associate b σ.palataliser).1)]

Before a floating vowel the palataliser has no root node of its own, whatever the base.

theorem CaviraniVandenWyngaerd2026.palataliser_place_subset_vowel : causative.palataliser.place.elements ⊆ causative.vowel.elements ∧ passPtcp.palataliser.place.elements ⊆ passPtcp.vowel.elements

A floating vowel has every element that its palataliser can leave afloat, so the two are one vowel when they meet on the base-final V slot.

theorem CaviraniVandenWyngaerd2026.derive_labial : derive p comparative = [(Morphology.CVSlot.C, p ⊔ { manner := ElementTheory.MR.simplex ElementTheory.Element.H }), (Morphology.CVSlot.V, PAL₁)] ∧ derive p causative = [(Morphology.CVSlot.C, p ⊔ { manner := ElementTheory.MR.simplex ElementTheory.Element.H })] ∧ derive m comparative = [(Morphology.CVSlot.C, m ⊔ { manner := ElementTheory.MR.simplex ElementTheory.Element.H }), (Morphology.CVSlot.C, { manner := ElementTheory.MR.simplex ElementTheory.Element.L ⊔ ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.simplex ElementTheory.Element.I })] ∧ derive l locDat = [(Morphology.CVSlot.C, l)]

The labials and the lateral before the comparative, the causative and the locative. /p/ takes the |H| and leaves |I| to the base-final V slot, or to the floating vowel. /m/ spreads its manner node, where the |I| docks, and /l/ spreads its root node, which repels it.

theorem CaviraniVandenWyngaerd2026.derive_comparative {b : ElementTheory.Segment} (h : ElementTheory.Element.H ∈ b.manner.elements) : derive b comparative = derive b locDat

A base with |H| at its manner node builds in the comparative what it builds in the locative, so a fricative cannot tell medium palatalisation from small.

The rows of the tables

def CaviraniVandenWyngaerd2026.alternant (form : Data.Forms.Form Forms.Cell) : Option (List Phonology.Segment)

The phonemes that the alternating consonant of a form writes, its second segment, read in the context of the whole form.

Equations

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

structure CaviraniVandenWyngaerd2026.Row : Type

A row of the tables pairs a base-final consonant and a suffix with the suffixed form.

• base : Phonology.Segment

  The base-final consonant.

• melody : Option ElementTheory.Segment

  The melody of the base-final consonant, if the paper analyses it.

• suffix : Suffix

  The suffix.

• form : Data.Forms.Form Forms.Cell

  The suffixed form.

def CaviraniVandenWyngaerd2026.suffixes : List (String × Suffix)

The suffixes, by the names of the relations in the data.

Equations

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

def CaviraniVandenWyngaerd2026.baseConsonant (form : Data.Forms.Form Forms.Cell) : Option (String × Phonology.Segment × Option ElementTheory.Segment)

The base-final consonant of a base form, the consonant of the tables that its second segment writes.

Equations

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

def CaviraniVandenWyngaerd2026.Row.ofRelation (rel : Data.Forms.FormRelation (Data.Forms.Form Forms.Cell)) : Option Row

The row of a relation between a base form and a suffixed form, with the base-final consonant of the base form.

Equations

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

theorem CaviraniVandenWyngaerd2026.isSome_ofRelation (rel : Data.Forms.FormRelation (Data.Forms.Form Forms.Cell)) : rel ∈ Forms.relations → rel.relation ≠ "possessive" → (Row.ofRelation rel).isSome = true

Every pair of the tables is a row, save the two possessives that stand in for a participle.

theorem CaviraniVandenWyngaerd2026.alternant_base (rel : Data.Forms.FormRelation (Data.Forms.Form Forms.Cell)) : rel ∈ Forms.relations → rel.relation ∈ ["locDatFSg", "comparative", "causative"] → alternant rel.form = Option.map (fun (x : String × Phonology.Segment × Option ElementTheory.Segment) => [x.2.1]) (baseConsonant rel.form)

A noun or an adjective writes the base-final consonant itself, read in the context of the whole form. The base form of a participle is an infinitive, whose theme vowel palatalises.

def CaviraniVandenWyngaerd2026.rows : List Row

The rows of the tables of small and big palatalisation, of the comparative and of the causative.

Equations

• CaviraniVandenWyngaerd2026.rows = List.filterMap CaviraniVandenWyngaerd2026.Row.ofRelation CaviraniVandenWyngaerd2026.Forms.relations

def CaviraniVandenWyngaerd2026.Row.roots (a : Row) : Option (List (Morphology.CVSlot × ElementTheory.Segment))

The root nodes that the analysis builds for a row, if it gives the base a melody.

Equations

• a.roots = Option.map (fun (x : ElementTheory.Segment) => CaviraniVandenWyngaerd2026.derive x a.suffix) a.melody

theorem CaviraniVandenWyngaerd2026.alternant_eq_secondPalatalization (a : Row) : a ∈ rows → a.suffix = locDat → a.base ∈ Czech.Phonology.palatalizing → alternant a.form = some [Czech.Phonology.secondPalatalization a.base]

Small palatalisation of a velar is the second palatalisation of velars.

Lexical access

def CaviraniVandenWyngaerd2026.lexicon : List ((Morphology.CVSlot × ElementTheory.Segment) × Phonology.Segment)

The phonetic lexicon that the rows induce, each root node that the analysis builds with the phoneme attested for it. A plain consonant is listed first, with its melody.

Equations

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

def CaviraniVandenWyngaerd2026.interpret (c : Morphology.CVSlot × ElementTheory.Segment) : Option Phonology.Segment

Lexical access pronounces a root node as the lexicon lists it.

Equations

• CaviraniVandenWyngaerd2026.interpret c = List.lookup c CaviraniVandenWyngaerd2026.lexicon

theorem CaviraniVandenWyngaerd2026.interpret_roots (a : Row) : a ∈ rows → a.base ≠ Czech.Phonology.h → ∀ c ∈ a.roots, List.mapM interpret c = alternant a.form

Outside /ɦ/, the root nodes that the analysis builds for a row are pronounced as the phonemes of its alternant. Since the lexicon is read off the rows, this says that there is a root node for each phoneme, two where a palatal segment follows a labial before a linked vowel, and that root nodes built alike are pronounced alike.

theorem CaviraniVandenWyngaerd2026.derive_h : derive (x ⊔ voice) comparative = derive (x ⊔ voice) locDat ∧ alternant Forms.knize = some [Czech.Phonology.z] ∧ alternant Forms.strozejsi = some [Czech.Phonology.ž]

As the voiced counterpart of /x/, /ɦ/ builds one structure under small and medium palatalisation, while knize has [z] and strožejší has [ʒ].

theorem CaviraniVandenWyngaerd2026.interpret_š : [x ⊔ PAL₁, x ⊔ PAL₃, s ⊔ PAL₃].Nodup ∧ ∀ c ∈ [x ⊔ PAL₁, x ⊔ PAL₃, s ⊔ PAL₃], interpret (Morphology.CVSlot.C, c) = some Czech.Phonology.š

Three structures are pronounced [ʃ], palatalised /x/ with unheaded and with headed |I|, and big-palatalised /s/.

theorem CaviraniVandenWyngaerd2026.interpret_medium : [k ⊔ PAL₁, k ⊔ PAL₂, k ⊔ PAL₃].Nodup ∧ [t ⊔ PAL₁, t ⊔ PAL₂, t ⊔ PAL₃].Nodup ∧ List.map (fun (c : ElementTheory.Segment) => interpret (Morphology.CVSlot.C, c)) [k ⊔ PAL₁, k ⊔ PAL₂, k ⊔ PAL₃] = [some Czech.Phonology.c, some Czech.Phonology.č, some Czech.Phonology.č] ∧ List.map (fun (c : ElementTheory.Segment) => interpret (Morphology.CVSlot.C, c)) [t ⊔ PAL₁, t ⊔ PAL₂, t ⊔ PAL₃] = [some Czech.Phonology.ť, some Czech.Phonology.ť, some Czech.Phonology.c]

The medium pattern goes with the big one on a velar and with the small one on a coronal: /k/ gives [ts], [tʃ], [tʃ] and /t/ gives [c], [c], [ts], though the three structures differ on each.