The person space and function-valued person features

This file defines the person space of Ackema and Neeleman: a nested chain of sets of atoms Sᵢ ⊆ Sᵢ₊ᵤ ⊆ Sᵢ₊ᵤ₊ₒ in which the speaker is an obligatory member of the innermost set and an addressee of the middle one, together with two privative person features interpreted as partial functions on it — PROX discards the outermost layer of a layered set and DIST selects it — and the feature structures built by applying them in sequence to the whole space. Third person selects the others layer, second person the addressee layer, first person the innermost set, and the inclusive the middle set; neither feature applies to a layer or to the innermost set, which bounds the inventory. Plural is defined only on an output of the person system with more than one member.

Main definitions

• Minimalist.Phi.PersonSpace: the nested person space over a type of atoms.
• PersonSpace.Region, PersonSpace.denote: the sets a feature structure can select and their denotations.
• PersonSpace.Feature, Feature.apply, PersonSpace.Spec, Spec.eval: the features as partial functions on regions, and feature structures evaluated on the whole space.
• PersonSpace.PluralDefined: the definedness condition of plural.

Main statements

• PersonSpace.Spec.eval_mem: every feature structure evaluates to one of the five regions or is incoherent.
• PersonSpace.denote_nonempty, PersonSpace.exists_denote_others_eq_empty: only the others layer can be empty.
• PersonSpace.nontrivial_denote_siu, PersonSpace.nontrivial_denote_siuo: the middle set and the whole space have two obligatory members.

References

• [ackema-neeleman-2018]

structure Minimalist.Phi.PersonSpace (α : Type u_1) : Type u_1

The person space: nested sets of atoms with the speaker an obligatory member of Sᵢ and an addressee of Sᵢ₊ᵤ; the remaining members are associates and others.

• speaker : α

  The speaker i.

• addressee : α

  The addressee u.

• Si : Set α

  Sᵢ: the speaker and any associates or co-speakers.

• Siu : Set α

  Sᵢ₊ᵤ: additionally an addressee and any associates or co-addressees.

• Siuo : Set α

  Sᵢ₊ᵤ₊ₒ: additionally the others.

• 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

inductive Minimalist.Phi.PersonSpace.Region : Type

The regions a feature structure can select: the three nested sets and the two layers between them.

• si : Region
• siu : Region
• siuo : Region
• addressees : Region
• others : Region

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instDecidableEqRegion : DecidableEq Region

Equations

• Minimalist.Phi.PersonSpace.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.Phi.PersonSpace.instReprRegion.repr : Region → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instReprRegion : Repr Region

Equations

• Minimalist.Phi.PersonSpace.instReprRegion = { reprPrec := Minimalist.Phi.PersonSpace.instReprRegion.repr }

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instFintypeRegion : Fintype Region

Equations

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

def Minimalist.Phi.PersonSpace.Region.pred : Region → Option Region

The predecessor of a layered set: Pred Sᵢ₊ᵤ = Sᵢ, Pred Sᵢ₊ᵤ₊ₒ = Sᵢ₊ᵤ.

Equations

• Minimalist.Phi.PersonSpace.Region.siuo.pred = some Minimalist.Phi.PersonSpace.Region.siu
• Minimalist.Phi.PersonSpace.Region.siu.pred = some Minimalist.Phi.PersonSpace.Region.si
• x✝.pred = none

inductive Minimalist.Phi.PersonSpace.Feature : Type

The two privative person features.

• prox : Feature
• dist : Feature

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instReprFeature : Repr Feature

Equations

• Minimalist.Phi.PersonSpace.instReprFeature = { reprPrec := Minimalist.Phi.PersonSpace.instReprFeature.repr }

def Minimalist.Phi.PersonSpace.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Phi.PersonSpace.instFintypeFeature : Fintype Feature

Equations

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

def Minimalist.Phi.PersonSpace.Feature.apply : Feature → Region → Option Region

PROX S = Pred S discards, and DIST S = S − Pred S selects, the outermost layer of a layered set; neither applies to an unlayered one.

Equations

• Minimalist.Phi.PersonSpace.Feature.prox.apply x✝ = x✝.pred
• Minimalist.Phi.PersonSpace.Feature.dist.apply Minimalist.Phi.PersonSpace.Region.siuo = some Minimalist.Phi.PersonSpace.Region.others
• Minimalist.Phi.PersonSpace.Feature.dist.apply Minimalist.Phi.PersonSpace.Region.siu = some Minimalist.Phi.PersonSpace.Region.addressees
• Minimalist.Phi.PersonSpace.Feature.dist.apply x✝ = none

@[reducible, inline]

abbrev Minimalist.Phi.PersonSpace.Spec : Type

A person feature structure: the features in order of application.

Equations

• Minimalist.Phi.PersonSpace.Spec = List Minimalist.Phi.PersonSpace.Feature

def Minimalist.Phi.PersonSpace.Spec.eval (fs : Spec) : Option Region

Apply the features in order to Sᵢ₊ᵤ₊ₒ; none when a feature meets an unlayered set.

Equations

• fs.eval = List.foldl (fun (acc : Option Minimalist.Phi.PersonSpace.Region) (f : Minimalist.Phi.PersonSpace.Feature) => acc.bind f.apply) (some Minimalist.Phi.PersonSpace.Region.siuo) fs

theorem Minimalist.Phi.PersonSpace.Spec.eval_mem (fs : Spec) : fs.eval = none ∨ fs.eval = some Region.siuo ∨ fs.eval = some Region.si ∨ fs.eval = some Region.siu ∨ fs.eval = some Region.addressees ∨ fs.eval = some Region.others

Every feature structure is incoherent or selects one of the five regions.

def Minimalist.Phi.PersonSpace.denote {α : Type u_1} (S : PersonSpace α) : Region → Set α

The set of atoms a region denotes.

Equations

• S.denote Minimalist.Phi.PersonSpace.Region.si = S.Si
• S.denote Minimalist.Phi.PersonSpace.Region.siu = S.Siu
• S.denote Minimalist.Phi.PersonSpace.Region.siuo = S.Siuo
• S.denote Minimalist.Phi.PersonSpace.Region.addressees = S.Siu \ S.Si
• S.denote Minimalist.Phi.PersonSpace.Region.others = S.Siuo \ S.Siu

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

theorem Minimalist.Phi.PersonSpace.speaker_mem_denote_si {α : Type u_1} (S : PersonSpace α) : S.speaker ∈ S.denote Region.si

theorem Minimalist.Phi.PersonSpace.speaker_mem_denote_siu {α : Type u_1} (S : PersonSpace α) : S.speaker ∈ S.denote Region.siu

theorem Minimalist.Phi.PersonSpace.speaker_mem_denote_siuo {α : Type u_1} (S : PersonSpace α) : S.speaker ∈ S.denote Region.siuo

theorem Minimalist.Phi.PersonSpace.addressee_mem_denote_addressees {α : Type u_1} (S : PersonSpace α) : S.addressee ∈ S.denote Region.addressees

theorem Minimalist.Phi.PersonSpace.speaker_notMem_denote_addressees {α : Type u_1} (S : PersonSpace α) : S.speaker ∉ S.denote Region.addressees

theorem Minimalist.Phi.PersonSpace.speaker_notMem_denote_others {α : Type u_1} (S : PersonSpace α) : S.speaker ∉ S.denote Region.others

theorem Minimalist.Phi.PersonSpace.addressee_notMem_denote_others {α : Type u_1} (S : PersonSpace α) : S.addressee ∉ S.denote Region.others

theorem Minimalist.Phi.PersonSpace.denote_nonempty {α : Type u_1} (S : PersonSpace α) {r : Region} (h : r ≠ Region.others) : (S.denote r).Nonempty

Every region but the others layer contains the speaker or the addressee.

theorem Minimalist.Phi.PersonSpace.exists_denote_others_eq_empty {α : Type u_1} {a b : α} (hab : a ≠ b) : ∃ (S : PersonSpace α), S.denote Region.others = ∅

The others layer can be empty.

theorem Minimalist.Phi.PersonSpace.nontrivial_denote_siu {α : Type u_1} (S : PersonSpace α) : (S.denote Region.siu).Nontrivial

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

theorem Minimalist.Phi.PersonSpace.nontrivial_denote_siuo {α : Type u_1} (S : PersonSpace α) : (S.denote Region.siuo).Nontrivial

The whole space has two obligatory members.

def Minimalist.Phi.PersonSpace.PluralDefined {α : Type u_1} (S : PersonSpace α) (r : Region) : Prop

Plural is defined on an output of the person system with more than one member, and not on the whole space.

Equations

• S.PluralDefined r = (r ≠ Minimalist.Phi.PersonSpace.Region.siuo ∧ (S.denote r).Nontrivial)

theorem Minimalist.Phi.PersonSpace.not_pluralDefined_siuo {α : Type u_1} (S : PersonSpace α) : ¬S.PluralDefined Region.siuo

theorem Minimalist.Phi.PersonSpace.not_pluralDefined_of_eq_empty {α : Type u_1} (S : PersonSpace α) {r : Region} (h : S.denote r = ∅) : ¬S.PluralDefined r