Scott (2021): Two Types of Resumptive Pronouns in Swahili

This file formalizes the paper's account of the resumptive pronouns that the objects of Swahili's monosyllabic prepositions require (§3.3): bound pronouns, the only option inside adjunct islands ((31)–(33)), match the head in person, while movement copies, diagnosed by parasitic gaps ((35)–(37)), never carry person. Both follow from the Vocabulary of (28) (resumptiveVocab) and the copy theory of movement. A pronoun is a PhraseStructure.Tree over D, Num, the animate n and, for local persons only, a Person projection ((40)–(44), pronoun), and the Vocabulary spells out the Fragment's paradigm of Table 2 (table2). A movement copy in a position with a phonological requirement is reduced rather than deleted, following [Lan06]: MaxElide removes the largest constituent whose residue can still be spelled out (Deletable, maxElideTarget), which is PersP, since -ye spells out [sg + n_anim] while nothing spells out Num alone ((46)–(48), maxElide_persP). So a movement copy of a local-person pronoun surfaces as the personless pronoun (movement_copy_personless), a bound pronoun is spelled out in full, and a copy in a subject or object position, which carries no requirement, is deleted ((17)–(18), gap_without_minimality); and since Num is above Pers, a deletion that keeps person keeps number (person_entails_number), the crosslinguistic pattern of the paper's conclusion. The paper's judgments (Data/Examples/Scott2021) instantiate the account: clefts allow either pronoun but fix number ((24)–(25), (29)), islands allow only the bound pronoun, and for every speaker of Table 4 a personless parasitic pronoun needs a personless true gap (cleft_rows, island_rows, parasitic_rows).

Implementation notes

• The structures are PhraseStructure.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.

References

• [Sco21]
• [Lan06]

The structure of pronouns (§5.1)

inductive Scott2021.DPCat : Type

The DP-internal projections of (40)–(41) are 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) : PhraseStructure.Tree DPCat String

A pronoun is [DP D [NumP Num [nP n_anim [PersP Pers]]]] ((41)), 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

A terminal contributes its person, its number, or the animate gender.

Equations

• Scott2021.terminalFeature Scott2021.DPCat.Pers "1" = some ⟨Minimalist.FeatureType.person, Person.first⟩
• Scott2021.terminalFeature Scott2021.DPCat.Pers "2" = some ⟨Minimalist.FeatureType.person, Person.second⟩
• Scott2021.terminalFeature Scott2021.DPCat.Num "sg" = some ⟨Minimalist.FeatureType.number, Number.singular⟩
• Scott2021.terminalFeature Scott2021.DPCat.Num "pl" = some ⟨Minimalist.FeatureType.number, Number.plural⟩
• Scott2021.terminalFeature Scott2021.DPCat.n "anim" = some ⟨Minimalist.FeatureType.gender, Gender.animate⟩
• Scott2021.terminalFeature x✝¹ x✝ = none

def Scott2021.featureList (t : PhraseStructure.Tree DPCat String) : List Minimalist.FeatureVal

The features at a tree's terminals, left to right.

Equations

• Scott2021.featureList t = List.filterMap (fun (x : Scott2021.DPCat × String) => match x with | (c, w) => Scott2021.terminalFeature c w) t.terminals

Vocabulary Insertion (§3.4)

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

The Vocabulary Items of (28), the 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 : PhraseStructure.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 ↑(Scott2021.featureList t)

def Scott2021.cellPerson (c : Agreement.Bundle) : Option Person

The person of a cell as the structures' person, third person being the absence of PersP.

Equations

• Scott2021.cellPerson c = if c.IsSAP then some c.person else none

def Scott2021.cellNumber (c : Agreement.Bundle) : Number

The number of a cell.

Equations

• Scott2021.cellNumber c = if c.IsPlural then Number.plural else Number.singular

theorem Scott2021.table2 (c : Agreement.Bundle) : c ∈ Agreement.Bundle.personNumberCells → Option.map Morphology.Morph.suff (spellout (pronoun (cellPerson c) (cellNumber c))) = Swahili.resumptive.realize c

Every cell of the resumptive paradigm of Table 2 is the Subset Principle's choice for the corresponding structure, by the Vocabulary of (28) ((43), (45)).

MaxElide (§5.2–5.3)

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

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

Equations

• Scott2021.deleteLayer c (RoseTree.node (PhraseStructure.Tree.Label.node k) children) = PhraseStructure.Tree.node k (Scott2021.deleteLayerAll c children)
• Scott2021.deleteLayer c x✝ = x✝

def Scott2021.deleteLayerAll (c : DPCat) : List (PhraseStructure.Tree DPCat String) → List (PhraseStructure.Tree DPCat String)

Equations

• Scott2021.deleteLayerAll c [] = []
• Scott2021.deleteLayerAll c (t :: ts) = if t.cat = c then Scott2021.deleteLayerAll c ts else Scott2021.deleteLayer c t :: Scott2021.deleteLayerAll c ts

def Scott2021.Deletable (t : PhraseStructure.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 : PhraseStructure.Tree DPCat String) (c : DPCat) : Decidable (Deletable t c)

Equations

• Scott2021.instDecidableDeletable t c = { decide := decide (c ≠ Scott2021.DPCat.D) && decide ((Scott2021.spellout (Scott2021.deleteLayer c t)).isSome = true), reflects_decide := ⋯ }

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 : PhraseStructure.Tree DPCat String) : Option DPCat

MaxElide chooses 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.FeatureVal) => decide (f.fst = Minimalist.FeatureType.person)) = true → ((featureList (deleteLayer c (pronoun (some Person.first) n))).any fun (f : Minimalist.FeatureVal) => decide (f.fst = Minimalist.FeatureType.number)) = true

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

Chain reduction (§5.2–5.3)

inductive Scott2021.Origin : Type

A resumptive is 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 ⋯

@[instance_reducible]

instance Scott2021.instReprOrigin : Repr Origin

Equations

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

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✝

def Scott2021.pronounce (t : PhraseStructure.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 removing PersP and the residue being 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 : PhraseStructure.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)

inductive Scott2021.Construction : Type

The constructions of the pool are simple clefts, clefts out of adjunct islands, and parasitic gaps.

• cleft : Construction
• island : Construction
• parasiticGap : Construction

@[instance_reducible]

instance Scott2021.instDecidableEqConstruction : DecidableEq Construction

Equations

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

@[instance_reducible]

instance Scott2021.instReprConstruction : Repr Construction

Equations

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

def Scott2021.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

structure Scott2021.Row : Type

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

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

@[instance_reducible]

instance Scott2021.instDecidableEqRow : DecidableEq Row

Equations

• Scott2021.instDecidableEqRow = Scott2021.instDecidableEqRow.decEq

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.instReprRow : Repr Row

Equations

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

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

Equations

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

def Scott2021.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem Scott2021.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Scott2021.rows : List Row

Equations

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

def Scott2021.Row.tree (r : Row) : PhraseStructure.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 = Construction.cleft → (r.accepted = true) = (pronounce r.tree Origin.bound true = some r.form ∨ pronounce r.tree Origin.movementCopy true = some r.form)

In a cleft 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 ((24)–(25), (29)).

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

Out of an adjunct island movement is blocked, so the form is accepted iff it is the bound pronoun's ((31)–(33)).

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

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