Caha (2009): The Nanosyntax of Case

This file formalizes Caha's Universal Contiguity (10): non-accidental case syncretism targets contiguous regions of a sequence of cases that is the same in every language, nominative, accusative, genitive, dative, instrumental, comitative. The evidence is the Slavic declensions of chapter 8, read along the Slavic sequence with the prepositional between the genitive and the dative (13). The paradigms of Caha's tables that are not contiguous are the ones whose syncretism he treats as a phonological conflation or an accidental homophony, a Ukrainian variant he leaves open, and a Slovene paradigm he passes over.

Main definitions

• sequence: the Case sequence (10b)
• slavicCase, form: the Slavic sequence (13), nominative, accusative, genitive, prepositional, dative, instrumental, and a paradigm's forms along it; the paradigms are the columns of the Serbian, Slovene, Czech, Slovak and Ukrainian tables of chapter 8, read from Data/Forms/Caha2009
• accounts, analyses: Caha's treatment of the paradigms with an offending syncretism
• czechCase, Declines: the Czech case at each place of the sequence, and a noun of the Czech fragment declining a paradigm of the tables at a place

Main results

• exists_position_lt: Blake's hierarchy orders the cases of the sequence as it does
• not_isContiguous_iff: the paradigms of the tables that are not contiguous
• supersetSpellable_form: Superset spellout generates the other paradigms
• isContiguous_analysis: the underlying forms Caha gives are contiguous
• isNone_iff_adjacent: the syncretisms (67) calls non-accidental are the adjacent ones
• declines_czechNouns, declines_hrad_mesto_iff, declines_colloquial_iff: Caha's literary Czech noun paradigms are the fragment's declensions after Short and Mluvnice češtiny

Implementation notes

Two cells are syncretic when their forms are identical, which ignores Caha's shading. The data records the segmentation each table prints and its departures: the column headings that are wrong (Czech kost is 'bone', not 'castle'; the Czech ta of note 26 is feminine singular; the Slovene dva of (16) is 'two', not 'both'), the nominatives printed with a weak form beside the strong one, and the tables' indexing of endings. Where the tables decline a word in two ways without naming the variety, as where two grammars decline a Ukrainian word differently, the second paradigm's identifier ends in _2.

TODO

• not_isContiguous_iff takes several seconds in the kernel, comparing forms as strings at every triple of cells; deciding it on the first occurrence of each form would compare each pair once.

References

• [Cah09]
• [Bla94b]
• [Sho93a]
• [KKP+86]

The Case sequence

def Caha2009.sequence : Fin 6 → Case

sequence is the Case sequence (10b): nominative, accusative, genitive, dative, instrumental, comitative.

Equations

• Caha2009.sequence = ![Case.nom, Case.acc, Case.gen, Case.dat, Case.inst, Case.com]

theorem Caha2009.exists_position_lt {i j : Fin 6} (h : i < j) : ∃ (p : Blake1994.Position) (q : Blake1994.Position), Blake1994.position (sequence i) = some p ∧ Blake1994.position (sequence j) = some q ∧ p < q

Blake's hierarchy, less the positions the sequence leaves out, orders the cases of the sequence as the sequence does (48): each has a position, and a later case a later one.

The Slavic tables

Caha's paradigms are the columns of the tables of chapter 8, read from Data/Forms/Caha2009 with the segmentation and the locator each table prints. A paradigm's form at a place of the Slavic sequence (13) is its form in the cell of that case.

def Caha2009.slavicCase : Fin 6 → UD.Case

slavicCase i is the case at the place i of the Slavic sequence (13): nominative, accusative, genitive, prepositional, dative, instrumental, the prepositional as UD's locative.

Equations

• Caha2009.slavicCase = ![UD.Case.Nom, UD.Case.Acc, UD.Case.Gen, UD.Case.Loc, UD.Case.Dat, UD.Case.Ins]

def Caha2009.form (p : Data.Forms.Paradigm Forms.Cell) : Morphology.Paradigm 6 String

form p i is the form the paradigm p gives the case at the place i of the Slavic sequence.

Equations

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

def Caha2009.number (p : Data.Forms.Paradigm Forms.Cell) : Option Number

number p is the number of the paradigm's cells.

Equations

• Caha2009.number p = p.forms.head?.bind fun (f : Data.Forms.Form Caha2009.Forms.Cell) => Option.bind f.cell.number Number.fromUD

Contiguity

inductive Caha2009.Account : Type

Caha accounts for an offending syncretism as a phonological conflation of distinct forms or as an accidental homophony of distinct lexical entries.

• conflation : Account
• accidental : Account

@[instance_reducible]

instance Caha2009.instDecidableEqAccount : DecidableEq Account

Equations

• Caha2009.instDecidableEqAccount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Caha2009.instReprAccount.repr : Account → ℕ → Std.Format

Equations

• Caha2009.instReprAccount.repr Caha2009.Account.conflation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Caha2009.Account.conflation")).group prec✝
• Caha2009.instReprAccount.repr Caha2009.Account.accidental prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Caha2009.Account.accidental")).group prec✝

@[instance_reducible]

instance Caha2009.instReprAccount : Repr Account

Equations

• Caha2009.instReprAccount = { reprPrec := Caha2009.instReprAccount.repr }

def Caha2009.accounts : List (Data.Forms.Paradigm Forms.Cell × Account)

accounts pairs each paradigm Caha accounts for with his account.

Equations

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

def Caha2009.offenders : List (Data.Forms.Paradigm Forms.Cell)

offenders lists the paradigms Caha accounts for, the Ukrainian variant of 'region' he leaves open (70), and the Slovene 'lady' (16), whose accusative–instrumental gospó he leaves unshaded although he takes that syncretism to be confined to the declension of 'this'.

Equations

• Caha2009.offenders = List.map Prod.fst Caha2009.accounts ++ [Caha2009.Forms.ukr_kraj_sg_2.paradigm, Caha2009.Forms.slv_gospa_sg.paradigm]

theorem Caha2009.not_isContiguous_iff (p : Data.Forms.Paradigm Forms.Cell) : p ∈ Forms.paradigms → (¬Morphology.IsContiguous (form p) ↔ p ∈ offenders)

A paradigm of the tables is not contiguous exactly when it is an offender.

theorem Caha2009.supersetSpellable_form {p : Data.Forms.Paradigm Forms.Cell} (hp : p ∈ Forms.paradigms) (h : p ∉ offenders) : Morphology.Containment.SupersetSpellable (form p)

Superset spellout generates every paradigm of the tables but the offenders.

def Caha2009.analyses : List (Data.Forms.Paradigm Forms.Cell × Morphology.Paradigm 6 String)

analyses pairs a paradigm with the underlying ending or lexical index Caha gives each cell, or "": the indexed endings of 'street' (40), the underlying endings of (19), (32), (52), (58) and note 26, and the endings of p. 270.

Equations

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

theorem Caha2009.isContiguous_analysis (a : Data.Forms.Paradigm Forms.Cell × Morphology.Paradigm 6 String) : a ∈ analyses → a.1 ∈ offenders ∧ Morphology.IsContiguous fun (i : Fin 6) => (form a.1 i, a.2 i)

Each analyzed paradigm is an offender, and its forms paired with their underlying endings are contiguous.

The Czech syncretisms

def Caha2009.czechCase : Fin 6 → Czech.Case

czechCase i is the Czech case at the place i of the Slavic sequence.

Equations

• Caha2009.czechCase = ![Czech.Case.nom, Czech.Case.acc, Czech.Case.gen, Czech.Case.loc, Czech.Case.dat, Czech.Case.inst]

def Caha2009.Adjacent (c d : Czech.Case) : Prop

Adjacent c d holds when d follows c in the Slavic sequence.

Equations

• Caha2009.Adjacent c d = ∃ (i : Fin 5), Caha2009.czechCase i.castSucc = c ∧ Caha2009.czechCase i.succ = d

@[instance_reducible]

instance Caha2009.instDecidableAdjacent (c d : Czech.Case) : Decidable (Adjacent c d)

Equations

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

def Caha2009.table67 : List (Czech.Case × Czech.Case × Option Account)

table67 is Caha's summary of the Czech syncretisms (67), each with his account, none for the non-accidental ones.

Equations

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

theorem Caha2009.isNone_iff_adjacent (r : Czech.Case × Czech.Case × Option Account) : r ∈ table67 → (r.2.2 = none ↔ Adjacent r.1 r.2.1)

The syncretisms (67) calls non-accidental are the ones of adjacent cases.

Caha's Czech nouns and Short's declensions

Caha's Czech noun paradigms are those of the fragment's declension classes, the classes of [Sho93a]'s tables with the stem conditions of [KKP+86]: each form of the literary paradigms is one of the forms the fragment gives the noun. The plural of kluk 'boy' depends on the stem conditions, since the tables alone would give kluki and klukech where Caha has kluci and klucích. Caha's hradu and městu are the locative singular in -u that Short describes beside the tables' -ě for the hard inanimates (p. 466) and the neuters (p. 467), and his colloquial paradigms depart from the literary declension in the locative and the instrumental.

def Caha2009.Declines (n : Czech.Noun) (p : Data.Forms.Paradigm Forms.Cell) (i : Fin 6) : Prop

A noun of the fragment declines a paradigm of the tables at a place of the sequence when the paradigm's form there is one of the noun's forms in that case and the paradigm's number.

Equations

• Caha2009.Declines n p i = ∃ m ∈ Caha2009.number p, ∃ (h : m ∈ Czech.Declension.numbers), Czech.Declension.segments (Caha2009.form p i) ∈ n.forms (Caha2009.czechCase i, ⟨m, h⟩)

@[instance_reducible]

instance Caha2009.instDecidableDeclines (n : Czech.Noun) (p : Data.Forms.Paradigm Forms.Cell) (i : Fin 6) : Decidable (Declines n p i)

Equations

• Caha2009.instDecidableDeclines n p i = Caha2009.instDecidableDeclines._aux_1 n p i

def Caha2009.czechNouns : List (Data.Forms.Paradigm Forms.Cell × Czech.Noun)

The literary paradigms of the tables that decline nouns of the fragment, with the nouns.

Equations

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

theorem Caha2009.declines_czechNouns (x : Data.Forms.Paradigm Forms.Cell × Czech.Noun) : x ∈ czechNouns → ∀ (i : Fin 6), Declines x.2 x.1 i

The fragment declines each literary paradigm of the tables at every place.

theorem Caha2009.kluk_pl_not_mem_table : Czech.Declension.segments (form Forms.ces_kluk_pl.paradigm 0) ∉ List.map (fun (x : List String) => Czech.kluk.stem ++ x) (Czech.Declension.Class.chlap.endings (Czech.Declension.Cell.of Czech.Case.nom Number.plural kluk_pl_not_mem_table._proof_1)) ∧ Czech.Declension.segments (form Forms.ces_kluk_pl.paradigm 3) ∉ List.map (fun (x : List String) => Czech.kluk.stem ++ x) (Czech.Declension.Class.chlap.endings (Czech.Declension.Cell.of Czech.Case.loc Number.plural kluk_pl_not_mem_table._proof_1))

The endings of Short's table on the bare stem do not give Caha's nominative kluci and locative klucích.

theorem Caha2009.declines_hrad_mesto_iff (i : Fin 6) : (Declines Czech.hrad Forms.ces_hrad_sg.paradigm i ↔ czechCase i ≠ Czech.Case.loc) ∧ (Declines Czech.mesto Forms.ces_mesto_sg.paradigm i ↔ czechCase i ≠ Czech.Case.loc)

The fragment declines Caha's hrad and město at every place but the locative, where Caha has hradu and městu and the fragment the tables' hradě and městě.

theorem Caha2009.declines_colloquial_iff (i : Fin 6) : (Declines Czech.kluk Forms.ces_kluk_pl_colloquial.paradigm i ↔ czechCase i ≠ Czech.Case.loc ∧ czechCase i ≠ Czech.Case.inst) ∧ (Declines Czech.muz Forms.ces_muz_pl_colloquial.paradigm i ↔ czechCase i ≠ Czech.Case.inst)

The colloquial klukách and klukama and mužema are not the literary declension, which the colloquial paradigms follow at the other places.