@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 Phenomena.Case.Typology, verifying that every attested pattern corresponds to a possible OT grammar.

@[irreducible]

def Phenomena.Case.Studies.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.
• Phenomena.Case.Studies.Aissen2003.interleavings [] x✝ = [x✝]
• Phenomena.Case.Studies.Aissen2003.interleavings x✝ [] = [x✝]

structure Phenomena.Case.Studies.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 Phenomena.Case.Studies.Aissen2003.instDecidableEqScale2Cand.decEq (x✝ x✝¹ : Scale2Cand) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Studies.Aissen2003.instDecidableEqScale2Cand : DecidableEq Scale2Cand

Equations

• Phenomena.Case.Studies.Aissen2003.instDecidableEqScale2Cand = Phenomena.Case.Studies.Aissen2003.instDecidableEqScale2Cand.decEq

def Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand.beq : Scale2Cand → Scale2Cand → Bool

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand.beq { high := a, low := a_1 } { high := b, low := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand : BEq Scale2Cand

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand = { beq := Phenomena.Case.Studies.Aissen2003.instBEqScale2Cand.beq }

instance Phenomena.Case.Studies.Aissen2003.instReprScale2Cand : Repr Scale2Cand

Equations

• Phenomena.Case.Studies.Aissen2003.instReprScale2Cand = { reprPrec := Phenomena.Case.Studies.Aissen2003.instReprScale2Cand.repr }

def Phenomena.Case.Studies.Aissen2003.instReprScale2Cand.repr : Scale2Cand → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Aissen2003.scale2Cands : List Scale2Cand

Equations

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

theorem Phenomena.Case.Studies.Aissen2003.scale2_nonempty : scale2Cands ≠ []

def Phenomena.Case.Studies.Aissen2003.starZeroHigh : Core.OT.NamedConstraint Scale2Cand

*Ø/High: penalize unmarked High objects.

Equations

• Phenomena.Case.Studies.Aissen2003.starZeroHigh = Theories.Phonology.Constraints.mkMark "*Ø/High" fun (c : Phenomena.Case.Studies.Aissen2003.Scale2Cand) => !c.high

def Phenomena.Case.Studies.Aissen2003.starZeroLow : Core.OT.NamedConstraint Scale2Cand

*Ø/Low: penalize unmarked Low objects.

Equations

• Phenomena.Case.Studies.Aissen2003.starZeroLow = Theories.Phonology.Constraints.mkMark "*Ø/Low" fun (c : Phenomena.Case.Studies.Aissen2003.Scale2Cand) => !c.low

def Phenomena.Case.Studies.Aissen2003.starBangLow : Core.OT.NamedConstraint Scale2Cand

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

Equations

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

def Phenomena.Case.Studies.Aissen2003.starBangHigh : Core.OT.NamedConstraint Scale2Cand

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

Equations

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

def Phenomena.Case.Studies.Aissen2003.iconicity2 : List (Core.OT.NamedConstraint Scale2Cand)

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

Equations

• Phenomena.Case.Studies.Aissen2003.iconicity2 = [Phenomena.Case.Studies.Aissen2003.starZeroHigh, Phenomena.Case.Studies.Aissen2003.starZeroLow]

def Phenomena.Case.Studies.Aissen2003.economy2 : List (Core.OT.NamedConstraint Scale2Cand)

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

Equations

• Phenomena.Case.Studies.Aissen2003.economy2 = [Phenomena.Case.Studies.Aissen2003.starBangLow, Phenomena.Case.Studies.Aissen2003.starBangHigh]

def Phenomena.Case.Studies.Aissen2003.rankings2 : List (List (Core.OT.NamedConstraint Scale2Cand))

All consistent rankings: interleavings of the two families.

Equations

• Phenomena.Case.Studies.Aissen2003.rankings2 = Phenomena.Case.Studies.Aissen2003.interleavings Phenomena.Case.Studies.Aissen2003.iconicity2 Phenomena.Case.Studies.Aissen2003.economy2

theorem Phenomena.Case.Studies.Aissen2003.rankings2_count : rankings2.length = 6

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

def Phenomena.Case.Studies.Aissen2003.optima2 : List (List Scale2Cand)

Compute optima for each consistent ranking.

Equations

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

def Phenomena.Case.Studies.Aissen2003.types2 : List (List Scale2Cand)

Distinct language types.

Equations

• Phenomena.Case.Studies.Aissen2003.types2 = Phenomena.Case.Studies.Aissen2003.optima2.eraseDups

theorem Phenomena.Case.Studies.Aissen2003.two_element_three_types : types2.length = 3

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

theorem Phenomena.Case.Studies.Aissen2003.no_low_without_high : (optima2.all fun (opts : List Scale2Cand) => opts.all fun (c : Scale2Cand) => !(c.low && !c.high)) = true

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

structure Phenomena.Case.Studies.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

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

Equations

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

instance Phenomena.Case.Studies.Aissen2003.instDecidableEqAnimCand : DecidableEq AnimCand

Equations

• Phenomena.Case.Studies.Aissen2003.instDecidableEqAnimCand = Phenomena.Case.Studies.Aissen2003.instDecidableEqAnimCand.decEq

instance Phenomena.Case.Studies.Aissen2003.instBEqAnimCand : BEq AnimCand

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqAnimCand = { beq := Phenomena.Case.Studies.Aissen2003.instBEqAnimCand.beq }

def Phenomena.Case.Studies.Aissen2003.instBEqAnimCand.beq : AnimCand → AnimCand → Bool

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqAnimCand.beq { hu := a, an := a_1, inan := a_2 } { hu := b, an := b_1, inan := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Phenomena.Case.Studies.Aissen2003.instBEqAnimCand.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Aissen2003.instReprAnimCand : Repr AnimCand

Equations

• Phenomena.Case.Studies.Aissen2003.instReprAnimCand = { reprPrec := Phenomena.Case.Studies.Aissen2003.instReprAnimCand.repr }

def Phenomena.Case.Studies.Aissen2003.instReprAnimCand.repr : AnimCand → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Aissen2003.animCands : List AnimCand

Equations

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

theorem Phenomena.Case.Studies.Aissen2003.anim_nonempty : animCands ≠ []

def Phenomena.Case.Studies.Aissen2003.starZeroHu : Core.OT.NamedConstraint AnimCand

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

Equations

• Phenomena.Case.Studies.Aissen2003.starZeroHu = Theories.Phonology.Constraints.mkMark "*Ø/Hu" fun (c : Phenomena.Case.Studies.Aissen2003.AnimCand) => !c.hu

def Phenomena.Case.Studies.Aissen2003.starZeroAn : Core.OT.NamedConstraint AnimCand

Equations

• Phenomena.Case.Studies.Aissen2003.starZeroAn = Theories.Phonology.Constraints.mkMark "*Ø/An" fun (c : Phenomena.Case.Studies.Aissen2003.AnimCand) => !c.an

def Phenomena.Case.Studies.Aissen2003.starZeroIn : Core.OT.NamedConstraint AnimCand

Equations

• Phenomena.Case.Studies.Aissen2003.starZeroIn = Theories.Phonology.Constraints.mkMark "*Ø/In" fun (c : Phenomena.Case.Studies.Aissen2003.AnimCand) => !c.inan

def Phenomena.Case.Studies.Aissen2003.starBangIn : Core.OT.NamedConstraint AnimCand

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

Equations

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

def Phenomena.Case.Studies.Aissen2003.starBangAn : Core.OT.NamedConstraint AnimCand

Equations

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

def Phenomena.Case.Studies.Aissen2003.starBangHu : Core.OT.NamedConstraint AnimCand

Equations

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

def Phenomena.Case.Studies.Aissen2003.animIconicity : List (Core.OT.NamedConstraint AnimCand)

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

Equations

• Phenomena.Case.Studies.Aissen2003.animIconicity = [Phenomena.Case.Studies.Aissen2003.starZeroHu, Phenomena.Case.Studies.Aissen2003.starZeroAn, Phenomena.Case.Studies.Aissen2003.starZeroIn]

def Phenomena.Case.Studies.Aissen2003.animEconomy : List (Core.OT.NamedConstraint AnimCand)

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

Equations

• Phenomena.Case.Studies.Aissen2003.animEconomy = [Phenomena.Case.Studies.Aissen2003.starBangIn, Phenomena.Case.Studies.Aissen2003.starBangAn, Phenomena.Case.Studies.Aissen2003.starBangHu]

def Phenomena.Case.Studies.Aissen2003.animRankings : List (List (Core.OT.NamedConstraint AnimCand))

All consistent rankings for the 3-element scale.

Equations

• Phenomena.Case.Studies.Aissen2003.animRankings = Phenomena.Case.Studies.Aissen2003.interleavings Phenomena.Case.Studies.Aissen2003.animIconicity Phenomena.Case.Studies.Aissen2003.animEconomy

theorem Phenomena.Case.Studies.Aissen2003.anim_rankings_count : animRankings.length = 20

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

def Phenomena.Case.Studies.Aissen2003.animOptima : List (List AnimCand)

Compute optima for each consistent ranking.

Equations

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

def Phenomena.Case.Studies.Aissen2003.animTypes : List (List AnimCand)

Distinct language types.

Equations

• Phenomena.Case.Studies.Aissen2003.animTypes = Phenomena.Case.Studies.Aissen2003.animOptima.eraseDups

theorem Phenomena.Case.Studies.Aissen2003.animacy_four_types : animTypes.length = 4

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

theorem Phenomena.Case.Studies.Aissen2003.animacy_all_monotone : (animOptima.all fun (opts : List AnimCand) => opts.all 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 Phenomena.Case.Studies.Aissen2003.anim_type_all : (animTypes.any fun (opts : List AnimCand) => opts.any fun (c : AnimCand) => c.hu && c.an && c.inan) = true

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

theorem Phenomena.Case.Studies.Aissen2003.anim_type_hu_an : (animTypes.any fun (opts : List AnimCand) => opts.any fun (c : AnimCand) => c.hu && c.an && !c.inan) = true

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

theorem Phenomena.Case.Studies.Aissen2003.anim_type_hu_only : (animTypes.any fun (opts : List AnimCand) => opts.any fun (c : AnimCand) => c.hu && !c.an && !c.inan) = true

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

theorem Phenomena.Case.Studies.Aissen2003.anim_type_none : (animTypes.any fun (opts : List AnimCand) => opts.any fun (c : AnimCand) => !c.hu && !c.an && !c.inan) = true

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

theorem Phenomena.Case.Studies.Aissen2003.no_in_without_an : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => !(c.inan && !c.an)) = true

Mark In without An: never generated.

theorem Phenomena.Case.Studies.Aissen2003.no_an_without_hu : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => !(c.an && !c.hu)) = true

Mark An without Hu: never generated.

theorem Phenomena.Case.Studies.Aissen2003.no_in_without_hu : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => !(c.inan && !c.hu)) = true

Mark In without Hu: never generated.

theorem Phenomena.Case.Studies.Aissen2003.no_in_only : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => !(c.inan && !c.an && !c.hu)) = true

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

def Phenomena.Case.Studies.Aissen2003.animCandToDOM (c : AnimCand) : Typology.DOMProfile

Convert an AnimCand to a one-dimensional animacy DOMProfile.

Equations

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

theorem Phenomena.Case.Studies.Aissen2003.ot_types_are_monotone_dom : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => Core.Prominence.DifferentialMarkingProfile.isMonotone (animCandToDOM c)) = true

Every OT-generated animacy type produces a monotone DOMProfile.

theorem Phenomena.Case.Studies.Aissen2003.spanish_matches_type3 : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Typology.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 Phenomena.Case.Studies.Aissen2003.russian_matches_type2 : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Typology.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 Phenomena.Case.Studies.Aissen2003.nodom_matches_type4 : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Typology.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 Phenomena.Case.Studies.Aissen2003.defCandToDOM (c : Scale2Cand) : Typology.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 Phenomena.Case.Studies.Aissen2003.catalan_matches_high_only : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Typology.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 Phenomena.Case.Studies.Aissen2003.turkish_matches_both : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Typology.turkishDOM.marks a d == (defCandToDOM { high := true, low := true }).marks a d) = true

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

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

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

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

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

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

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

theorem Phenomena.Case.Studies.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 Phenomena.Case.Studies.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 Minimalism.CaseVal
• animacy : Core.Prominence.AnimacyLevel
• definiteness : Core.Prominence.DefinitenessLevel

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

Equations

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

instance Phenomena.Case.Studies.Aissen2003.instDecidableEqProminentNP : DecidableEq ProminentNP

Equations

• Phenomena.Case.Studies.Aissen2003.instDecidableEqProminentNP = Phenomena.Case.Studies.Aissen2003.instDecidableEqProminentNP.decEq

instance Phenomena.Case.Studies.Aissen2003.instBEqProminentNP : BEq ProminentNP

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqProminentNP = { beq := Phenomena.Case.Studies.Aissen2003.instBEqProminentNP.beq }

def Phenomena.Case.Studies.Aissen2003.instBEqProminentNP.beq : ProminentNP → ProminentNP → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Case.Studies.Aissen2003.instBEqProminentNP.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Aissen2003.instReprProminentNP : Repr ProminentNP

Equations

• Phenomena.Case.Studies.Aissen2003.instReprProminentNP = { reprPrec := Phenomena.Case.Studies.Aissen2003.instReprProminentNP.repr }

def Phenomena.Case.Studies.Aissen2003.instReprProminentNP.repr : ProminentNP → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Aissen2003.ProminentNP.toNP (pnp : ProminentNP) : Minimalism.NPInDomain

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

Equations

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

structure Phenomena.Case.Studies.Aissen2003.TransClause : Type

A transitive clause: subject c-commands object.

• subject : ProminentNP
• object : ProminentNP

instance Phenomena.Case.Studies.Aissen2003.instDecidableEqTransClause : DecidableEq TransClause

Equations

• Phenomena.Case.Studies.Aissen2003.instDecidableEqTransClause = Phenomena.Case.Studies.Aissen2003.instDecidableEqTransClause.decEq

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

Equations

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

instance Phenomena.Case.Studies.Aissen2003.instBEqTransClause : BEq TransClause

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqTransClause = { beq := Phenomena.Case.Studies.Aissen2003.instBEqTransClause.beq }

def Phenomena.Case.Studies.Aissen2003.instBEqTransClause.beq : TransClause → TransClause → Bool

Equations

• Phenomena.Case.Studies.Aissen2003.instBEqTransClause.beq { subject := a, object := a_1 } { subject := b, object := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Case.Studies.Aissen2003.instBEqTransClause.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Aissen2003.instReprTransClause : Repr TransClause

Equations

• Phenomena.Case.Studies.Aissen2003.instReprTransClause = { reprPrec := Phenomena.Case.Studies.Aissen2003.instReprTransClause.repr }

def Phenomena.Case.Studies.Aissen2003.instReprTransClause.repr : TransClause → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Aissen2003.derivation (lang : Minimalism.CaseLanguageType) (tc : TransClause) : List Minimalism.CasedNP

Run the dependent case algorithm on a transitive clause.

Equations

• Phenomena.Case.Studies.Aissen2003.derivation lang tc = Minimalism.assignCases lang [tc.subject.toNP, tc.object.toNP]

def Phenomena.Case.Studies.Aissen2003.objectCase (lang : Minimalism.CaseLanguageType) (tc : TransClause) : Option Minimalism.CaseVal

Abstract case assigned to the object.

Equations

• Phenomena.Case.Studies.Aissen2003.objectCase lang tc = Minimalism.getCaseOf tc.object.label (Phenomena.Case.Studies.Aissen2003.derivation lang tc)

def Phenomena.Case.Studies.Aissen2003.objectOvert (lang : Minimalism.CaseLanguageType) (dom : Typology.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

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

def Phenomena.Case.Studies.Aissen2003.mkTrans (a : Core.Prominence.AnimacyLevel) (d : Core.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 Phenomena.Case.Studies.Aissen2003.object_always_acc : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => objectCase Minimalism.CaseLanguageType.accusative (mkTrans a d) == some Minimalism.CaseVal.acc) = true

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

theorem Phenomena.Case.Studies.Aissen2003.subject_always_nom : (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => Minimalism.getCaseOf "subj" (derivation Minimalism.CaseLanguageType.accusative (mkTrans a d)) == some Minimalism.CaseVal.nom) = true

The subject always gets NOM (unmarked case).

def Phenomena.Case.Studies.Aissen2003.overtProfile (lang : Minimalism.CaseLanguageType) (dom : Typology.DOMProfile) : Typology.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 Phenomena.Case.Studies.Aissen2003.ot_pipeline_monotone : (animOptima.all fun (opts : List AnimCand) => opts.all fun (c : AnimCand) => Core.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Minimalism.CaseLanguageType.accusative (animCandToDOM c))) = true

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

theorem Phenomena.Case.Studies.Aissen2003.attested_pipeline_monotone : (Typology.allDOMProfiles.all fun (dom : Typology.DOMProfile) => Core.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Minimalism.CaseLanguageType.accusative dom)) = true

The pipeline preserves monotonicity for all attested DOM languages.

theorem Phenomena.Case.Studies.Aissen2003.full_pipeline_faithful_and_monotone : (Typology.allDOMProfiles.all fun (dom : Typology.DOMProfile) => (Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => decide ((overtProfile Minimalism.CaseLanguageType.accusative dom).marks a d = dom.marks a d)) && Core.Prominence.DifferentialMarkingProfile.isMonotone (overtProfile Minimalism.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.