Aissen (2003): Differential Object Marking: Iconicity vs. Economy

The higher in prominence a direct object, the more likely it is to be overtly case-marked. Aissen derives this in OT: harmonic alignment of the animacy and definiteness scales with the relational scale, locally conjoined with *Ø_C, yields a fixed subhierarchy of iconicity constraints *Oj/X & *Ø_C ("penalize a zero-marked object at prominence X"), and a single economy constraint *STRUC_C ("penalize overt case morphology") interpolates into it. The interpolation point is the grammar: an object is obligatorily marked iff its iconicity constraint outranks *STRUC_C, so each of the n + 1 points on an n-level scale is a language type, and every type marks an upward-closed segment of the scale. The subhierarchies' derivation by harmonic alignment (the paper's §§2–3) is taken as given; the constraint lists below are written directly in their derived ranking.

A language's zone, a set of cells of the grid of animacy and definiteness, records obligatory marking — the zone whose constraints strictly dominate *STRUC_C. The paper's optional zones (constraints that rerank with *STRUC_C, stochastically in Boersma's sense) are noted in docstrings but not represented.

Main results

• dom_fits, dom_obligatory_zone_upperSet — the paper's (33b): every attested system fits Figure 4's product prominence order (Alignment.Fits), its obligatory zone an upper set.
• figure2_typology / figure2_languages — the six interpolation points on the definiteness subhierarchy generate exactly the six cutoff systems, matched type-for-type to Kalkatungu, Catalan, Pitjantjatjara, Hebrew, Turkish, and Written Japanese.
• figure3_typology / figure3_languages — likewise for the animacy scale.
• two_dimensional_systems — Hindi and both stages of Spanish need both scales.

References

• [Ais03]

The definiteness scale

inductive Aissen2003.DefinitenessScale : Type

A position on the Definiteness Scale (13), Pronoun > Name > Definite > Indefinite Specific > NonSpecific, which extends the familiar hierarchy definite > specific > non-specific to proper names and personal pronouns.

• nonSpecific : DefinitenessScale
• indefiniteSpecific : DefinitenessScale
• definite : DefinitenessScale
• properName : DefinitenessScale
• personalPronoun : DefinitenessScale

@[instance_reducible]

instance Aissen2003.instDecidableEqDefinitenessScale : DecidableEq DefinitenessScale

Equations

• Aissen2003.instDecidableEqDefinitenessScale x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aissen2003.instReprDefinitenessScale : Repr DefinitenessScale

Equations

• Aissen2003.instReprDefinitenessScale = { reprPrec := Aissen2003.instReprDefinitenessScale.repr }

def Aissen2003.instReprDefinitenessScale.repr : DefinitenessScale → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aissen2003.instFintypeDefinitenessScale : Fintype DefinitenessScale

Equations

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

def Aissen2003.DefinitenessScale.dimensions : DefinitenessScale → Reference.Nominality × Reference.DefinitenessDegree

A position is a nominality and a degree of definiteness, pronouns and names counting as the high end of the definites.

Equations

• Aissen2003.DefinitenessScale.personalPronoun.dimensions = (Reference.Nominality.pronoun, Reference.DefinitenessDegree.definite)
• Aissen2003.DefinitenessScale.properName.dimensions = (Reference.Nominality.properName, Reference.DefinitenessDegree.definite)
• Aissen2003.DefinitenessScale.definite.dimensions = (Reference.Nominality.commonNoun, Reference.DefinitenessDegree.definite)
• Aissen2003.DefinitenessScale.indefiniteSpecific.dimensions = (Reference.Nominality.commonNoun, Reference.DefinitenessDegree.specific)
• Aissen2003.DefinitenessScale.nonSpecific.dimensions = (Reference.Nominality.commonNoun, Reference.DefinitenessDegree.nonSpecific)

@[instance_reducible]

instance Aissen2003.DefinitenessScale.instLinearOrder : LinearOrder DefinitenessScale

The scale is ordered by nominality first and then by degree of definiteness.

Equations

• Aissen2003.DefinitenessScale.instLinearOrder = LinearOrder.lift' (⇑toLex ∘ Aissen2003.DefinitenessScale.dimensions) Aissen2003.DefinitenessScale.instLinearOrder._proof_1

def Aissen2003.DefinitenessScale.all : List DefinitenessScale

The positions, most prominent first.

Equations

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

def Aissen2003.DefinitenessScale.nominality (d : DefinitenessScale) : Reference.Nominality

The nominality of a position.

Equations

• d.nominality = d.dimensions.1

def Aissen2003.DefinitenessScale.degree (d : DefinitenessScale) : Reference.DefinitenessDegree

The degree of definiteness of a position, pronouns and names being definite.

Equations

• d.degree = d.dimensions.2

def Aissen2003.DefinitenessScale.definiteness (d : DefinitenessScale) : Reference.Definiteness

The definiteness of a position, definite for pronouns, names and definite NPs.

Equations

• d.definiteness = d.degree.definiteness

theorem Aissen2003.DefinitenessScale.nominality_monotone : Monotone nominality

theorem Aissen2003.DefinitenessScale.degree_monotone : Monotone degree

theorem Aissen2003.DefinitenessScale.definiteness_monotone : Monotone definiteness

The DOM systems of the paper

The one-dimensional definiteness systems are the six interpolation types of Figure 2, one cited language each; Ritharngu and Dhargari instantiate the clean animacy types of Figure 3 (Yiddish and Sinhalese sit at its optional-zone points). Hindi, Persian, and the two stages of Spanish are the two-dimensional systems of §5.

@[reducible, inline]

abbrev Aissen2003.catalanDOM : Set (Reference.Animacy × DefinitenessScale)

Catalan marks only strong personal-pronoun objects, with a (Figure 2, §4.1).

Equations

• Aissen2003.catalanDOM = Set.Ici (Reference.Animacy.inanimate, Aissen2003.DefinitenessScale.personalPronoun)

@[reducible, inline]

abbrev Aissen2003.pitjantjatjaraDOM : Set (Reference.Animacy × DefinitenessScale)

Pitjantjatjara case-marks only pronoun and proper-name objects (Figure 2).

Equations

• Aissen2003.pitjantjatjaraDOM = Set.Ici (Reference.Animacy.inanimate, Aissen2003.DefinitenessScale.properName)

theorem Aissen2003.catalan_pitjantjatjara_nominality (a : Reference.Animacy) (d : DefinitenessScale) : ((a, d) ∈ catalanDOM ↔ d.nominality = Reference.Nominality.pronoun) ∧ ((a, d) ∈ pitjantjatjaraDOM ↔ Reference.Nominality.properName ≤ d.nominality)

Catalan's and Pitjantjatjara's cuts lie in the nominality the scale puts above the definites: Catalan marks exactly the pronouns, and Pitjantjatjara the pronouns and names.

@[reducible, inline]

abbrev Aissen2003.hebrewDOM : Set (Reference.Animacy × DefinitenessScale)

Hebrew has ʔet obligatorily on pronoun, proper-name and definite objects (Figure 2, §4.1).

Equations

• Aissen2003.hebrewDOM = Set.Ici (Reference.Animacy.inanimate, Aissen2003.DefinitenessScale.definite)

theorem Aissen2003.hebrew_marks_definites (a : Reference.Animacy) (d : DefinitenessScale) : (a, d) ∈ hebrewDOM ↔ d.definiteness = Reference.Definiteness.definite

Hebrew's DOM distinguishes definites from indefinites, marking an object just when it is definite, pronouns and names included.

@[reducible, inline]

abbrev Aissen2003.turkishDOM : Set (Reference.Animacy × DefinitenessScale)

Turkish marks every object but the non-specific ones, so unlike Hebrew it marks specific indefinites obligatorily (Figure 2, Tableaux 1–2); the zone is the fragment's, read through the degree of definiteness.

Equations

• Aissen2003.turkishDOM = {c : Reference.Animacy × Aissen2003.DefinitenessScale | c.2.degree ∈ Turkish.ObjectMarking.accusative}

@[reducible, inline]

abbrev Aissen2003.persianDOM : Set (Reference.Animacy × DefinitenessScale)

Persian has -rā obligatorily on all definites regardless of animacy and, exactly as in Turkish, on specific indefinites (§5.3). Animacy enters only in the optional zone, the non-specific indefinites, so the obligatory zone is one-dimensional.

Equations

• Aissen2003.persianDOM = Set.Ici (Reference.Animacy.inanimate, Aissen2003.DefinitenessScale.indefiniteSpecific)

@[reducible, inline]

abbrev Aissen2003.writtenJapaneseDOM : Set (Reference.Animacy × DefinitenessScale)

Written Japanese case-marks all objects, DOM extended to the whole scale, "thereby ceasing to be differential" (Figures 2–3, fn. 33).

Equations

• Aissen2003.writtenJapaneseDOM = Set.univ

@[reducible, inline]

abbrev Aissen2003.ritharnguDOM : Set (Reference.Animacy × DefinitenessScale)

Ritharngu case-marks all human objects obligatorily; the "some animates" spillover the paper reports is in the optional zone (Figure 3).

Equations

• Aissen2003.ritharnguDOM = Set.Ici (Reference.Animacy.human, Aissen2003.DefinitenessScale.nonSpecific)

@[reducible, inline]

abbrev Aissen2003.dhargariDOM : Set (Reference.Animacy × DefinitenessScale)

Dhargari case-marks all animate objects (Figure 3).

Equations

• Aissen2003.dhargariDOM = Set.Ici (Reference.Animacy.animate, Aissen2003.DefinitenessScale.nonSpecific)

@[reducible, inline]

abbrev Aissen2003.noDOM : Set (Reference.Animacy × DefinitenessScale)

The system with no DOM marks no object, Kalkatungu in Figures 2–3, where *STRUC_C dominates the whole subhierarchy.

Equations

• Aissen2003.noDOM = ∅

@[reducible, inline]

abbrev Aissen2003.hindiDOM : Set (Reference.Animacy × DefinitenessScale)

Hindi marks with -ko (§5.2, Figure 7). It is obligatory on human objects down to specific indefinites and on animate pronouns and proper names, which "assimilate to the human class"; optional on human non-specifics, animate definites and below, and inanimate definites; and excluded on other inanimates.

Equations

• Aissen2003.hindiDOM = Set.Ici (Reference.Animacy.human, Aissen2003.DefinitenessScale.indefiniteSpecific) ∪ Set.Ici (Reference.Animacy.animate, Aissen2003.DefinitenessScale.properName)

@[reducible, inline]

abbrev Aissen2003.cmcSpanishDOM : Set (Reference.Animacy × DefinitenessScale)

The Spanish of the Cantar de Mio Cid has a obligatorily on exactly the personal pronouns and proper names of humans and animals (§5.1, Figure 5), and optionally on human common NPs and geographic proper names.

Equations

• Aissen2003.cmcSpanishDOM = Set.Ici (Reference.Animacy.animate, Aissen2003.DefinitenessScale.properName)

@[reducible, inline]

abbrev Aissen2003.spanishDOM : Set (Reference.Animacy × DefinitenessScale)

Modern Spanish is the CMC system with *STRUC_C demoted below the human-definite and human-specific constraints, so a is now also obligatory with definite and specific human objects (§5.4, Figure 9). The obligatory zone coincides with Hindi's; the two differ in their optional zones (Figure 7 against Figure 9).

Equations

• Aissen2003.spanishDOM = Set.Ici (Reference.Animacy.human, Aissen2003.DefinitenessScale.indefiniteSpecific) ∪ Set.Ici (Reference.Animacy.animate, Aissen2003.DefinitenessScale.properName)

def Aissen2003.allDOMZones : List (Set (Reference.Animacy × DefinitenessScale))

The DOM systems cited in the paper.

Equations

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

Monotonicity: the (33b) universal

noncomputable def Aissen2003.marking (z : Set (Reference.Animacy × DefinitenessScale)) : ArgumentRole → Reference.Animacy × DefinitenessScale → Option Unit

The marking of a DOM system, the object overtly marked on its zone and no other role marked.

Equations

• Aissen2003.marking z ArgumentRole.P x✝ = if x✝ ∈ z then some () else none
• Aissen2003.marking z x✝¹ x✝ = none

theorem Aissen2003.fits_marking_iff (z : Set (Reference.Animacy × DefinitenessScale)) : Alignment.Fits (marking z) ↔ IsUpperSet z

A DOM system fits the prominence order of Figure 4 exactly when its zone is an upper set.

theorem Aissen2003.dom_obligatory_zone_upperSet (z : Set (Reference.Animacy × DefinitenessScale)) : z ∈ allDOMZones → IsUpperSet z

In every attested system the obligatorily marked cells form an upper set in the product prominence order of Figure 4, which is (33b) order-theoretically.

theorem Aissen2003.dom_fits (z : Set (Reference.Animacy × DefinitenessScale)) : z ∈ allDOMZones → Alignment.Fits (marking z)

Every attested system fits the prominence order, so no language obligatorily marks a less prominent object while leaving a more prominent one unmarked.

theorem Aissen2003.isUpperSet_iff_eq_empty_or_Ici {α : Type u_1} [LinearOrder α] [WellFoundedLT α] {s : Set α} : IsUpperSet s ↔ s = ∅ ∨ ∃ (a : α), s = Set.Ici a

On a finite scale the upper sets are the empty set and the cones above each position, so each of the n + 1 interpolation points of an n-level subhierarchy is a cutoff type.

def Aissen2003.AnimacyOnly (z : Set (Reference.Animacy × DefinitenessScale)) : Prop

A zone depends on animacy alone.

Equations

• Aissen2003.AnimacyOnly z = ∀ (a : Reference.Animacy) (d d' : Aissen2003.DefinitenessScale), (a, d) ∈ z ↔ (a, d') ∈ z

def Aissen2003.DefinitenessOnly (z : Set (Reference.Animacy × DefinitenessScale)) : Prop

A zone depends on definiteness alone.

Equations

• Aissen2003.DefinitenessOnly z = ∀ (a a' : Reference.Animacy) (d : Aissen2003.DefinitenessScale), (a, d) ∈ z ↔ (a', d) ∈ z

@[instance_reducible]

instance Aissen2003.instDecidableAnimacyOnlyOfDecidablePredProdAnimacyDefinitenessScaleMemSet (z : Set (Reference.Animacy × DefinitenessScale)) [DecidablePred fun (x : Reference.Animacy × DefinitenessScale) => x ∈ z] : Decidable (AnimacyOnly z)

Equations

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

@[instance_reducible]

instance Aissen2003.instDecidableDefinitenessOnlyOfDecidablePredProdAnimacyDefinitenessScaleMemSet (z : Set (Reference.Animacy × DefinitenessScale)) [DecidablePred fun (x : Reference.Animacy × DefinitenessScale) => x ∈ z] : Decidable (DefinitenessOnly z)

Equations

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

theorem Aissen2003.definiteness_systems_one_dimensional : DefinitenessOnly catalanDOM ∧ DefinitenessOnly pitjantjatjaraDOM ∧ DefinitenessOnly hebrewDOM ∧ DefinitenessOnly turkishDOM ∧ DefinitenessOnly persianDOM ∧ DefinitenessOnly writtenJapaneseDOM

The Figure 2 and §5.3 systems are animacy-blind.

theorem Aissen2003.animacy_systems_one_dimensional : AnimacyOnly ritharnguDOM ∧ AnimacyOnly dhargariDOM

The Figure 3 systems are definiteness-blind.

theorem Aissen2003.two_dimensional_systems : (¬AnimacyOnly hindiDOM ∧ ¬DefinitenessOnly hindiDOM) ∧ (¬AnimacyOnly cmcSpanishDOM ∧ ¬DefinitenessOnly cmcSpanishDOM) ∧ ¬AnimacyOnly spanishDOM ∧ ¬DefinitenessOnly spanishDOM

Hindi and both stages of Spanish are genuinely two-dimensional (§5), since neither scale alone determines the obligatory zone.

The interpolation engine

The paper evaluates candidates per input: for an object at prominence level ℓ, GEN offers a case-marked and a zero-marked parse. *Oj/ℓ & *Ø_C penalizes the zero-marked parse; *STRUC_C penalizes the case-marked one. A grammar linearizes the fixed subhierarchy with *STRUC_C interpolated, and the winner at ℓ is the marked parse iff ℓ's iconicity constraint outranks *STRUC_C.

def Aissen2003.starStruc {L : Type} : OptimalityTheory.Constraint (L × Bool)

*STRUC_C penalizes overt case morphology, so the case-marked parse violates it. Candidates are level–marking pairs, and true is the marked parse.

Equations

• Aissen2003.starStruc = OptimalityTheory.Constraint.binary fun (x : L × Bool) => x.2 = true

def Aissen2003.starZero {L : Type} [DecidableEq L] (ℓ : L) : OptimalityTheory.Constraint (L × Bool)

*Oj/ℓ & *Ø_C is violated by a zero-marked object at level ℓ.

Equations

• Aissen2003.starZero ℓ = OptimalityTheory.Constraint.binary fun (c : L × Bool) => c.1 = ℓ ∧ c.2 = false

def Aissen2003.interpolation {L : Type} [DecidableEq L] (levels : List L) (k : ℕ) : List (OptimalityTheory.Constraint (L × Bool))

The iconicity subhierarchy of a scale (most prominent level first) with *STRUC_C interpolated at position k.

Equations

• Aissen2003.interpolation levels k = (List.map Aissen2003.starZero levels).insertIdx k Aissen2003.starStruc

def Aissen2003.markedWins {L : Type} [DecidableEq L] (ranking : List (OptimalityTheory.Constraint (L × Bool))) (ℓ : L) : Bool

Whether the case-marked parse wins for an object at level ℓ.

Equations

• Aissen2003.markedWins ranking ℓ = decide ((OptimalityTheory.Tableau.ofRanking [(ℓ, true), (ℓ, false)] ranking ⋯).optimal = {(ℓ, true)})

theorem Aissen2003.tableaux_1_2 : markedWins (interpolation DefinitenessScale.all 3) DefinitenessScale.indefiniteSpecific = false ∧ markedWins (interpolation DefinitenessScale.all 4) DefinitenessScale.indefiniteSpecific = true

Tableaux 1–2 evaluate a specific indefinite object. In Hebrew *STRUC_C outranks *Oj/Spec & *Ø_C and the zero parse wins; in Turkish the ranking is reversed and the marked parse wins.

theorem Aissen2003.figure2_typology : List.map (fun (k : ℕ) => List.map (markedWins (interpolation DefinitenessScale.all k)) DefinitenessScale.all) (List.range 6) = [[false, false, false, false, false], [true, false, false, false, false], [true, true, false, false, false], [true, true, true, false, false], [true, true, true, true, false], [true, true, true, true, true]]

The six interpolation points on the definiteness subhierarchy of Figure 2 generate exactly the six cutoff systems, and no non-monotone pattern arises.

theorem Aissen2003.figure2_languages : (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ noDOM ↔ markedWins (interpolation DefinitenessScale.all 0) d = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ catalanDOM ↔ markedWins (interpolation DefinitenessScale.all 1) d = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ pitjantjatjaraDOM ↔ markedWins (interpolation DefinitenessScale.all 2) d = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ hebrewDOM ↔ markedWins (interpolation DefinitenessScale.all 3) d = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ turkishDOM ↔ markedWins (interpolation DefinitenessScale.all 4) d = true) ∧ ∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ writtenJapaneseDOM ↔ markedWins (interpolation DefinitenessScale.all 5) d = true

Figure 2 cites "one language for each of the possible DOM types", and each cited language's obligatory grid is its interpolation type's predicted pattern.

theorem Aissen2003.persian_same_type_as_turkish (c : Reference.Animacy × DefinitenessScale) : c ∈ persianDOM ↔ c ∈ turkishDOM

Persian's obligatory grid realizes the same interpolation type as Turkish's, since specific indefinites "require the suffix -rā, exactly as ... the accusative suffix in Turkish" (§5.3).

theorem Aissen2003.figure3_typology : List.map (fun (k : ℕ) => List.map (markedWins (interpolation Reference.Animacy.all k)) Reference.Animacy.all) (List.range 4) = [[false, false, false], [true, false, false], [true, true, false], [true, true, true]]

The four interpolation points on the animacy subhierarchy of Figure 3 generate exactly the four cutoff systems.

theorem Aissen2003.figure3_languages : (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ noDOM ↔ markedWins (interpolation Reference.Animacy.all 0) a = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ ritharnguDOM ↔ markedWins (interpolation Reference.Animacy.all 1) a = true) ∧ (∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ dhargariDOM ↔ markedWins (interpolation Reference.Animacy.all 2) a = true) ∧ ∀ (a : Reference.Animacy) (d : DefinitenessScale), (a, d) ∈ writtenJapaneseDOM ↔ markedWins (interpolation Reference.Animacy.all 3) a = true

Figure 3's cleanly cutoff languages match their types, Kalkatungu with none, Ritharngu with the humans, Dhargari with the animates, and Written Japanese and Dhalandji with all.

theorem Aissen2003.no_reversed_system (k : ℕ) : k < 4 → ∀ (a a' : Reference.Animacy), a ≤ a' → markedWins (interpolation Reference.Animacy.all k) a = true → markedWins (interpolation Reference.Animacy.all k) a' = true

"This account predicts that the reverse is not found, e.g., languages in which only inanimates are case-marked", since every interpolation grammar marks an upward-closed segment of the scale.