Two types of resumptive pronouns in Swahili

[Sco21]: the resumptive pronouns that objects of monosyllabic prepositions require are of two kinds. Bound pronouns, the only option in adjunct islands ((31)–(33)), match the head in person; movement copies, diagnosed by parasitic gaps ((35)–(37)), never carry person. Both follow from one Vocabulary ((28)) and the copy theory of movement: a movement copy in a position with a phonological requirement is reduced rather than deleted ([Lan06]), and MaxElide removes the largest constituent whose residue can still be spelled out — PersP, since -ye spells out [sg + n_anim] while nothing spells out Num alone ((46)–(48)).

Main definitions

• pronoun: the pronoun structures of (40)–(44), with PersP only for local persons.
• resumptiveVocab, spellout: the Vocabulary Items of (28) over a pronoun's features.
• Deletable, maxElideTarget: a layer is deletable when its residue has an exponent; MaxElide takes the largest such layer.
• pronounce: the chain reduction of a copy — full deletion, or PersP deletion where Minimality forbids deleting the copy — against a bound pronoun's full spell-out.

Main results

• table2: the paradigm of the Fragment's resumptivePronoun is (28) over the structures (42) and (44).
• maxElide_persP: PersP is the unique deletable layer, by the Vocabulary.
• cleft_rows, island_rows, parasitic_rows: the data pool — clefts allow either pronoun but fix number, islands allow only the bound pronoun, and a personless parasitic pronoun needs a personless true gap for every speaker of Table 4.
• person_entails_number: any deletion that keeps person keeps number, since Num is above Pers (§6).

Implementation notes

The structures are Syntax.Trees over the four DP-internal categories, so MaxElide is structural deletion rather than feature removal; features are read off the terminals for Vocabulary Insertion. The interspeaker variation of Table 4 beyond its first two rows is not derived, as the paper does not derive it.

The structure of pronouns (§5.1)

inductive Scott2021.DPCat : Type

The DP-internal projections of (40)–(41): D, Num, the animate n, and the Person projection that only local-person pronouns have.

• D : DPCat
• Num : DPCat
• n : DPCat
• Pers : DPCat

@[instance_reducible]

instance Scott2021.instDecidableEqDPCat : DecidableEq DPCat

Equations

• Scott2021.instDecidableEqDPCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Scott2021.instReprDPCat : Repr DPCat

Equations

• Scott2021.instReprDPCat = { reprPrec := Scott2021.instReprDPCat.repr }

def Scott2021.instReprDPCat.repr : DPCat → ℕ → Std.Format

Equations

• Scott2021.instReprDPCat.repr Scott2021.DPCat.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2021.DPCat.D")).group prec✝
• Scott2021.instReprDPCat.repr Scott2021.DPCat.Num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2021.DPCat.Num")).group prec✝
• Scott2021.instReprDPCat.repr Scott2021.DPCat.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2021.DPCat.n")).group prec✝
• Scott2021.instReprDPCat.repr Scott2021.DPCat.Pers prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2021.DPCat.Pers")).group prec✝

@[instance_reducible]

instance Scott2021.instFintypeDPCat : Fintype DPCat

Equations

• Scott2021.instFintypeDPCat = { elems := { val := ↑Scott2021.DPCat.enumList, nodup := Scott2021.DPCat.enumList_nodup }, complete := Scott2021.instFintypeDPCat._proof_1 }

def Scott2021.pronoun (person : Option Person) (number : Number) : Syntax.Tree DPCat String

A pronoun ((41)): [DP D [NumP Num [nP n_anim [PersP Pers]]]], without PersP for the personless pronouns of (42).

Equations

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

def Scott2021.terminalFeature : DPCat → String → Option Minimalist.FeatureVal

The feature a terminal contributes: person, number, or the animate gender (encoded as gender 1).

Equations

• Scott2021.terminalFeature Scott2021.DPCat.Pers "1" = some (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Person.first))
• Scott2021.terminalFeature Scott2021.DPCat.Pers "2" = some (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Person.second))
• Scott2021.terminalFeature Scott2021.DPCat.Num "sg" = some (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number Number.singular))
• Scott2021.terminalFeature Scott2021.DPCat.Num "pl" = some (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number Number.plural))
• Scott2021.terminalFeature Scott2021.DPCat.n "anim" = some (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.gender 1))
• Scott2021.terminalFeature x✝¹ x✝ = none

def Scott2021.featureList : Syntax.Tree DPCat String → List Minimalist.GramFeature

The features at a tree's terminals, in depth-first order.

Equations

• Scott2021.featureList (Syntax.Tree.terminal c w) = match Scott2021.terminalFeature c w with | some fv => [Minimalist.GramFeature.valued fv] | none => []
• Scott2021.featureList (Syntax.Tree.node a children) = Scott2021.featureListAll✝ children
• Scott2021.featureList (Syntax.Tree.trace a a_1) = []
• Scott2021.featureList (Syntax.Tree.bind a a_1 body) = Scott2021.featureList body

Vocabulary Insertion (§3.4)

def Scott2021.resumptiveVocab : List (DistributedMorphology.VocabularyItem Minimalist.GramFeature String)

The Vocabulary Items of (28): person-specified animate entries and the personless animate defaults -ye and -o.

Equations

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

def Scott2021.spellout (t : Syntax.Tree DPCat String) : Option String

The exponent of a pronoun structure, by the Subset Principle over (28).

Equations

• Scott2021.spellout t = DistributedMorphology.subsetPrinciple Scott2021.resumptiveVocab (DistributedMorphology.Neighborhood.ofBundle (Scott2021.featureList t))

def Scott2021.relPerson : Swahili.RelPerson → Option Person

The Fragment's person cells as the structures' person: third person is the absence of PersP.

Equations

• Scott2021.relPerson Swahili.RelPerson.first = some Person.first
• Scott2021.relPerson Swahili.RelPerson.second = some Person.second
• Scott2021.relPerson Swahili.RelPerson.third = none

theorem Scott2021.table2 (p : Swahili.RelPerson) (n : Swahili.RelGramNum) : Option.map (fun (x : String) => "-" ++ x) (spellout (pronoun (relPerson p) n.toNumber)) = some (Swahili.resumptivePronoun p n)

Table 2 from (28): every cell of the Fragment's resumptive paradigm is the Subset Principle's choice for the corresponding structure ((43), (45)).

MaxElide (§5.2–5.3)

def Scott2021.deleteLayer (c : DPCat) : Syntax.Tree DPCat String → Syntax.Tree DPCat String

Delete the constituent of category c — the subtree it heads — from a tree.

Equations

• Scott2021.deleteLayer c (Syntax.Tree.node k children) = Syntax.Tree.node k (Scott2021.deleteLayerAll✝ c children)
• Scott2021.deleteLayer c x✝ = x✝

def Scott2021.Deletable (t : Syntax.Tree DPCat String) (c : DPCat) : Prop

A layer of a pronoun is deletable when what remains can still be spelled out — MaxElide's condition ((48)): deleting PersP leaves [sg + n_anim], which -ye spells out, while deleting nP leaves Num alone, which nothing spells out.

Equations

• Scott2021.Deletable t c = (c ≠ Scott2021.DPCat.D ∧ (Scott2021.spellout (Scott2021.deleteLayer c t)).isSome = true)

@[instance_reducible]

instance Scott2021.instDecidableDeletable (t : Syntax.Tree DPCat String) (c : DPCat) : Decidable (Deletable t c)

Equations

• Scott2021.instDecidableDeletable t c = Scott2021.instDecidableDeletable._aux_1 t c

def Scott2021.layers : List DPCat

The layers of a pronoun, outermost first.

Equations

• Scott2021.layers = [Scott2021.DPCat.D, Scott2021.DPCat.Num, Scott2021.DPCat.n, Scott2021.DPCat.Pers]

def Scott2021.maxElideTarget (t : Syntax.Tree DPCat String) : Option DPCat

MaxElide: the largest deletable constituent.

Equations

• Scott2021.maxElideTarget t = List.find? (fun (c : Scott2021.DPCat) => decide (Scott2021.Deletable t c)) Scott2021.layers

theorem Scott2021.maxElide_persP (p : Person) (n : Number) : p = Person.first ∨ p = Person.second → maxElideTarget (pronoun (some p) n) = some DPCat.Pers

In a local-person pronoun PersP is the unique deletable layer, so MaxElide deletes it ((46)–(47)).

theorem Scott2021.person_entails_number (c : DPCat) (n : Number) : ((featureList (deleteLayer c (pronoun (some Person.first) n))).any fun (f : Minimalist.GramFeature) => match f with | Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person a)) => true | x => false) = true → ((featureList (deleteLayer c (pronoun (some Person.first) n))).any fun (f : Minimalist.GramFeature) => match f with | Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number a)) => true | x => false) = true

Deleting a layer can keep person only if it keeps number: Num is above Pers (§6).

Chain reduction (§5.2–5.3)

inductive Scott2021.Origin : Type

How a resumptive relates to the head: a base-generated bound pronoun, or a lower copy of Ā-movement.

• bound : Origin
• movementCopy : Origin

@[instance_reducible]

instance Scott2021.instDecidableEqOrigin : DecidableEq Origin

Equations

• Scott2021.instDecidableEqOrigin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Scott2021.instReprOrigin.repr : Origin → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Scott2021.instReprOrigin.repr Scott2021.Origin.bound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2021.Origin.bound")).group prec✝

@[instance_reducible]

instance Scott2021.instReprOrigin : Repr Origin

Equations

• Scott2021.instReprOrigin = { reprPrec := Scott2021.instReprOrigin.repr }

def Scott2021.pronounce (t : Syntax.Tree DPCat String) : Origin → (minimality : Bool) → Option String

The pronounced form. A bound pronoun is spelled out in full. A movement copy is deleted by Economy of Pronunciation unless its position carries the bimoraic Minimality requirement of a monosyllabic preposition (§3.3), where Phonological Recoverability forces partial deletion: MaxElide removes PersP and the residue is spelled out.

Equations

• Scott2021.pronounce t Scott2021.Origin.bound x✝ = Scott2021.spellout t
• Scott2021.pronounce t Scott2021.Origin.movementCopy true = Scott2021.spellout (Scott2021.deleteLayer Scott2021.DPCat.Pers t)
• Scott2021.pronounce t Scott2021.Origin.movementCopy false = none

theorem Scott2021.gap_without_minimality (t : Syntax.Tree DPCat String) : pronounce t Origin.movementCopy false = none

Subjects and objects, with no Minimality requirement, leave a gap ((17)–(18)).

theorem Scott2021.movement_copy_personless (p : Person) (n : Number) : p = Person.first ∨ p = Person.second → pronounce (pronoun (some p) n) Origin.movementCopy true = pronounce (pronoun none n) Origin.bound true

A movement copy under Minimality loses its person and surfaces as the personless pronoun ((36)).

The data pool (§3.4, §4)

structure Scott2021.Row : Type

A cell of the pool: the antecedent's person and number, the construction, the resumptive form or forms, and the judgment.

• construction : String
• person : Person
• number : Number
• form : String
• parasitic : Option String
• accepted : Bool

def Scott2021.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Scott2021.instDecidableEqRow : DecidableEq Row

Equations

• Scott2021.instDecidableEqRow = Scott2021.instDecidableEqRow.decEq

def Scott2021.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Scott2021.instReprRow : Repr Row

Equations

• Scott2021.instReprRow = { reprPrec := Scott2021.instReprRow.repr }

def Scott2021.Row.ofExample (ex : Data.Examples.LinguisticExample) : Option Row

Equations

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

theorem Scott2021.row_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Row.ofExample ex).isSome = true

def Scott2021.rows : List Row

Equations

• Scott2021.rows = List.filterMap Scott2021.Row.ofExample Scott2021.Examples.all

def Scott2021.Row.tree (r : Row) : Syntax.Tree DPCat String

The antecedent's structure.

Equations

• r.tree = Scott2021.pronoun (some r.person) r.number

theorem Scott2021.cleft_rows (r : Row) : r ∈ rows → r.construction = "cleft" → (r.accepted = true) = (pronounce r.tree Origin.bound true = some r.form ∨ pronounce r.tree Origin.movementCopy true = some r.form)

Clefts ((24)–(25), (29)): either the bound pronoun or the movement copy is available, so the form is accepted iff it is one of the two — which fixes number while leaving person optional.

theorem Scott2021.island_rows (r : Row) : r ∈ rows → r.construction = "island" → (r.accepted = true) = (pronounce r.tree Origin.bound true = some r.form)

Adjunct islands ((31)–(33)): movement is blocked, so the form is accepted iff it is the bound pronoun's.

theorem Scott2021.parasitic_rows (r : Row) : r ∈ rows → r.construction = "parasiticGap" → r.parasitic = pronounce r.tree Origin.movementCopy true → (r.accepted = true) = (some r.form = pronounce r.tree Origin.movementCopy true)

Parasitic gaps ((36)–(37), Table 4): a movement copy in the parasitic position is licensed only by a movement copy in the true-gap position — for every speaker, ye … ye is in and mi … ye is out.