de Hoop and Malchukov (2008): Case-marking strategies

This file formalizes the two case-marking strategies of [dHM08]: the identifying function, (10), by which case encodes a property of the argument itself, and the distinguishing function, (15), by which case tells the two arguments of a transitive clause apart. Both are violable constraints evaluated against ECONOMY in the bidirectional Optimality Theory of [Blu00], on the assumption that a morphologically unmarked case is the absence of case, as in [Ais03]. Arguments are strong or weak by their discourse prominence, and a strong subject is the typical, distinguishable one while a strong object is the atypical, subject-like one, so DISTINGUISHABILITY targets the weak subject and the strong object where IDENTIFY targets the strong argument in either position. The superoptimal pairs of the tableaux follow: the strategies converge in differential object marking, both marking the strong object as in Hindi, and diverge in differential subject marking, IDENTIFY marking the volitional subject of Manipuri and DISTINGUISHABILITY the weak subject of Fore, which explains the robustness of the one alternation and the variability of the other. In a symmetrical alternation between two overt cases, Lezgian's ergative and oblique or Finnish's accusative and partitive, DISTINGUISHABILITY is vacuously satisfied, so the alternation is necessarily due to IDENTIFY. Section 4 replaces ECONOMY by PAIP, (42), which penalizes case on the primary actant, the argument encoded like the intransitive subject, so that differential marking is free of it on the object of a nominative-accusative and the subject of an ergative-absolutive language, where differential object and subject marking are found, while the other two alternations conflict with IDENTIFY and are resolved by voice, the passive making the object and the antipassive the subject the unmarked argument.

Implementation notes

A form is Option C over the language's overt cases, none the absence of case; the asymmetrical games have one overt case, and the symmetrical game omits the caseless form since the Case Filter outranks ECONOMY there. Superoptimality is the computable BidirectionalOT.superoptimal, and each tableau is one decide.

TODO

Tableau (41) for Aranda lists the ergative on the inanimate subject as a third superoptimal pair, blocked under [Blu00]'s definition by the ergative on the first person, which shares its form with a better profile; the paper keeps it by arguing that the one ergative form cannot be ambiguous between a first person and an inanimate. aranda states what the blocking relation gives, the first person marked and the intermediate types caseless.

References

• [dHM08]
• [Blu00]
• [Ais03]

Strength and position

inductive DeHoopMalchukov2008.Strength : Type

The strength of an argument, its discourse prominence: animate, definite and volitional arguments are strong, A and P, and the others weak, a and p.

• strong : Strength
• weak : Strength

@[instance_reducible]

instance DeHoopMalchukov2008.instDecidableEqStrength : DecidableEq Strength

Equations

• DeHoopMalchukov2008.instDecidableEqStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeHoopMalchukov2008.instReprStrength : Repr Strength

Equations

• DeHoopMalchukov2008.instReprStrength = { reprPrec := DeHoopMalchukov2008.instReprStrength.repr }

def DeHoopMalchukov2008.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

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

def DeHoopMalchukov2008.Strength.opposite : Strength → Strength

The other strength.

Equations

• DeHoopMalchukov2008.Strength.strong.opposite = DeHoopMalchukov2008.Strength.weak
• DeHoopMalchukov2008.Strength.weak.opposite = DeHoopMalchukov2008.Strength.strong

inductive DeHoopMalchukov2008.Position : Type

The two core positions of a transitive clause.

• subject : Position
• object : Position

@[instance_reducible]

instance DeHoopMalchukov2008.instDecidableEqPosition : DecidableEq Position

Equations

• DeHoopMalchukov2008.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeHoopMalchukov2008.instReprPosition : Repr Position

Equations

• DeHoopMalchukov2008.instReprPosition = { reprPrec := DeHoopMalchukov2008.instReprPosition.repr }

def DeHoopMalchukov2008.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

def DeHoopMalchukov2008.Position.confusable : Position → Strength

The argument DISTINGUISHABILITY must mark, the one confusable with its co-argument: the weak subject, which lacks the agent's prominence, and the strong object, which has it.

Equations

• DeHoopMalchukov2008.Position.subject.confusable = DeHoopMalchukov2008.Strength.weak
• DeHoopMalchukov2008.Position.object.confusable = DeHoopMalchukov2008.Strength.strong

The constraints

def DeHoopMalchukov2008.identify {C : Type u_1} {M : Type u_2} [DecidableEq C] [DecidableEq M] (c : C) (m : M) : OptimalityTheory.Constraint (Option C × M)

IDENTIFY, (9): case c identifies the meaning m, so a pair violates it by having either without the other.

Equations

• DeHoopMalchukov2008.identify c m = OptimalityTheory.Constraint.binary fun (p : Option C × M) => ¬(p.1 = some c ↔ p.2 = m)

def DeHoopMalchukov2008.distinguish {C : Type u_1} {M : Type u_2} [DecidableEq M] (m : M) : OptimalityTheory.Constraint (Option C × M)

DISTINGUISHABILITY, (15), for the confusable meaning m: violated by leaving it caseless.

Equations

• DeHoopMalchukov2008.distinguish m = OptimalityTheory.Constraint.binary fun (p : Option C × M) => p.1.isNone = true ∧ p.2 = m

def DeHoopMalchukov2008.economy {C : Type u_1} {M : Type u_2} : OptimalityTheory.Constraint (Option C × M)

ECONOMY: violated by any morphological case.

Equations

• DeHoopMalchukov2008.economy = OptimalityTheory.Constraint.binary fun (p : Option C × M) => p.1.isSome = true

Asymmetrical differential marking

def DeHoopMalchukov2008.asymmetrical : Finset (Option Unit × Strength)

The asymmetrical game: one overt case against its absence, for either strength.

Equations

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

theorem DeHoopMalchukov2008.identify_marks_strong : BidirectionalOT.superoptimal asymmetrical (BidirectionalOT.profile [identify () Strength.strong, economy]) = {(some (), Strength.strong), (none, Strength.weak)}

Tableaux (18), (31) and (39): IDENTIFY over ECONOMY marks the strong argument in either position, Manipuri's ergative on the volitional subject, Hindi's accusative and Central Pomo's patientive on the strong object.

theorem DeHoopMalchukov2008.distinguish_marks_confusable (pos : Position) : BidirectionalOT.superoptimal asymmetrical (BidirectionalOT.profile [distinguish pos.confusable, economy]) = {(some (), pos.confusable), (none, pos.confusable.opposite)}

Tableaux (21), (26), (32) and (35): DISTINGUISHABILITY over ECONOMY marks the confusable argument, the weak subject in Fore and Dyirbal and the strong object in Hindi and Awtuw.

theorem DeHoopMalchukov2008.converge_iff (pos : Position) : BidirectionalOT.superoptimal asymmetrical (BidirectionalOT.profile [identify () Strength.strong, economy]) = BidirectionalOT.superoptimal asymmetrical (BidirectionalOT.profile [distinguish pos.confusable, economy]) ↔ pos = Position.object

The strategies converge in differential object marking and diverge in differential subject marking: they select the same pairs exactly when the confusable argument is the strong one.

Symmetrical differential marking

inductive DeHoopMalchukov2008.Overt : Type

The two overt cases of a symmetrical alternation: the one identifying the strong argument, Lezgian's ergative and Finnish's accusative, and the other, their oblique and partitive.

• identifying : Overt
• other : Overt

@[instance_reducible]

instance DeHoopMalchukov2008.instDecidableEqOvert : DecidableEq Overt

Equations

• DeHoopMalchukov2008.instDecidableEqOvert x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeHoopMalchukov2008.instReprOvert : Repr Overt

Equations

• DeHoopMalchukov2008.instReprOvert = { reprPrec := DeHoopMalchukov2008.instReprOvert.repr }

def DeHoopMalchukov2008.instReprOvert.repr : Overt → ℕ → Std.Format

Equations

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

def DeHoopMalchukov2008.symmetrical : Finset (Option Overt × Strength)

The symmetrical game: both overt cases and no caseless form, the Case Filter outranking ECONOMY.

Equations

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

theorem DeHoopMalchukov2008.symmetrical_identify : BidirectionalOT.superoptimal symmetrical (BidirectionalOT.profile [identify Overt.identifying Strength.strong, economy]) = {(some Overt.identifying, Strength.strong), (some Overt.other, Strength.weak)}

Tableaux (24) and (29): IDENTIFY pairs each overt case with a strength, ergative with the volitional and oblique with the nonvolitional subject in Lezgian, accusative with the strong and partitive with the weak object in Finnish.

theorem DeHoopMalchukov2008.distinguish_symmetrical (m : Strength) (p : Option Overt × Strength) : p ∈ symmetrical → distinguish m p = 0

DISTINGUISHABILITY is vacuously satisfied throughout a symmetrical game, every candidate being case-marked.

theorem DeHoopMalchukov2008.symmetrical_distinguish (m : Strength) : BidirectionalOT.superoptimal symmetrical (BidirectionalOT.profile [distinguish m, economy]) = symmetrical

So it cannot drive a symmetrical alternation: under DISTINGUISHABILITY over ECONOMY every pair is superoptimal and no case is paired with a strength. Symmetrical differential marking is necessarily due to IDENTIFY.

Both strategies at once

inductive DeHoopMalchukov2008.ArandaSubject : Type

Aranda's subject types along the hierarchy (40): the first person pronoun, the intermediate persons, humans and animates, and the inanimate noun.

• firstPerson : ArandaSubject
• intermediate : ArandaSubject
• inanimate : ArandaSubject

@[instance_reducible]

instance DeHoopMalchukov2008.instDecidableEqArandaSubject : DecidableEq ArandaSubject

Equations

• DeHoopMalchukov2008.instDecidableEqArandaSubject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeHoopMalchukov2008.instReprArandaSubject : Repr ArandaSubject

Equations

• DeHoopMalchukov2008.instReprArandaSubject = { reprPrec := DeHoopMalchukov2008.instReprArandaSubject.repr }

def DeHoopMalchukov2008.instReprArandaSubject.repr : ArandaSubject → ℕ → Std.Format

Equations

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

def DeHoopMalchukov2008.arandaSubjects : Finset (Option Unit × ArandaSubject)

The Aranda game: the ergative against its absence, for each subject type.

Equations

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

theorem DeHoopMalchukov2008.aranda : BidirectionalOT.superoptimal arandaSubjects (BidirectionalOT.profile [distinguish ArandaSubject.inanimate, identify () ArandaSubject.firstPerson, economy]) = {(some (), ArandaSubject.firstPerson), (none, ArandaSubject.intermediate)}

Tableau (41): with DISTINGUISHABILITY over IDENTIFY over ECONOMY, the first person takes the ergative by IDENTIFY and the intermediate types stay caseless; the paper's ergative on the inanimate is blocked by the first person's, see the module's TODO.

PAIP and the alignment of differential marking

inductive DeHoopMalchukov2008.Alignment : Type

The alignment of a language's core cases.

• nominativeAccusative : Alignment
• ergativeAbsolutive : Alignment

@[instance_reducible]

instance DeHoopMalchukov2008.instDecidableEqAlignment : DecidableEq Alignment

Equations

• DeHoopMalchukov2008.instDecidableEqAlignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DeHoopMalchukov2008.instReprAlignment.repr : Alignment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeHoopMalchukov2008.instReprAlignment : Repr Alignment

Equations

• DeHoopMalchukov2008.instReprAlignment = { reprPrec := DeHoopMalchukov2008.instReprAlignment.repr }

def DeHoopMalchukov2008.Alignment.primaryActant : Alignment → Position

The primary actant, the argument of a transitive clause encoded like the intransitive subject: the nominative subject or the absolutive object.

Equations

• DeHoopMalchukov2008.Alignment.nominativeAccusative.primaryActant = DeHoopMalchukov2008.Position.subject
• DeHoopMalchukov2008.Alignment.ergativeAbsolutive.primaryActant = DeHoopMalchukov2008.Position.object

def DeHoopMalchukov2008.paip {C : Type u_1} {M : Type u_2} (al : Alignment) : OptimalityTheory.Constraint (Position × Option C × M)

PAIP, (42): avoid marking the unmarked argument, an overt case on the primary actant.

Equations

• DeHoopMalchukov2008.paip al = OptimalityTheory.Constraint.binary fun (p : DeHoopMalchukov2008.Position × Option C × M) => p.1 = al.primaryActant ∧ p.2.1.isSome = true

theorem DeHoopMalchukov2008.paip_eq_zero_iff {C : Type u_1} {M : Type u_2} (al : Alignment) (pos : Position) (c : C) (m : M) : paip al (pos, some c, m) = 0 ↔ pos ≠ al.primaryActant

Differential marking is free of PAIP off the primary actant and violates it there: object marking in a nominative-accusative and subject marking in an ergative-absolutive language satisfy it, which is where differential object and subject marking are found.