Everdell (2023): Arguments and Adjuncts in O'dam, Chapter 5

This file formalizes the account of applicativization in O'dam (Southeastern Tepehuan) in Chapter 5 of [Eve23]. The applicative suffixes -dha and -tuda add exactly one syntactic argument, and the thematic role of that argument is predictable from the argument structure of the base verb through the hierarchy (273): an agent is added to a base with a single distinct argument; failing that, an entailed participant that is not a syntactic object and is compatible with an animate referent is promoted to object; failing that, a beneficiary is added, which makes benefaction the elsewhere function of the applicatives rather than their core. A base with three arguments takes no applicative, since a verb of O'dam has at most three: hypertransitivity is banned, so the ditransitives 'give' and 'ask' have no applied form.

Base.arguments counts the base's arguments as the applicative counts them: the subject and the objects co-referenced on the verb, plus the incorporated nominal of a denominal -ta verb of creation, minus an object not maximally distinct from the subject in the sense of [Nas07], which is what unites the exceptional transitives of Table 5.2 (lexical middles, verbs of ingestion, verbs of perception). Entailed participants that are not objects, whether implicit objects or entailed locations, do not count. That is the chapter's argument that locative expressions and instruments are adjuncts: a motion verb co-referencing only its subject gains an agent like any intransitive, and an entailed location is promoted the way an implicit object is.

rows are the chapter's verbs (Tables 5.1, 5.2, 5.6 and 5.7, the promotion cases of §5.2 and §5.3, the ditransitives, the denominal verbs of creation and the suppletive paradigms of §5.4), and rows_role derives each one's attested function, an applicative attaching only to the alternant of a suppletive paradigm with the most arguments. role_eq_beneficiary_iff is the chapter's two-part elsewhere condition and role_eq_none_iff the hypertransitivity ban. causativizability places O'dam on the causativizability hierarchy of [Kre12], which the chapter invokes to explain why ingestives and middles pattern with intransitives: the applicatives reach unergatives but not simple transitives.

Implementation notes

• Promotion is modelled by its precondition. The applied form entails that the promoted participant is animate, so only a participant compatible with an animate referent is promotable: implicit objects (buyers, hearers, the person something is hidden from) always are, entailed locations are or are not by the speakers' judgments (§5.3 against §5.4.1), and instruments never are, since a -k1'n 'with' phrase rejects an animate referent. The chapter's case that promotion adds animacy rather than the change of possession of the dative alternation ([BN10b]) or of Kinyarwanda applicatives stays in prose: the possession implicature runs from the promoted source to the subject with baabu' 'take out from under' and is absent with nui'ña' 'push'.
• The agent-adding use is the causative-applicative syncretism of [SP02], which the chapter declines to read as two morphemes: one suffix adds an agent or an object depending on the base. Unlike the Kinyarwanda -ish of [Jer17], an O'dam applicative has one function with a given base; the two senses of m11ya' ('burn', 'ignite') are two bases.
• Verb classes are only those the chapter names; the Table 5.1 verbs it does not classify are Class.plain. The subtype of a beneficiary (deputative, recipient, basic) and the role of an entailed participant are recorded in the rows and play no part in the model.

TODO

• torkia' 'bark' is the one base with two functions (agent as a verb of sound emission, promotion of the addressee as a verb of speaking), and aga' 'talk' and jiiñkia' 'yell' promote a hearer they do not entail, by analogy with the speaking class; the rows record only the sound-emission use of torkia'.
• The denominal mar-ta' 'have children' and ak-cha' 'make a river' take an applicative whose applied object is a co-agent or the diverted theme rather than a beneficiary; the model predicts of them only that no agent is added.

References

• [Eve23]
• [Nas07]
• [Kre12]
• [BN10b]
• [Jer17]
• [SP02]

inductive Everdell2023.Class : Type

The verb classes the chapter names; plain is any other verb.

• unaccusative : Class
• unergative : Class
• motion : Class
• ingestion : Class
• perception : Class
• middle : Class
• denominal : Class
• plain : Class

@[instance_reducible]

instance Everdell2023.instDecidableEqClass : DecidableEq Class

Equations

• Everdell2023.instDecidableEqClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Everdell2023.instReprClass : Repr Class

Equations

• Everdell2023.instReprClass = { reprPrec := Everdell2023.instReprClass.repr }

def Everdell2023.instReprClass.repr : Class → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Everdell2023.instReprClass.repr Everdell2023.Class.motion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Everdell2023.Class.motion")).group prec✝
• Everdell2023.instReprClass.repr Everdell2023.Class.middle prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Everdell2023.Class.middle")).group prec✝
• Everdell2023.instReprClass.repr Everdell2023.Class.plain prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Everdell2023.Class.plain")).group prec✝

def Everdell2023.Class.Nondistinct : Class → Prop

A lexical middle, verb of ingestion or verb of perception: the subject is not maximally distinct from the object ([Nas07]), so the applicative counts the two as one argument.

Equations

• Everdell2023.Class.ingestion.Nondistinct = True
• Everdell2023.Class.perception.Nondistinct = True
• Everdell2023.Class.middle.Nondistinct = True
• x✝.Nondistinct = False

@[instance_reducible]

instance Everdell2023.instDecidablePredClassNondistinct : DecidablePred Class.Nondistinct

Equations

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

inductive Everdell2023.Participant : Type

A participant entailed by the base verb that is not one of its syntactic objects: an implicit object that cannot be expressed in the base clause, an entailed location that must be expressed as a locative phrase, or an entailed instrument.

• implicitObject : Participant
• locative (animate : Bool) : Participant
• instrument : Participant

@[instance_reducible]

instance Everdell2023.instDecidableEqParticipant : DecidableEq Participant

Equations

• Everdell2023.instDecidableEqParticipant = Everdell2023.instDecidableEqParticipant.decEq

def Everdell2023.instDecidableEqParticipant.decEq (x✝ x✝¹ : Participant) : Decidable (x✝ = x✝¹)

Equations

• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.implicitObject Everdell2023.Participant.implicitObject = isTrue ⋯
• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.implicitObject (Everdell2023.Participant.locative animate) = isFalse ⋯
• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.implicitObject Everdell2023.Participant.instrument = isFalse Everdell2023.instDecidableEqParticipant.decEq._proof_4
• Everdell2023.instDecidableEqParticipant.decEq (Everdell2023.Participant.locative animate) Everdell2023.Participant.implicitObject = isFalse ⋯
• Everdell2023.instDecidableEqParticipant.decEq (Everdell2023.Participant.locative a) (Everdell2023.Participant.locative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Everdell2023.instDecidableEqParticipant.decEq (Everdell2023.Participant.locative animate) Everdell2023.Participant.instrument = isFalse ⋯
• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.instrument Everdell2023.Participant.implicitObject = isFalse Everdell2023.instDecidableEqParticipant.decEq._proof_8
• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.instrument (Everdell2023.Participant.locative animate) = isFalse ⋯
• Everdell2023.instDecidableEqParticipant.decEq Everdell2023.Participant.instrument Everdell2023.Participant.instrument = isTrue ⋯

def Everdell2023.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Everdell2023.instReprParticipant : Repr Participant

Equations

• Everdell2023.instReprParticipant = { reprPrec := Everdell2023.instReprParticipant.repr }

def Everdell2023.Participant.Animate : Participant → Prop

Compatibility with an animate referent, the precondition of promotion.

Equations

• Everdell2023.Participant.implicitObject.Animate = True
• (Everdell2023.Participant.locative a).Animate = (a = true)
• Everdell2023.Participant.instrument.Animate = False

@[instance_reducible]

instance Everdell2023.instDecidablePredParticipantAnimate : DecidablePred Participant.Animate

Equations

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

structure Everdell2023.Base : Type

The argument structure of a base verb as the applicative reads it.

• verbClass : Class

  The semantic class.

• objects : ℕ

  The objects co-referenced on the verb.

• entailed : Option Participant

  An entailed participant that is not a syntactic object.

def Everdell2023.instDecidableEqBase.decEq (x✝ x✝¹ : Base) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Everdell2023.instDecidableEqBase : DecidableEq Base

Equations

• Everdell2023.instDecidableEqBase = Everdell2023.instDecidableEqBase.decEq

def Everdell2023.instReprBase.repr : Base → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Everdell2023.instReprBase : Repr Base

Equations

• Everdell2023.instReprBase = { reprPrec := Everdell2023.instReprBase.repr }

inductive Everdell2023.Role : Type

The thematic roles an applied argument can bear.

• agent : Role
• promoted : Role
• beneficiary : Role

@[instance_reducible]

instance Everdell2023.instDecidableEqRole : DecidableEq Role

Equations

• Everdell2023.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Everdell2023.instReprRole.repr : Role → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Everdell2023.instReprRole.repr Everdell2023.Role.agent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Everdell2023.Role.agent")).group prec✝
• Everdell2023.instReprRole.repr Everdell2023.Role.promoted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Everdell2023.Role.promoted")).group prec✝

@[instance_reducible]

instance Everdell2023.instReprRole : Repr Role

Equations

• Everdell2023.instReprRole = { reprPrec := Everdell2023.instReprRole.repr }

def Everdell2023.hierarchy : List Role

(273): the roles in the order the applicative tries them, benefaction last.

Equations

• Everdell2023.hierarchy = [Everdell2023.Role.agent, Everdell2023.Role.promoted, Everdell2023.Role.beneficiary]

def Everdell2023.maxArguments : ℕ

A verb of O'dam has at most three syntactic arguments.

Equations

• Everdell2023.maxArguments = 3

def Everdell2023.Base.arguments (b : Base) : ℕ

Distinct syntactic arguments: the subject and the objects, an incorporated nominal counted in, an object not distinct from the subject counted out.

Equations

• b.arguments = 1 + ((b.objects + if b.verbClass = Everdell2023.Class.denominal then 1 else 0) - if b.verbClass.Nondistinct then 1 else 0)

def Everdell2023.Base.Promotable (b : Base) : Prop

The base entails a participant that promotion can make an animate object.

Equations

• b.Promotable = ∃ p ∈ b.entailed, p.Animate

@[instance_reducible]

instance Everdell2023.Base.instDecidablePromotable (b : Base) : Decidable b.Promotable

Equations

• b.instDecidablePromotable = id inferInstance

def Everdell2023.Base.Available (b : Base) : Role → Prop

A role is available when the applied form stays within maxArguments and the base has what the role needs: a single distinct argument for a new agent, an agent already (two arguments) and a promotable participant for promotion, an agent already for a beneficiary.

Equations

• b.Available Everdell2023.Role.agent = (b.arguments + 1 ≤ Everdell2023.maxArguments ∧ b.arguments = 1)
• b.Available Everdell2023.Role.promoted = (b.arguments + 1 ≤ Everdell2023.maxArguments ∧ 2 ≤ b.arguments ∧ b.Promotable)
• b.Available Everdell2023.Role.beneficiary = (b.arguments + 1 ≤ Everdell2023.maxArguments ∧ 2 ≤ b.arguments)

@[instance_reducible]

instance Everdell2023.Base.instDecidableAvailable (b : Base) (r : Role) : Decidable (b.Available r)

Equations

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

def Everdell2023.Base.role (b : Base) : Option Role

The role of the applied argument: the first available role of the hierarchy, none when the base takes no applicative.

Equations

• b.role = List.find? (fun (r : Everdell2023.Role) => decide (b.Available r)) Everdell2023.hierarchy

theorem Everdell2023.Base.one_le_arguments (b : Base) : 1 ≤ b.arguments

theorem Everdell2023.Base.role_eq (b : Base) : b.role = if b.arguments = 1 then some Role.agent else if b.arguments = 2 then if b.Promotable then some Role.promoted else some Role.beneficiary else none

The hierarchy read as a case split on the base's arguments.

theorem Everdell2023.Base.role_eq_agent_iff (b : Base) : b.role = some Role.agent ↔ b.arguments = 1

theorem Everdell2023.Base.role_eq_promoted_iff (b : Base) : b.role = some Role.promoted ↔ b.arguments = 2 ∧ b.Promotable

theorem Everdell2023.Base.role_eq_beneficiary_iff (b : Base) : b.role = some Role.beneficiary ↔ b.arguments = 2 ∧ ¬b.Promotable

The elsewhere condition of §5.5: a beneficiary is added only to a basic transitive base that lacks an implicit object or entailed location compatible with an animate referent.

theorem Everdell2023.Base.role_eq_none_iff (b : Base) : b.role = none ↔ maxArguments ≤ b.arguments

The hypertransitivity ban: a base takes no applicative exactly when the applied form would exceed three arguments.

theorem Everdell2023.Base.role_eq_agent_of_nondistinct (b : Base) (h : b.verbClass.Nondistinct) (ho : b.objects = 1) : b.role = some Role.agent

An exceptional transitive of Table 5.2 gains an agent like an intransitive.

theorem Everdell2023.Base.role_eq_beneficiary_of_denominal (b : Base) (h : b.verbClass = Class.denominal) (ho : b.objects = 0) (he : b.entailed = none) : b.role = some Role.beneficiary

A denominal verb of creation with no co-referenced object and no entailed participant gains a beneficiary, not an agent: the incorporated nominal is its second argument.

theorem Everdell2023.Base.role_ne_promoted_of_instrument (b : Base) (h : b.entailed = some Participant.instrument) : b.role ≠ some Role.promoted

An entailed instrument is never promoted (§5.4.1).

The chapter's verbs

structure Everdell2023.Row : Type

A verb of the chapter with its attested applicative function; paradigm numbers the suppletive paradigms of §5.4.

• base : Base
• observed : Option Role
• paradigm : Option ℕ

def Everdell2023.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Everdell2023.instDecidableEqRow : DecidableEq Row

Equations

• Everdell2023.instDecidableEqRow = Everdell2023.instDecidableEqRow.decEq

@[instance_reducible]

instance Everdell2023.instReprRow : Repr Row

Equations

• Everdell2023.instReprRow = { reprPrec := Everdell2023.instReprRow.repr }

def Everdell2023.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

def Everdell2023.classTable : List (String × Class)

Equations

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

def Everdell2023.entailedTable : List (String × Option Participant)

Equations

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

def Everdell2023.roleTable : List (String × Option Role)

Equations

• Everdell2023.roleTable = [("agent", some Everdell2023.Role.agent), ("promotion", some Everdell2023.Role.promoted), ("beneficiary", some Everdell2023.Role.beneficiary), ("blocked", none)]

def Everdell2023.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem Everdell2023.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Everdell2023.rows : List Row

Equations

• Everdell2023.rows = List.filterMap Everdell2023.Row.ofDatum Everdell2023.Examples.all

def Everdell2023.paradigmMax (p : ℕ) : ℕ

The most arguments any alternant of suppletive paradigm p has.

Equations

• Everdell2023.paradigmMax p = List.foldl max 0 (List.filterMap (fun (r : Everdell2023.Row) => if r.paradigm = some p then some r.base.arguments else none) Everdell2023.rows)

def Everdell2023.Row.Host (r : Row) : Prop

Within a suppletive paradigm the applicative attaches only to the alternant with the most arguments (§5.4); a verb outside any paradigm hosts it freely.

Equations

• r.Host = ∀ p ∈ r.paradigm, Everdell2023.paradigmMax p ≤ r.base.arguments

@[instance_reducible]

instance Everdell2023.instDecidablePredRowHost : DecidablePred Row.Host

Equations

• Everdell2023.instDecidablePredRowHost r = id inferInstance

theorem Everdell2023.rows_role (r : Row) : r ∈ rows → r.observed = if r.Host then r.base.role else none

Every verb's attested function is the role the hierarchy assigns to its base, and a suppletive alternant takes no applicative when a paradigm-mate has more arguments.

O'dam on the causativizability hierarchy

def Everdell2023.Base.tier (b : Base) : Option Krejci2012.Tier

The tier of the causativizability hierarchy of [Kre12] a base verb belongs to.

Equations

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

def Everdell2023.causativizability : Krejci2012.Causative

O'dam's row for Table 2.8 of [Kre12], read off the rows: the tiers whose verbs gain an agent from the applicative.

Equations

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

theorem Everdell2023.causativizability_type : causativizability.type = some Krejci2012.Tier.unergative

The applicatives reach unergatives but not simple transitives, Krejci's third type.

theorem Everdell2023.causativizability_respectsHierarchy : causativizability.RespectsHierarchy