Ackema and Neeleman (2018): Features of Person: From the Inventory of Persons to Their Morphological Realization

Ackema and Neeleman derive the inventory of persons from two privative features that act as partial functions on a layered set, a set of atoms with a chain of predecessors. PROX discards the outermost layer and DIST selects it, and neither applies to a set with no predecessor. Their input is the person space: three nested sets, with the speaker an obligatory member of the innermost and an addressee of the next. Third person is [DIST], second [PROX–DIST], first [PROX–PROX] and the inclusive [PROX].

Number applies to the output of person, and plural requires more than one member. The inclusive has two obligatory members and so no singular, which leaves three singular pronouns and four plural ones. Only [DIST] can deliver the empty set, so expletives are third person singular. Spell-out rules mention features with multiplicity, and Maximal Encoding uses the applicable rule mentioning the most: Dutch has no rule mentioning two PROX, so wij realizes both the inclusive and the exclusive.

Main statements

• Layered.isSome_eval_iff, isSome_eval_layered_iff: a feature structure has an output iff it is no longer than its input is deep and only its last feature is DIST, which on the person space leaves the four persons and the structure with no feature.
• mem_inventory_iff: the seven pronouns are those with a denotation in some person space.
• canBeExpletive_iff, acceptable_iff_canBeExpletive: only the third person singular can denote the empty set, as the paper's expletive examples require.
• dutch_paradigm, dutch_referential: the Dutch rules realize the inventory, each pronoun at the referential categories its fragment entry records.

Implementation notes

• A layered set carries its predecessors, so the set a feature leaves unlayered has none. The paper defines the predecessor on the three sets of the person space.
• The features are defined over any type with a difference, so the same definitions compute the participants a structure delivers over finite sets of discourse roles (preimage_atom_eval).
• A pronoun without PL denotes a set with at most one member, the chapter's provisional singular. Its impersonal pronoun, the structure with no feature, is left to later chapters.
• Gender is not analysed, so the third person singular rule inserts hij where the paper lists hij, zij and het.

TODO

• The honorific feature and the polite pronouns recruited by impoverishment.
• The context operators that fix the speaker and the addressee, and their shifting.

References

• P. Ackema and A. Neeleman, Features of Person: From the Inventory of Persons to Their Morphological Realization (2018)
• M. Cysouw, The Paradigmatic Structure of Person Marking (2003)
• D. Harbour, Impossible Persons (2016)

Layered sets and the person features

structure AckemaNeeleman2018.Layered (β : Type u_5) : Type u_5

A layered set is a set with the chain of its predecessors, the nearest first. A set with no predecessor is unlayered.

• set : β

  The set itself.

• preds : List β

  Pred S, Pred (Pred S) and so on.

def AckemaNeeleman2018.Layered.pred {β : Type u_2} : Layered β → Option (Layered β)

Pred S, with the predecessors that remain.

Equations

• { set := set, preds := [] }.pred = none
• { set := set, preds := p :: ps }.pred = some { set := p, preds := ps }

def AckemaNeeleman2018.Layered.map {β : Type u_2} {γ : Type u_3} (g : β → γ) (S : Layered β) : Layered γ

The image of a layered set under a map of sets.

Equations

• AckemaNeeleman2018.Layered.map g S = { set := g S.set, preds := List.map g S.preds }

inductive AckemaNeeleman2018.Feature : Type

The two privative person features.

• prox : Feature
• dist : Feature

@[instance_reducible]

instance AckemaNeeleman2018.instDecidableEqFeature : DecidableEq Feature

Equations

• AckemaNeeleman2018.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AckemaNeeleman2018.Feature.apply {β : Type u_2} [SDiff β] : Feature → Layered β → Option (Layered β)

PROX S = Pred S discards the outermost layer of a layered set and DIST S = S − Pred S selects it, leaving an unlayered set. Neither applies to an unlayered set.

Equations

• AckemaNeeleman2018.Feature.prox.apply x✝ = x✝.pred
• AckemaNeeleman2018.Feature.dist.apply x✝ = Option.map (fun (P : AckemaNeeleman2018.Layered β) => { set := x✝.set \ P.set, preds := [] }) x✝.pred

theorem AckemaNeeleman2018.Feature.length_preds_lt {β : Type u_2} [SDiff β] {S T : Layered β} {f : Feature} (h : f.apply S = some T) : T.preds.length < S.preds.length

theorem AckemaNeeleman2018.Feature.apply_map {β : Type u_2} {γ : Type u_3} [SDiff β] [SDiff γ] {g : β → γ} (hg : ∀ (s t : β), g (s \ t) = g s \ g t) (f : Feature) (S : Layered β) : f.apply (Layered.map g S) = Option.map (Layered.map g) (f.apply S)

def AckemaNeeleman2018.Layered.eval {β : Type u_2} [SDiff β] (S : Layered β) (fs : List Feature) : Option (Layered β)

The output of a person feature structure on a layered set, its features applied in order.

Equations

• S.eval fs = List.foldlM (fun (S : AckemaNeeleman2018.Layered β) (f : AckemaNeeleman2018.Feature) => f.apply S) S fs

@[simp]

theorem AckemaNeeleman2018.Layered.eval_nil {β : Type u_2} [SDiff β] (S : Layered β) : S.eval [] = some S

@[simp]

theorem AckemaNeeleman2018.Layered.eval_cons {β : Type u_2} [SDiff β] (S : Layered β) (f : Feature) (fs : List Feature) : S.eval (f :: fs) = (f.apply S).bind fun (x : Layered β) => x.eval fs

theorem AckemaNeeleman2018.Layered.isSome_eval_iff {β : Type u_2} [SDiff β] {S : Layered β} {fs : List Feature} : (S.eval fs).isSome = true ↔ fs.length ≤ S.preds.length ∧ ∀ f ∈ fs.dropLast, f = Feature.prox

A feature structure has an output on a layered set iff it has at most as many features as the set has predecessors and only its last feature is DIST.

theorem AckemaNeeleman2018.Layered.length_preds_add_length_le {β : Type u_2} [SDiff β] {S T : Layered β} {fs : List Feature} (h : S.eval fs = some T) : T.preds.length + fs.length ≤ S.preds.length

Every feature of a structure removes a layer.

theorem AckemaNeeleman2018.Layered.eval_eq_some_self_iff {β : Type u_2} [SDiff β] {S : Layered β} {fs : List Feature} : S.eval fs = some S ↔ fs = []

theorem AckemaNeeleman2018.Layered.eval_map {β : Type u_2} {γ : Type u_3} [SDiff β] [SDiff γ] {g : β → γ} (hg : ∀ (s t : β), g (s \ t) = g s \ g t) (S : Layered β) (fs : List Feature) : (map g S).eval fs = Option.map (map g) (S.eval fs)

The features commute with a map of sets that preserves differences.

The person space

structure AckemaNeeleman2018.PersonSpace (α : Type u_5) : Type u_5

The person space is a nest of three sets of atoms. The speaker is an obligatory member of the innermost, Sᵢ, and an addressee of the next, Sᵢ₊ᵤ; their other members are associates of the two, and the remaining members of the whole space Sᵢ₊ᵤ₊ₒ are the others.

• speaker : α

  The speaker i.

• addressee : α

  The addressee u.

• Si : Set α

  Sᵢ.

• Siu : Set α

  Sᵢ₊ᵤ.

• Siuo : Set α

  Sᵢ₊ᵤ₊ₒ.

• speaker_mem : self.speaker ∈ self.Si
• addressee_mem : self.addressee ∈ self.Siu
• addressee_notMem : self.addressee ∉ self.Si
• Si_subset : self.Si ⊆ self.Siu
• Siu_subset : self.Siu ⊆ self.Siuo

def AckemaNeeleman2018.PersonSpace.layered {α : Type u_1} (S : PersonSpace α) : Layered (Set α)

The input to the person features is the whole space, with predecessor Sᵢ₊ᵤ, whose predecessor is Sᵢ.

Equations

• S.layered = { set := S.Siuo, preds := [S.Siu, S.Si] }

def AckemaNeeleman2018.PersonSpace.atom {α : Type u_1} (S : PersonSpace α) : Discourse.Role → α

The atom bearing a discourse role.

Equations

• S.atom Discourse.Role.speaker = S.speaker
• S.atom Discourse.Role.addressee = S.addressee

theorem AckemaNeeleman2018.PersonSpace.speaker_ne_addressee {α : Type u_1} (S : PersonSpace α) : S.speaker ≠ S.addressee

theorem AckemaNeeleman2018.PersonSpace.nontrivial_Siu {α : Type u_1} (S : PersonSpace α) : S.Siu.Nontrivial

Sᵢ₊ᵤ has two obligatory members, the speaker and an addressee.

theorem AckemaNeeleman2018.PersonSpace.nontrivial_Siuo {α : Type u_1} (S : PersonSpace α) : S.Siuo.Nontrivial

The inventory of persons

def AckemaNeeleman2018.third : List Feature

Third person [DIST].

Equations

• AckemaNeeleman2018.third = [AckemaNeeleman2018.Feature.dist]

def AckemaNeeleman2018.second : List Feature

Second person [PROX–DIST].

Equations

• AckemaNeeleman2018.second = [AckemaNeeleman2018.Feature.prox, AckemaNeeleman2018.Feature.dist]

def AckemaNeeleman2018.first : List Feature

First person [PROX–PROX].

Equations

• AckemaNeeleman2018.first = [AckemaNeeleman2018.Feature.prox, AckemaNeeleman2018.Feature.prox]

def AckemaNeeleman2018.inclusive : List Feature

First person inclusive [PROX].

Equations

• AckemaNeeleman2018.inclusive = [AckemaNeeleman2018.Feature.prox]

theorem AckemaNeeleman2018.eval_third {α : Type u_1} (S : PersonSpace α) : S.layered.eval third = some { set := S.Siuo \ S.Siu, preds := [] }

theorem AckemaNeeleman2018.eval_second {α : Type u_1} (S : PersonSpace α) : S.layered.eval second = some { set := S.Siu \ S.Si, preds := [] }

theorem AckemaNeeleman2018.eval_first {α : Type u_1} (S : PersonSpace α) : S.layered.eval first = some { set := S.Si, preds := [] }

theorem AckemaNeeleman2018.eval_inclusive {α : Type u_1} (S : PersonSpace α) : S.layered.eval inclusive = some { set := S.Siu, preds := [S.Si] }

theorem AckemaNeeleman2018.isSome_eval_layered_iff {α : Type u_1} (S : PersonSpace α) {fs : List Feature} : (S.layered.eval fs).isSome = true ↔ fs ∈ [[], inclusive, first, second, third]

The person features have an output for exactly five structures, the four persons and the structure with no feature.

theorem AckemaNeeleman2018.eq_nil_or_of_eval {α : Type u_1} {S : PersonSpace α} {fs : List Feature} {L : Layered (Set α)} (h : S.layered.eval fs = some L) : fs = [] ∨ fs = inclusive ∨ fs = first ∨ fs = second ∨ fs = third

theorem AckemaNeeleman2018.nonempty_of_eval {α : Type u_1} {S : PersonSpace α} {fs : List Feature} {L : Layered (Set α)} (h : S.layered.eval fs = some L) (hfs : fs ≠ third) : L.set.Nonempty

Every structure but [DIST] delivers a nonempty set, the two inner sets having an obligatory member each.

Participants

The speaker and the addressee are placed alike in every person space, so the participants in the set a feature structure delivers do not depend on the space.

def AckemaNeeleman2018.participants (fs : List Feature) : Option (Finset Discourse.Role)

The discourse participants in the set a feature structure delivers, computed in the space of the speaker and the addressee alone.

Equations

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

theorem AckemaNeeleman2018.preimage_atom_eval {α : Type u_1} (S : PersonSpace α) (fs : List Feature) : Option.map (fun (x : Layered (Set α)) => S.atom ⁻¹' x.set) (S.layered.eval fs) = Option.map SetLike.coe (participants fs)

In every person space the participants in the set a feature structure delivers are its participants.

theorem AckemaNeeleman2018.ofParticipants_participants : Option.map Person.ofParticipants (participants first) = some Person.firstExclusive ∧ Option.map Person.ofParticipants (participants inclusive) = some Person.firstInclusive ∧ Option.map Person.ofParticipants (participants second) = some Person.second ∧ Option.map Person.ofParticipants (participants third) = some Person.third

The four person structures deliver the participants of the four persons of the quadripartition.

Number

Number is interpreted on the output of the person features. Without PL the output has at most one member, and PL requires more than one.

def AckemaNeeleman2018.PersonSpace.PluralDefined {α : Type u_1} (S : PersonSpace α) (L : Layered (Set α)) : Prop

PL is defined on a set with more than one member that the person features deliver, and not on their input.

Equations

• S.PluralDefined L = (L.set.Nontrivial ∧ L ≠ S.layered)

theorem AckemaNeeleman2018.PersonSpace.pluralDefined_iff {α : Type u_1} {S : PersonSpace α} {fs : List Feature} {L : Layered (Set α)} (h : S.layered.eval fs = some L) : S.PluralDefined L ↔ L.set.Nontrivial ∧ fs ≠ []

PL is defined on the output of a feature structure with more than one member, unless the structure has no feature.

structure AckemaNeeleman2018.Pronoun : Type

A pronoun is a person feature structure under a number node, with PL or without.

• person : List Feature

  The person feature structure.

• plural : Bool

  Whether the number node bears PL.

def AckemaNeeleman2018.instDecidableEqPronoun.decEq (x✝ x✝¹ : Pronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance AckemaNeeleman2018.instDecidableEqPronoun : DecidableEq Pronoun

Equations

• AckemaNeeleman2018.instDecidableEqPronoun = AckemaNeeleman2018.instDecidableEqPronoun.decEq

def AckemaNeeleman2018.Pronoun.Denotes {α : Type u_1} (p : Pronoun) (S : PersonSpace α) (L : Layered (Set α)) : Prop

A pronoun denotes a set in a person space that its person features deliver and its number accepts.

Equations

• p.Denotes S L = (S.layered.eval p.person = some L ∧ if p.plural = true then S.PluralDefined L else L.set.Subsingleton)

def AckemaNeeleman2018.inventory : List Pronoun

The seven pronouns, three singular and four plural.

Equations

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

theorem AckemaNeeleman2018.mem_inventory_iff {p : Pronoun} : p ∈ inventory ↔ ∃ (S : PersonSpace ℕ) (L : Layered (Set ℕ)), p.Denotes S L

The inventory consists of the pronouns with a denotation in some person space. The inclusive has no singular, its set having two obligatory members, and the structure with no feature neither a singular nor a plural, PL not being defined on its set.

def AckemaNeeleman2018.Pronoun.categories (p : Pronoun) : Finset Person.Category

The referential categories a pronoun covers are those with the participants its person features deliver that are groups exactly when it is plural.

Equations

• p.categories = {c : Person.Category | AckemaNeeleman2018.participants p.person = some c.participants ∧ (c.IsGroup ↔ p.plural = true)}

theorem AckemaNeeleman2018.map_categories_inventory : List.map Pronoun.categories inventory = [{Person.Category.speaker}, {Person.Category.addressee}, {Person.Category.other}, {Person.Category.speakerAddressee, Person.Category.speakerAddresseeOthers}, {Person.Category.speakerOthers}, {Person.Category.addresseeOthers}, {Person.Category.others}]

The seven pronouns cover the eight referential categories between them, the inclusive covering the speaker and addressee both alone and with others.

Expletives

def AckemaNeeleman2018.Pronoun.CanBeExpletive (p : Pronoun) : Prop

A pronoun can be an expletive when it denotes the empty set in some person space.

Equations

• p.CanBeExpletive = ∃ (S : AckemaNeeleman2018.PersonSpace ℕ) (L : AckemaNeeleman2018.Layered (Set ℕ)), p.Denotes S L ∧ L.set = ∅

theorem AckemaNeeleman2018.canBeExpletive_iff {p : Pronoun} : p.CanBeExpletive ↔ p = { person := third, plural := false }

Only the third person singular can be an expletive, since DIST alone can deliver the empty set and PL is not defined on it.

@[instance_reducible]

instance AckemaNeeleman2018.instDecidablePredPronounCanBeExpletive : DecidablePred Pronoun.CanBeExpletive

Equations

• AckemaNeeleman2018.instDecidablePredPronounCanBeExpletive x✝ = decidable_of_iff (x✝ = { person := AckemaNeeleman2018.third, plural := false }) ⋯

def AckemaNeeleman2018.subject? (e : Datum) : Option Pronoun

The subject pronoun of an example, by its person label.

Equations

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

theorem AckemaNeeleman2018.acceptable_iff_canBeExpletive (e : Datum) : e ∈ Examples.all → e.feature? "phenomenon" = some "expletive" → ∃ p ∈ subject? e, e.judgment = Judgment.acceptable ↔ p.CanBeExpletive

The paper reports an expletive subject acceptable exactly when its pronoun can be an expletive.

Spell-out and Maximal Encoding

structure AckemaNeeleman2018.SpellOut (E : Type u_5) : Type u_5

A spell-out rule inserts a form for the person features it mentions, counted with multiplicity, with PL or without.

• features : Multiset Feature

  The person features mentioned.

• plural : Bool

  Whether PL is mentioned.

• exponent : E

  The form inserted.

@[instance_reducible]

instance AckemaNeeleman2018.instRuleSpellOutPronoun {E : Type u_4} : Morphology.Exponence.Rule (SpellOut E) Pronoun E

A rule applies to a pronoun that has every feature it mentions.

Equations

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

@[instance_reducible]

instance AckemaNeeleman2018.instDecidableRelSpellOutPronounApplies {E : Type u_4} : DecidableRel Morphology.Exponence.Applies

Equations

• AckemaNeeleman2018.instDecidableRelSpellOutPronounApplies x✝¹ x✝ = { decide := decide (x✝¹.features ≤ ↑x✝.person) && decide (x✝¹.plural ≤ x✝.plural), reflects_decide := ⋯ }

def AckemaNeeleman2018.SpellOut.size {E : Type u_4} (r : SpellOut E) : ℕ

The number of features a rule mentions.

Equations

• r.size = r.features.card + r.plural.toNat

theorem AckemaNeeleman2018.shared_features : ↑first ∩ ↑second = {Feature.prox} ∧ ↑second ∩ ↑third = {Feature.dist} ∧ ↑first ∩ ↑third = 0

The second person shares PROX with the first and DIST with the third, which share nothing.

theorem AckemaNeeleman2018.applies_of_inter_le {E : Type u_4} {r : SpellOut E} {n : Bool} {fs gs hs : List Feature} (hf : Morphology.Exponence.Applies r { person := fs, plural := n }) (hg : Morphology.Exponence.Applies r { person := gs, plural := n }) (h : ↑fs ∩ ↑gs ≤ ↑hs) : Morphology.Exponence.Applies r { person := hs, plural := n }

A rule applying to two pronouns of one number applies to any pronoun of that number with the features they share.

theorem AckemaNeeleman2018.applies_second_of_first_of_third {E : Type u_4} {r : SpellOut E} {n : Bool} (h₁ : Morphology.Exponence.Applies r { person := first, plural := n }) (h₃ : Morphology.Exponence.Applies r { person := third, plural := n }) : Morphology.Exponence.Applies r { person := second, plural := n }

No rule singles out the first and the third person against the second.

theorem AckemaNeeleman2018.applies_first_of_inclusive_of_second {E : Type u_4} {r : SpellOut E} {n : Bool} (h₁ : Morphology.Exponence.Applies r { person := inclusive, plural := n }) (h₂ : Morphology.Exponence.Applies r { person := second, plural := n }) : Morphology.Exponence.Applies r { person := first, plural := n }

No rule singles out the inclusive and the second person against the exclusive.

theorem AckemaNeeleman2018.applies_exclusive_iff_first {E : Type u_4} {r : SpellOut E} (h : r.plural = false) : Morphology.Exponence.Applies r { person := first, plural := true } ↔ Morphology.Exponence.Applies r { person := first, plural := false }

A rule not mentioning PL applies to the exclusive exactly when it applies to the first singular, the two sharing their person structure.

def AckemaNeeleman2018.dutch : Morphology.Exponence.RuleSet (SpellOut PersonalPronoun)

The spell-out rules of the Dutch strong subject pronouns, none of which mentions two PROX.

Equations

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

theorem AckemaNeeleman2018.dutch_paradigm : List.map (dutch.realize SpellOut.size) inventory = [some Dutch.Pronouns.ik, some Dutch.Pronouns.jij, some Dutch.Pronouns.hij, some Dutch.Pronouns.wij, some Dutch.Pronouns.wij, some Dutch.Pronouns.jullie, some Dutch.Pronouns.zij_pl]

Under Maximal Encoding the rule mentioning the most features is used, so the Dutch rules realize the inventory with one form for the inclusive and the exclusive.

theorem AckemaNeeleman2018.dutch_referential (r : SpellOut PersonalPronoun) : r ∈ dutch → ∀ (c : Person.Category), c ∈ r.exponent.referential ↔ ∃ p ∈ inventory, dutch.realize SpellOut.size p = some r.exponent ∧ c ∈ p.categories

Each Dutch pronoun denotes the referential categories that the pronouns it realizes cover.

def AckemaNeeleman2018.clusive {E : Type u_4} (a b : E) : Morphology.Exponence.RuleSet (SpellOut E)

A rule set with a rule mentioning two PROX and a rule mentioning one, both with PL.

Equations

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

theorem AckemaNeeleman2018.clusive_split {E : Type u_4} (a b : E) : (clusive a b).realize SpellOut.size { person := first, plural := true } = some a ∧ (clusive a b).realize SpellOut.size { person := inclusive, plural := true } = some b

A rule mentioning two PROX gives the exclusive a form of its own. It blocks the rule mentioning one on the exclusive and cannot apply to the inclusive.