Taos verbal agreement prefixes

The Taos (Kiowa-Tanoan, Northern Tiwa) verb carries a prefix that agrees with up to three arguments, the agent, the goal and the object, linearized in that order ([Wat84]). Persons are first, second and third; the agreement categories are singular, dual, plural and inverse (Number.Inverse.Category), the last being what a D head shows when its inherent and natural number value one feature both ways ([Har11]). Objects in the paradigm are third person, the dummy object no, or a reflexive. The complete paradigm is Table 3 of the online appendix to [Mid26], from [KK87] as corroborated by [Har16d], transcribed here cell by cell; form looks a cell up.

Main declarations

• Taos.Cell, Taos.prefixes, Taos.form: the paradigm and its lookup.
• Taos.classI to Taos.classIV: the four noun classes by inherent number, with the agreement category each shows for each natural number (Taos.classI_category and kin, the appendix's Table 21).

Implementation notes

• Forms are given as the appendix prints them, with acute for high tone, circumflex for falling tone and an ogonek for nasalization; ∅ is the empty string. A cell with two free variants (ku ~ mây) has two rows, and form returns the first.
• The appendix's Table 3 lists reflexive objects for the one-argument prefixes only; the reflexives of possessive and ditransitive prefixes appear in its Table 16 and are not transcribed here.
• Rows whose label spans several numbers in the source (a bare person, or 1s/d) are expanded to one row per cell; the cells two such labels both cover (1 3i and 1i 3, 3 3i and 3i 3) appear once.

References

• J. Middleton, A remark on the ordering of impoverishment rules: differences between Taos and Basque
• C. Kontak and J. Kunkel, Grammar sketch of Northern Tiwa, Taos dialect
• J. P. Harrington, The ethnogeography of the Tewa Indians
• D. Harbour, Valence and atomic number
• D. Harbour, The Kiowa case for feature insertion
• L. J. Watkins, A grammar of Kiowa

@[reducible, inline]

abbrev Taos.Argument : Type

An agent or goal: its person and agreement category.

Equations

• Taos.Argument = (Person × Number.Inverse.Category)

inductive Taos.Object : Type

The object a prefix agrees with: the dummy object no, a third person object of some category, or a reflexive.

• dummy : Object
• third (n : Number.Inverse.Category) : Object
• reflexive : Object

def Taos.instDecidableEqObject.decEq (x✝ x✝¹ : Object) : Decidable (x✝ = x✝¹)

Equations

• Taos.instDecidableEqObject.decEq Taos.Object.dummy Taos.Object.dummy = isTrue ⋯
• Taos.instDecidableEqObject.decEq Taos.Object.dummy (Taos.Object.third n) = isFalse ⋯
• Taos.instDecidableEqObject.decEq Taos.Object.dummy Taos.Object.reflexive = isFalse Taos.instDecidableEqObject.decEq._proof_4
• Taos.instDecidableEqObject.decEq (Taos.Object.third n) Taos.Object.dummy = isFalse ⋯
• Taos.instDecidableEqObject.decEq (Taos.Object.third a) (Taos.Object.third b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Taos.instDecidableEqObject.decEq (Taos.Object.third n) Taos.Object.reflexive = isFalse ⋯
• Taos.instDecidableEqObject.decEq Taos.Object.reflexive Taos.Object.dummy = isFalse Taos.instDecidableEqObject.decEq._proof_8
• Taos.instDecidableEqObject.decEq Taos.Object.reflexive (Taos.Object.third n) = isFalse ⋯
• Taos.instDecidableEqObject.decEq Taos.Object.reflexive Taos.Object.reflexive = isTrue ⋯

@[instance_reducible]

instance Taos.instDecidableEqObject : DecidableEq Object

Equations

• Taos.instDecidableEqObject = Taos.instDecidableEqObject.decEq

@[instance_reducible]

instance Taos.instReprObject : Repr Object

Equations

• Taos.instReprObject = { reprPrec := Taos.instReprObject.repr }

def Taos.instReprObject.repr : Object → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Taos.instReprObject.repr Taos.Object.dummy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Taos.Object.dummy")).group prec✝
• Taos.instReprObject.repr Taos.Object.reflexive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Taos.Object.reflexive")).group prec✝

structure Taos.Cell : Type

A cell of the paradigm: the agent, the goal and the object, each possibly absent.

• agent : Option Argument

  The agent.

• goal : Option Argument

  The goal.

• object : Option Object

  The object.

def Taos.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Taos.instDecidableEqCell : DecidableEq Cell

Equations

• Taos.instDecidableEqCell = Taos.instDecidableEqCell.decEq

@[instance_reducible]

instance Taos.instReprCell : Repr Cell

Equations

• Taos.instReprCell = { reprPrec := Taos.instReprCell.repr }

def Taos.instReprCell.repr : Cell → ℕ → Std.Format

Equations

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

def Taos.prefixes : List (Cell × String)

The paradigm, Table 3 of the appendix to [Mid26].

Equations

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

def Taos.form (c : Cell) : Option String

The prefix of a cell.

Equations

• Taos.form c = List.lookup c Taos.prefixes

Noun classes

The four classes by inherent number ([Har03a], [Har11]; appendix Table 21): 'one or two', 'two or more', 'two', and 'any number'.

def Taos.classI : Number.Inverse.Valuation

Class I, inherently [+minimal]: 'one or two'.

Equations

• Taos.classI = { atomic := ∅, minimal := {true} }

def Taos.classII : Number.Inverse.Valuation

Class II, inherently [−atomic]: 'two or more'.

Equations

• Taos.classII = { atomic := {false}, minimal := ∅ }

def Taos.classIII : Number.Inverse.Valuation

Class III, inherently [−atomic +minimal]: 'two'.

Equations

• Taos.classIII = { atomic := {false}, minimal := {true} }

def Taos.classIV : Number.Inverse.Valuation

Class IV, with no inherent number: 'any number'.

Equations

• Taos.classIV = ∅

theorem Taos.classI_category : (classI.agree (Number.Inverse.Valuation.ofNumber Number.singular)).category = some Number.Inverse.Category.singular ∧ (classI.agree (Number.Inverse.Valuation.ofNumber Number.dual)).category = some Number.Inverse.Category.dual ∧ (classI.agree (Number.Inverse.Valuation.ofNumber Number.plural)).category = some Number.Inverse.Category.inverse

Class I agrees singular, dual, inverse for one, two, and more referents.

theorem Taos.classII_category : (classII.agree (Number.Inverse.Valuation.ofNumber Number.singular)).category = some Number.Inverse.Category.inverse ∧ (classII.agree (Number.Inverse.Valuation.ofNumber Number.dual)).category = some Number.Inverse.Category.dual ∧ (classII.agree (Number.Inverse.Valuation.ofNumber Number.plural)).category = some Number.Inverse.Category.plural

Class II agrees inverse, dual, plural.

theorem Taos.classIII_category : (classIII.agree (Number.Inverse.Valuation.ofNumber Number.singular)).category = some Number.Inverse.Category.inverse ∧ (classIII.agree (Number.Inverse.Valuation.ofNumber Number.dual)).category = some Number.Inverse.Category.dual ∧ (classIII.agree (Number.Inverse.Valuation.ofNumber Number.plural)).category = some Number.Inverse.Category.inverse

Class III agrees inverse, dual, inverse.

theorem Taos.classIV_category : (classIV.agree (Number.Inverse.Valuation.ofNumber Number.singular)).category = some Number.Inverse.Category.singular ∧ (classIV.agree (Number.Inverse.Valuation.ofNumber Number.dual)).category = some Number.Inverse.Category.dual ∧ (classIV.agree (Number.Inverse.Valuation.ofNumber Number.plural)).category = some Number.Inverse.Category.plural

Class IV agrees as its natural number.

theorem Taos.dual_le_inverse (c : Number.Inverse.Valuation) : c ∈ [classI, classII, classIII, classIV] → ∀ n ∈ [Number.singular, Number.dual, Number.plural], (c.agree (Number.Inverse.Valuation.ofNumber n)).IsInverse → (Number.Inverse.Valuation.ofNumber Number.dual).atomic ⊆ (c.agree (Number.Inverse.Valuation.ofNumber n)).atomic ∧ (Number.Inverse.Valuation.ofNumber Number.dual).minimal ⊆ (c.agree (Number.Inverse.Valuation.ofNumber n)).minimal

Every inverse valuation of Table 21 contains the dual's values: the dual's features are a proper part of the inverse's.