Stump 2006: heteroclisis and paradigm linkage

[stump-2006]

Heteroclisis — a lexeme whose paradigm draws on two or more inflection classes — regulated by rules of paradigm linkage. The universal default rule (5) links each content cell ⟨L, σ⟩ to ⟨root L, σ⟩; a heteroclite lexeme carries an override (the shape of the Czech rule (14)) routing part of its paradigm to a coradical of a different class.

Czech PRAMEN 'spring' (Table 1, after Heim 1982): singular cells inflect soft-masculine (like POKOJ 'room'), plural cells hard-masculine (like MOST 'bridge'). The two stems are phonologically identical — [stump-2006] holds that the paradigm still "exhibits a kind of stem alternation", the stems differing in class alone; footnote 5 defends class-distinct, form-identical stem alternants against the No Blur Principle. Formally: the linkage is invariant along the form projection yet heteroclite along the class projection (heteroclisis_without_form_suppletion), and heteroclisis entails stem non-invariance (Linkage.IsHeteroclite.isSuppletive).

Sanskrit HR̥D(AYA) 'heart' (Table 4): direct-case cells are built on hr̥daya (neuter a-stem declension, like ĀSYA), oblique cells on hr̥d (neuter consonant-stem declension) — heteroclisis riding on genuine stem suppletion, occupying the grid cell PRAMEN leaves empty. Together the two lexemes witness that form-invariance and class-invariance are independent below stem invariance.

Main results

• realize_matches_table1 — the rule-(5)-plus-override linkage reproduces all 42 word forms of Table 1 for POKOJ, MOST, and PRAMEN
• pramen_heteroclite / heteroclisis_without_form_suppletion — PRAMEN is heteroclite with phonologically constant stems
• pramen_stem_alternation — the entailment instance: PRAMEN's linkage is suppletive in the broad sense (two stems) despite form identity
• hrd_heteroclite_and_form_suppletive — HR̥D(AYA) is heteroclite and form-suppletive
• soft_hard_contrast — the two declensions PRAMEN juxtaposes ordinarily contrast, so its split is detectable cell by cell

Czech: the two masculine declensions of Table 1

inductive Stump2006.Decl : Type

The two Czech masculine inanimate declensions Table 1 juxtaposes.

• softMasc : Decl
• hardMasc : Decl

@[instance_reducible]

instance Stump2006.instDecidableEqDecl : DecidableEq Decl

Equations

• Stump2006.instDecidableEqDecl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeDecl : Fintype Decl

Equations

• Stump2006.instFintypeDecl = { elems := { val := ↑Stump2006.Decl.enumList, nodup := Stump2006.Decl.enumList_nodup }, complete := Stump2006.instFintypeDecl._proof_1 }

@[instance_reducible]

instance Stump2006.instReprDecl : Repr Decl

Equations

• Stump2006.instReprDecl = { reprPrec := Stump2006.instReprDecl.repr }

def Stump2006.instReprDecl.repr : Decl → ℕ → Std.Format

Equations

• Stump2006.instReprDecl.repr Stump2006.Decl.softMasc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Decl.softMasc")).group prec✝
• Stump2006.instReprDecl.repr Stump2006.Decl.hardMasc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Decl.hardMasc")).group prec✝

inductive Stump2006.Case : Type

The seven Czech cases, in Table 1's row order.

• nom : Case
• gen : Case
• dat : Case
• acc : Case
• voc : Case
• loc : Case
• ins : Case

@[instance_reducible]

instance Stump2006.instDecidableEqCase : DecidableEq Case

Equations

• Stump2006.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeCase : Fintype Case

Equations

• Stump2006.instFintypeCase = { elems := { val := ↑Stump2006.Case.enumList, nodup := Stump2006.Case.enumList_nodup }, complete := Stump2006.instFintypeCase._proof_1 }

def Stump2006.instReprCase.repr : Case → ℕ → Std.Format

Equations

• Stump2006.instReprCase.repr Stump2006.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.nom")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.gen")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.dat")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.acc")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.voc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.voc")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.loc")).group prec✝
• Stump2006.instReprCase.repr Stump2006.Case.ins prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Case.ins")).group prec✝

@[instance_reducible]

instance Stump2006.instReprCase : Repr Case

Equations

• Stump2006.instReprCase = { reprPrec := Stump2006.instReprCase.repr }

inductive Stump2006.Num : Type

Grammatical number.

• sg : Num
• pl : Num

@[instance_reducible]

instance Stump2006.instDecidableEqNum : DecidableEq Num

Equations

• Stump2006.instDecidableEqNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeNum : Fintype Num

Equations

• Stump2006.instFintypeNum = { elems := { val := ↑Stump2006.Num.enumList, nodup := Stump2006.Num.enumList_nodup }, complete := Stump2006.instFintypeNum._proof_1 }

@[instance_reducible]

instance Stump2006.instReprNum : Repr Num

Equations

• Stump2006.instReprNum = { reprPrec := Stump2006.instReprNum.repr }

def Stump2006.instReprNum.repr : Num → ℕ → Std.Format

Equations

• Stump2006.instReprNum.repr Stump2006.Num.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Num.sg")).group prec✝
• Stump2006.instReprNum.repr Stump2006.Num.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.Num.pl")).group prec✝

structure Stump2006.CzCell : Type

A content cell: case and number (masculine gender held constant).

• case : Case
• num : Num

def Stump2006.instDecidableEqCzCell.decEq (x✝ x✝¹ : CzCell) : Decidable (x✝ = x✝¹)

Equations

• Stump2006.instDecidableEqCzCell.decEq { case := a, num := a_1 } { case := b, num := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instDecidableEqCzCell : DecidableEq CzCell

Equations

• Stump2006.instDecidableEqCzCell = Stump2006.instDecidableEqCzCell.decEq

@[instance_reducible]

instance Stump2006.instFintypeCzCell : Fintype CzCell

Equations

• Stump2006.instFintypeCzCell = Fintype.ofEquiv ((_ : Stump2006.Case) × Stump2006.Num) Stump2006.CzCell.proxyTypeEquiv

@[instance_reducible]

instance Stump2006.instReprCzCell : Repr CzCell

Equations

• Stump2006.instReprCzCell = { reprPrec := Stump2006.instReprCzCell.repr }

def Stump2006.instReprCzCell.repr : CzCell → ℕ → Std.Format

Equations

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

inductive Stump2006.CzNoun : Type

The three lexemes of Table 1.

• pokoj : CzNoun
• most : CzNoun
• pramen : CzNoun

@[instance_reducible]

instance Stump2006.instDecidableEqCzNoun : DecidableEq CzNoun

Equations

• Stump2006.instDecidableEqCzNoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeCzNoun : Fintype CzNoun

Equations

• Stump2006.instFintypeCzNoun = { elems := { val := ↑Stump2006.CzNoun.enumList, nodup := Stump2006.CzNoun.enumList_nodup }, complete := Stump2006.instFintypeCzNoun._proof_1 }

@[instance_reducible]

instance Stump2006.instReprCzNoun : Repr CzNoun

Equations

• Stump2006.instReprCzNoun = { reprPrec := Stump2006.instReprCzNoun.repr }

def Stump2006.instReprCzNoun.repr : CzNoun → ℕ → Std.Format

Equations

• Stump2006.instReprCzNoun.repr Stump2006.CzNoun.pokoj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzNoun.pokoj")).group prec✝
• Stump2006.instReprCzNoun.repr Stump2006.CzNoun.most prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzNoun.most")).group prec✝
• Stump2006.instReprCzNoun.repr Stump2006.CzNoun.pramen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzNoun.pramen")).group prec✝

inductive Stump2006.CzStem : Type

The stem inventory: one stem each for POKOJ and MOST, and PRAMEN's two class-distinct coradicals. pramenS and pramenH are distinct stems sharing a phonological form — the alternant pair of [stump-2006]'s footnote 5.

• pokoj : CzStem
• most : CzStem
• pramenS : CzStem
• pramenH : CzStem

@[instance_reducible]

instance Stump2006.instDecidableEqCzStem : DecidableEq CzStem

Equations

• Stump2006.instDecidableEqCzStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeCzStem : Fintype CzStem

Equations

• Stump2006.instFintypeCzStem = { elems := { val := ↑Stump2006.CzStem.enumList, nodup := Stump2006.CzStem.enumList_nodup }, complete := Stump2006.instFintypeCzStem._proof_1 }

def Stump2006.instReprCzStem.repr : CzStem → ℕ → Std.Format

Equations

• Stump2006.instReprCzStem.repr Stump2006.CzStem.pokoj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzStem.pokoj")).group prec✝
• Stump2006.instReprCzStem.repr Stump2006.CzStem.most prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzStem.most")).group prec✝
• Stump2006.instReprCzStem.repr Stump2006.CzStem.pramenS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzStem.pramenS")).group prec✝
• Stump2006.instReprCzStem.repr Stump2006.CzStem.pramenH prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CzStem.pramenH")).group prec✝

@[instance_reducible]

instance Stump2006.instReprCzStem : Repr CzStem

Equations

• Stump2006.instReprCzStem = { reprPrec := Stump2006.instReprCzStem.repr }

def Stump2006.CzStem.form : CzStem → String

A stem's phonological form.

Equations

• Stump2006.CzStem.pokoj.form = "pokoj"
• Stump2006.CzStem.most.form = "most"
• Stump2006.CzStem.pramenS.form = "pramen"
• Stump2006.CzStem.pramenH.form = "pramen"

def Stump2006.CzStem.decl : CzStem → Decl

A stem's inflection-class membership — the projection heteroclisis is stated along.

Equations

• Stump2006.CzStem.pokoj.decl = Stump2006.Decl.softMasc
• Stump2006.CzStem.most.decl = Stump2006.Decl.hardMasc
• Stump2006.CzStem.pramenS.decl = Stump2006.Decl.softMasc
• Stump2006.CzStem.pramenH.decl = Stump2006.Decl.hardMasc

def Stump2006.root : CzNoun → CzStem

Each lexeme's root, as stipulated lexically (rule (5) reads it off).

Equations

• Stump2006.root Stump2006.CzNoun.pokoj = Stump2006.CzStem.pokoj
• Stump2006.root Stump2006.CzNoun.most = Stump2006.CzStem.most
• Stump2006.root Stump2006.CzNoun.pramen = Stump2006.CzStem.pramenS

def Stump2006.czLinkage : Morphology.Linkage CzNoun CzStem CzCell

The linkage: the universal default rule (5) routes every cell to the root; PRAMEN's plural cells carry the override of the shape of rule (14), routing them to the hard-masculine coradical.

Equations

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

def Stump2006.ending : Decl → CzCell → String

The case/number endings of the two declensions, read off Table 1's POKOJ and MOST columns.

Equations

• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.nom, num := Stump2006.Num.sg } = ""
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.gen, num := Stump2006.Num.sg } = "e"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.dat, num := Stump2006.Num.sg } = "i"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.acc, num := Stump2006.Num.sg } = ""
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.voc, num := Stump2006.Num.sg } = "i"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.loc, num := Stump2006.Num.sg } = "i"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.ins, num := Stump2006.Num.sg } = "em"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.nom, num := Stump2006.Num.pl } = "e"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.gen, num := Stump2006.Num.pl } = "ů"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.dat, num := Stump2006.Num.pl } = "ům"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.acc, num := Stump2006.Num.pl } = "e"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.voc, num := Stump2006.Num.pl } = "e"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.loc, num := Stump2006.Num.pl } = "ích"
• Stump2006.ending Stump2006.Decl.softMasc { case := Stump2006.Case.ins, num := Stump2006.Num.pl } = "i"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.nom, num := Stump2006.Num.sg } = ""
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.gen, num := Stump2006.Num.sg } = "u"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.dat, num := Stump2006.Num.sg } = "u"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.acc, num := Stump2006.Num.sg } = ""
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.voc, num := Stump2006.Num.sg } = "e"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.loc, num := Stump2006.Num.sg } = "ě"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.ins, num := Stump2006.Num.sg } = "em"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.nom, num := Stump2006.Num.pl } = "y"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.gen, num := Stump2006.Num.pl } = "ů"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.dat, num := Stump2006.Num.pl } = "ům"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.acc, num := Stump2006.Num.pl } = "y"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.voc, num := Stump2006.Num.pl } = "y"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.loc, num := Stump2006.Num.pl } = "ech"
• Stump2006.ending Stump2006.Decl.hardMasc { case := Stump2006.Case.ins, num := Stump2006.Num.pl } = "y"

def Stump2006.czRealize (z : CzStem) (σ : CzCell) : String

Realization of a form cell: the stem's form plus its own declension's ending — realization rules "are sensitive to a stem's inflection-class membership" ([stump-2006] §3.1).

Equations

• Stump2006.czRealize z σ = z.form ++ Stump2006.ending z.decl σ

def Stump2006.table1 : CzNoun → CzCell → String

Table 1's forms, transcribed verbatim.

Equations

• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.nom, num := Stump2006.Num.sg } = "pokoj"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.gen, num := Stump2006.Num.sg } = "pokoje"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.dat, num := Stump2006.Num.sg } = "pokoji"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.acc, num := Stump2006.Num.sg } = "pokoj"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.voc, num := Stump2006.Num.sg } = "pokoji"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.loc, num := Stump2006.Num.sg } = "pokoji"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.ins, num := Stump2006.Num.sg } = "pokojem"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.nom, num := Stump2006.Num.pl } = "pokoje"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.gen, num := Stump2006.Num.pl } = "pokojů"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.dat, num := Stump2006.Num.pl } = "pokojům"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.acc, num := Stump2006.Num.pl } = "pokoje"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.voc, num := Stump2006.Num.pl } = "pokoje"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.loc, num := Stump2006.Num.pl } = "pokojích"
• Stump2006.table1 Stump2006.CzNoun.pokoj { case := Stump2006.Case.ins, num := Stump2006.Num.pl } = "pokoji"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.nom, num := Stump2006.Num.sg } = "most"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.gen, num := Stump2006.Num.sg } = "mostu"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.dat, num := Stump2006.Num.sg } = "mostu"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.acc, num := Stump2006.Num.sg } = "most"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.voc, num := Stump2006.Num.sg } = "moste"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.loc, num := Stump2006.Num.sg } = "mostě"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.ins, num := Stump2006.Num.sg } = "mostem"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.nom, num := Stump2006.Num.pl } = "mosty"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.gen, num := Stump2006.Num.pl } = "mostů"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.dat, num := Stump2006.Num.pl } = "mostům"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.acc, num := Stump2006.Num.pl } = "mosty"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.voc, num := Stump2006.Num.pl } = "mosty"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.loc, num := Stump2006.Num.pl } = "mostech"
• Stump2006.table1 Stump2006.CzNoun.most { case := Stump2006.Case.ins, num := Stump2006.Num.pl } = "mosty"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.nom, num := Stump2006.Num.sg } = "pramen"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.gen, num := Stump2006.Num.sg } = "pramene"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.dat, num := Stump2006.Num.sg } = "prameni"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.acc, num := Stump2006.Num.sg } = "pramen"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.voc, num := Stump2006.Num.sg } = "prameni"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.loc, num := Stump2006.Num.sg } = "prameni"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.ins, num := Stump2006.Num.sg } = "pramenem"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.nom, num := Stump2006.Num.pl } = "prameny"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.gen, num := Stump2006.Num.pl } = "pramenů"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.dat, num := Stump2006.Num.pl } = "pramenům"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.acc, num := Stump2006.Num.pl } = "prameny"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.voc, num := Stump2006.Num.pl } = "prameny"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.loc, num := Stump2006.Num.pl } = "pramenech"
• Stump2006.table1 Stump2006.CzNoun.pramen { case := Stump2006.Case.ins, num := Stump2006.Num.pl } = "prameny"

theorem Stump2006.realize_matches_table1 (n : CzNoun) (σ : CzCell) : czLinkage.realize czRealize n σ = {(table1 n σ, σ)}

The default-plus-override linkage reproduces every form of Table 1.

theorem Stump2006.soft_hard_contrast : ending Decl.softMasc { case := Case.gen, num := Num.sg } ≠ ending Decl.hardMasc { case := Case.gen, num := Num.sg }

The two declensions ordinarily contrast — no case/number cell has them merely notational variants across the whole ending inventory, and e.g. the genitive singular separates them outright. PRAMEN's split is therefore detectable ([stump-2006] on POKOJ vs MOST vs PRAMEN).

theorem Stump2006.pramen_heteroclite : czLinkage.IsHeteroclite CzStem.decl

PRAMEN is heteroclite: its correspondents draw on both declensions ([stump-2006] Table 1, rule (14)).

theorem Stump2006.heteroclisis_without_form_suppletion : czLinkage.InvariantAlong CzStem.form ∧ czLinkage.IsHeteroclite CzStem.decl

Heteroclisis without form suppletion: the linkage is invariant along the form projection — every lexeme's stems are phonologically constant — yet heteroclite along the class projection. Form-invariance and class-invariance are independent ([stump-2006] fn. 5, against reading the No Blur Principle as excluding class-only stem alternants).

theorem Stump2006.pramen_stem_alternation : czLinkage.IsSuppletive

The entailment instance: PRAMEN's class split makes the linkage suppletive in the broad sense — two stems — even though no form alternation is audible, [stump-2006]'s "a kind of stem alternation".

Sanskrit HR̥D(AYA): heteroclisis riding on stem suppletion (Table 4)

Direct cases (nominative, vocative, accusative) are built on hr̥daya, oblique cases on hr̥d; the a-stem hr̥daya follows the neuter a-stem declension, the consonant-stem hr̥d the neuter consonant-stem declension. Cells are abstracted to the direct/oblique split the prose states.

inductive Stump2006.CaseClass : Type

The direct/oblique case-class split.

• direct : CaseClass
• oblique : CaseClass

@[instance_reducible]

instance Stump2006.instDecidableEqCaseClass : DecidableEq CaseClass

Equations

• Stump2006.instDecidableEqCaseClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeCaseClass : Fintype CaseClass

Equations

• Stump2006.instFintypeCaseClass = { elems := { val := ↑Stump2006.CaseClass.enumList, nodup := Stump2006.CaseClass.enumList_nodup }, complete := Stump2006.instFintypeCaseClass._proof_1 }

def Stump2006.instReprCaseClass.repr : CaseClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Stump2006.instReprCaseClass.repr Stump2006.CaseClass.direct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.CaseClass.direct")).group prec✝

@[instance_reducible]

instance Stump2006.instReprCaseClass : Repr CaseClass

Equations

• Stump2006.instReprCaseClass = { reprPrec := Stump2006.instReprCaseClass.repr }

inductive Stump2006.SktDecl : Type

The two Sanskrit neuter declensions involved.

• aStem : SktDecl
• consStem : SktDecl

@[instance_reducible]

instance Stump2006.instDecidableEqSktDecl : DecidableEq SktDecl

Equations

• Stump2006.instDecidableEqSktDecl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeSktDecl : Fintype SktDecl

Equations

• Stump2006.instFintypeSktDecl = { elems := { val := ↑Stump2006.SktDecl.enumList, nodup := Stump2006.SktDecl.enumList_nodup }, complete := Stump2006.instFintypeSktDecl._proof_1 }

@[instance_reducible]

instance Stump2006.instReprSktDecl : Repr SktDecl

Equations

• Stump2006.instReprSktDecl = { reprPrec := Stump2006.instReprSktDecl.repr }

def Stump2006.instReprSktDecl.repr : SktDecl → ℕ → Std.Format

Equations

• Stump2006.instReprSktDecl.repr Stump2006.SktDecl.aStem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.SktDecl.aStem")).group prec✝
• Stump2006.instReprSktDecl.repr Stump2006.SktDecl.consStem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.SktDecl.consStem")).group prec✝

inductive Stump2006.SktStem : Type

HR̥D(AYA)'s two suppletive stems.

• hrdaya : SktStem
• hrd : SktStem

@[instance_reducible]

instance Stump2006.instDecidableEqSktStem : DecidableEq SktStem

Equations

• Stump2006.instDecidableEqSktStem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeSktStem : Fintype SktStem

Equations

• Stump2006.instFintypeSktStem = { elems := { val := ↑Stump2006.SktStem.enumList, nodup := Stump2006.SktStem.enumList_nodup }, complete := Stump2006.instFintypeSktStem._proof_1 }

def Stump2006.instReprSktStem.repr : SktStem → ℕ → Std.Format

Equations

• Stump2006.instReprSktStem.repr Stump2006.SktStem.hrdaya prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.SktStem.hrdaya")).group prec✝
• Stump2006.instReprSktStem.repr Stump2006.SktStem.hrd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.SktStem.hrd")).group prec✝

@[instance_reducible]

instance Stump2006.instReprSktStem : Repr SktStem

Equations

• Stump2006.instReprSktStem = { reprPrec := Stump2006.instReprSktStem.repr }

def Stump2006.SktStem.form : SktStem → String

Stem forms (romanized without diacritics in identifiers; forms carry them).

Equations

• Stump2006.SktStem.hrdaya.form = "hr̥daya"
• Stump2006.SktStem.hrd.form = "hr̥d"

def Stump2006.SktStem.decl : SktStem → SktDecl

Stem class: a-stems decline as a-stems, consonant-stems as consonant-stems ("because hr̥daya is a neuter stem ending in a … because hr̥d is a neuter stem ending in a consonant", [stump-2006] on Table 4).

Equations

• Stump2006.SktStem.hrdaya.decl = Stump2006.SktDecl.aStem
• Stump2006.SktStem.hrd.decl = Stump2006.SktDecl.consStem

inductive Stump2006.SktNoun : Type

The single lexeme HR̥D(AYA).

• hrdaya : SktNoun

@[instance_reducible]

instance Stump2006.instDecidableEqSktNoun : DecidableEq SktNoun

Equations

• Stump2006.instDecidableEqSktNoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Stump2006.instFintypeSktNoun : Fintype SktNoun

Equations

• Stump2006.instFintypeSktNoun = { elems := { val := ↑Stump2006.SktNoun.enumList, nodup := Stump2006.SktNoun.enumList_nodup }, complete := Stump2006.instFintypeSktNoun._proof_1 }

def Stump2006.instReprSktNoun.repr : SktNoun → ℕ → Std.Format

Equations

• Stump2006.instReprSktNoun.repr Stump2006.SktNoun.hrdaya prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stump2006.SktNoun.hrdaya")).group prec✝

@[instance_reducible]

instance Stump2006.instReprSktNoun : Repr SktNoun

Equations

• Stump2006.instReprSktNoun = { reprPrec := Stump2006.instReprSktNoun.repr }

def Stump2006.sktLinkage : Morphology.Linkage SktNoun SktStem CaseClass

The suppletive linkage: direct cells on hr̥daya, oblique on hr̥d.

Equations

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

theorem Stump2006.hrd_heteroclite_and_form_suppletive : sktLinkage.IsHeteroclite SktStem.decl ∧ ¬sktLinkage.InvariantAlong SktStem.form

HR̥D(AYA) occupies the doubly-deviant grid cell: heteroclite and form-suppletive — "it is because of this stem suppletion that the paradigm of HR̥D(AYA) is heteroclite" ([stump-2006] on Table 4). Contrast PRAMEN, heteroclite with constant form.