Documentation

Studies.Stump2006

Stump (2006): Heteroclisis and paradigm linkage #

This file formalizes Stump's account of heteroclisis, the property of a lexeme whose paradigm contains forms built on stems of two or more inflection classes. A rule of paradigm linkage gives a content cell of a lexeme a form correspondent built on one of the lexeme's stems: the universal default assigns the root, and narrower language-specific rules override it by Pāṇini's principle, assigning a coradical, a stem that differs from the root in form or in inflection class. The paper's rules (5), (14), (15), (17) and (18), with the endings of the Czech declension fragment, after Short's tables and the rules of Mluvnice češtiny, realize every form of the Czech nouns in its Tables 1, 6 and 8, read from the forms data, once the masculine a-stems' nominative plural in -ové is read from their own class and FILOSOF's, which neither grammar gives, is supplied. The heteroclisis of Czech PRAMEN is morphosyntactically conditioned, its inflection class fixed by the property sets its cells express, whereas that of Sanskrit AHAN is morphologically conditioned, following a pattern of alternation among Strong, Middle and Weakest stems. Stump's Sanskrit rules of paradigm linkage (20a,b) "are independently motivated by the need to account for the pattern of stem alternation in nonheteroclite paradigms such as the masculine and neuter paradigms of PRATYAÑC" (p. 295): one list of rules gives the grades of PRATYAÑC's stems, which share a declension, and the stems of AHAN, which do not. The paper measures how closely a heteroclite paradigm's class boundary follows an inflectional category, and claims that the categories serving as absolute correlates are privileged: every rule of paradigm linkage sensitive to some category is sensitive to a privileged one.

Main definitions #

Main results #

Implementation notes #

A Czech noun's segments are the stem of its entry in the Czech noun fragment, the citation form less the nominative singular ending of its class, so PŘEDSEDA's root and coradical share the segments předsed. A stem's endings are the fragment's endings of its noun in the class that the stem's declension is for the noun's animacy, with the velar vocative singular -u and locative plural -ích and the noun's lexical nominative plural, MUŽ's -i or -ové and FILOLOG's -ové, and the stem is inflected as the fragment inflects it, palatalized before the masculine locative plural -ích and the animate nominative plural -i. Where the paper and the grammars differ the paper's forms stand and the difference is stated: the nominative and vocative plurals in -ové of PŘEDSEDA and SLUHA, realized on the hard-masculine coradical, whose class gives -i, are read from their own class, and FILOSOF's, which neither grammar gives, is an override; Stump's hard-feminine roots for the masculine a-stems rebuild Short's separate hrdina declension; and his soft-masculine coradical of velar stems gives the locative plurals in -ích that Mluvnice češtiny's rule gives the hard-masculine stem. Sanskrit endings are read off exemplars, chosen by declension among PRATYAÑC, NĀMAN and MANAS. Rules compete by domain inclusion, the rendering of Pāṇini's principle, and selection falls back on the root, by (5) and (12). Gender is taken as lexical: PRATYAÑC's masculine and neuter are two lexemes, clause (ii) of f₁ is vacuous, and the feminine, whose ī-stem pratīcī (n. 18) would make PRATYAÑC heteroclite, is left out, as are n. 21's stem indexing and n. 22's alternants. Sanskrit sandhi (aho-bhis, pratyag-) is unstated, so no forms are built. Rows are filtered by language.

References #

Cells and the attested forms #

@[reducible, inline]

A content cell of a Czech noun is a cell of Short's declension tables, pairing a case of the Czech inventory with a number, gender being constant within a paradigm.

Equations
Instances For

    The case of a form's cell.

    Equations
    Instances For

      The number of a form's cell.

      Equations
      Instances For

        czForms are the Czech rows of the forms data, those of Tables 1, 6 and 8.

        Equations
        Instances For

          The Czech nouns of Tables 1, 6 and 8 are POKOJ 'room', PRAMEN 'spring', MOST 'bridge', ŽENA 'woman', PŘEDSEDA 'president', FILOSOF 'philosopher', SLUHA 'servant', FILOLOG 'philologist' and MUŽ 'man'.

          Instances For
            @[instance_reducible]
            Equations
            def Stump2006.instReprCzNoun.repr :
            CzNoun → ℕ → Std.Format
            Equations
            Instances For
              @[instance_reducible]
              Equations

              l.paramId is the concept that the forms of l express in the forms data.

              Equations
              Instances For
                def Stump2006.attested (l : CzNoun) (σ : CzCell) :
                Finset (List String)

                The attested forms of a cell are the segments of every row of the forms data for the noun whose case code decodes to the comparative value of the cell's case and whose number code to its number, so a cell with two alternants has two.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Stump2006.attested_nonempty (l : CzNoun) (σ : CzCell) :
                  (attested l σ).Nonempty

                  Every cell has an attested form, so no statement about the attested forms holds for want of a row.

                  FILOSOF's dative singular has two alternants, filosofovi and filosofu.

                  Stems and lexical entries #

                  inductive Stump2006.Decl :

                  The three declensions the tables juxtapose are the soft masculine, the hard masculine and the hard feminine.

                  Instances For
                    @[instance_reducible]
                    instance Stump2006.instDecidableEqDecl :
                    DecidableEq Decl
                    Equations
                    @[instance_reducible]
                    Equations
                    @[instance_reducible]
                    Equations
                    def Stump2006.instReprDecl.repr :
                    Decl → ℕ → Std.Format
                    Equations
                    Instances For

                      A declension is, for animate and for inanimate stems, a declension of Short's tables, the soft masculine being that of muž or stroj, the hard masculine that of chlap or hrad, and the hard feminine that of žena.

                      Equations
                      Instances For
                        theorem Stump2006.Decl.toClass_injective (a : Bool) :
                        Function.Injective fun (x : Decl) => x.toClass a

                        For either animacy, distinct declensions are distinct classes of Short's.

                        Decl.ofClass k is the declension of the root of a noun of Short's class k, where the nouns of the tables include one: the soft masculine for muž and stroj, the hard masculine for chlap and hrad, and the hard feminine for žena and for the masculine a-stems of hrdina, whose roots the paper takes to be hard-feminine.

                        Equations
                        Instances For
                          theorem Stump2006.Decl.ofClass_toClass (d : Decl) (a : Bool) :
                          ofClass (d.toClass a) = some d

                          The root declension of the class a declension is, for either animacy, is that declension.

                          structure Stump2006.Stem :

                          A stem is individuated, as in the paper, by its lexeme and its inflection class; its form is the lexeme's, so two stems of one lexeme are class-distinct and form-identical.

                          • lexeme : CzNoun

                            lexeme is the noun whose stem this is.

                          • decl : Decl

                            decl is the declension the stem inflects in.

                          Instances For
                            def Stump2006.instDecidableEqStem.decEq (x✝ x✝¹ : Stem) :
                            Decidable (x✝ = x✝¹)
                            Equations
                            Instances For
                              def Stump2006.instReprStem.repr :
                              Stem → ℕ → Std.Format
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[instance_reducible]
                                Equations

                                A lexical entry records a noun's stem segments, the declension of its root, whether it inflects as animate, and whether it belongs to the PRAMEN class of rule (14).

                                • lexeme : CzNoun

                                  lexeme is the noun the entry describes.

                                • segments : List String

                                  segments are the segments of the noun's stems.

                                • rootDecl : Decl

                                  rootDecl is the declension of the noun's root.

                                • animate : Bool

                                  animate records whether the noun inflects as animate.

                                • pramenClass : Bool

                                  pramenClass records membership in the PRAMEN class, a lexical stipulation.

                                Instances For
                                  def Stump2006.instDecidableEqEntry.decEq (x✝ x✝¹ : Entry) :
                                  Decidable (x✝ = x✝¹)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[instance_reducible]
                                    Equations
                                    def Stump2006.instReprEntry.repr :
                                    Entry → ℕ → Std.Format
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      entry l is the lexical entry of l, read off its noun. The segments are the noun's stem, the root declension is that of the noun's singular class, so that PRAMEN's root is soft-masculine (p. 289) and PŘEDSEDA's and SLUHA's are hard-feminine, and the noun inflects as animate when its gender is the masculine animate. Membership in the PRAMEN class, which PRAMEN, PŘEDSEDA and SLUHA have, is the lexical stipulation of rule (14).

                                      Equations
                                      Instances For
                                        def Stump2006.Stem.segments (z : Stem) :
                                        List String

                                        The segments of a stem are those of its lexeme's entry.

                                        Equations
                                        Instances For

                                          The root of a noun, its default stem (n. 8), inflects in the root declension.

                                          Equations
                                          Instances For

                                            A stem is a root when it inflects in its lexeme's root declension.

                                            Equations
                                            Instances For

                                              The hard-masculine coradical of a noun of the PRAMEN class is its stem in the hard-masculine declension.

                                              Equations
                                              Instances For

                                                A noun belongs to the PŘEDSEDA subclass, "a subclass of masculine animate members of the PRAMEN class" (p. 290), when it is an animate member of the PRAMEN class.

                                                Equations
                                                Instances For
                                                  @[instance_reducible]
                                                  Equations

                                                  inferSoftMasc is the Czech rule of stem inference (18) (p. 292), which reads "If lexeme L has a stem s belonging to the hard-masculine declension and s ends in a back obstruent, then L has s′ as its soft-masculine coradical, where s′ is like s except that it belongs to the soft-masculine declension." The back obstruents are Short's velars.

                                                  Equations
                                                  Instances For

                                                    The hard-masculine stem of a noun is its root if that is hard-masculine, and otherwise its hard-masculine coradical.

                                                    Equations
                                                    Instances For

                                                      The soft-masculine coradical of a noun is the stem that rule (18) infers from its hard-masculine stem.

                                                      Equations
                                                      Instances For

                                                        Rule (18) supplies a soft-masculine coradical to SLUHA, whose hard-masculine stem is a coradical, and to FILOLOG, whose hard-masculine stem is its root, and to no other noun.

                                                        A hard-masculine coradical is a stem of its own noun.

                                                        A soft-masculine coradical is a stem of its own noun.

                                                        Rules of paradigm linkage #

                                                        @[reducible, inline]

                                                        A rule of paradigm linkage, instantiated for one noun, gives the cells of its domain form correspondents built on its exponent, a stem. Rules are ordered by Pāṇini's principle, by which "competition between two or more morphological markings is resolved in favor of the marking having the narrowest 'meaning'" (n. 5): a rule whose domain is included in another's is the more specific.

                                                        Equations
                                                        Instances For

                                                          plural is the set of plural cells, {plural X} in the paper's notation.

                                                          Equations
                                                          Instances For

                                                            datLocSg is the set of dative and locative singular cells.

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

                                                              locPl is the locative plural cell, {locative plural X} in the paper's notation.

                                                              Equations
                                                              Instances For
                                                                def Stump2006.rule14 (e : Entry) :
                                                                Option CellRule

                                                                Rule (14) (p. 289) reads "Where L is a nominal lexeme that belongs to the PRAMEN class and has s as its hard-masculine coradical, if σ = {plural X}, then the content-cell ⟨L, σ⟩ has ⟨s, σ⟩ as its form-correspondent."

                                                                Equations
                                                                Instances For
                                                                  def Stump2006.rule15 (e : Entry) :
                                                                  Option CellRule

                                                                  Rule (15) (p. 290) reads "Where L is a nominal lexeme that belongs to the PŘEDSEDA subclass and has s as its hard-masculine coradical, if σ = {α singular X} and α = dative or locative, then the content-cell ⟨L, σ⟩ has ⟨s, σ⟩ as its form-correspondent."

                                                                  Equations
                                                                  Instances For
                                                                    def Stump2006.rule17 (e : Entry) :
                                                                    Option CellRule

                                                                    Rule (17) (p. 292) reads "Where L is a nominal lexeme having s as its soft-masculine coradical, if σ = {locative plural X}, then the content-cell ⟨L, σ⟩ has ⟨s, σ⟩ as its form-correspondent."

                                                                    Equations
                                                                    Instances For

                                                                      The language-specific rules of paradigm linkage applying to a noun are those of (14), (15) and (17) whose coradicals and classes the noun has. The universal default (5) is not among them: it is the root that Linkage.ofRules falls back on.

                                                                      Equations
                                                                      Instances For

                                                                        czRules l are the rules of paradigm linkage of the noun l.

                                                                        Equations
                                                                        Instances For

                                                                          czRoot l is the root of l, the stem that rule (5), the universal default rule of paradigm linkage (p. 286), gives every cell that none of the rules of l reaches.

                                                                          Equations
                                                                          Instances For

                                                                            The stem of a cell's form correspondent is the one Pāṇini's principle selects, that of an applicable rule no applicable rule is narrower than, or the root where no rule applies.

                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Stump2006.entry_lexeme (l : CzNoun) :
                                                                              (entry l).lexeme = l

                                                                              Every noun's entry describes that noun.

                                                                              Every rule for a noun assigns a stem of that noun.

                                                                              theorem Stump2006.stemFor_lexeme (l : CzNoun) (σ : CzCell) :
                                                                              (stemFor l σ).lexeme = l

                                                                              A noun's cells are all built on its own stems.

                                                                              Realization #

                                                                              def Stump2006.Stem.classEndings (z : Stem) (σ : CzCell) :
                                                                              List (List String)

                                                                              The endings of a stem at a cell are the fragment's endings of its noun in the class its declension is for the noun's animacy: the class's endings on the noun's stem, a velar stem of the hard masculines taking the vocative singular -u (Short, p. 465; Mluvnice češtiny, p. 292) and a velar stem of the hard masculines or the masculine a-stems the locative plural -ích (Mluvnice češtiny, p. 292), with the noun's lexical nominative plural.

                                                                              Equations
                                                                              Instances For
                                                                                def Stump2006.Stem.tableEndings (z : Stem) (σ : CzCell) :
                                                                                Finset (List String)

                                                                                The endings of a stem at a cell in the fragment are its class endings, less the -u alternating with -ovi, which is "restricted to roots belonging to the hard-masculine declension" (n. 14). The restriction is Stump's, and the fact it derives is Mluvnice češtiny's: "-u mají pouze jména podtypu I.A s tzv. skloňováním tvrdým" '-u is had only by the nouns of subtype I.A, with the so-called hard declension', and "V III. typu má D a L sg podobu jedinou, nevariantní, a to -ovi: předsedovi, husitovi, sluhovi, rikšovi" 'in type III the dative and locative singular have a single, non-variant form, -ovi' (p. 292).

                                                                                Equations
                                                                                Instances For

                                                                                  nomVocPl is the set of nominative and vocative plural cells.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    def Stump2006.classNomPl (l : CzNoun) :
                                                                                    Option (List (List String))

                                                                                    The nominative and vocative plural endings of a noun of the masculine a-declension, read from its own class. PŘEDSEDA and SLUHA take their plural on the hard-masculine coradical, whose class gives chlapi's -i (Short, Table 9.2), but their class gives hrdinové (Short, Table 9.5), and Mluvnice češtiny names the nouns in -a among those with one form, předsed-ové (p. 293).

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Stump2006.nomPlOverride :
                                                                                      CzNoun → Option (List (List String))

                                                                                      The nominative and vocative plural endings of Tables 6 and 8 that neither grammar gives: FILOSOF's -ové. Short's tables leave out the "many formally and semantically distinctive groups with nominative plural in -é or -ové" without placing filosof in one (Short, p. 466), and Mluvnice češtiny gives no plural of filozof, its borrowed compounds in -ové being those in -graf, -fil, -fob and -nom (p. 296).

                                                                                      Equations
                                                                                      Instances For
                                                                                        def Stump2006.suppliedNomPl (l : CzNoun) :
                                                                                        Option (List (List String))

                                                                                        The nominative and vocative plural endings the study supplies beyond the fragment's endings of the stem: those of the noun's own class, and otherwise the override.

                                                                                        Equations
                                                                                        Instances For
                                                                                          def Stump2006.Stem.endings (z : Stem) (σ : CzCell) :
                                                                                          Finset (List String)

                                                                                          The endings of a stem at a cell are those of the fragment, save at the nominative and vocative plural of a noun whose endings there the study supplies, the vocative plural being the nominative (Short, p. 465).

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Stump2006.Stem.inflect (z : Stem) (σ : CzCell) (e : List String) :
                                                                                            List String

                                                                                            A stem is inflected with an ending as the fragment inflects the noun's stem in the stem's class, palatalized before the masculine locative plural -ích and the animate nominative plural -i (Mluvnice češtiny, p. 279). So the soft-masculine coradical of a velar stem palatalizes before -ích, as Short's geolozích (Short, p. 462) and sluzích (Short, p. 467) show.

                                                                                            Equations
                                                                                            Instances For
                                                                                              def Stump2006.czRealize (z : Stem) (σ : CzCell) :
                                                                                              Finset (List String)

                                                                                              The form cell ⟨z, σ⟩ is realized as z inflected with each of its endings.

                                                                                              Equations
                                                                                              Instances For
                                                                                                def Stump2006.czRealizeTable (z : Stem) (σ : CzCell) :
                                                                                                Finset (List String)

                                                                                                The realization by the fragment's endings alone, without the endings the study supplies.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  The Czech paradigm linkage gives each content cell the stem its rules select, and preserves its property set.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    theorem Stump2006.czRealize_stemFor (l : CzNoun) (σ : CzCell) :
                                                                                                    czRealize (stemFor l σ) σ = attested l σ

                                                                                                    Each cell's selected stem realizes exactly the attested forms.

                                                                                                    The rules of paradigm linkage, with the endings of the fragment and those the study supplies, realize every form of Tables 1, 6 and 8.

                                                                                                    theorem Stump2006.czRealizeTable_eq_czRealize {z : Stem} {σ : CzCell} (h : σ ∉ nomVocPl ∨ suppliedNomPl z.lexeme = none) :

                                                                                                    Off the nominative and vocative plural, and for a noun whose endings there the study does not supply, a stem is realized by the fragment's endings alone.

                                                                                                    The study supplies the nominative plural of PŘEDSEDA, SLUHA and FILOSOF alone.

                                                                                                    theorem Stump2006.czRealizeTable_stemFor_iff (l : CzNoun) (σ : CzCell) :
                                                                                                    czRealizeTable (stemFor l σ) σ = attested l σ ↔ σ ∉ nomVocPl ∨ l ≠ CzNoun.predseda ∧ l ≠ CzNoun.sluha ∧ l ≠ CzNoun.filosof

                                                                                                    The fragment's endings alone realize the attested forms at every cell but the nominative and vocative plural of PŘEDSEDA, SLUHA and FILOSOF, where Tables 6 and 8 give -ové: MUŽ's and FILOLOG's nominative plurals are the fragment's.

                                                                                                    theorem Stump2006.coradical_no_u (l : CzNoun) :
                                                                                                    (entry l).InPredsedaSubclass → ∀ σ ∈ datLocSg, czRealize { lexeme := l, decl := Decl.hardMasc } σ = {(entry l).segments ++ ["o", "v", "i"]}

                                                                                                    The hard-masculine coradical of a noun of the PŘEDSEDA subclass realizes the dative and locative singular with -ovi alone, the prediction of n. 14 that předsed and sluh lack the -u alternant. It agrees with Short's hrdinovi (Table 9.5) and his remark that "-ovi is specifically associated with animates" (Short, p. 467), and with Mluvnice češtiny's single form předsedovi, sluhovi (p. 292).

                                                                                                    theorem Stump2006.predseda_eq_hrdina (σ : CzCell) :
                                                                                                    czRealize (stemFor CzNoun.predseda σ) σ = (List.map (fun (x : List String) => Czech.predseda.stem ++ x) (Czech.predseda.cls.endings σ)).toFinset

                                                                                                    PŘEDSEDA's paradigm, derived by rules (14) and (15) from a hard-feminine root and a hard-masculine coradical, is Short's paradigm of the masculine a-stems, hrdina (Table 9.5), on its stem.

                                                                                                    theorem Stump2006.predseda_table_eq_hrdina_iff (σ : CzCell) :
                                                                                                    czRealizeTable (stemFor CzNoun.predseda σ) σ = (List.map (fun (x : List String) => Czech.predseda.stem ++ x) (Czech.predseda.cls.endings σ)).toFinset ↔ σ ∉ nomVocPl

                                                                                                    Without its own class's nominative plural, PŘEDSEDA's paradigm agrees with hrdina's in twelve of its fourteen cells, the nominative and vocative plural of the hard-masculine coradical being chlapi's -i (Short, Table 9.2).

                                                                                                    SLUHA's paradigm is hrdina's on its stem but in the locative plural, where rules (17) and (18) give the palatalized sluzích for the table's -ech.

                                                                                                    Rules (17) and (18), with the second palatalization, give SLUHA's locative plural sluzích, the form both grammars give (Short, p. 467; Mluvnice češtiny, pp. 292, 300). The fragment's rule that a velar stem of the hard masculines takes -ích on the palatalized stem gives SLUHA's hard-masculine coradical the same form, so the form alone does not decide between Stump's route through the soft-masculine coradical and the grammar's rule, which differ in the class the cell inflects in and so in the degrees of correlation.

                                                                                                    Rules (17) and (18), with the second palatalization, give FILOLOG's locative plural filolozích, as Short gives geolozích for geolog 'geologist' (Short, p. 462) and Mluvnice češtiny filolozích itself (p. 295). The fragment's velar rule gives FILOLOG's hard-masculine root the same form.

                                                                                                    Heteroclisis #

                                                                                                    cellClass l σ is the declension that the cell σ of l inflects in.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      PRAMEN is heteroclite, its paradigm drawing on stems of two declensions.

                                                                                                      Exactly PRAMEN, PŘEDSEDA, SLUHA and FILOLOG are heteroclite.

                                                                                                      Every noun's stems share their segments, so the heteroclite nouns alternate between stems that differ in declension alone.

                                                                                                      PRAMEN's paradigm "exhibits a kind of stem suppletion" (pp. 282–283), since its two stems, though phonologically identical, are two stems.

                                                                                                      PRAMEN's class in each cell, as rule (14) assigns it, is the class the fragment gives kořen in that cell's number, stroj in the singular and hrady in the plural (Short, p. 469), Mluvnice češtiny listing kořen and pramen together among the masculines in -en- that decline soft in the singular and hard in the plural (p. 310).

                                                                                                      The degree of correlation #

                                                                                                      def Stump2006.degreeNum {C : Type u_1} {V : Type u_2} {K : Type u_3} [Fintype C] [Fintype V] [Fintype K] [DecidableEq V] [DecidableEq K] (A : C → V) (cls : C → K) :
                                                                                                      ℕ

                                                                                                      degreeNum A cls is the numerator of the degree of A-correlation (p. 309), the sum over the values v of A of "the largest number of cells in P that carry the specification v and inflect as members of the same inflection class".

                                                                                                      Equations
                                                                                                      • Stump2006.degreeNum A cls = ∑ v : V, Finset.univ.sup fun (k : K) => {σ : C | A σ = v ∧ cls σ = k}.card
                                                                                                      Instances For
                                                                                                        theorem Stump2006.degreeNum_le_card {C : Type u_1} {V : Type u_2} {K : Type u_3} [Fintype C] [Fintype V] [Fintype K] [DecidableEq V] [DecidableEq K] (A : C → V) (cls : C → K) :
                                                                                                        degreeNum A cls ≤ Fintype.card C

                                                                                                        The count never exceeds the number of cells.

                                                                                                        theorem Stump2006.degreeNum_eq_card_iff {C : Type u_1} {V : Type u_2} {K : Type u_3} [Fintype C] [Fintype V] [Fintype K] [DecidableEq V] [DecidableEq K] (A : C → V) (cls : C → K) :
                                                                                                        degreeNum A cls = Fintype.card C ↔ Function.FactorsThrough cls A

                                                                                                        The count is the number of cells exactly when the class split factors through the category.

                                                                                                        def Stump2006.degree {C : Type u_1} {V : Type u_2} {K : Type u_3} [Fintype C] [Fintype V] [Fintype K] [DecidableEq V] [DecidableEq K] (A : C → V) (cls : C → K) :
                                                                                                        ℚ

                                                                                                        The degree of A-correlation (p. 309) is the count over the number of cells.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          theorem Stump2006.degree_eq_one_iff {C : Type u_1} {V : Type u_2} {K : Type u_3} [Fintype C] [Fintype V] [Fintype K] [DecidableEq V] [DecidableEq K] [Nonempty C] {A : C → V} {cls : C → K} :
                                                                                                          degree A cls = 1 ↔ Function.FactorsThrough cls A

                                                                                                          The degree is one exactly when the class split factors through the category.

                                                                                                          Correlates of heteroclisis #

                                                                                                          The paper's classification of heteroclite paradigms applies to any cells pairing a case in A with a number in B, and to any class map cls giving the inflection class of each cell.

                                                                                                          The inflectional categories of a noun are number and case.

                                                                                                          Instances For
                                                                                                            @[instance_reducible]
                                                                                                            Equations
                                                                                                            def Stump2006.instReprCategory.repr :
                                                                                                            Category → ℕ → Std.Format
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[instance_reducible]
                                                                                                              Equations
                                                                                                              def Stump2006.Category.proj {A : Type u_1} {B : Type u_2} :
                                                                                                              Category → A × B → A ⊕ B

                                                                                                              c.proj σ is the value of the category c at the cell σ.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                def Stump2006.IsAbsoluteCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} (c : Category) (cls : A × B → K) :

                                                                                                                A category is an absolute correlate of a paradigm's heteroclisis "if and only if the degree of A-correlation in that paradigm is 1.0" (p. 309), that is, when the paradigm's class split factors through the category.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def Stump2006.IsCloven {A : Type u_1} {B : Type u_2} {K : Type u_3} (cls : A × B → K) :

                                                                                                                  A paradigm is cloven when it is heteroclite, two of its cells inflecting in distinct classes, and has an absolute correlate (p. 309).

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    def Stump2006.IsFractured {A : Type u_1} {B : Type u_2} {K : Type u_3} (cls : A × B → K) :

                                                                                                                    A paradigm is fractured when it is heteroclite, two of its cells inflecting in distinct classes, and lacks any absolute correlate (p. 309).

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      theorem Stump2006.cellClass_eq_of_isAbsoluteCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} {cls : A × B → K} (hn : IsAbsoluteCorrelate Category.number cls) (hc : IsAbsoluteCorrelate Category.case cls) (σ τ : A × B) :
                                                                                                                      cls σ = cls τ

                                                                                                                      A class split factoring through both categories is constant.

                                                                                                                      def Stump2006.projOn {A : Type u_1} {B : Type u_2} (S : Finset Category) (σ : A × B) :
                                                                                                                      Option A × Option B

                                                                                                                      projOn S σ records the values at σ of the categories in S.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def Stump2006.IsIntersectiveCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} (cls : A × B → K) (S : Finset Category) :

                                                                                                                        Categories are intersective correlates of a paradigm's heteroclisis when "for each well-formed property set τ specified for exactly the categories A₁, . . . , A_n there is a single inflection class C such that every cell in P realizing τ inflects as a member of C" (p. 313).

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          theorem Stump2006.projOn_eq_of_subset {A : Type u_1} {B : Type u_2} {S T : Finset Category} (hST : S ⊆ T) {σ τ : A × B} (h : projOn T σ = projOn T τ) :
                                                                                                                          projOn S σ = projOn S τ

                                                                                                                          Cells agreeing in more categories agree in fewer.

                                                                                                                          theorem Stump2006.IsIntersectiveCorrelate.mono {A : Type u_1} {B : Type u_2} {K : Type u_3} {cls : A × B → K} {S T : Finset Category} (h : IsIntersectiveCorrelate cls S) (hST : S ⊆ T) :

                                                                                                                          Adding categories to intersective correlates keeps them intersective correlates.

                                                                                                                          theorem Stump2006.isIntersectiveCorrelate_singleton_iff {A : Type u_1} {B : Type u_2} {K : Type u_3} {cls : A × B → K} {c : Category} :

                                                                                                                          A single category is an intersective correlate exactly when it is an absolute one.

                                                                                                                          theorem Stump2006.isIntersectiveCorrelate_univ {A : Type u_1} {B : Type u_2} {K : Type u_3} (cls : A × B → K) :
                                                                                                                          IsIntersectiveCorrelate cls Finset.univ

                                                                                                                          Both categories together are an intersective correlate of every paradigm.

                                                                                                                          theorem Stump2006.minimal_univ_of_isFractured {A : Type u_1} {B : Type u_2} {K : Type u_3} {cls : A × B → K} (h : IsFractured cls) :
                                                                                                                          Minimal (IsIntersectiveCorrelate cls) Finset.univ

                                                                                                                          The minimal intersective correlate of a fractured paradigm is the pair of both categories.

                                                                                                                          def Stump2006.SensitiveTo {A : Type u_1} {B : Type u_2} {E : Type u_5} (r : Morphology.Exponence.DomainRule (A × B) E) (c : Category) :

                                                                                                                          A rule is sensitive to the value of a category when its applicability does not factor through the other category.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def Stump2006.Privileged {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} (cls : L → A × B → K) (c : Category) :

                                                                                                                            A category is privileged for a family cls of class maps, one for each lexeme, when it serves as an absolute correlate of a cloven paradigm: "the inflectional categories serving as absolute correlates of heteroclisis in a given language are PRIVILEGED" (p. 315).

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              def Stump2006.SatisfiesPCR {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} {E : Type u_5} (cls : L → A × B → K) (rules : L → Morphology.Exponence.RuleSet (Morphology.Exponence.DomainRule (A × B) E)) :

                                                                                                                              A system of rules satisfies the privileged category restriction (40) (p. 316), which reads "If a rule of paradigm linkage applies to lexemes belonging to a privileged syntactic category C and this rule is sensitive to the value of any inflectional category, then it is sensitive to the value of a privileged inflectional category for members of C." The lexemes L are taken to form one privileged syntactic category, so the antecedent on the syntactic category is left implicit.

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                def Stump2006.IsMaximalCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Fintype K] [DecidableEq K] (c : Category) (cls : A × B → K) :

                                                                                                                                A category is a maximal correlate when its degree "is higher than any other inflectional category's degree of correlation in that paradigm" (p. 309).

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  theorem Stump2006.isAbsoluteCorrelate_iff_degree {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Fintype K] [DecidableEq K] [Nonempty (A × B)] {c : Category} {cls : A × B → K} :
                                                                                                                                  IsAbsoluteCorrelate c cls ↔ degree c.proj cls = 1

                                                                                                                                  A category is an absolute correlate exactly when its degree of correlation is one.

                                                                                                                                  theorem Stump2006.IsAbsoluteCorrelate.isMaximalCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [Fintype K] [DecidableEq K] {c : Category} {cls : A × B → K} (hl : ∃ (σ : A × B) (τ : A × B), cls σ ≠ cls τ) (h : IsAbsoluteCorrelate c cls) :

                                                                                                                                  An absolute correlate of a heteroclite paradigm is its maximal correlate.

                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableIsAbsoluteCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] (c : Category) (cls : A × B → K) :
                                                                                                                                  Decidable (IsAbsoluteCorrelate c cls)
                                                                                                                                  Equations
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableIsMaximalCorrelate {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] [Fintype K] (c : Category) (cls : A × B → K) :
                                                                                                                                  Decidable (IsMaximalCorrelate c cls)
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableIsCloven {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] (cls : A × B → K) :
                                                                                                                                  Decidable (IsCloven cls)
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableIsFractured {A : Type u_1} {B : Type u_2} {K : Type u_3} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] (cls : A × B → K) :
                                                                                                                                  Decidable (IsFractured cls)
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableSensitiveTo {A : Type u_1} {B : Type u_2} {E : Type u_5} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (r : Morphology.Exponence.DomainRule (A × B) E) (c : Category) :
                                                                                                                                  Decidable (SensitiveTo r c)
                                                                                                                                  Equations
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidablePrivilegedOfFintype {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] [Fintype L] (cls : L → A × B → K) (c : Category) :
                                                                                                                                  Decidable (Privileged cls c)
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  @[instance_reducible]
                                                                                                                                  instance Stump2006.instDecidableSatisfiesPCROfFintype {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} {E : Type u_5} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] [DecidableEq K] [Fintype L] (cls : L → A × B → K) (rules : L → Morphology.Exponence.RuleSet (Morphology.Exponence.DomainRule (A × B) E)) :
                                                                                                                                  Decidable (SatisfiesPCR cls rules)
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.

                                                                                                                                  Correlates of Czech heteroclisis #

                                                                                                                                  PRAMEN's degree of number correlation is 14/14 and its degree of case correlation .50.

                                                                                                                                  PŘEDSEDA's degree of number correlation is .86 (= 12/14) and its degree of case correlation .64.

                                                                                                                                  SLUHA's degree of number correlation is .79 (= 11/14) and its degree of case correlation .57.

                                                                                                                                  FILOLOG's degrees of number and of case correlation are both .93 (= 13/14) (p. 313).

                                                                                                                                  PRAMEN's paradigm is cloven.

                                                                                                                                  PŘEDSEDA's paradigm is fractured.

                                                                                                                                  SLUHA's paradigm is fractured.

                                                                                                                                  FILOLOG's paradigm is fractured.

                                                                                                                                  Number is a maximal correlate of heteroclisis in the fractured paradigms of PŘEDSEDA and SLUHA, as (38) (p. 312) has it: "just as number is the absolute correlate of heteroclisis in the cloven paradigm of Czech PRAMEN, it is likewise the maximal correlate of heteroclisis in the fractured paradigms of PŘEDSEDA and SLUHA."

                                                                                                                                  FILOLOG's fractured paradigm has no maximal correlate (p. 313), so (38), by which maximal correlates of fractured paradigms "tend to be" the absolute correlates of cloven ones, states a tendency.

                                                                                                                                  Rules sensitive to a category #

                                                                                                                                  theorem Stump2006.isAbsoluteCorrelate_of_rules {V : Type u_1} (l : CzNoun) (A : CzCell → V) (h : ∀ r ∈ czRules l, Function.FactorsThrough (Morphology.Exponence.Applies r) A) :
                                                                                                                                  Function.FactorsThrough (fun (σ : CzCell) => (stemFor l σ).decl) A

                                                                                                                                  Rules whose applicability sees only A make a noun's class split factor through A. So by (41a), number "would be an absolute correlate of heteroclisis in the cloven paradigms of type-I verbal lexemes" (p. 317).

                                                                                                                                  A category is an absolute correlate of a noun's paradigm when none of its rules is sensitive to the other category.

                                                                                                                                  Number is an absolute correlate of PRAMEN's heteroclisis because (14), its one language-specific rule, is insensitive to case, as is the default (5).

                                                                                                                                  Number is a maximal correlate of heteroclisis in PRAMEN's paradigm, as of any paradigm it is an absolute correlate of.

                                                                                                                                  The privileged category restriction #

                                                                                                                                  Number is privileged for Czech nouns.

                                                                                                                                  Case is not privileged, for "in Czech, for example, number is the only privileged inflectional category among the categories relevant for nominal inflection" (p. 316).

                                                                                                                                  The Czech rules satisfy (40), since (14) is sensitive to number and (15) and (17), though sensitive to case, are "also sensitive to the value of the privileged inflectional category for nouns" (p. 316).

                                                                                                                                  genitive is the set of genitive cells.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    A hypothetical system adds to the Czech rules one giving the genitive cells of the PŘEDSEDA subclass the hard-masculine coradical, a rule sensitive to case alone. It is modelled on the paper's hypothetical (41) and Table 26, whose type-II rule is sensitive to tense and person but not number; it leaves PRAMEN, and so the privilege of number, untouched.

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

                                                                                                                                      The hypothetical system violates (40), so the restriction is not vacuous.

                                                                                                                                      Claim (39) (p. 313) holds for Czech nouns, every fractured paradigm having a privileged category among its minimal intersective correlates. The claim "is trivially true of fractured paradigms in which only two inflectional categories are distinguished" (p. 313), as here.

                                                                                                                                      Sanskrit cells, stems and form property sets #

                                                                                                                                      @[reducible, inline]
                                                                                                                                      abbrev Stump2006.SktCase :
                                                                                                                                      Finset Case

                                                                                                                                      The Sanskrit cases are the nominative, vocative, accusative, instrumental, dative, ablative, genitive and locative.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible, inline]

                                                                                                                                        The Sanskrit numbers are the singular, the dual and the plural.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[reducible, inline]

                                                                                                                                          A Sanskrit content cell pairs a case with a number, gender being constant within a paradigm.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def Stump2006.SktCell.of (c : Case) (n : Number) (hc : c ∈ SktCase := by decide) (hn : n ∈ SktNumber := by decide) :

                                                                                                                                            SktCell.of c n is the cell of case c and number n.

                                                                                                                                            Equations
                                                                                                                                            Instances For

                                                                                                                                              The genders of the Sanskrit paradigms considered are the masculine and the neuter.

                                                                                                                                              Instances For
                                                                                                                                                @[instance_reducible]
                                                                                                                                                Equations
                                                                                                                                                def Stump2006.instReprSktGender.repr :
                                                                                                                                                SktGender → ℕ → Std.Format
                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  The Sanskrit declensions considered are the neuter a-stem declension of HṚD(AYA)'s hṛdaya (Table 4), the general consonant-stem declension, followed by HṚD(AYA)'s hṛd and by every stem of PRATYAÑC (Table 9), and the neuter an-stem and neuter as-stem declensions (Table 10).

                                                                                                                                                  Instances For
                                                                                                                                                    @[instance_reducible]
                                                                                                                                                    Equations
                                                                                                                                                    def Stump2006.instReprSktDecl.repr :
                                                                                                                                                    SktDecl → ℕ → Std.Format
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[instance_reducible]
                                                                                                                                                      Equations

                                                                                                                                                      A stem is individuated, as in the paper, by its form and the declension it inflects in.

                                                                                                                                                      • form : String

                                                                                                                                                        form is the form of the stem.

                                                                                                                                                      • decl : SktDecl

                                                                                                                                                        decl is the declension the stem inflects in.

                                                                                                                                                      Instances For
                                                                                                                                                        def Stump2006.instDecidableEqSktStem.decEq (x✝ x✝¹ : SktStem) :
                                                                                                                                                        Decidable (x✝ = x✝¹)
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          def Stump2006.instReprSktStem.repr :
                                                                                                                                                          SktStem → ℕ → Std.Format
                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            @[instance_reducible]
                                                                                                                                                            Equations

                                                                                                                                                            A form case is a case or the property [nominative ∨ accusative] that the operator ∨ joins, "such that any rule realizing p or p′ also realizes [p ∨ p′]" (p. 286).

                                                                                                                                                            Instances For
                                                                                                                                                              @[reducible, inline]

                                                                                                                                                              A form property set pairs a form case with a number. It omits gender, which is lexical for the lexemes considered.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                ι σ is the form property set specified exactly as the content property set σ.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  theorem Stump2006.ι_injective :
                                                                                                                                                                  Function.Injective ι

                                                                                                                                                                  Distinct content property sets have distinct identically specified form property sets.

                                                                                                                                                                  The property mapping f₁ g of a lexeme of gender g is (10) (p. 288), which reads "Where α is any gender and β is any oblique case: (i) if σ = {neut nom X} or {neut acc X}, then f₁(σ) = {neut [nom ∨ acc] X}; (ii) if σ = {α β X}, then f₁(σ) = {β X}; (iii) otherwise f₁(σ) = σ." Gender being lexical here and absent from form property sets, clause (ii) is vacuous.

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For

                                                                                                                                                                    Sanskrit HṚD(AYA) (Table 4) #

                                                                                                                                                                    HṚD(AYA) 'heart' is the Sanskrit noun of Table 4.

                                                                                                                                                                    Instances For
                                                                                                                                                                      @[instance_reducible]
                                                                                                                                                                      Equations
                                                                                                                                                                      @[instance_reducible]
                                                                                                                                                                      Equations
                                                                                                                                                                      def Stump2006.instReprSktNoun.repr :
                                                                                                                                                                      SktNoun → ℕ → Std.Format
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                        abbrev Stump2006.direct :
                                                                                                                                                                        Finset Case

                                                                                                                                                                        The direct cases are the nominative, vocative and accusative.

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For

                                                                                                                                                                          hrdStem σ is the stem of the cell σ, since "the direct ... case forms of HṚD(AYA) are built on the stem hṛdaya, while its remaining, oblique case forms are built on the stem hṛd" (p. 282). Its stems' declensions follow their final segments, for "because hṛdaya is a neuter stem ending in a, it follows the neuter a-stem declension ..., but because hṛd is a neuter stem ending in a consonant, it instead follows the neuter consonant-stem declension" (p. 282).

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For

                                                                                                                                                                            hrdLinkage is the paradigm linkage of HṚD(AYA), whose stem alternation "is not the effect of any regular rule of inflectional exponence, but is instead simply stipulated in HṚD(AYA)'s lexical entry" (p. 282). HṚD(AYA) is neuter, and its property sets map by f₁.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For

                                                                                                                                                                              hrdClass σ is the declension that the cell σ of HṚD(AYA) inflects in.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For

                                                                                                                                                                                HṚD(AYA)'s stems also differ in form, its heteroclisis being an effect of stem suppletion, unlike PRAMEN's (segments_invariant).

                                                                                                                                                                                HṚD(AYA)'s paradigm is cloven, as the paper counts it (p. 313), with case as its absolute correlate, for "in Sanskrit, for example, cloven noun paradigms have case as their absolute correlate" (p. 310).

                                                                                                                                                                                Sanskrit stem grades (§3.2) #

                                                                                                                                                                                "In instances of morphosyntactically conditioned heteroclisis, the choice of inflection class in the realization of a paradigm's individual cells is directly determined by the morphosyntactic property sets expressed by those cells; in instances of morphologically conditioned heteroclisis, the choice of inflection class in the realization of a paradigm's individual cells is instead determined by an independently observable pattern of stem alternation" (p. 293). PRAMEN's is of the first sort. In Sanskrit, rules (20a,b) give each cell of an alternating nominal its Strong, Middle or Weakest stem by the strength (19) of its property set and by the ending that follows; they make PRATYAÑC 'westerly' alternate among stems of one declension and AHAN 'day' among stems of two.

                                                                                                                                                                                The grades of an alternating Sanskrit stem are the Strong, the Middle and the Weakest.

                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[instance_reducible]
                                                                                                                                                                                  Equations
                                                                                                                                                                                  @[instance_reducible]
                                                                                                                                                                                  Equations
                                                                                                                                                                                  def Stump2006.instReprGrade.repr :
                                                                                                                                                                                  Grade → ℕ → Std.Format
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[instance_reducible]
                                                                                                                                                                                    Equations

                                                                                                                                                                                    A property set is strong or weak, as (19) defines.

                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[instance_reducible]
                                                                                                                                                                                      Equations
                                                                                                                                                                                      def Stump2006.instReprStrength.repr :
                                                                                                                                                                                      Strength → ℕ → Std.Format
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[instance_reducible]
                                                                                                                                                                                        Equations

                                                                                                                                                                                        Clause (19a) makes strong the direct-case property sets of a masculine and the direct-case plural ones of a neuter.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Clause (19b) makes weak the accusative plural property set of a masculine.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For

                                                                                                                                                                                            Clause (19b) is narrower than (19a), for "because 19b is the more narrowly applicable of the two clauses, it overrides 19a, in accordance with Pāṇini's principle" (n. 19).

                                                                                                                                                                                            The strength of a property set is given by (19) (p. 294), which reads "Where α is masculine or feminine, β is any direct case (nominative, vocative, or accusative), and γ is any number (singular, dual, or plural), a. instances of {α β γ} and {neuter β plural} are strong by default; b. but instances of {α accusative plural} are weak; in addition, c. any gender/case/number combination that is not strong according to (a) is weak." Clause (19b) overrides (19a) by Pāṇini's principle, and (19c) is the default.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              def Stump2006.weak (g : SktGender) :
                                                                                                                                                                                              Finset SktCell

                                                                                                                                                                                              weak g is the set of weak property sets of a lexeme of gender g.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                def Stump2006.SktRow (pid : String) (g : SktGender) (σ : SktCell) (f : Data.Forms.Form Forms.Cell) :
                                                                                                                                                                                                Bool

                                                                                                                                                                                                A Sanskrit row expresses the concept pid in the gender g at the cell σ.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def Stump2006.sktRows (pid : String) (g : SktGender) (σ : SktCell) :

                                                                                                                                                                                                  sktRows pid g σ are the Sanskrit rows expressing the concept pid in the gender g at the cell σ, those of Tables 9 and 10.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    The ending of a row is what follows its stem alternant, nothing for a bare stem.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def Stump2006.SktDecl.exemplar :
                                                                                                                                                                                                      SktDecl → Option String

                                                                                                                                                                                                      d.exemplar is the concept whose rows exemplify the declension d, PRATYAÑC 'westerly' for the general consonant-stem declension and, for the neuter an-stem and as-stem declensions, NĀMAN 'name' and MANAS 'mind', which Table 10 sets beside AHAN. The tables print no a-stem paradigm.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                        The row realizing a form case is that of the case itself, or of the nominative for the join [nominative ∨ accusative], the accusative row agreeing with it (sktEndings_nomAcc).

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          def Stump2006.sktEndings (d : SktDecl) (g : SktGender) (τ : SktForm) :
                                                                                                                                                                                                          List (List String)

                                                                                                                                                                                                          sktEndings d g τ are the endings of the declension d for the gender g at the form property set τ, those of its exemplar's row.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                            The neuter nominative and accusative rows of every exemplar share their endings.

                                                                                                                                                                                                            def Stump2006.sktVowels :
                                                                                                                                                                                                            List String

                                                                                                                                                                                                            sktVowels are the vowels of Sanskrit.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • Stump2006.sktVowels = ["a", "ā", "i", "ī", "u", "ū", "ṛ", "ṝ", "ḷ", "e", "ai", "o", "au"]
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Stump2006.VowelInitial (e : List String) :

                                                                                                                                                                                                              An ending is vowel-initial when its first segment begins with a vowel.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                The lexemes of §3.2 are the adjective PRATYAÑC 'westerly' and the noun AHAN 'day'. PRATYAÑC's masculine and neuter paradigms (Table 9) are indexed separately, gender being lexical for the nouns that share their cells.

                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[instance_reducible]
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  def Stump2006.instReprSktLex.repr :
                                                                                                                                                                                                                  SktLex → ℕ → Std.Format
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[instance_reducible]
                                                                                                                                                                                                                    Equations

                                                                                                                                                                                                                    A lexical entry records a lexeme's gender, its root, the Strong stem, and whichever of a Middle and a Weakest coradical it has, for "some alternating nominals possess only two stems: a Strong stem and a single Weak stem. Others have a Strong stem and two Weak stems" (p. 293).

                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def Stump2006.instDecidableEqSktEntry.decEq (x✝ x✝¹ : SktEntry) :
                                                                                                                                                                                                                      Decidable (x✝ = x✝¹)
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[instance_reducible]
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        def Stump2006.instReprSktEntry.repr :
                                                                                                                                                                                                                        SktEntry → ℕ → Std.Format
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          sktEntry l is the lexical entry of l. PRATYAÑC's root is its Strong stem pratyañc, and pratyac and pratīc are its Middle and Weakest coradicals, all three following "the general consonant-stem declension" (p. 294). For AHAN, "ahan is identified as AHAN's root (= its Strong stem), ahas as its Middle coradical, and ahn as its Weakest coradical", where "ahan and its zero-grade counterpart ahn inflect according to the neuter an-stem declension, while ahas inflects according to the neuter as-stem declension" (p. 295).

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

                                                                                                                                                                                                                            The stems of an entry are its root and its coradicals.

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[reducible, inline]

                                                                                                                                                                                                                              A Sanskrit rule of paradigm linkage gives the cells of its domain form correspondents built on its exponent, a stem.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                Rule (20a) (p. 294) reads "Where L is a nominal lexeme having s_w as its Weakest coradical and σ is a weak property set, if the realization of the form-cell ⟨s_w, f₁(σ)⟩ is s_w[vowel]X, then the content-cell ⟨L, σ⟩ has ⟨s_w, f₁(σ)⟩ as its form-correspondent." Its domain is read off the endings of s_w's declension rather than listed.

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

                                                                                                                                                                                                                                  Rule (20b) (p. 294) reads "If L is a nominal lexeme having s_m as its Middle coradical and σ is a weak property set, then the content-cell ⟨L, σ⟩ has ⟨s_m, f₁(σ)⟩ as its form-correspondent."

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                    The rules (20a,b) that apply to a lexeme are those whose coradicals it has. The Sanskrit default (12) is not among them: it is the root that Exponence.RuleSet.realizeMinimalD falls back on.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                      sktRules l are the rules of paradigm linkage of the lexeme l.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                        sktRoot l is the root of l, the stem that the Sanskrit rule of paradigm linkage (12) (p. 289) gives every cell that no rule of l reaches: "Where L is a nominal lexeme having r as its root, the content-cell ⟨L, σ⟩ has ⟨r, f₁(σ)⟩ as its form-correspondent."

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          The stem of a cell is the one Pāṇini's principle selects, by which "20a will, as the narrower of the two rules, override 20b in any instance in which the former rule is applicable" (p. 295).

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                            The Sanskrit paradigm linkage gives each content cell the stem its rules select, with the form property set that f₁ maps its property set to.

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

                                                                                                                                                                                                                                              The grade of a stem in an entry is weakest for its Weakest coradical, middle for its Middle coradical, and strong for its root.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                grade l σ is the grade of the stem that the rules select at the cell σ of l.

                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  sktClass l σ is the declension that the cell σ of l inflects in.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                    The rules against Tables 9 and 10 #

                                                                                                                                                                                                                                                    l.paramId is the concept that the forms of l express in the forms data.

                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      l.analyses σ are the paper's analyses of the rows of the forms data for the cell σ of l.

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        theorem Stump2006.sktEndings_length (l : SktLex) (σ : SktCell) (z : SktStem) :
                                                                                                                                                                                                                                                        z ∈ (sktEntry l).weakest → (sktEndings z.decl (sktEntry l).gender (f₁ (sktEntry l).gender σ)).length = 1

                                                                                                                                                                                                                                                        Every lexeme's Weakest coradical has one exemplar row at each cell, so the vowel test of (20a) never fails for want of a row.

                                                                                                                                                                                                                                                        theorem Stump2006.rule20a_lt_rule20b (l : SktLex) (a : SktRule) :
                                                                                                                                                                                                                                                        a ∈ rule20a (sktEntry l) → ∀ b ∈ rule20b (sktEntry l), a < b

                                                                                                                                                                                                                                                        Rule (20a) is narrower than (20b) for each lexeme (p. 295).

                                                                                                                                                                                                                                                        theorem Stump2006.rules_match_table9 (l : SktLex) :
                                                                                                                                                                                                                                                        l ∈ [SktLex.pratyancM, SktLex.pratyancN] → ∀ (σ : SktCell), List.map (fun (x : Forms.Analysis) => Option.map gradeOf x.grade) (l.analyses σ) = [some (grade l σ)]

                                                                                                                                                                                                                                                        The rules (19) and (20a,b) give every cell of PRATYAÑC's masculine and neuter paradigms the grade that Table 9 (p. 294) shades it with, each cell having one row.

                                                                                                                                                                                                                                                        theorem Stump2006.rules_match_table10 (σ : SktCell) :
                                                                                                                                                                                                                                                        List.map (fun (x : Forms.Analysis) => x.stem) (SktLex.ahan.analyses σ) = [some (sktStem SktLex.ahan σ).form]

                                                                                                                                                                                                                                                        The rules give every cell of AHAN the stem that Table 10 (p. 296) and p. 295 build it on, each cell having one row.

                                                                                                                                                                                                                                                        Heteroclisis from stem alternation #

                                                                                                                                                                                                                                                        The exponent of a rule of an entry is one of its stems.

                                                                                                                                                                                                                                                        theorem Stump2006.sktStem_mem_stems (l : SktLex) (σ : SktCell) :
                                                                                                                                                                                                                                                        sktStem l σ ∈ (sktEntry l).stems

                                                                                                                                                                                                                                                        Each cell is built on one of its lexeme's stems.

                                                                                                                                                                                                                                                        A lexeme of §3.2 is heteroclite exactly when two of its cells differ in class.

                                                                                                                                                                                                                                                        A lexeme whose stems all follow one declension is not heteroclite.

                                                                                                                                                                                                                                                        Neither of PRATYAÑC's paradigms is heteroclite, since "the coradicals pratyac and pratīc belong to the same declension as the root pratyañc" (p. 318), so that "all of their forms follow the general consonant-stem declension" (p. 294).

                                                                                                                                                                                                                                                        AHAN is heteroclite, since of the three stems its paradigm is built on, "ahan and its zero-grade counterpart ahn inflect according to the neuter an-stem declension, while ahas inflects according to the neuter as-stem declension" (p. 295).

                                                                                                                                                                                                                                                        AHAN's cells have the grades of neuter PRATYAÑC's, though (20a) tests the an-stem endings for the one and the consonant-stem endings for the other: the rules "independently motivated by the need to account for the pattern of stem alternation in nonheteroclite paradigms such as the masculine and neuter paradigms of PRATYAÑC ... also account for the patterns of declension-class alternation exhibited by heteroclite nouns such as AHAN" (p. 295).

                                                                                                                                                                                                                                                        Fourteen of AHAN's cells inflect in the neuter an-stem declension and ten in the neuter as-stem declension.

                                                                                                                                                                                                                                                        AHAN's degree of case correlation is .71 (= 17/24), as Table 21 (p. 312) prints it, and its degree of number correlation, which the paper does not print, is 7/12.

                                                                                                                                                                                                                                                        AHAN's paradigm is fractured, as Table 25 (p. 317) classes it.

                                                                                                                                                                                                                                                        Case is the maximal correlate of AHAN's heteroclisis, as Table 21 (p. 312) has it.

                                                                                                                                                                                                                                                        The property mapping f₁ #

                                                                                                                                                                                                                                                        PRATYAÑC's masculine paradigm preserves property sets, f₁ mapping every masculine property set to its identically specified form property set.

                                                                                                                                                                                                                                                        The nominative and accusative cells of a neuter lexeme share their form correspondents, f₁ joining their property sets and the rules selecting one stem for both.

                                                                                                                                                                                                                                                        The Sanskrit linkage is syncretic, AHAN's nominative and accusative singular sharing their form correspondent.

                                                                                                                                                                                                                                                        The Sanskrit linkage is unfaithful, the nominative singular of a neuter mapping to a form property set with the joined case [nominative ∨ accusative].

                                                                                                                                                                                                                                                        The privileged category restriction in Sanskrit #

                                                                                                                                                                                                                                                        @[reducible, inline]

                                                                                                                                                                                                                                                        The Sanskrit nominals considered are HṚD(AYA) and the lexemes of §3.2.

                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          sktClasses n σ is the declension that the cell σ of the nominal n inflects in.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                            The rules of paradigm linkage of a nominal are those of (20a,b) it instantiates, and none for HṚD(AYA), whose stem alternation is "simply stipulated in HṚD(AYA)'s lexical entry" (p. 282).

                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                              Case is privileged for Sanskrit nominals, "a privileged inflectional category for Sanskrit nouns" (p. 318), as the absolute correlate of HṚD(AYA)'s cloven paradigm.

                                                                                                                                                                                                                                                              Number is not privileged for Sanskrit nominals, since HṚD(AYA)'s absolute correlate is case, PRATYAÑC is not heteroclite and AHAN's paradigm is fractured.

                                                                                                                                                                                                                                                              Rules (20a,b) are sensitive to case, for "in the inflection of Sanskrit PRATYAÑC, the rules 20a,b assigning form-correspondents containing the Middle and Weakest coradicals pratyac and pratīc are sensitive to case, a privileged inflectional category for Sanskrit nouns" (p. 318).

                                                                                                                                                                                                                                                              Rules (20a,b) are sensitive to number as well as to case.

                                                                                                                                                                                                                                                              The Sanskrit rules satisfy (40), since each, though sensitive to number as well, is sensitive to case, which is privileged.

                                                                                                                                                                                                                                                              Russian MAT' (Table 5) #

                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                              abbrev Stump2006.RuNumber :
                                                                                                                                                                                                                                                              Finset Number

                                                                                                                                                                                                                                                              The Russian numbers are the singular and the plural.

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                @[reducible, inline]

                                                                                                                                                                                                                                                                A Russian content cell pairs one of the six cases with a number; the prepositional is the locative.

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  MAT' is the one Russian lexeme considered.

                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    @[instance_reducible]
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    def Stump2006.instReprRuNoun.repr :
                                                                                                                                                                                                                                                                    RuNoun → ℕ → Std.Format
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      @[instance_reducible]
                                                                                                                                                                                                                                                                      Equations

                                                                                                                                                                                                                                                                      MAT' has "a radical stem mat' in the singular direct-case forms and an extended stem mater' elsewhere" (p. 283).

                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        @[instance_reducible]
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        @[instance_reducible]
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        def Stump2006.instReprRuStem.repr :
                                                                                                                                                                                                                                                                        RuStem → ℕ → Std.Format
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                          matLinkage builds MAT' on mat' in the nominative and accusative singular and on mater' elsewhere.

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

                                                                                                                                                                                                                                                                            MAT' is suppletive but not heteroclite, for "suppletion in itself does not necessitate heteroclisis" (p. 283).