Wechsler & Zlatić (2000): A Theory of Agreement and Its Application to Serbo-Croatian

This file formalizes [WZ00]'s theory of agreement. A noun carries two feature bundles: CONCORD, with case, number and gender, read by NP-internal targets, and the referential INDEX of [PS94], with person, number and gender, read by pronouns and finite verbs. Declension class, concord, index and semantics are tied by a chain of three binary constraints (4): a class I noun has masculine or neuter concord gender and a class II or III noun feminine (DecCon); concord and index share number and gender (ConInd); a noun restricted to females or males has feminine or masculine index, and an aggregate-denoting count noun a plural one, other nouns a singular one (IndSem). A regular noun satisfies every link, and a hybrid noun breaks one: Steva the first, deca the second, makaze the third, while braća breaks two (brokenLinks). Of the seven two-type mismatch patterns a priori, the three the theory predicts are the initial segments of the chain, and exactly those are attested (predicted_patterns). Agreement itself is compatibility of a target's bundle with the bundle it reads, which on deca puts feminine singular on the modifiers and neuter plural on the pronoun at once (deca_mixed_agreement) and lets the concord-unmarked plural relative pronoun kojih modify it. Since only the index touches the semantics, semantic agreement can surface on a concord reader only if it surfaces on the pronouns: the index readers form a lower set of [Cor91]'s Agreement Hierarchy however the open predicate position is resolved (indexReaders_lowerSet).

Implementation notes

Lexical entries carry the singular citation form's concord number for count nouns and the lexically fixed values for collectives and pluralia tantum, whose declension is the value "pl" of the paper's summary table rather than a numbered class, and whose concord gender, left open there, is supplied as feminine. The disjunctively sex-specified nouns sudija and mušterija are entered as their resolved variants. Concord-ending syncretism, participle agreement, coordination resolution and the HPSG spell-out function are not formalized.

References

• [WZ00]
• [Cor91]
• [Cor98]
• [PS94]

Feature bundles

inductive WechslerZlatic2000.Declension : Type

The Serbo-Croatian declension classes of Table 1, with pluralia tantum outside the singular classification.

• I : Declension
• II : Declension
• III : Declension
• pluralia : Declension

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqDeclension : DecidableEq Declension

Equations

• WechslerZlatic2000.instDecidableEqDeclension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprDeclension.repr : Declension → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprDeclension : Repr Declension

Equations

• WechslerZlatic2000.instReprDeclension = { reprPrec := WechslerZlatic2000.instReprDeclension.repr }

structure WechslerZlatic2000.ConcordF : Type

The lexical CONCORD features, number and gender; case is contextual.

• number : Number
• gender : Gender

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqConcordF : DecidableEq ConcordF

Equations

• WechslerZlatic2000.instDecidableEqConcordF = WechslerZlatic2000.instDecidableEqConcordF.decEq

def WechslerZlatic2000.instDecidableEqConcordF.decEq (x✝ x✝¹ : ConcordF) : Decidable (x✝ = x✝¹)

Equations

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

def WechslerZlatic2000.instReprConcordF.repr : ConcordF → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprConcordF : Repr ConcordF

Equations

• WechslerZlatic2000.instReprConcordF = { reprPrec := WechslerZlatic2000.instReprConcordF.repr }

structure WechslerZlatic2000.IndexF : Type

The INDEX features (8): person, number and gender.

• person : Person
• number : Number
• gender : Gender

def WechslerZlatic2000.instDecidableEqIndexF.decEq (x✝ x✝¹ : IndexF) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqIndexF : DecidableEq IndexF

Equations

• WechslerZlatic2000.instDecidableEqIndexF = WechslerZlatic2000.instDecidableEqIndexF.decEq

@[instance_reducible]

instance WechslerZlatic2000.instReprIndexF : Repr IndexF

Equations

• WechslerZlatic2000.instReprIndexF = { reprPrec := WechslerZlatic2000.instReprIndexF.repr }

def WechslerZlatic2000.instReprIndexF.repr : IndexF → ℕ → Std.Format

Equations

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

inductive WechslerZlatic2000.SexRestriction : Type

The sex a noun's referent is lexically restricted to, if any (18).

• female : SexRestriction
• male : SexRestriction
• unrestricted : SexRestriction

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqSexRestriction : DecidableEq SexRestriction

Equations

• WechslerZlatic2000.instDecidableEqSexRestriction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprSexRestriction.repr : SexRestriction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprSexRestriction : Repr SexRestriction

Equations

• WechslerZlatic2000.instReprSexRestriction = { reprPrec := WechslerZlatic2000.instReprSexRestriction.repr }

inductive WechslerZlatic2000.Count : Type

The COUNT value of a count noun (22).

• one : Count
• aggregate : Count

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqCount : DecidableEq Count

Equations

• WechslerZlatic2000.instDecidableEqCount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprCount.repr : Count → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprCount : Repr Count

Equations

• WechslerZlatic2000.instReprCount = { reprPrec := WechslerZlatic2000.instReprCount.repr }

structure WechslerZlatic2000.Noun : Type

The agreement-relevant lexical entry of a noun: the four positions of the chain.

• decl : Declension
• concord : ConcordF
• index : IndexF
• sex : SexRestriction
• count : Option Count

def WechslerZlatic2000.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqNoun : DecidableEq Noun

Equations

• WechslerZlatic2000.instDecidableEqNoun = WechslerZlatic2000.instDecidableEqNoun.decEq

def WechslerZlatic2000.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprNoun : Repr Noun

Equations

• WechslerZlatic2000.instReprNoun = { reprPrec := WechslerZlatic2000.instReprNoun.repr }

The chain (4)

def WechslerZlatic2000.DecCon (n : Noun) : Prop

DecCon (15): class I nouns have masculine or neuter concord gender, class II and III nouns feminine; the constraint does not reach pluralia tantum.

Equations

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

def WechslerZlatic2000.ConInd (n : Noun) : Prop

ConInd (17): concord and index share number and gender.

Equations

• WechslerZlatic2000.ConInd n = (n.concord.number = n.index.number ∧ n.concord.gender = n.index.gender)

def WechslerZlatic2000.IndSemGen (n : Noun) : Prop

IndSemGen (18): a female-restricted noun has feminine index, a male-restricted one masculine.

Equations

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

def WechslerZlatic2000.IndSemNum (n : Noun) : Prop

IndSemNum (22): aggregate reference gives plural index, anything else singular.

Equations

• WechslerZlatic2000.IndSemNum n = match n.count with | some WechslerZlatic2000.Count.aggregate => n.index.number = Number.plural | x => n.index.number = Number.singular

def WechslerZlatic2000.IndSem (n : Noun) : Prop

The index–semantics link, both halves.

Equations

• WechslerZlatic2000.IndSem n = (WechslerZlatic2000.IndSemGen n ∧ WechslerZlatic2000.IndSemNum n)

@[instance_reducible]

instance WechslerZlatic2000.instDecidableDecCon (n : Noun) : Decidable (DecCon n)

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instDecidableConInd (n : Noun) : Decidable (ConInd n)

Equations

• WechslerZlatic2000.instDecidableConInd n = id inferInstance

@[instance_reducible]

instance WechslerZlatic2000.instDecidableIndSemGen (n : Noun) : Decidable (IndSemGen n)

Equations

• WechslerZlatic2000.instDecidableIndSemGen n = id inferInstance

@[instance_reducible]

instance WechslerZlatic2000.instDecidableIndSemNum (n : Noun) : Decidable (IndSemNum n)

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instDecidableIndSem (n : Noun) : Decidable (IndSem n)

Equations

• WechslerZlatic2000.instDecidableIndSem n = { decide := decide (WechslerZlatic2000.IndSemGen n) && decide (WechslerZlatic2000.IndSemNum n), reflects_decide := ⋯ }

inductive WechslerZlatic2000.ChainLink : Type

The three links of the chain, left to right.

• decCon : ChainLink
• conInd : ChainLink
• indSem : ChainLink

@[instance_reducible]

instance WechslerZlatic2000.instDecidableEqChainLink : DecidableEq ChainLink

Equations

• WechslerZlatic2000.instDecidableEqChainLink x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def WechslerZlatic2000.instReprChainLink.repr : ChainLink → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance WechslerZlatic2000.instReprChainLink : Repr ChainLink

Equations

• WechslerZlatic2000.instReprChainLink = { reprPrec := WechslerZlatic2000.instReprChainLink.repr }

@[instance_reducible]

instance WechslerZlatic2000.instFintypeChainLink : Fintype ChainLink

Equations

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

def WechslerZlatic2000.linkHolds (n : Noun) : ChainLink → Prop

Whether a link holds of a noun.

Equations

• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.decCon = WechslerZlatic2000.DecCon n
• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.conInd = WechslerZlatic2000.ConInd n
• WechslerZlatic2000.linkHolds n WechslerZlatic2000.ChainLink.indSem = WechslerZlatic2000.IndSem n

@[instance_reducible]

instance WechslerZlatic2000.instDecidableLinkHolds (n : Noun) (l : ChainLink) : Decidable (linkHolds n l)

Equations

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

def WechslerZlatic2000.brokenLinks (n : Noun) : Finset ChainLink

The mismatch pattern of a noun: its broken links (5).

Equations

• WechslerZlatic2000.brokenLinks n = {l : WechslerZlatic2000.ChainLink | ¬WechslerZlatic2000.linkHolds n l}

def WechslerZlatic2000.Regular (n : Noun) : Prop

A noun is regular when every link holds.

Equations

• WechslerZlatic2000.Regular n = ∀ (l : WechslerZlatic2000.ChainLink), WechslerZlatic2000.linkHolds n l

@[instance_reducible]

instance WechslerZlatic2000.instDecidableRegular (n : Noun) : Decidable (Regular n)

Equations

• WechslerZlatic2000.instDecidableRegular n = { decide := decide (∀ a ∈ Finset.univ, WechslerZlatic2000.linkHolds n a), reflects_decide := ⋯ }

The lexicon (Table 3)

def WechslerZlatic2000.knjiga : Noun

knjiga 'book': regular class II.

Equations

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

def WechslerZlatic2000.rad : Noun

rad 'work': regular class I.

Equations

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

def WechslerZlatic2000.žena : Noun

žena 'woman': regular and female-denoting.

Equations

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

def WechslerZlatic2000.muž : Noun

muž 'husband': regular and male-denoting.

Equations

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

def WechslerZlatic2000.kit : Noun

kit 'whale': masculine with no sex restriction (21).

Equations

• WechslerZlatic2000.kit = WechslerZlatic2000.rad

def WechslerZlatic2000.steva : Noun

Steva: a male name declining in class II (28); sudija 'judge' and mušterija 'customer' applied to males pattern alike (19a), (30b).

Equations

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

def WechslerZlatic2000.sudijaFemale : Noun

sudija applied to a female (19b): the other resolution of the disjunction (20).

Equations

• WechslerZlatic2000.sudijaFemale = WechslerZlatic2000.žena

def WechslerZlatic2000.mušterijaUnsexed : Noun

mušterija with the male restriction absent (30a), (32a).

Equations

• WechslerZlatic2000.mušterijaUnsexed = WechslerZlatic2000.knjiga

def WechslerZlatic2000.deca : Noun

deca 'children': feminine singular concord, neuter plural index (45).

Equations

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

def WechslerZlatic2000.gospoda : Noun

gospoda 'gentlemen': like deca, male-restricted with masculine plural index (40).

Equations

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

def WechslerZlatic2000.braća : Noun

braća 'brothers': male-restricted with feminine singular concord and neuter plural index (39).

Equations

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

def WechslerZlatic2000.makaze : Noun

makaze 'scissors' read as one pair: plural throughout against singular reference (35).

Equations

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

def WechslerZlatic2000.devojče : Noun

devojče 'girl': female-denoting with neuter index (11).

Equations

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

theorem WechslerZlatic2000.regular_lexicon : Regular knjiga ∧ Regular rad ∧ Regular žena ∧ Regular muž ∧ Regular sudijaFemale ∧ Regular mušterijaUnsexed

The regular nouns satisfy the whole chain.

theorem WechslerZlatic2000.hybrid_lexicon : brokenLinks steva = {ChainLink.decCon} ∧ brokenLinks deca = {ChainLink.conInd} ∧ brokenLinks gospoda = {ChainLink.conInd} ∧ brokenLinks makaze = {ChainLink.indSem} ∧ brokenLinks devojče = {ChainLink.indSem} ∧ brokenLinks braća = {ChainLink.conInd, ChainLink.indSem}

The hybrid nouns break exactly the links of Table 3.

Seven patterns, three predicted

def WechslerZlatic2000.bipartitions : Finset (Finset (Fin 4))

A two-type mismatch pattern is a bipartition of the four chain positions, identified with the cell of the declension position.

Equations

• WechslerZlatic2000.bipartitions = {S : Finset (Fin 4) | 0 ∈ S ∧ S ≠ Finset.univ}

def WechslerZlatic2000.ChainLink.position : ChainLink → Fin 4

The position of the break at a link.

Equations

• WechslerZlatic2000.ChainLink.decCon.position = 0
• WechslerZlatic2000.ChainLink.conInd.position = 1
• WechslerZlatic2000.ChainLink.indSem.position = 2

def WechslerZlatic2000.cell (l : ChainLink) : Finset (Fin 4)

The cell of the declension position when the chain breaks at one link: the positions up to the break.

Equations

• WechslerZlatic2000.cell l = {x : Fin 4 | x ≤ l.position}

def WechslerZlatic2000.IsInitialSegment (S : Finset (Fin 4)) : Prop

A pattern the chain can produce is an initial segment of the chain.

Equations

• WechslerZlatic2000.IsInitialSegment S = ∀ i ∈ S, ∀ j ≤ i, j ∈ S

@[instance_reducible]

instance WechslerZlatic2000.instDecidablePredFinsetFinOfNatNatIsInitialSegment : DecidablePred IsInitialSegment

Equations

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

theorem WechslerZlatic2000.seven_patterns : bipartitions.card = 7

Seven patterns a priori (n. 3).

theorem WechslerZlatic2000.predicted_patterns : Finset.filter IsInitialSegment bipartitions = Finset.image cell Finset.univ ∧ (Finset.image cell Finset.univ).card = 3 ∧ brokenLinks steva = {ChainLink.decCon} ∧ brokenLinks deca = {ChainLink.conInd} ∧ brokenLinks makaze = {ChainLink.indSem}

The predicted patterns are the three single breaks, and they are attested by Steva, deca and makaze.

Agreement as compatibility

def WechslerZlatic2000.concordBundle (c : Case) (n : Flat Number) (g : Flat Gender) : Agreement.Bundle

The bundle of an NP-internal target: its case, and its concord number and gender where it is marked for them.

Equations

• WechslerZlatic2000.concordBundle c n g Agreement.Dimension.case = ↑c
• WechslerZlatic2000.concordBundle c n g Agreement.Dimension.number = n
• WechslerZlatic2000.concordBundle c n g Agreement.Dimension.gender = g
• WechslerZlatic2000.concordBundle c n g x✝ = ⊥

def WechslerZlatic2000.indexBundle (p : Person) (n : Number) (g : Gender) : Agreement.Bundle

The bundle of an index-reading target, a pronoun or a finite verb.

Equations

• WechslerZlatic2000.indexBundle p n g Agreement.Dimension.person = ↑p
• WechslerZlatic2000.indexBundle p n g Agreement.Dimension.number = ↑n
• WechslerZlatic2000.indexBundle p n g Agreement.Dimension.gender = ↑g
• WechslerZlatic2000.indexBundle p n g x✝ = ⊥

def WechslerZlatic2000.Noun.concordAt (n : Noun) (c : Case) : Agreement.Bundle

The noun's concord bundle at a case value.

Equations

• n.concordAt c = WechslerZlatic2000.concordBundle c ↑n.concord.number ↑n.concord.gender

def WechslerZlatic2000.Noun.indexTarget (n : Noun) : Agreement.Bundle

The noun's index bundle.

Equations

• n.indexTarget = WechslerZlatic2000.indexBundle n.index.person n.index.number n.index.gender

def WechslerZlatic2000.ConcordAgrees (a : Agreement.Bundle) (n : Noun) (c : Case) : Prop

Concord: the target's bundle is compatible with the noun's concord at the case.

Equations

• WechslerZlatic2000.ConcordAgrees a n c = Compat a (n.concordAt c)

def WechslerZlatic2000.IndexAgrees (p : Agreement.Bundle) (n : Noun) : Prop

Index agreement: the target's bundle is compatible with the noun's index.

Equations

• WechslerZlatic2000.IndexAgrees p n = Compat p n.indexTarget

@[instance_reducible]

instance WechslerZlatic2000.instDecidableConcordAgrees (a : Agreement.Bundle) (n : Noun) (c : Case) : Decidable (ConcordAgrees a n c)

Equations

• WechslerZlatic2000.instDecidableConcordAgrees a n c = { decide := decide (PartialUnify.unify a (n.concordAt c) ≠ ⊤), reflects_decide := ⋯ }

@[instance_reducible]

instance WechslerZlatic2000.instDecidableIndexAgrees (p : Agreement.Bundle) (n : Noun) : Decidable (IndexAgrees p n)

Equations

• WechslerZlatic2000.instDecidableIndexAgrees p n = { decide := decide (PartialUnify.unify p n.indexTarget ≠ ⊤), reflects_decide := ⋯ }

def WechslerZlatic2000.ovu : Agreement.Bundle

ovu dobru: accusative feminine singular modifiers (41).

Equations

• WechslerZlatic2000.ovu = WechslerZlatic2000.concordBundle Case.acc ↑Number.singular ↑Gender.feminine

def WechslerZlatic2000.ona : Agreement.Bundle

ona: the neuter plural pronoun (41).

Equations

• WechslerZlatic2000.ona = WechslerZlatic2000.indexBundle Person.third Number.plural Gender.neuter

def WechslerZlatic2000.kojih : Agreement.Bundle

kojih: the genitive plural relative pronoun, unmarked for concord number and gender (57).

Equations

• WechslerZlatic2000.kojih = WechslerZlatic2000.concordBundle Case.gen ⊥ ⊥

theorem WechslerZlatic2000.knjiga_agrees : ConcordAgrees (concordBundle Case.nom ↑Number.singular ↑Gender.feminine) knjiga Case.nom ∧ IndexAgrees (indexBundle Person.third Number.singular Gender.feminine) knjiga

On a regular noun the two bundles agree with the same targets (6).

theorem WechslerZlatic2000.deca_mixed_agreement : ConcordAgrees ovu deca Case.acc ∧ IndexAgrees ona deca ∧ ¬ConcordAgrees (concordBundle Case.acc ↑Number.plural ↑Gender.neuter) deca Case.acc ∧ ¬IndexAgrees (indexBundle Person.third Number.singular Gender.feminine) deca

Mixed agreement on deca (41): the feminine singular modifiers read CONCORD and the neuter plural pronoun reads INDEX, while the crossed targets fail (62).

theorem WechslerZlatic2000.kojih_agrees : ConcordAgrees kojih deca Case.gen

kojih agrees in concord with deca (56): unmarked features are compatible with anything.

theorem WechslerZlatic2000.compat_number_indexTarget_iff (n : Noun) (hn : ConInd n) (t : Agreement.Bundle) : Compat (t Agreement.Dimension.number) (n.indexTarget Agreement.Dimension.number) ↔ Compat (t Agreement.Dimension.number) (n.concordAt Case.nom Agreement.Dimension.number)

On a noun whose concord and index match, number agreement with the index is number agreement with the concord: the single-bundle illusion of regular nouns.

The Agreement Hierarchy (63)

def WechslerZlatic2000.readsIndex (predicate : Bool) : Agreement.Position → Prop

Whether a position reads INDEX, given how the open predicate position resolves: attributives lack indices, pronouns have them.

Equations

• WechslerZlatic2000.readsIndex predicate Agreement.Position.attributive = False
• WechslerZlatic2000.readsIndex predicate Agreement.Position.predicate = (predicate = true)
• WechslerZlatic2000.readsIndex predicate Agreement.Position.relativePronoun = True
• WechslerZlatic2000.readsIndex predicate Agreement.Position.personalPronoun = True

@[instance_reducible]

instance WechslerZlatic2000.instDecidablePredPositionReadsIndex (p : Bool) : DecidablePred (readsIndex p)

Equations

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

theorem WechslerZlatic2000.indexReaders_lowerSet (p : Bool) : IsLowerSet {t : Agreement.Position | readsIndex p t}

The index readers form a lower set of the hierarchy, whichever way the predicate position resolves: semantic agreement, which only the index connects to, surfaces on a more syntactic target only if it surfaces on the more semantic ones.