Smith, Moskal, Xu, Kang and Bobaljik (2019): Case and Number Suppletion in Pronouns

This file formalizes Smith, Moskal, Xu, Kang and Bobaljik's extension of Bobaljik's containment account of suppletion from adjectival degree to pronominal case, over the case hierarchy of Caha, and to pronominal number, over a hierarchy in which the dual contains the plural (Greenberg's Universal 34, the paper's (26)). Each hierarchy is a three-grade containment structure, so Elsewhere insertion over it generates exactly the contiguous patterns and excludes *ABA (generable_iff_contiguous, aba_not_generable); the attested AAA, ABB and ABC patterns are read off the pronoun paradigms of Data/Forms/SmithMoskalEtAl2019 (paradigm, lezgian_aaa, icelandic_abb, russian_abb, awtuw_abb), and the rules (15) for the Icelandic first person generate its ABB (icelandic_abb_generated).

The domains diverge on AAB. Under the structural adjacency Bobaljik assumes for degree, terminal rules with adjacent contexts cannot distinguish the second and third grades, so AAB is unattested for degree (realize_one_eq_two_of_terminal_adjacent, aab_not_generable_of_terminal_adjacent); section 3.6 finds genuine AAB in pronominal case, the absolutive and ergative sharing a base yet remaining distinct where a syncretic {A=A}B pattern would not (wardaman_aab, khinalugh_aab, genuine_aab, archi_syncretic), and section 4.2 finds it in pronominal number (yagua_aab, wambaya_aab, dehu_aab). The paper's section 3.7 replaces adjacency by the accessibility domain of Moskal, the first category-defining node above the root and one node above that: the domain bounds which heads may condition root suppletion (DomainLocal), the plateau reappears for any vocabulary whose conditioning heads lie in a domain (realize_const_of_terminal_domainLocal), terminal adjacency is its smallest nontrivial instance (domainLocal_of_terminal_adjacent), and the rules (20) for Wardaman, local at the trivial domain of a pronoun, generate the attested AAB while containment and the Elsewhere condition still exclude ABA (wardaman_aab_generated, wardaman_realize_contiguous).

Implementation notes

• A paradigm is three rows of the form table in the order of the hierarchy, its cells the base letters the paper's pattern labels assign (Base); the case hierarchy is read as unmarked, dependent and oblique, absolutive, ergative and dative in the ergative languages and nominative, accusative and dative otherwise, and the number hierarchy as singular, plural and dual.
• The paper's counts stay in prose: for case, Table 9 records ABB in fifty-seven languages, ABC in two, AAB in ten and a single doubtful ABA, the Archi second person plural; for number, Table 32 records forty-eight ABB, nineteen ABC, three AAB and one doubtful ABA in Yagua.
• The rules (20) are stated for featural containment and are transposed to the three-cell structural hierarchy of section 3.1; the exponent of the number-and-case portmanteau (20a) and the affixes (20c) to (20e) fall outside the three cells.

References

• [SMX+19]
• [Bob12]
• [Cah09]
• [Mos15b]
• [Mer94]

TODO

Section 4.3's number containment hypothesis, [±augmented] containing [±singular] with the marked value of a feature visible to suppletion, is not formalized; the number hierarchy is the containment of section 4.1.

Paradigms from the form table

def SmithMoskalEtAl2019.baseOf (a : Forms.Analysis) : ℕ

The base class the paper's pattern label assigns a form.

Equations

• SmithMoskalEtAl2019.baseOf a = match a.base with | SmithMoskalEtAl2019.Forms.Base.a => 0 | SmithMoskalEtAl2019.Forms.Base.b => 1

def SmithMoskalEtAl2019.paradigm (a b c : Forms.Analysis) : Morphology.Paradigm 3 ℕ

Three cells in the order of the hierarchy as a paradigm of base classes.

Equations

• SmithMoskalEtAl2019.paradigm a b c = ![SmithMoskalEtAl2019.baseOf a, SmithMoskalEtAl2019.baseOf b, SmithMoskalEtAl2019.baseOf c]

def SmithMoskalEtAl2019.wardaman3sg : Morphology.Paradigm 3 ℕ

Wardaman third singular, absolutive, ergative and dative (Table 25, [Mer94]).

Equations

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

def SmithMoskalEtAl2019.khinalugh2sg : Morphology.Paradigm 3 ℕ

Khinalugh second singular (Table 24).

Equations

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

def SmithMoskalEtAl2019.icelandic1sg : Morphology.Paradigm 3 ℕ

Icelandic first singular, nominative, accusative and dative (Table 6).

Equations

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

def SmithMoskalEtAl2019.russian1sg : Morphology.Paradigm 3 ℕ

Russian first singular (Table 10).

Equations

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

def SmithMoskalEtAl2019.lezgian1sg : Morphology.Paradigm 3 ℕ

Lezgian first singular (Table 11).

Equations

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

def SmithMoskalEtAl2019.awtuw1 : Morphology.Paradigm 3 ℕ

Awtuw first person, singular, plural and dual (Table 33).

Equations

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

def SmithMoskalEtAl2019.yagua2 : Morphology.Paradigm 3 ℕ

Yagua second person (Table 46).

Equations

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

def SmithMoskalEtAl2019.wambaya1incl : Morphology.Paradigm 3 ℕ

Wambaya first inclusive (Table 46).

Equations

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

def SmithMoskalEtAl2019.dehu3m : Morphology.Paradigm 3 ℕ

Dehu third masculine (Table 46).

Equations

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

Containment excludes ABA, sections 3.3 and 4.2

theorem SmithMoskalEtAl2019.generable_iff_contiguous (p : Morphology.Paradigm 3 ℕ) : Morphology.Containment.ElsewhereGenerable p ↔ Morphology.IsContiguous p

Over a three-grade containment hierarchy a pattern is generable by Elsewhere insertion exactly when it is contiguous, for case and for number alike.

theorem SmithMoskalEtAl2019.aba_not_generable : ¬Morphology.Containment.ElsewhereGenerable ![0, 1, 0]

No ABA pattern is generable. This is the reading that excludes the apparent Archi second plural for case and the doubtful Yagua third person for number.

theorem SmithMoskalEtAl2019.lezgian_aaa : Setoid.ker lezgian1sg = Setoid.ker Morphology.Paradigm.aaa

Of the attested patterns of the case hierarchy, Lezgian's is AAA and Icelandic's and Russian's are ABB.

theorem SmithMoskalEtAl2019.icelandic_abb : Setoid.ker icelandic1sg = Setoid.ker Morphology.Paradigm.abb

theorem SmithMoskalEtAl2019.russian_abb : Setoid.ker russian1sg = Setoid.ker Morphology.Paradigm.abb

theorem SmithMoskalEtAl2019.awtuw_abb : Setoid.ker awtuw1 = Setoid.ker Morphology.Paradigm.abb

Awtuw's plural and dual share a base, the attested ABB of the number hierarchy.

def SmithMoskalEtAl2019.icelandicVocab : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule 3 String)

The rules (15) for the Icelandic first singular are an accusative-conditioned m- and an elsewhere ég. By containment the m- base spreads to the dative.

Equations

• SmithMoskalEtAl2019.icelandicVocab = [{ exponent := "ég", spans := 0, context := none }, { exponent := "m", spans := 0, context := some 1 }]

theorem SmithMoskalEtAl2019.icelandic_abb_generated : Setoid.ker (Morphology.Containment.realize icelandicVocab) = Setoid.ker Morphology.Paradigm.abb

Structural adjacency and the absence of AAB for degree, section 2

theorem SmithMoskalEtAl2019.realize_one_eq_two_of_terminal_adjacent {v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule 3 ℕ)} (hT : Morphology.Containment.Terminal v) (hA : Morphology.Containment.Adjacent v) : Morphology.Containment.realize v 1 = Morphology.Containment.realize v 2

Under [Bob12]'s structural adjacency, terminal rules with adjacent contexts cannot distinguish the second grade from the third.

theorem SmithMoskalEtAl2019.aab_not_generable_of_terminal_adjacent {v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule 3 ℕ)} (hT : Morphology.Containment.Terminal v) (hA : Morphology.Containment.Adjacent v) {a b : ℕ} (hab : a ≠ b) : Morphology.Containment.realize v ≠ ![some a, some a, some b]

So no AAB pattern is generable under structural adjacency.

AAB attested for case, section 3.6, and for number, section 4.2

theorem SmithMoskalEtAl2019.wardaman_aab : Setoid.ker wardaman3sg = Setoid.ker Morphology.Paradigm.aab

Wardaman and Khinalugh are AAB, contiguous with the third cell alone suppletive.

theorem SmithMoskalEtAl2019.khinalugh_aab : Setoid.ker khinalugh2sg = Setoid.ker Morphology.Paradigm.aab

theorem SmithMoskalEtAl2019.genuine_aab : Forms.wardaman_3sg_abs.form ≠ Forms.wardaman_3sg_erg.form ∧ Forms.khinalugh_2sg_abs.form ≠ Forms.khinalugh_2sg_erg.form

The Wardaman and Khinalugh AAB is genuine rather than syncretism, since the absolutive and ergative are distinct forms on one base, where the Archi second singular's are identical, the {A=A}B of Table 20 the paper sets aside as a two-way contrast.

theorem SmithMoskalEtAl2019.archi_syncretic : Forms.archi_2sg_abs.form = Forms.archi_2sg_erg.form

theorem SmithMoskalEtAl2019.yagua_aab : Setoid.ker yagua2 = Setoid.ker Morphology.Paradigm.aab

The number witnesses of Table 46 are AAB.

theorem SmithMoskalEtAl2019.wambaya_aab : Setoid.ker wambaya1incl = Setoid.ker Morphology.Paradigm.aab

theorem SmithMoskalEtAl2019.dehu_aab : Setoid.ker dehu3m = Setoid.ker Morphology.Paradigm.aab

theorem SmithMoskalEtAl2019.aab_contiguous_not_adjacent_generable : Morphology.IsContiguous wardaman3sg ∧ Morphology.IsContiguous yagua2 ∧ ∀ (v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule 3 ℕ)), Morphology.Containment.Terminal v → Morphology.Containment.Adjacent v → Morphology.Containment.realize v ≠ ![some 0, some 0, some 1]

The attested AAB patterns are contiguous, so containment admits them, yet no terminal vocabulary under structural adjacency generates them, so the pronominal data refute the adjacency condition.

Accessibility domains, section 3.7

Adjacency is too strict: Tamil supplets for the dative across the plural morpheme, so locality may have to appeal to domains rather than adjacency. The accessibility domain of [Mos15b], the heads merged when the root's cycle is fixed, bounds which heads may condition root suppletion; a lexical noun or adjective has a category node that keeps case and the superlative outside the domain, a pronoun has none and every case head is visible.

def SmithMoskalEtAl2019.DomainLocal {n : ℕ} {F : Type u_1} (d : Fin n) (v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule n F)) : Prop

Every conditioning head lies within the accessibility domain [0, d]. This bounds the contexts of rules, not the spans they expone.

Equations

• SmithMoskalEtAl2019.DomainLocal d v = ∀ it ∈ v, ∀ (c : Fin n), it.context = some c → c ≤ d

@[instance_reducible]

instance SmithMoskalEtAl2019.instDecidableDomainLocal {n : ℕ} {F : Type u_1} (d : Fin n) (v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule n F)) : Decidable (DomainLocal d v)

Equations

• SmithMoskalEtAl2019.instDecidableDomainLocal d v = id inferInstance

theorem SmithMoskalEtAl2019.threshold_le_of_terminal_domainLocal {n : ℕ} {F : Type u_1} {d : Fin n} {v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule n F)} (hT : Morphology.Containment.Terminal v) (hD : DomainLocal d v) {it : Morphology.Containment.SpanRule n F} (hit : it ∈ v) : it.threshold ≤ d

Terminal rules local to a domain have thresholds inside it.

theorem SmithMoskalEtAl2019.realize_const_of_terminal_domainLocal {n : ℕ} {F : Type u_1} {d : Fin n} {v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule n F)} (hT : Morphology.Containment.Terminal v) (hD : DomainLocal d v) {g g' : Fin n} (hg : d ≤ g) (hg' : d ≤ g') : Morphology.Containment.realize v g = Morphology.Containment.realize v g'

With terminal rules whose contexts lie in a domain, realization is constant above the domain. At the comparative this is the no-AAB plateau of degree without an adjacency condition.

theorem SmithMoskalEtAl2019.domainLocal_of_terminal_adjacent {n : ℕ} {F : Type u_1} {d : Fin n} (hd : 1 ≤ ↑d) {v : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule n F)} (hT : Morphology.Containment.Terminal v) (hA : Morphology.Containment.Adjacent v) : DomainLocal d v

Terminal adjacency is locality at any domain containing the first head.

def SmithMoskalEtAl2019.wardamanVocab : Morphology.Exponence.RuleSet (Morphology.Containment.SpanRule 3 String)

The rules (20b) and (20f) for the Wardaman third person are a dative-conditioned gunga and an elsewhere narnaj.

Equations

• SmithMoskalEtAl2019.wardamanVocab = [{ exponent := "narnaj", spans := 0, context := none }, { exponent := "gunga", spans := 0, context := some 2 }]

theorem SmithMoskalEtAl2019.wardaman_aab_generated : wardamanVocab.Antihomophonous ∧ DomainLocal 2 wardamanVocab ∧ Setoid.ker (Morphology.Containment.realize wardamanVocab) = Setoid.ker Morphology.Paradigm.aab

The Wardaman vocabulary is antihomophonous and local at the trivial domain of a pronoun, and generates the attested AAB.

theorem SmithMoskalEtAl2019.wardaman_not_adjacent_not_grounded : ¬Morphology.Containment.Adjacent wardamanVocab ∧ ¬Morphology.Containment.Grounded wardamanVocab

The same vocabulary satisfies neither structural adjacency nor [Bob12]'s markedness condition (202), so the attested pronominal AAB refutes both as conditions on suppletion in general.

theorem SmithMoskalEtAl2019.wardaman_realize_contiguous : Morphology.IsContiguous (Morphology.Containment.realize wardamanVocab)

ABA stays excluded at the trivial domain, where containment with the Elsewhere condition suffices.