Taos Verbal Agreement Fragment

[KK87] [Wat84] [Har16c] [Har14a] [Har16a] [Mid26]

Taos (Kiowa-Tanoan, Northern Tiwa) verbal agreement prefixes index up to three arguments — agent (A), goal (G), object (O) — linearized in that order [Wat84]. The prefix decomposes into person and number morphemes whose exponence and ordering are described by [Mid26] (building on [Har03], [Har08], [Har11], [Har14a]).

This fragment provides only the morpheme inventory and a representation of agreement prefixes as FeatureBundle lists. The postsyntactic rules of impoverishment and metathesis that derive the surface forms — and the theorems about ordering — live in Studies/Middleton2026.lean.

Person and Number Features (Harbour)

Number features are [±atomic] and [±minimal] ([Har14a]); person features are [±participant] and [±author] ([Har16a]). Their denotations on Taos:

• singular s = [+atomic +minimal]
• dual d = [−atomic +minimal]
• plural p = [−atomic −minimal]
• 1 = [+participant +author]
• 2 = [+participant −author]
• 3 = [−participant −author]

(Following [Mid26] fn. 4, [−atomic] is used in place of A&N's [−singular] for direct compatibility with [Har14a].)

inductive Taos.Agreement.ArgRole : Type

Argument position in a Taos verbal prefix. The linearization is A G O (agent, goal, object) per [Wat84].

• agent : ArgRole
• goal : ArgRole
• object : ArgRole

@[implicit_reducible]

instance Taos.Agreement.instDecidableEqArgRole : DecidableEq ArgRole

Equations

• Taos.Agreement.instDecidableEqArgRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Taos.Agreement.instReprArgRole : Repr ArgRole

Equations

• Taos.Agreement.instReprArgRole = { reprPrec := Taos.Agreement.instReprArgRole.repr }

def Taos.Agreement.instReprArgRole.repr : ArgRole → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Taos.Agreement.fAtomic (b : Bool) : Minimalist.FeatureVal

A [±atomic] feature ([Har14a]).

Equations

• Taos.Agreement.fAtomic b = Minimalist.FeatureVal.atomic b

@[reducible, inline]

abbrev Taos.Agreement.fMinimal (b : Bool) : Minimalist.FeatureVal

A [±minimal] feature ([Har14a]).

Equations

• Taos.Agreement.fMinimal b = Minimalist.FeatureVal.minimal b

@[reducible, inline]

abbrev Taos.Agreement.fParticipant (b : Bool) : Minimalist.FeatureVal

A [±participant] feature ([Har16a]).

Equations

• Taos.Agreement.fParticipant b = Minimalist.FeatureVal.participant b

@[reducible, inline]

abbrev Taos.Agreement.fAuthor (b : Bool) : Minimalist.FeatureVal

A [±author] feature ([Har16a]).

Equations

• Taos.Agreement.fAuthor b = Minimalist.FeatureVal.author b

def Taos.Agreement.person1 : List Minimalist.FeatureVal

1st person bundle: [+participant +author].

Equations

• Taos.Agreement.person1 = [Taos.Agreement.fParticipant true, Taos.Agreement.fAuthor true]

def Taos.Agreement.person2 : List Minimalist.FeatureVal

2nd person bundle: [+participant −author].

Equations

• Taos.Agreement.person2 = [Taos.Agreement.fParticipant true, Taos.Agreement.fAuthor false]

def Taos.Agreement.person3 : List Minimalist.FeatureVal

3rd person bundle: [−participant −author].

Equations

• Taos.Agreement.person3 = [Taos.Agreement.fParticipant false, Taos.Agreement.fAuthor false]

def Taos.Agreement.numSg : List Minimalist.FeatureVal

Singular: [+atomic +minimal].

Equations

• Taos.Agreement.numSg = [Taos.Agreement.fAtomic true, Taos.Agreement.fMinimal true]

def Taos.Agreement.numDu : List Minimalist.FeatureVal

Dual: [−atomic +minimal].

Equations

• Taos.Agreement.numDu = [Taos.Agreement.fAtomic false, Taos.Agreement.fMinimal true]

def Taos.Agreement.numPl : List Minimalist.FeatureVal

Plural: [−atomic −minimal].

Equations

• Taos.Agreement.numPl = [Taos.Agreement.fAtomic false, Taos.Agreement.fMinimal false]

def Taos.Agreement.argBundle (person number : List Minimalist.FeatureVal) : Minimalist.FeatureBundle

An argument bundle = its person features then its number features, aligned per the Taos ordering convention [±part]:[±auth]:[±atom]:[±min] ([Mid26] ex. 4 and 5).

Equations

• Taos.Agreement.argBundle person number = Minimalist.FeatureBundle.ofGramFeatures (List.map Minimalist.GramFeature.valued (person ++ number))

def Taos.Agreement.prefix_1s3i_possessive_goal : Minimalist.FeatureBundle

The 1s:3i possessive prefix tó — the case in §4.2.5 where a paradigmatic rule must precede a syntagmatic one. Goal is 1s, object is 3i (3rd inverse). The agent slot is empty in possessive prefixes.

Equations

• Taos.Agreement.prefix_1s3i_possessive_goal = Taos.Agreement.argBundle Taos.Agreement.person1 Taos.Agreement.numSg

def Taos.Agreement.prefix_1d3p_agent : Minimalist.FeatureBundle

The 1d:3p prefix opénôw — fully-articulated, no impoverishment.

Equations

• Taos.Agreement.prefix_1d3p_agent = Taos.Agreement.argBundle Taos.Agreement.person1 Taos.Agreement.numDu

def Taos.Agreement.prefix_3s_agent : Minimalist.FeatureBundle

The 3s agent (transitive) bundle, the target of paradigmatic rule (35) 3s → ∅ / [[A _] (O)].

Equations

• Taos.Agreement.prefix_3s_agent = Taos.Agreement.argBundle Taos.Agreement.person3 Taos.Agreement.numSg

inductive Taos.Agreement.Morpheme : Type

The Taos morphemes named in [Mid26]. We carry them as strings; vocabulary insertion is not modeled in this fragment (it would require a full DM exponent-competition model). The relevant facts are exponence rules (20–22), (31), (33), (34), (38), (42).

• pé : Morpheme
• n : Morpheme
• o : Morpheme
• m : Morpheme
• k : Morpheme
• mo : Morpheme
• w : Morpheme
• i : Morpheme
• u : Morpheme
• ô : Morpheme

@[implicit_reducible]

instance Taos.Agreement.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Taos.Agreement.instDecidableEqMorpheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Taos.Agreement.instReprMorpheme : Repr Morpheme

Equations

• Taos.Agreement.instReprMorpheme = { reprPrec := Taos.Agreement.instReprMorpheme.repr }

def Taos.Agreement.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

def Taos.Agreement.Morpheme.surface : Morpheme → String

Render a morpheme as its surface form.

Equations

• Taos.Agreement.Morpheme.pé.surface = "pé"
• Taos.Agreement.Morpheme.n.surface = "n"
• Taos.Agreement.Morpheme.o.surface = "o"
• Taos.Agreement.Morpheme.m.surface = "m"
• Taos.Agreement.Morpheme.k.surface = "k"
• Taos.Agreement.Morpheme.mo.surface = "mo"
• Taos.Agreement.Morpheme.w.surface = "w"
• Taos.Agreement.Morpheme.i.surface = "i"
• Taos.Agreement.Morpheme.u.surface = "u"
• Taos.Agreement.Morpheme.ô.surface = "ô"