Scott (2023): Pronouns and Agreement in San Juan Atitán Mam

This file formalizes the dissertation's account of agreement and pronoun form in San Juan Atitán Mam. Agreement is copying under the interaction and satisfaction theory of Agree (54): a probe copies the features of its interaction condition from the first goal that satisfies it. The probe on Infl (73) interacts with author and number and is satisfied by φ or by transitive Voice (inflProbe), so in a transitive clause it halts at transitive Voice before reaching either argument and copies nothing (inflProbe_transitive), while in an intransitive clause it reaches the subject (inflProbe_intransitive); the agreeing-object grammar of standard Mam differs in the one disjunct (standardInflProbe_transitive). Which head agrees with which argument is read off the probes (agreedBy).

Vocabulary Insertion realizes the copied features by the Extended Subset Principle (53) over the Vocabulary of Tables 4.7, 4.8 and 4.10 and of (59), (65) and (66) (vocabulary), which derives the Fragment's Set A and Set B paradigms (setA_realize, setB_realize) and the default Set B of a transitive clause, where Infl carries no φ (setB_transitive). A pronoun hosts every item its features license, so first-person pronouns are bimorphemic (§4.4.1, insertAll). A probe that copies a goal's features flags the goal with its category (§4.4.3.2, Feat.flag), and the impoverishment rule (84) deletes number from a flagged first-person pronoun (rule84), bleeding the bases qin and qo: the reduced subject and possessor series and the full independent series of Table 4.25 are both derived from one Vocabulary (form_flagged, form_unflagged), and the optional rule (93) reduces second-person plural in Set A contexts alone (form_rule93). The dissertation's judgments (Data/Examples/Scott2023) instantiate the derivation (pronoun_rows).

Implementation notes

• Features are Harbour's bivalent person and number features (Table 4.4) with the head a Set A or Set B terminal sits on and the flag a copying probe leaves; the person features of a cell are Harbour's signs of its referential category (Harbour2016.signOf), and the two pronoun series the derivation targets are the fragment's Mam.independent and Mam.subjPoss. Contextual specifications of Vocabulary Items are features of the same terminal, so the Extended Subset Principle is the substrate's subsetPrinciple over sites.
• Multiple insertion (§4.4.1) is read with the Extended Subset Principle: every applicable item is inserted unless a more specific applicable item realizes what it realizes, which is what keeps the generic plural qa out of the second-person plural q=i.
• The object is licensed by Voice under pure satisfaction (§4.4.4.1), a probe that copies nothing and so flags nothing; only the φ-copying probes are modeled, so the object is unflagged.
• Search domains are the clause spines of (56), (60) and (64): in a transitive clause Infl encounters transitive Voice first, then the object, which has moved above the subject (§3.4.1).
• The default Set A of super-extended ergative clauses (§2.6.3, §3.4.3.3) is data here; the dissertation leaves its derivation open.

References

• [Sco23]
• [Dea24]
• [Har16a]
• [Noy92]

Features and Vocabulary

inductive Scott2023.Locus : Type

The loci of agreement are Infl, the Set B locus, and v/n, Voice or Poss, the Set A locus (Tables 4.7, 4.8).

• infl : Locus
• vn : Locus

@[instance_reducible]

instance Scott2023.instDecidableEqLocus : DecidableEq Locus

Equations

• Scott2023.instDecidableEqLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Scott2023.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

• Scott2023.instReprLocus.repr Scott2023.Locus.infl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.Locus.infl")).group prec✝
• Scott2023.instReprLocus.repr Scott2023.Locus.vn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.Locus.vn")).group prec✝

@[instance_reducible]

instance Scott2023.instReprLocus : Repr Locus

Equations

• Scott2023.instReprLocus = { reprPrec := Scott2023.instReprLocus.repr }

The cells

inductive Scott2023.PronCell : Type

The seven person–number cells of the pronominal paradigm (Table 4.4), the quadripartition of persons crossed with number less the impossible first person singular inclusive.

• firstSg : PronCell
• firstPlExcl : PronCell
• firstPlIncl : PronCell
• secondSg : PronCell
• secondPl : PronCell
• thirdSg : PronCell
• thirdPl : PronCell

@[instance_reducible]

instance Scott2023.instDecidableEqPronCell : DecidableEq PronCell

Equations

• Scott2023.instDecidableEqPronCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Scott2023.instReprPronCell : Repr PronCell

Equations

• Scott2023.instReprPronCell = { reprPrec := Scott2023.instReprPronCell.repr }

def Scott2023.instReprPronCell.repr : PronCell → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Scott2023.instReprPronCell.repr Scott2023.PronCell.firstSg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.PronCell.firstSg")).group prec✝
• Scott2023.instReprPronCell.repr Scott2023.PronCell.thirdSg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.PronCell.thirdSg")).group prec✝
• Scott2023.instReprPronCell.repr Scott2023.PronCell.thirdPl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.PronCell.thirdPl")).group prec✝

def Scott2023.PronCell.category : PronCell → Person.Category

The referential category of a cell.

Equations

• Scott2023.PronCell.firstSg.category = Person.Category.speaker
• Scott2023.PronCell.firstPlExcl.category = Person.Category.speakerOthers
• Scott2023.PronCell.firstPlIncl.category = Person.Category.speakerAddressee
• Scott2023.PronCell.secondSg.category = Person.Category.addressee
• Scott2023.PronCell.secondPl.category = Person.Category.addresseeOthers
• Scott2023.PronCell.thirdSg.category = Person.Category.other
• Scott2023.PronCell.thirdPl.category = Person.Category.others

def Scott2023.PronCell.person : PronCell → Person

The person of a cell as the agreement paradigms see it, first against non-first.

Equations

• Scott2023.PronCell.firstSg.person = Person.first
• Scott2023.PronCell.firstPlExcl.person = Person.first
• Scott2023.PronCell.firstPlIncl.person = Person.first
• Scott2023.PronCell.secondSg.person = Person.second
• Scott2023.PronCell.secondPl.person = Person.second
• Scott2023.PronCell.thirdSg.person = Person.third
• Scott2023.PronCell.thirdPl.person = Person.third

def Scott2023.PronCell.number : PronCell → Number

The number of a cell.

Equations

• Scott2023.PronCell.firstSg.number = Number.singular
• Scott2023.PronCell.secondSg.number = Number.singular
• Scott2023.PronCell.thirdSg.number = Number.singular
• Scott2023.PronCell.firstPlExcl.number = Number.plural
• Scott2023.PronCell.firstPlIncl.number = Number.plural
• Scott2023.PronCell.secondPl.number = Number.plural
• Scott2023.PronCell.thirdPl.number = Number.plural

def Scott2023.PronCell.bundle : PronCell → Agreement.Bundle

The cell of the fragment's pronoun paradigms, with clusivity on the person.

Equations

• Scott2023.PronCell.firstSg.bundle = Agreement.Bundle.personNumber Person.first Number.singular
• Scott2023.PronCell.firstPlExcl.bundle = Agreement.Bundle.personNumber Person.firstExclusive Number.plural
• Scott2023.PronCell.firstPlIncl.bundle = Agreement.Bundle.personNumber Person.firstInclusive Number.plural
• Scott2023.PronCell.secondSg.bundle = Agreement.Bundle.personNumber Person.second Number.singular
• Scott2023.PronCell.secondPl.bundle = Agreement.Bundle.personNumber Person.second Number.plural
• Scott2023.PronCell.thirdSg.bundle = Agreement.Bundle.personNumber Person.third Number.singular
• Scott2023.PronCell.thirdPl.bundle = Agreement.Bundle.personNumber Person.third Number.plural

def Scott2023.PronCell.sign (c : PronCell) : Person.Feature → Bool

The person features of a cell (Table 4.4) are Harbour's sign of its category, [±author] and [±participant], the latter an addressee feature under which the first person singular and exclusive are [−participant].

Equations

• c.sign = Harbour2016.signOf c.category

def Scott2023.PronCell.singular (c : PronCell) : Bool

Whether a cell is singular.

Equations

• c.singular = decide (c.number = Number.singular)

def Scott2023.independentOf (c : PronCell) : Option PersonalPronoun

The fragment's independent pronoun of a cell.

Equations

• Scott2023.independentOf c = Mam.independent.realize c.bundle

def Scott2023.subjPossOf (c : PronCell) : Option PersonalPronoun

The fragment's subject and possessor pronoun of a cell.

Equations

• Scott2023.subjPossOf c = Mam.subjPoss.realize c.bundle

Features and Vocabulary Items

inductive Scott2023.Feat : Type

A feature of a terminal is one of Harbour's bivalent person and number features (Table 4.4), the locus a Set A or Set B terminal sits on, or the flag a probe leaves on a goal whose features it has copied (§4.4.3.2, Table 4.26).

• author (b : Bool) : Feat
• participant (b : Bool) : Feat
• singular (b : Bool) : Feat
• head (l : Locus) : Feat
• flag (l : Locus) : Feat

@[instance_reducible]

instance Scott2023.instDecidableEqFeat : DecidableEq Feat

Equations

• Scott2023.instDecidableEqFeat = Scott2023.instDecidableEqFeat.decEq

def Scott2023.instDecidableEqFeat.decEq (x✝ x✝¹ : Feat) : Decidable (x✝ = x✝¹)

Equations

• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.author a) (Scott2023.Feat.author b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.author b) (Scott2023.Feat.participant b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.author b) (Scott2023.Feat.singular b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.author b) (Scott2023.Feat.head l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.author b) (Scott2023.Feat.flag l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.participant b) (Scott2023.Feat.author b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.participant a) (Scott2023.Feat.participant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.participant b) (Scott2023.Feat.singular b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.participant b) (Scott2023.Feat.head l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.participant b) (Scott2023.Feat.flag l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.singular b) (Scott2023.Feat.author b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.singular b) (Scott2023.Feat.participant b_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.singular a) (Scott2023.Feat.singular b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.singular b) (Scott2023.Feat.head l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.singular b) (Scott2023.Feat.flag l) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.head l) (Scott2023.Feat.author b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.head l) (Scott2023.Feat.participant b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.head l) (Scott2023.Feat.singular b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.head a) (Scott2023.Feat.head b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.head l) (Scott2023.Feat.flag l_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.flag l) (Scott2023.Feat.author b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.flag l) (Scott2023.Feat.participant b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.flag l) (Scott2023.Feat.singular b) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.flag l) (Scott2023.Feat.head l_1) = isFalse ⋯
• Scott2023.instDecidableEqFeat.decEq (Scott2023.Feat.flag a) (Scott2023.Feat.flag b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Scott2023.instReprFeat.repr : Feat → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Scott2023.instReprFeat : Repr Feat

Equations

• Scott2023.instReprFeat = { reprPrec := Scott2023.instReprFeat.repr }

def Scott2023.cellFeats (c : PronCell) : List Feat

The features of a pronoun in a paradigm cell (Table 4.4).

Equations

• Scott2023.cellFeats c = [Scott2023.Feat.author (c.sign Person.Feature.author), Scott2023.Feat.participant (c.sign Person.Feature.participant), Scott2023.Feat.singular c.singular]

structure Scott2023.Item : Type

A Vocabulary Item, as the dissertation writes them, has the features it realizes, its contextual specification, and its exponent.

• realized : List Feat
• context : List Feat
• exponent : Morphology.Morph

def Scott2023.instDecidableEqItem.decEq (x✝ x✝¹ : Item) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Scott2023.instDecidableEqItem : DecidableEq Item

Equations

• Scott2023.instDecidableEqItem = Scott2023.instDecidableEqItem.decEq

@[instance_reducible]

instance Scott2023.instReprItem : Repr Item

Equations

• Scott2023.instReprItem = { reprPrec := Scott2023.instReprItem.repr }

def Scott2023.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

def Scott2023.Item.site (i : Item) : List Feat

Everything an item requires of its terminal.

Equations

• i.site = i.realized ++ i.context

def Scott2023.Item.toVI (i : Item) : DistributedMorphology.VocabularyItem Feat Morphology.Morph

The item for the substrate's Subset Principle keeps its site and exponent.

Equations

• i.toVI = { site := ↑i.site, exponent := i.exponent }

def Scott2023.vocabulary : List Item

The Vocabulary lists Set A (Table 4.7), Set B with its context-free first-person plural and its Elsewhere item (Table 4.8), the pronominal base qin (Table 4.10), the plurals q and qa ((65), (66)), and the disagreement enclitic at its two disagreeing values (59), listed last as the items are linearized in Vocabulary order.

Equations

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

def Scott2023.insert1 (t : List Feat) : Option Morphology.Morph

Single insertion at an agreement terminal inserts the most specific applicable item, by the Extended Subset Principle (53).

Equations

• Scott2023.insert1 t = DistributedMorphology.subsetPrinciple (List.map Scott2023.Item.toVI Scott2023.vocabulary) ↑t

def Scott2023.insertAll (t : List Feat) : List Morphology.Morph

Multiple insertion at a pronoun (§4.4.1) inserts every applicable item, unless a more specific applicable item realizes what it realizes.

Equations

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

Agreement (§3.4.2, §4.4.2)

structure Scott2023.Encounter : Type

On its search a probe meets an argument bearing φ, or the transitive Voice head.

• role : Option ArgumentRole
• phi : Bool
• voiceTR : Bool

def Scott2023.instDecidableEqEncounter.decEq (x✝ x✝¹ : Encounter) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Scott2023.instDecidableEqEncounter : DecidableEq Encounter

Equations

• Scott2023.instDecidableEqEncounter = Scott2023.instDecidableEqEncounter.decEq

@[instance_reducible]

instance Scott2023.instReprEncounter : Repr Encounter

Equations

• Scott2023.instReprEncounter = { reprPrec := Scott2023.instReprEncounter.repr }

def Scott2023.instReprEncounter.repr : Encounter → ℕ → Std.Format

Equations

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

def Scott2023.voiceTR : Encounter

The transitive Voice head.

Equations

• Scott2023.voiceTR = { role := none, phi := false, voiceTR := true }

def Scott2023.dp (r : ArgumentRole) : Encounter

An argument bearing φ.

Equations

• Scott2023.dp r = { role := some r, phi := true, voiceTR := false }

def Scott2023.inflProbe : Minimalist.Probe Encounter

The probe on Infl (73) interacts with φ and is satisfied by φ or by transitive Voice, so either halts it, and it agrees with a goal only if the goal bears φ.

Equations

• Scott2023.inflProbe = { int := fun (e : Scott2023.Encounter) => e.phi, sat := fun (e : Scott2023.Encounter) => e.phi || e.voiceTR }

def Scott2023.standardInflProbe : Minimalist.Probe Encounter

The probe on Infl of the agreeing-object grammar (56), satisfied by φ alone.

Equations

• Scott2023.standardInflProbe = Minimalist.Probe.relativized fun (x : Scott2023.Encounter) => x.phi

def Scott2023.vnProbe : Minimalist.Probe Encounter

The probe on Voice or Poss, satisfied by the φ of its specifier.

Equations

• Scott2023.vnProbe = Minimalist.Probe.relativized fun (x : Scott2023.Encounter) => x.phi

def Scott2023.inflDomain : ArgumentRole → List Encounter

Infl's search domain in the clause of an argument (60), (64) is transitive Voice, then the object, which has moved above the subject, then the subject; or the intransitive subject.

Equations

• Scott2023.inflDomain ArgumentRole.A = [Scott2023.voiceTR, Scott2023.dp ArgumentRole.P, Scott2023.dp ArgumentRole.A]
• Scott2023.inflDomain ArgumentRole.P = [Scott2023.voiceTR, Scott2023.dp ArgumentRole.P, Scott2023.dp ArgumentRole.A]
• Scott2023.inflDomain ArgumentRole.S = [Scott2023.dp ArgumentRole.S]
• Scott2023.inflDomain ArgumentRole.R = []
• Scott2023.inflDomain ArgumentRole.T = []

def Scott2023.vnDomain : ArgumentRole → List Encounter

The search domain of Voice or Poss is its specifier, the transitive subject.

Equations

• Scott2023.vnDomain ArgumentRole.A = [Scott2023.dp ArgumentRole.A]
• Scott2023.vnDomain x✝ = []

theorem Scott2023.inflProbe_transitive (rest : List Encounter) : inflProbe.agree (voiceTR :: rest) = none

In a transitive clause Infl's probe halts at transitive Voice and agrees with nothing, whatever lies below (60), (61).

theorem Scott2023.inflProbe_intransitive : inflProbe.agree [dp ArgumentRole.S] = some (dp ArgumentRole.S)

In an intransitive clause Infl's probe agrees with the subject (64).

theorem Scott2023.standardInflProbe_transitive (rest : List Encounter) : standardInflProbe.agree (voiceTR :: dp ArgumentRole.P :: rest) = some (dp ArgumentRole.P)

Under the agreeing-object grammar Infl's probe passes transitive Voice and agrees with the object (56), (57).

def Scott2023.agreedBy (r : ArgumentRole) : Option Locus

The probe that copies an argument's features sits on Infl for the intransitive subject and on Voice or Poss for the transitive subject; no probe copies the object's.

Equations

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

theorem Scott2023.agreedBy_S : agreedBy ArgumentRole.S = some Locus.infl

theorem Scott2023.agreedBy_A : agreedBy ArgumentRole.A = some Locus.vn

theorem Scott2023.agreedBy_P : agreedBy ArgumentRole.P = none

def Scott2023.copied (c : PronCell) : List Feat

A probe copies author and number (73a).

Equations

• Scott2023.copied c = [Scott2023.Feat.author (c.sign Person.Feature.author), Scott2023.Feat.singular c.singular]

def Scott2023.inflTerminal (r : ArgumentRole) (c : PronCell) : List Feat

The Set B terminal on Infl in the clause of an argument in a cell carries the copied features if Infl agreed with the argument, at the Infl locus.

Equations

• Scott2023.inflTerminal r c = (if Scott2023.agreedBy r = some Scott2023.Locus.infl then Scott2023.copied c else []) ++ [Scott2023.Feat.head Scott2023.Locus.infl]

def Scott2023.vnTerminal (c : PronCell) : List Feat

The Set A terminal on Voice or Poss agreeing with a cell.

Equations

• Scott2023.vnTerminal c = Scott2023.copied c ++ [Scott2023.Feat.head Scott2023.Locus.vn]

theorem Scott2023.setB_realize (c : PronCell) : Agreement.Paradigm.realize Mam.setBExponent (Agreement.Bundle.personNumber c.person c.number) = Option.map (fun (x : Morphology.Morph) => [x]) (insert1 (inflTerminal ArgumentRole.S c))

The Fragment's Set B paradigm (Table 4.6) is the Vocabulary's spell-out of what Infl copies from an intransitive subject; 2SG and 3SG fall to the Elsewhere item.

theorem Scott2023.setB_transitive (c : PronCell) : insert1 (inflTerminal ArgumentRole.P c) = some (Morphology.Morph.procl "tz'")

By default Set B (61), with no features copied, inserts the Elsewhere item tz'=, whatever the object's cell.

theorem Scott2023.setA_realize (c : PronCell) : Agreement.Paradigm.realize (Mam.setAExponent Phonology.Segment.Class.consonant) (Agreement.Bundle.personNumber c.person c.number) = Option.map (fun (x : Morphology.Morph) => [x]) (insert1 (vnTerminal c))

The Fragment's Set A paradigm (Table 4.5, pre-consonantal) is the Vocabulary's spell-out of what Voice or Poss copies.

theorem Scott2023.chin_beats_qin : insert1 (copied PronCell.firstSg ++ [Feat.head Locus.infl]) = some (Morphology.Morph.free "chin") ∧ insert1 (copied PronCell.firstSg) = some (Morphology.Morph.free "qin")

chin and qin compete (Table 4.10): both realize first-person singular, the Infl-specified item wins on Infl, and only the context-free base is available off it.

Pronoun form (§4.4)

inductive Scott2023.Dim : Type

The dimension an impoverishment rule deletes.

• author : Dim
• participant : Dim
• singular : Dim

@[instance_reducible]

instance Scott2023.instDecidableEqDim : DecidableEq Dim

Equations

• Scott2023.instDecidableEqDim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Scott2023.instReprDim : Repr Dim

Equations

• Scott2023.instReprDim = { reprPrec := Scott2023.instReprDim.repr }

def Scott2023.instReprDim.repr : Dim → ℕ → Std.Format

Equations

• Scott2023.instReprDim.repr Scott2023.Dim.author prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.Dim.author")).group prec✝
• Scott2023.instReprDim.repr Scott2023.Dim.participant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.Dim.participant")).group prec✝
• Scott2023.instReprDim.repr Scott2023.Dim.singular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Scott2023.Dim.singular")).group prec✝

def Scott2023.delete (t : List Feat) (d : Dim) : List Feat

Delete a dimension from a terminal.

Equations

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

def Scott2023.flagged (t : List Feat) : Bool

Whether a terminal carries the flag of some probe.

Equations

• Scott2023.flagged t = t.any fun (f : Scott2023.Feat) => match f with | Scott2023.Feat.flag l => true | x => false

def Scott2023.rule84 : DistributedMorphology.ImpoverishmentRule (List Feat) Dim

The impoverishment rule (84) deletes number from a first-person pronoun a probe has flagged.

Equations

• Scott2023.rule84 = DistributedMorphology.ImpoverishmentRule.ofFocus (fun (t : List Scott2023.Feat) => Scott2023.Feat.author true ∈ t ∧ Scott2023.flagged t = true) Scott2023.Dim.singular

def Scott2023.rule93 : DistributedMorphology.ImpoverishmentRule (List Feat) Dim

The optional rule (93) deletes number from a second-person pronoun flagged by Voice or Poss.

Equations

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

theorem Scott2023.rule84_paradigmatic : rule84.Paradigmatic

def Scott2023.pronounTerminal (l : Option Locus) (c : PronCell) : List Feat

A pronoun terminal in a cell, flagged by the probe that copied its features, if any.

Equations

• Scott2023.pronounTerminal l c = Scott2023.cellFeats c ++ (Option.map (fun (l : Scott2023.Locus) => [Scott2023.Feat.flag l]) l).getD []

def Scott2023.formWith (rules : List (DistributedMorphology.ImpoverishmentRule (List Feat) Dim)) (l : Option Locus) (c : PronCell) : List Morphology.Morph

The form of a pronoun in a cell under a grammar with impoverishment rules rules, flagged by l: the rules apply and every licensed item is inserted.

Equations

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

def Scott2023.form (l : Option Locus) (c : PronCell) : List Morphology.Morph

The form of a pronoun under the grammar of (84).

Equations

• Scott2023.form l c = Scott2023.formWith [Scott2023.rule84] l c

def Scott2023.morphemes : Option PersonalPronoun → List Morphology.Morph

The morphemes of the Fragment's pronoun entries (Table 4.9) are qin=i, qo'=y, qo, =i, q=i, qa, and the null third-person singular.

Equations

• One or more equations did not get rendered due to their size.
• Scott2023.morphemes none = []

theorem Scott2023.form_unflagged (c : PronCell) : form none c = morphemes (independentOf c)

In the independent series (Table 4.25), an unflagged pronoun, an object or the subject of a non-verbal predicate, hosts every item its features license.

theorem Scott2023.form_flagged (l : Locus) (c : PronCell) : form (some l) c = morphemes (subjPossOf c)

In the subject and possessor series (Table 4.25), a pronoun flagged by either locus loses its number if first person, so the bases qin and qo are bled and the enclitic remains.

theorem Scott2023.form_rule93 : formWith [rule84, rule93] (some Locus.vn) PronCell.secondPl = [Morphology.Morph.encl "i"] ∧ formWith [rule84, rule93] (some Locus.infl) PronCell.secondPl = morphemes (subjPossOf PronCell.secondPl)

With the optional rule (93), second-person plural reduces to the enclitic in a Set A context but not in a Set B context ((89)–(91)).

def Scott2023.formAt (r : ArgumentRole) (c : PronCell) : List Morphology.Morph

An argument in a cell takes the form flagged by the probe that agreed with it.

Equations

• Scott2023.formAt r c = Scott2023.form (Scott2023.agreedBy r) c

theorem Scott2023.formAt_eq (c : PronCell) : formAt ArgumentRole.S c = morphemes (subjPossOf c) ∧ formAt ArgumentRole.A c = morphemes (subjPossOf c) ∧ formAt ArgumentRole.P c = morphemes (independentOf c)

Reduction is nominatively aligned ((3), (8)): subjects take the reduced series and the object the independent series.

theorem Scott2023.encl_mem_independent_iff (c : PronCell) : Morphology.Morph.encl "i" ∈ morphemes (independentOf c) ↔ c.sign Person.Feature.author ≠ c.sign Person.Feature.participant

The disagreement generalization ([Noy92], §4.3.3), read off the fragment: a cell's independent pronoun contains the enclitic exactly when its author and participant features disagree.

theorem Scott2023.reduced_iff_author (c : PronCell) : subjPossOf c ≠ independentOf c ↔ c.sign Person.Feature.author = true

Reduction is first-personhood: the subject and possessor pronoun differs from the independent one exactly at the [+author] cells (Table 4.1).

The judgments

def Scott2023.spell (ms : List Morphology.Morph) : String

A pronoun is spelled as its morphemes with clitic boundaries.

Equations

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

structure Scott2023.Row : Type

A judgment of the pool records the position's flag, the cell, the pronoun, whether the optional rule (93) is in force, and the judgment.

• flag : Option Locus
• cell : PronCell
• pronoun : String
• optional : Bool
• accepted : Bool

@[instance_reducible]

instance Scott2023.instDecidableEqRow : DecidableEq Row

Equations

• Scott2023.instDecidableEqRow = Scott2023.instDecidableEqRow.decEq

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

Equations

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

@[instance_reducible]

instance Scott2023.instReprRow : Repr Row

Equations

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

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

Equations

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

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

Equations

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

def Scott2023.rows : List Row

The pronoun judgments of §4.4.

Equations

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

theorem Scott2023.pronoun_rows (r : Row) : r ∈ rows → (r.accepted = true ↔ spell (form r.flag r.cell) = r.pronoun ∨ r.optional = true ∧ spell (formWith [rule84, rule93] r.flag r.cell) = r.pronoun)

A pronoun is accepted exactly when it is the derived form, under (84) or, where the row invokes it, the optional (93).