@cite{aissen-2003}: Differential Object Marking @cite{aissen-2003}

Differential Object Marking: Iconicity vs. Economy. Natural Language & Linguistic Theory 21(3): 435–483.

Formalizes the core OT analysis: Harmonic Alignment of prominence scales with the relational scale (Subj > Obj) derives two constraint families:

• Iconicity (*Ø/X): penalizes zero-marked objects at prominence level X. Fixed ranking: *Ø most prominent >>... >> *Ø least prominent.
• Economy (*!/X): penalizes marked objects at prominence level X. Fixed ranking: *!/least prominent >>... >> *!/most prominent.

Rankings are fixed within each family but free between families. The factorial typology over all consistent interleavings predicts exactly the attested DOM patterns.

Key Results

Scale Size	Consistent Rankings	Language Types	Impossible Patterns
2 elements	6	3	Mark low without high
3 elements	20	4	Any non-monotone pattern

For the 3-element animacy scale {Hu > An > In}, 4 of 8 logically possible patterns are generated — exactly the monotone ones (Table 17, p. 476).

Connection to Existing Infrastructure

The predicted DOM profiles are matched against the DOMProfile language data in §0 below, verifying that every attested pattern corresponds to a possible OT grammar.

@[reducible, inline]

abbrev Aissen2003.DOMProfile : Type

A DOM (Differential Object Marking) profile: a DifferentialMarkingProfile specialized to role P + channel flagging.

Each cell (a, d) records whether an object with animacy level a and definiteness level d obligatorily receives an overt DOM marker (e.g., Spanish a, Turkish -(y)I, Hindi -ko).

DOM is the P-flagging instance of @cite{just-2024}'s general differential marking framework. Monotonicity (isMonotone), isAnimacyOnly, and isDefinitenessOnly are all inherited from DifferentialMarkingProfile.

Equations

• Aissen2003.DOMProfile = Features.Prominence.DifferentialMarkingProfile

def Aissen2003.spanishDOM : DOMProfile

Spanish: a-marking for human direct objects regardless of definiteness. One-dimensional (animacy-based), cutoff between human and animate.

Equations

• Aissen2003.spanishDOM = Features.Prominence.DifferentialMarkingProfile.animacyCutoffP "Spanish" Features.Prominence.MarkingChannel.flagging Features.Prominence.AnimacyLevel.human

def Aissen2003.russianDOM : DOMProfile

Russian: animate accusative (genitive form used as accusative for animate nouns). One-dimensional (animacy-based), cutoff between animate and inanimate.

Equations

• Aissen2003.russianDOM = Features.Prominence.DifferentialMarkingProfile.animacyCutoffP "Russian" Features.Prominence.MarkingChannel.flagging Features.Prominence.AnimacyLevel.animate

def Aissen2003.turkishDOM : DOMProfile

Turkish: -(y)I marking for definite direct objects regardless of animacy. One-dimensional (definiteness-based), cutoff between definite and indefinite specific.

Equations

• Aissen2003.turkishDOM = Features.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Turkish" Features.Prominence.MarkingChannel.flagging Features.Prominence.DefinitenessLevel.definite

def Aissen2003.hebrewDOM : DOMProfile

Hebrew: ʔet marking for definite direct objects regardless of animacy. Same one-dimensional definiteness cutoff as Turkish.

Equations

• Aissen2003.hebrewDOM = Features.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Hebrew" Features.Prominence.MarkingChannel.flagging Features.Prominence.DefinitenessLevel.definite

def Aissen2003.persianDOM : DOMProfile

Persian: -rā marking for definite direct objects. One-dimensional (definiteness-based) for obligatory marking; optional extension to specific indefinite animates.

Equations

• Aissen2003.persianDOM = Features.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Persian" Features.Prominence.MarkingChannel.flagging Features.Prominence.DefinitenessLevel.definite

def Aissen2003.catalanDOM : DOMProfile

Catalan: a-marking restricted to personal pronouns. The most restrictive DOM pattern attested.

Equations

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

def Aissen2003.hindiDOM : DOMProfile

Hindi-Urdu: -ko marking conditioned by BOTH animacy and definiteness. Two-dimensional DOM with a staircase cutoff.

Equations

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

def Aissen2003.noDOMProfile : DOMProfile

No DOM: trivially monotone. Included in allDOMProfiles to match OT Type 4 (no marking) via nodom_matches_type4 in §6.

Equations

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

def Aissen2003.allDOMProfiles : List DOMProfile

All DOM profiles in the sample (7 attested + 1 no-marking baseline).

Equations

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

theorem Aissen2003.allDOMProfiles_count : allDOMProfiles.length = 8

theorem Aissen2003.spanish_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone spanishDOM = true

theorem Aissen2003.russian_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone russianDOM = true

theorem Aissen2003.turkish_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone turkishDOM = true

theorem Aissen2003.hebrew_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone hebrewDOM = true

theorem Aissen2003.persian_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone persianDOM = true

theorem Aissen2003.catalan_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone catalanDOM = true

theorem Aissen2003.hindi_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone hindiDOM = true

theorem Aissen2003.no_dom_monotone : Features.Prominence.DifferentialMarkingProfile.isMonotone noDOMProfile = true

theorem Aissen2003.dom_monotonicity_universal : (allDOMProfiles.all fun (x : DOMProfile) => Features.Prominence.DifferentialMarkingProfile.isMonotone x) = true

Aissen's DOM monotonicity universal: all attested DOM patterns in the sample form upper sets in the bidimensional animacy × definiteness grid. No language marks a less-prominent object while leaving a more-prominent one unmarked.

theorem Aissen2003.spanish_animacy_only : Features.Prominence.DifferentialMarkingProfile.isAnimacyOnly spanishDOM = true

theorem Aissen2003.russian_animacy_only : Features.Prominence.DifferentialMarkingProfile.isAnimacyOnly russianDOM = true

theorem Aissen2003.turkish_definiteness_only : Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly turkishDOM = true

theorem Aissen2003.hebrew_definiteness_only : Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly hebrewDOM = true

theorem Aissen2003.persian_definiteness_only : Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly persianDOM = true

theorem Aissen2003.catalan_definiteness_only : Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly catalanDOM = true

theorem Aissen2003.hindi_not_animacy_only : Features.Prominence.DifferentialMarkingProfile.isAnimacyOnly hindiDOM = false

Hindi DOM depends on both animacy and definiteness — it cannot be reduced to a single scale.

theorem Aissen2003.hindi_not_definiteness_only : Features.Prominence.DifferentialMarkingProfile.isDefinitenessOnly hindiDOM = false

theorem Aissen2003.human_dominates_animate : (allDOMProfiles.all fun (p : DOMProfile) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => if p.marks Features.Prominence.AnimacyLevel.animate d = true then p.marks Features.Prominence.AnimacyLevel.human d else true) = true

In all sample languages, human objects are never less marked than animate objects at the same definiteness level.

theorem Aissen2003.animate_dominates_inanimate : (allDOMProfiles.all fun (p : DOMProfile) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => if p.marks Features.Prominence.AnimacyLevel.inanimate d = true then p.marks Features.Prominence.AnimacyLevel.animate d else true) = true

In all sample languages, animate objects are never less marked than inanimate objects at the same definiteness level.

theorem Aissen2003.pronoun_dominates_properName : (allDOMProfiles.all fun (p : DOMProfile) => Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => if p.marks a Features.Prominence.DefinitenessLevel.properName = true then p.marks a Features.Prominence.DefinitenessLevel.personalPronoun else true) = true

In all sample languages, pronouns are never less marked than proper names at the same animacy level.

theorem Aissen2003.definite_dominates_indefiniteSpecific : (allDOMProfiles.all fun (p : DOMProfile) => Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => if p.marks a Features.Prominence.DefinitenessLevel.indefiniteSpecific = true then p.marks a Features.Prominence.DefinitenessLevel.definite else true) = true

In all sample languages, definite NPs are never less marked than indefinite specific NPs at the same animacy level.

theorem Aissen2003.top_cell_marked_if_any : (allDOMProfiles.all fun (p : DOMProfile) => if (Features.Prominence.AnimacyLevel.all.any fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.any fun (d : Features.Prominence.DefinitenessLevel) => p.marks a d) = true then p.marks Features.Prominence.AnimacyLevel.human Features.Prominence.DefinitenessLevel.personalPronoun else true) = true

If any cell is marked, the most prominent cell (human, pronoun) is also marked.

theorem Aissen2003.bottom_cell_unmarked : (allDOMProfiles.all fun (p : DOMProfile) => p.marks Features.Prominence.AnimacyLevel.inanimate Features.Prominence.DefinitenessLevel.nonSpecific == false) = true

The least prominent cell (inanimate, non-specific) is unmarked in all DOM languages in the sample.

theorem Aissen2003.grid_size : Features.Prominence.AnimacyLevel.all.length * Features.Prominence.DefinitenessLevel.all.length = 15

The bidimensional grid has 3 × 5 = 15 cells per language.

def Aissen2003.totalMarkedCells : ℕ

Total marked cells across all sample languages.

Equations

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

theorem Aissen2003.total_marked_cells_value : totalMarkedCells = 52

Marked cells: Spanish (5) + Russian (10) + Turkish (9) + Hebrew (9) + Persian (9) + Catalan (3) + Hindi (7) + NoDOM (0) = 52.

@[irreducible]

def Aissen2003.interleavings {α : Type} : List α → List α → List (List α)

All interleavings of two lists, preserving internal order of each.

Given two constraint families with fixed internal rankings, this generates all total orders consistent with both. The number of interleavings of lists of lengths m and n is C(m+n, m).

Equations

• One or more equations did not get rendered due to their size.
• Aissen2003.interleavings [] x✝ = [x✝]
• Aissen2003.interleavings x✝ [] = [x✝]

structure Aissen2003.Scale2Cand : Type

DOM candidate for a 2-element prominence scale {High > Low}. true = overtly case-marked; false = zero-marked.

• high : Bool
• low : Bool

def Aissen2003.instDecidableEqScale2Cand.decEq (x✝ x✝¹ : Scale2Cand) : Decidable (x✝ = x✝¹)

Equations

• Aissen2003.instDecidableEqScale2Cand.decEq { high := a, low := a_1 } { high := b, low := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aissen2003.instDecidableEqScale2Cand : DecidableEq Scale2Cand

Equations

• Aissen2003.instDecidableEqScale2Cand = Aissen2003.instDecidableEqScale2Cand.decEq

@[implicit_reducible]

instance Aissen2003.instReprScale2Cand : Repr Scale2Cand

Equations

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

def Aissen2003.instReprScale2Cand.repr : Scale2Cand → ℕ → Std.Format

Equations

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

def Aissen2003.scale2Cands : List Scale2Cand

Equations

• Aissen2003.scale2Cands = [{ high := true, low := true }, { high := true, low := false }, { high := false, low := true }, { high := false, low := false }]

def Aissen2003.starZeroHigh : Core.Constraint.OT.NamedConstraint Scale2Cand

*Ø/High: penalize unmarked High objects.

Equations

• Aissen2003.starZeroHigh = Core.Constraint.OT.mkMark "*Ø/High" fun (c : Aissen2003.Scale2Cand) => c.high = false

def Aissen2003.starZeroLow : Core.Constraint.OT.NamedConstraint Scale2Cand

*Ø/Low: penalize unmarked Low objects.

Equations

• Aissen2003.starZeroLow = Core.Constraint.OT.mkMark "*Ø/Low" fun (c : Aissen2003.Scale2Cand) => c.low = false

def Aissen2003.starBangLow : Core.Constraint.OT.NamedConstraint Scale2Cand

*!/Low: penalize marked Low objects (economy).

Equations

• Aissen2003.starBangLow = Phonology.Constraints.mkDep "*!/Low" fun (c : Aissen2003.Scale2Cand) => c.low = true

def Aissen2003.starBangHigh : Core.Constraint.OT.NamedConstraint Scale2Cand

*!/High: penalize marked High objects (economy).

Equations

• Aissen2003.starBangHigh = Phonology.Constraints.mkDep "*!/High" fun (c : Aissen2003.Scale2Cand) => c.high = true

def Aissen2003.iconicity2 : List (Core.Constraint.OT.NamedConstraint Scale2Cand)

Iconicity family (fixed: *Ø/High >> *Ø/Low).

Equations

• Aissen2003.iconicity2 = [Aissen2003.starZeroHigh, Aissen2003.starZeroLow]

def Aissen2003.economy2 : List (Core.Constraint.OT.NamedConstraint Scale2Cand)

Economy family (fixed: *!/Low >> *!/High).

Equations

• Aissen2003.economy2 = [Aissen2003.starBangLow, Aissen2003.starBangHigh]

def Aissen2003.rankings2 : List (List (Core.Constraint.OT.NamedConstraint Scale2Cand))

All consistent rankings: interleavings of the two families.

Equations

• Aissen2003.rankings2 = Aissen2003.interleavings Aissen2003.iconicity2 Aissen2003.economy2

theorem Aissen2003.rankings2_count : rankings2.length = 6

There are exactly 6 consistent rankings (C(4,2) = 6).

def Aissen2003.optima2 : List (Finset Scale2Cand)

Compute optima for each consistent ranking.

Equations

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

def Aissen2003.types2 : List (Finset Scale2Cand)

Distinct language types.

Equations

• Aissen2003.types2 = Aissen2003.optima2.eraseDups

theorem Aissen2003.two_element_three_types : types2.length = 3

The 2-element scale yields exactly 3 language types, not 4 (Table 14, p. 473).

theorem Aissen2003.no_low_without_high : (optima2.all fun (opts : Finset Scale2Cand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : Scale2Cand) => !(c.low && !c.high)) = true

The impossible pattern — mark Low without High — is never optimal.

structure Aissen2003.AnimCand : Type

DOM candidate for the 3-element animacy scale {Hu > An > In}. true = overtly case-marked; false = zero-marked.

• hu : Bool
• an : Bool
• inan : Bool

@[implicit_reducible]

instance Aissen2003.instDecidableEqAnimCand : DecidableEq AnimCand

Equations

• Aissen2003.instDecidableEqAnimCand = Aissen2003.instDecidableEqAnimCand.decEq

def Aissen2003.instDecidableEqAnimCand.decEq (x✝ x✝¹ : AnimCand) : Decidable (x✝ = x✝¹)

Equations

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

def Aissen2003.instReprAnimCand.repr : AnimCand → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aissen2003.instReprAnimCand : Repr AnimCand

Equations

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

def Aissen2003.animCands : List AnimCand

Equations

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

def Aissen2003.starZeroHu : Core.Constraint.OT.NamedConstraint AnimCand

Iconicity: *Ø/Hu >> *Ø/An >> *Ø/In.

Equations

• Aissen2003.starZeroHu = Core.Constraint.OT.mkMark "*Ø/Hu" fun (c : Aissen2003.AnimCand) => c.hu = false

def Aissen2003.starZeroAn : Core.Constraint.OT.NamedConstraint AnimCand

Equations

• Aissen2003.starZeroAn = Core.Constraint.OT.mkMark "*Ø/An" fun (c : Aissen2003.AnimCand) => c.an = false

def Aissen2003.starZeroIn : Core.Constraint.OT.NamedConstraint AnimCand

Equations

• Aissen2003.starZeroIn = Core.Constraint.OT.mkMark "*Ø/In" fun (c : Aissen2003.AnimCand) => c.inan = false

def Aissen2003.starBangIn : Core.Constraint.OT.NamedConstraint AnimCand

Economy: *!/In >> *!/An >> *!/Hu.

Equations

• Aissen2003.starBangIn = Phonology.Constraints.mkDep "*!/In" fun (c : Aissen2003.AnimCand) => c.inan = true

def Aissen2003.starBangAn : Core.Constraint.OT.NamedConstraint AnimCand

Equations

• Aissen2003.starBangAn = Phonology.Constraints.mkDep "*!/An" fun (c : Aissen2003.AnimCand) => c.an = true

def Aissen2003.starBangHu : Core.Constraint.OT.NamedConstraint AnimCand

Equations

• Aissen2003.starBangHu = Phonology.Constraints.mkDep "*!/Hu" fun (c : Aissen2003.AnimCand) => c.hu = true

def Aissen2003.animIconicity : List (Core.Constraint.OT.NamedConstraint AnimCand)

Iconicity family (fixed: *Ø/Hu >> *Ø/An >> *Ø/In).

Equations

• Aissen2003.animIconicity = [Aissen2003.starZeroHu, Aissen2003.starZeroAn, Aissen2003.starZeroIn]

def Aissen2003.animEconomy : List (Core.Constraint.OT.NamedConstraint AnimCand)

Economy family (fixed: *!/In >> *!/An >> *!/Hu).

Equations

• Aissen2003.animEconomy = [Aissen2003.starBangIn, Aissen2003.starBangAn, Aissen2003.starBangHu]

def Aissen2003.animRankings : List (List (Core.Constraint.OT.NamedConstraint AnimCand))

All consistent rankings for the 3-element scale.

Equations

• Aissen2003.animRankings = Aissen2003.interleavings Aissen2003.animIconicity Aissen2003.animEconomy

theorem Aissen2003.anim_rankings_count : animRankings.length = 20

There are exactly 20 consistent rankings (C(6,3) = 20).

def Aissen2003.animOptima : List (Finset AnimCand)

Compute optima for each consistent ranking.

Equations

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

def Aissen2003.animTypes : List (Finset AnimCand)

Distinct language types.

Equations

• Aissen2003.animTypes = Aissen2003.animOptima.eraseDups

theorem Aissen2003.animacy_four_types : animTypes.length = 4

The 3-element animacy scale yields exactly 4 language types, not 8 (Table 17, p. 476).

theorem Aissen2003.animacy_all_monotone : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => (if c.an = true then c.hu else true) && if c.inan = true then c.an else true) = true

Every generated type is monotone: if An is marked then Hu is too; if In is marked then An is too (Aissen's central prediction).

theorem Aissen2003.anim_type_all : (animTypes.any fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAny opts fun (c : AnimCand) => c.hu && c.an && c.inan) = true

Type 1: mark all (Hu + An + In). Extreme iconicity.

theorem Aissen2003.anim_type_hu_an : (animTypes.any fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAny opts fun (c : AnimCand) => c.hu && c.an && !c.inan) = true

Type 2: mark Hu + An only. Russian pattern (animate accusative).

theorem Aissen2003.anim_type_hu_only : (animTypes.any fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAny opts fun (c : AnimCand) => c.hu && !c.an && !c.inan) = true

Type 3: mark Hu only. Spanish pattern (personal a).

theorem Aissen2003.anim_type_none : (animTypes.any fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAny opts fun (c : AnimCand) => !c.hu && !c.an && !c.inan) = true

Type 4: mark none. No DOM (economy dominates).

theorem Aissen2003.no_in_without_an : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => !(c.inan && !c.an)) = true

Mark In without An: never generated.

theorem Aissen2003.no_an_without_hu : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => !(c.an && !c.hu)) = true

Mark An without Hu: never generated.

theorem Aissen2003.no_in_without_hu : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => !(c.inan && !c.hu)) = true

Mark In without Hu: never generated.

theorem Aissen2003.no_in_only : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => !(c.inan && !c.an && !c.hu)) = true

Mark In only (without An or Hu): never generated.

def Aissen2003.animCandToDOM (c : AnimCand) : DOMProfile

Convert an AnimCand to a one-dimensional animacy DOMProfile.

Equations

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

theorem Aissen2003.ot_types_are_monotone_dom : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => Features.Prominence.DifferentialMarkingProfile.isMonotone (animCandToDOM c)) = true

Every OT-generated animacy type produces a monotone DOMProfile.

theorem Aissen2003.spanish_matches_type3 : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => spanishDOM.marks a d == (animCandToDOM { hu := true, an := false, inan := false }).marks a d) = true

Spanish DOM (human only) matches OT Type 3 (Hu only).

theorem Aissen2003.russian_matches_type2 : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => russianDOM.marks a d == (animCandToDOM { hu := true, an := true, inan := false }).marks a d) = true

Russian DOM (animate+) matches OT Type 2 (Hu + An).

theorem Aissen2003.nodom_matches_type4 : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => noDOMProfile.marks a d == (animCandToDOM { hu := false, an := false, inan := false }).marks a d) = true

No-DOM profile matches OT Type 4 (none marked).

The 2-element definiteness scale {Pro > D} from §4 of the paper, where "D" covers definite NPs (including proper names). This gives the same 3-type factorial typology as any 2-element scale.

def Aissen2003.defCandToDOM (c : Scale2Cand) : DOMProfile

Convert a Scale2Cand to a definiteness-based DOMProfile. High = personalPronoun, Low = properName + definite (i.e., ≥ definite).

Equations

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

theorem Aissen2003.catalan_matches_high_only : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => catalanDOM.marks a d == (defCandToDOM { high := true, low := false }).marks a d) = true

Catalan DOM (pronouns only) matches 2-element Type 2 (High only).

theorem Aissen2003.turkish_matches_both : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => turkishDOM.marks a d == (defCandToDOM { high := true, low := true }).marks a d) = true

Turkish DOM (definite+) matches 2-element Type 1 (both marked).

theorem Aissen2003.hebrew_matches_both : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => hebrewDOM.marks a d == (defCandToDOM { high := true, low := true }).marks a d) = true

Hebrew DOM (definite+) also matches 2-element Type 1.

theorem Aissen2003.animacy_excludes_half : animCands.length = 8 ∧ animTypes.length = 4

Of 8 logically possible 3-element patterns, OT generates exactly 4.

theorem Aissen2003.two_element_excludes_one : scale2Cands.length = 4 ∧ types2.length = 3

Of 4 logically possible 2-element patterns, OT generates exactly 3.

theorem Aissen2003.ranking_counts : rankings2.length = 6 ∧ animRankings.length = 20

The number of consistent rankings grows as C(2n, n). For n=2: C(4,2) = 6. For n=3: C(6,3) = 20.

structure Aissen2003.ProminentNP : Type

An NP enriched with referential prominence properties.

Structural case assignment (dependent case) is blind to these properties — it cares only about c-command and lexical case. DOM then consults prominence to decide overt realization.

• label : String
• lexicalCase : Option Core.Case
• animacy : Features.Prominence.AnimacyLevel
• definiteness : Features.Prominence.DefinitenessLevel

@[implicit_reducible]

instance Aissen2003.instDecidableEqProminentNP : DecidableEq ProminentNP

Equations

• Aissen2003.instDecidableEqProminentNP = Aissen2003.instDecidableEqProminentNP.decEq

def Aissen2003.instDecidableEqProminentNP.decEq (x✝ x✝¹ : ProminentNP) : Decidable (x✝ = x✝¹)

Equations

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

def Aissen2003.instReprProminentNP.repr : ProminentNP → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aissen2003.instReprProminentNP : Repr ProminentNP

Equations

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

def Aissen2003.ProminentNP.toNP (pnp : ProminentNP) : Syntax.Case.NPInDomain

Strip prominence, yielding the NP that the case algorithm sees.

Equations

• pnp.toNP = { label := pnp.label, lexicalCase := pnp.lexicalCase }

structure Aissen2003.TransClause : Type

A transitive clause: subject c-commands object.

• subject : ProminentNP
• object : ProminentNP

@[implicit_reducible]

instance Aissen2003.instDecidableEqTransClause : DecidableEq TransClause

Equations

• Aissen2003.instDecidableEqTransClause = Aissen2003.instDecidableEqTransClause.decEq

def Aissen2003.instDecidableEqTransClause.decEq (x✝ x✝¹ : TransClause) : Decidable (x✝ = x✝¹)

Equations

• Aissen2003.instDecidableEqTransClause.decEq { subject := a, object := a_1 } { subject := b, object := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aissen2003.instReprTransClause : Repr TransClause

Equations

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

def Aissen2003.instReprTransClause.repr : TransClause → ℕ → Std.Format

Equations

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

def Aissen2003.derivation (lang : Syntax.Case.CaseLanguageType) (tc : TransClause) : List Syntax.Case.CasedNP

Run the dependent case algorithm on a transitive clause.

Equations

• Aissen2003.derivation lang tc = Syntax.Case.assignCases lang [tc.subject.toNP, tc.object.toNP]

def Aissen2003.objectCase (lang : Syntax.Case.CaseLanguageType) (tc : TransClause) : Option Core.Case

Abstract case assigned to the object.

Equations

• Aissen2003.objectCase lang tc = Syntax.Case.getCaseOf tc.object.label (Aissen2003.derivation lang tc)

def Aissen2003.objectOvert (lang : Syntax.Case.CaseLanguageType) (dom : DOMProfile) (tc : TransClause) : Bool

Whether the object receives overt case morphology.

Two conditions:

1. The dependent case algorithm assigns ACC (syntax).
2. The DOM profile marks this prominence cell (morphology).

Equations

• Aissen2003.objectOvert lang dom tc = (Aissen2003.objectCase lang tc == some UD.Case.acc && dom.marks tc.object.animacy tc.object.definiteness)

def Aissen2003.mkTrans (a : Features.Prominence.AnimacyLevel) (d : Features.Prominence.DefinitenessLevel) : TransClause

A standard transitive clause with a fixed subject (human pronoun) and a variable-prominence object. Both lack lexical case.

Equations

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

theorem Aissen2003.object_always_acc : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => objectCase Syntax.Case.CaseLanguageType.accusative (mkTrans a d) == some UD.Case.acc) = true

In accusative transitives, the object receives abstract ACC regardless of its animacy or definiteness. Dependent case is prominence-blind.

theorem Aissen2003.subject_always_nom : (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => Syntax.Case.getCaseOf "subj" (derivation Syntax.Case.CaseLanguageType.accusative (mkTrans a d)) == some UD.Case.nom) = true

The subject always gets NOM (unmarked case).

def Aissen2003.overtProfile (lang : Syntax.Case.CaseLanguageType) (dom : DOMProfile) : DOMProfile

The overt marking profile produced by running the full pipeline (dependent case + DOM filter).

Equations

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

theorem Aissen2003.ot_pipeline_monotone : (animOptima.all fun (opts : Finset AnimCand) => Core.Constraint.Evaluation.Finset.checkAll opts fun (c : AnimCand) => Features.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Syntax.Case.CaseLanguageType.accusative (animCandToDOM c))) = true

Every OT-predicted animacy type, run through the full pipeline, produces a monotone overt marking profile.

theorem Aissen2003.attested_pipeline_monotone : (allDOMProfiles.all fun (dom : DOMProfile) => Features.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Syntax.Case.CaseLanguageType.accusative dom)) = true

The pipeline preserves monotonicity for all attested DOM languages.

theorem Aissen2003.full_pipeline_faithful_and_monotone : (allDOMProfiles.all fun (dom : DOMProfile) => (Features.Prominence.AnimacyLevel.all.all fun (a : Features.Prominence.AnimacyLevel) => Features.Prominence.DefinitenessLevel.all.all fun (d : Features.Prominence.DefinitenessLevel) => decide ((overtProfile Syntax.Case.CaseLanguageType.accusative dom).marks a d = dom.marks a d)) && Features.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Syntax.Case.CaseLanguageType.accusative dom)) = true

All 8 attested DOM profiles, run through the accusative case pipeline, produce overt marking that is faithful to the DOM input AND monotone.