Documentation

Studies.McGinnis2013

McGinnis (2013): Agree and Fission in Georgian Plurals #

McGinnis derives the number suffixes of the Georgian verb from one fused tense–aspect–mood node, which agrees in number with at most one argument and fissions during Vocabulary Insertion. T's number probe looks for [Group] first on the subject and then on a first- or second-person object clitic, and Impoverishment removes the [Group] of a dative first-person plural, whose plurality then shows only through [Multispeaker] in the prefix gv-. Each suffix discharges the features it spells out, so the third-person plural screeve suffix leaves no [Group] for -t, and -t leaves no [#] for the default -s.

Main results #

rows_realized: a form of the pool is grammatical iff its prefix and suffixes are those the analysis inserts.
one_exponent_per_feature: in every clause the suffixes realize disjoint parts of T's node, so there is no double plural marking, which Fission alone would not exclude (fission_alone_allows_double_plural).
setB_realize, setA_realize: the analysis yields the agreement affixes of the Fragment's two sets, gv- without -t included.

Implementation notes #

An item's contextual features are read off the fused node as it stands before insertion, so they are never discharged.
Only the aorist and optative screeves are modelled, and the null second-person prefix without its x- allomorph.
[DAT] is the feature the Set B prefixes spell out, borne by the argument that the Fragment's second-series pattern marks by Set B, though that pattern makes the direct object nominative.

References #

Features #

inductive McGinnis2013.Feature :

The features are the geometry nodes, dative case, and the interpretable TAM features, namely aorist, optative, and the feature the optative shares with the present, future, and conjunctive.

node (n : Phi.Geometry.Node) : Feature
dat : Feature
aorist : Feature
optative : Feature
ftam : Feature

Instances For

@[instance_reducible]

instance McGinnis2013.instDecidableEqFeature :

DecidableEq Feature

Equations

McGinnis2013.instDecidableEqFeature = McGinnis2013.instDecidableEqFeature.decEq

def McGinnis2013.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance McGinnis2013.instReprFeature :

Equations

McGinnis2013.instReprFeature = { reprPrec := McGinnis2013.instReprFeature.repr }

def McGinnis2013.instReprFeature.repr :

Feature → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
McGinnis2013.instReprFeature.repr McGinnis2013.Feature.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McGinnis2013.Feature.dat")).group prec✝
McGinnis2013.instReprFeature.repr McGinnis2013.Feature.ftam prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McGinnis2013.Feature.ftam")).group prec✝

Instances For

@[instance_reducible]

instance McGinnis2013.instFintypeFeature :

Fintype Feature

Equations

McGinnis2013.instFintypeFeature = Fintype.ofEquiv (Phi.Geometry.Node ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit) McGinnis2013.Feature.proxyTypeEquiv

def McGinnis2013.Feature.toNode? :

Feature → Option Phi.Geometry.Node

f.toNode? is the geometry node f is, if any.

Equations

(McGinnis2013.Feature.node n).toNode? = some n
x✝.toNode? = none

Instances For

def McGinnis2013.Feature.IsUnder (a : Phi.Geometry.Node) (f : Feature) :

A feature lies under the node a when it is a node depending on a. The person features lie under Participant and the number features under Individuation.

Equations

McGinnis2013.Feature.IsUnder a f = ∃ n ∈ f.toNode?, a ≤ n

Instances For

@[instance_reducible]

instance McGinnis2013.Feature.instDecidablePredIsUnder (a : Phi.Geometry.Node) :

DecidablePred (IsUnder a)

Equations

McGinnis2013.Feature.instDecidablePredIsUnder a f = f.toNode?.decidableExistsMem

def McGinnis2013.Feature.IsInterpretable (f : Feature) :

The interpretable features are those of tense, aspect, and mood.

Equations

f.IsInterpretable = (f = McGinnis2013.Feature.aorist ∨ f = McGinnis2013.Feature.optative ∨ f = McGinnis2013.Feature.ftam)

Instances For

@[instance_reducible]

instance McGinnis2013.Feature.instDecidablePredIsInterpretable :

DecidablePred IsInterpretable

Equations

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

def McGinnis2013.site (ns : List Phi.Geometry.Node) (extra : List Feature) :

The site mentioning the nodes ns bears every node at or below them, since a dependent brings what it depends on, and the further features extra.

Equations

McGinnis2013.site ns extra = List.map McGinnis2013.Feature.node (List.flatMap Phi.Geometry.Node.below ns).eraseDups ++ extra

Instances For

theorem McGinnis2013.node_mem_site {a : Phi.Geometry.Node} {ns : List Phi.Geometry.Node} {extra : List Feature} :

Feature.node a ∈ site ns extra ↔ (∃ n ∈ ns, ⊥ < a ∧ a ≤ n) ∨ Feature.node a ∈ extra

A site bears a node iff the node lies below a mentioned one, the root aside, or is among the further features: sites are closed downward.

theorem McGinnis2013.site_subset_site {a b : Phi.Geometry.Node} (h : a ≤ b) (extra : List Feature) :

site [a] extra ⊆ site [b] extra

A dependent node's site contains its dominator's, so geometric dependence is site inclusion and hence engine ranking (VocabularyItem.le_iff).

Arguments #

structure McGinnis2013.Argument :

An agreeing argument has a person and a number.

person : Person
number : Number

Instances For

@[instance_reducible]

instance McGinnis2013.instDecidableEqArgument :

DecidableEq Argument

Equations

McGinnis2013.instDecidableEqArgument = McGinnis2013.instDecidableEqArgument.decEq

def McGinnis2013.instDecidableEqArgument.decEq (x✝ x✝¹ : Argument) :

Decidable (x✝ = x✝¹)

Equations

McGinnis2013.instDecidableEqArgument.decEq { person := a, number := a_1 } { person := b, number := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[instance_reducible]

instance McGinnis2013.instReprArgument :

Equations

McGinnis2013.instReprArgument = { reprPrec := McGinnis2013.instReprArgument.repr }

def McGinnis2013.instReprArgument.repr :

Argument → ℕ → Std.Format

Equations

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

Instances For

def McGinnis2013.Argument.features (a : Argument) :

Georgian activates neither Addressee nor Minimal ((4)), so a pronoun's first person is Participant with Speaker, its plural adding Multispeaker, its second person is bare Participant, its plural is Group under [#], and only its third person has Class.

Equations

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

Instances For

def McGinnis2013.caseFeatures (m : Georgian.Marking) :

A Set B marking spells out [DAT] ((9)), and a Set A marking no case.

Equations

McGinnis2013.caseFeatures m = if m.affixes = some Georgian.AffixSet.B then [McGinnis2013.Feature.dat] else []

Instances For

def McGinnis2013.Argument.asSubject (a : Argument) :

The subject of a transitive verb in the second series bears its φ-features and the case of its marking.

Equations

a.asSubject = a.features ++ McGinnis2013.caseFeatures (Georgian.pattern Georgian.VerbClass.transitive Georgian.Series.aorist).subject

Instances For

def McGinnis2013.Argument.asObject (a : Argument) :

The direct object of a transitive verb in the second series bears its φ-features and the case of its marking.

Equations

a.asObject = a.features ++ McGinnis2013.caseFeatures (Georgian.pattern Georgian.VerbClass.transitive Georgian.Series.aorist).directObject

Instances For

def McGinnis2013.impoverishment :

DistributedMorphology.ImpoverishmentRule (List Feature) Feature

Impoverishment deletes the [Group] of a dative first-person pronoun at the spell-out of vP, after case and before T's number probe ((8)).

Equations

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

Instances For

def McGinnis2013.impoverish (b : List Feature) :

impoverish b is the pronoun b after Impoverishment.

Equations

McGinnis2013.impoverish b = DistributedMorphology.ImpoverishmentRule.apply List.erase McGinnis2013.impoverishment ↑b

Instances For

Agree #

def McGinnis2013.personProbe :

Minimalist.Probe (List Feature)

v's person probe is specified for [Participant].

Equations

McGinnis2013.personProbe = Minimalist.Probe.relativized fun (x : List McGinnis2013.Feature) => x.contains (McGinnis2013.Feature.node Phi.Geometry.Node.participant)

Instances For

def McGinnis2013.numberProbe :

Minimalist.Probe (List Feature)

T's number probe is specified for [Group], so a goal without [Group] does not halt its search and T probes again ([Bej03]).

Equations

McGinnis2013.numberProbe = Minimalist.Probe.relativized fun (x : List McGinnis2013.Feature) => x.contains (McGinnis2013.Feature.node Phi.Geometry.Node.group)

Instances For

def McGinnis2013.prefixNode (subj obj : Argument) :

v's probe finds a participant object first, else a participant subject ((7), (9)), and its agreement node copies the goal's person features and case.

Equations

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

Instances For

def McGinnis2013.numberGoals (subj obj : Argument) :

List (List Feature)

T's number probe searches the subject and then the object if it is a first- or second-person clitic moved to T, both after Impoverishment; a third-person object stays below T ((6), (7)).

Equations

McGinnis2013.numberGoals subj obj = List.map McGinnis2013.impoverish (subj.asSubject :: if obj.person = Person.third then [] else [obj.asObject])

Instances For

def McGinnis2013.numberContent (subj obj : Argument) :

T copies the number content of its goal, and keeps the bare [#] when no goal bears [Group], the probe's [Group] then deleting ((5)).

Equations

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

Instances For

inductive McGinnis2013.Screeve :

The two screeves treated are the aorist (10) and the optative (13).

aorist : Screeve
optative : Screeve

Instances For

@[instance_reducible]

instance McGinnis2013.instDecidableEqScreeve :

DecidableEq Screeve

Equations

McGinnis2013.instDecidableEqScreeve x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McGinnis2013.instReprScreeve.repr :

Screeve → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance McGinnis2013.instReprScreeve :

Equations

McGinnis2013.instReprScreeve = { reprPrec := McGinnis2013.instReprScreeve.repr }

@[instance_reducible]

instance McGinnis2013.instFintypeScreeve :

Fintype Screeve

Equations

McGinnis2013.instFintypeScreeve = { elems := { val := ↑McGinnis2013.Screeve.enumList, nodup := McGinnis2013.Screeve.enumList_nodup }, complete := McGinnis2013.instFintypeScreeve._proof_1 }

def McGinnis2013.Screeve.features :

Screeve → List Feature

A screeve bears its interpretable features.

Equations

Instances For

def McGinnis2013.tamNode (s : Screeve) (subj obj : Argument) :

The fused TAM node bears the screeve's features, the subject's person features, and the number content T agreed with.

Equations

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

Instances For

Vocabulary #

def McGinnis2013.gv :

DistributedMorphology.VocabularyItem Feature String

The prefix items are those of (9).

Equations

McGinnis2013.gv = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.multispeaker] [McGinnis2013.Feature.dat]) "gv"

Instances For

def McGinnis2013.m :

DistributedMorphology.VocabularyItem Feature String

Equations

McGinnis2013.m = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.speaker] [McGinnis2013.Feature.dat]) "m"

Instances For

def McGinnis2013.g :

DistributedMorphology.VocabularyItem Feature String

Equations

McGinnis2013.g = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.participant] [McGinnis2013.Feature.dat]) "g"

Instances For

def McGinnis2013.v :

DistributedMorphology.VocabularyItem Feature String

Equations

McGinnis2013.v = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.speaker] []) "v"

Instances For

def McGinnis2013.participantNull :

DistributedMorphology.VocabularyItem Feature String

Equations

McGinnis2013.participantNull = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.participant] []) ""

Instances For

def McGinnis2013.elsewhere :

DistributedMorphology.VocabularyItem Feature String

Equations

McGinnis2013.elsewhere = DistributedMorphology.VocabularyItem.ofFeatures [] ""

Instances For

def McGinnis2013.prefixes :

List (DistributedMorphology.VocabularyItem Feature String)

Equations

McGinnis2013.prefixes = [McGinnis2013.gv, McGinnis2013.m, McGinnis2013.g, McGinnis2013.v, McGinnis2013.participantNull, McGinnis2013.elsewhere]

Instances For

def McGinnis2013.plural :

DistributedMorphology.VocabularyItem Feature String

The plural suffix -t (13c) takes its [#] from the geometry.

Equations

McGinnis2013.plural = DistributedMorphology.VocabularyItem.ofFeatures (McGinnis2013.site [Phi.Geometry.Node.group] []) "t"

Instances For

def McGinnis2013.participantNumber :

DistributedMorphology.VocabularyItem Feature String

A null suffix (13d) realizes the [#] of a participant.

Equations

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

Instances For

def McGinnis2013.defaultNumber :

DistributedMorphology.VocabularyItem Feature String

The suffix -s (13e) realizes [#] by default.

Equations

McGinnis2013.defaultNumber = { site := { focus := McGinnis2013.site [Phi.Geometry.Node.individuation] [], leftCtx := [[McGinnis2013.Feature.ftam]] }, exponent := "s" }

Instances For

def McGinnis2013.Screeve.vocabulary :

Screeve → List (DistributedMorphology.VocabularyItem Feature String)

A screeve's Vocabulary lists the aorist items (10) or the optative items (13) in scansion order.

Equations

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

Instances For

def McGinnis2013.personPrefix (subj obj : Argument) :

Option String

The person prefix wins Elsewhere competition at v's agreement node.

Equations

McGinnis2013.personPrefix subj obj = DistributedMorphology.subsetPrinciple McGinnis2013.prefixes ↑(McGinnis2013.prefixNode subj obj)

Instances For

def McGinnis2013.suffixItems (s : Screeve) (subj obj : Argument) :

List (DistributedMorphology.VocabularyItem Feature String)

Strict scansion with local Fission inserts these items at the fused node, whose own features stand as context to every item.

Equations

McGinnis2013.suffixItems s subj obj = DistributedMorphology.insertions s.vocabulary { focus := [], leftCtx := [McGinnis2013.tamNode s subj obj] } [McGinnis2013.tamNode s subj obj]

Instances For

def McGinnis2013.suffixes (s : Screeve) (subj obj : Argument) :

List String

The overt suffixes are the inserted items' nonnull exponents.

Equations

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

Instances For

The data pool #

structure McGinnis2013.Row :

A row records the arguments, screeve, attested prefix and suffixes, and judgment.

subj : Argument
obj : Argument
screeve : Screeve
prefix_ : String
suffixes : List String
judgment : Judgment

Instances For

@[instance_reducible]

instance McGinnis2013.instReprRow :

Repr Row

Equations

McGinnis2013.instReprRow = { reprPrec := McGinnis2013.instReprRow.repr }

def McGinnis2013.instReprRow.repr :

Row → ℕ → Std.Format

Equations

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

Instances For

def McGinnis2013.Row.ofDatum (ex : Datum) :

Option Row

Equations

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

Instances For

theorem McGinnis2013.row_ofDatum_isSome (ex : Datum) :

ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def McGinnis2013.rows :

List Row

The rows are the forms of (2)–(6), (12), (15), (21)–(23), (26).

Equations

McGinnis2013.rows = List.filterMap McGinnis2013.Row.ofDatum McGinnis2013.Examples.all

Instances For

theorem McGinnis2013.rows_realized (r : Row) :

r ∈ rows → (r.judgment = Judgment.acceptable ↔ personPrefix r.subj r.obj = some r.prefix_ ∧ suffixes r.screeve r.subj r.obj = r.suffixes)

Agree and Fission. A form is grammatical iff its prefix is the Subset Principle's winner and its suffixes are what scansion inserts, so a clause has one Group, no -t after -es, no -s beside -t, and no -t for a dative first-person plural.

One exponent per feature #

theorem McGinnis2013.nodup_features_append (a : Argument) (m : Georgian.Marking) :

(a.features ++ caseFeatures m).Nodup

An argument's bundle bears each feature once.

theorem McGinnis2013.tamNode_nodup (s : Screeve) (subj obj : Argument) :

(tamNode s subj obj).Nodup

T's fused node bears each feature once, since the screeve's features, the subject's person features, and the number content of T's goal are disjoint.

theorem McGinnis2013.one_exponent_per_feature (s : Screeve) (subj obj : Argument) :

List.Pairwise (fun (i j : DistributedMorphology.VocabularyItem Feature String) => i.site.focus.Disjoint j.site.focus) (suffixItems s subj obj)

No double plural marking (§3.3.1). T bears each feature once, so the suffixes realize disjoint parts of its node. At most one realizes [Group], whence -es and -n exclude -t, and at most one realizes [#], whence -t excludes -s.

theorem McGinnis2013.fission_alone_allows_double_plural :

have node := Screeve.aorist.features ++ List.filter (fun (x : Feature) => decide (Feature.IsUnder Phi.Geometry.Node.individuation x)) { person := Person.third, number := Number.plural }.features ++ List.filter (fun (x : Feature) => decide (Feature.IsUnder Phi.Geometry.Node.individuation x)) { person := Person.second, number := Number.plural }.features; List.filter (fun (x : String) => decide (x ≠ "")) (List.map (fun (x : DistributedMorphology.VocabularyItem Feature String) => x.exponent) (DistributedMorphology.insertions Screeve.aorist.vocabulary { focus := [], leftCtx := [node] } [node])) = ["es", "t"]

Fission alone does not exclude double plural marking (§3.3.1). Were T to agree in number with both a plural third-person subject and a plural second-person object, its node would bear two [Group]s, and scansion would insert both -es and -t, the starred (3b); T's single [#] probe is what excludes it.

The ranking #

def McGinnis2013.rank (i : DistributedMorphology.VocabularyItem Feature String) :

Lex (ℕ × Lex (ℕ × ℕ))

An item ranks by the number of interpretable features it discharges, then by its Subset Principle specificity, its intrinsic features leading and its contextual ones breaking ties.

Equations

McGinnis2013.rank i = toLex (List.countP (fun (x : McGinnis2013.Feature) => decide x.IsInterpretable) i.site.focus, i.specificity)

Instances For

theorem McGinnis2013.vocabulary_ranked (s : Screeve) :

List.Pairwise (fun (i j : DistributedMorphology.VocabularyItem Feature String) => rank j < rank i) s.vocabulary

Each screeve's Vocabulary descends in rank, since interpretable features are discharged as soon as possible ((10c), (13a)) and -t ranks above -s ((20)).

theorem McGinnis2013.specificity_number :

participantNumber.specificity < plural.specificity ∧ defaultNumber.specificity < participantNumber.specificity

Intrinsic features lead the ranking, so -t (13c) ranks above the null participant suffix (13d) though it mentions fewer features, and contextual ones break ties, so (13d) ranks above -s (13e).

theorem McGinnis2013.prefix_ranking :

m.site.focus ⊆ gv.site.focus ∧ g.site.focus ⊆ m.site.focus ∧ participantNull.site.focus ⊆ v.site.focus ∧ elsewhere.site.focus ⊆ participantNull.site.focus

The geometry ranks the prefixes (9a) above (9b) above (9c) and (9d) above (9e) above (9f), Multispeaker depending on Speaker and Speaker on Participant.

theorem McGinnis2013.plural_site :

plural.site.focus = [Feature.node Phi.Geometry.Node.individuation, Feature.node Phi.Geometry.Node.group]

The geometry supplies the [#] of the revised -t (13c), the site of Group being [#, Group].

The agreement sets #

def McGinnis2013.agreementAffixes (subj obj : Argument) :

List Morphology.Morph

An aorist clause's agreement affixes are its person prefix and plural -t, the affixes the Fragment's agreement sets list.

Equations

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

Instances For

theorem McGinnis2013.setB_realize (p : Person) :

p ∈ [Person.first, Person.second, Person.third] → ∀ n ∈ [Number.singular, Number.plural], Georgian.setB.realize (Agreement.Bundle.personNumber p n) = some (agreementAffixes { person := Person.third, number := Number.singular } { person := p, number := n })

With a third-person singular subject each object receives its Set B affixes ([Hew95]), gv- without -t for the first person plural.

theorem McGinnis2013.setA_realize (p : Person) :

p ∈ [Person.first, Person.second] → ∀ n ∈ [Number.singular, Number.plural], Georgian.setA.realize (Agreement.Bundle.personNumber p n) = some (agreementAffixes { person := p, number := n } { person := Person.third, number := Number.singular })

With a third-person singular object each participant subject receives its Set A affixes.

theorem McGinnis2013.setB_plural_from_T :

Georgian.setB.realize (Agreement.Bundle.personNumber Person.second Number.plural) = some [Morphology.Morph.pref "g", Morphology.Morph.suff "t"] ∧ agreementAffixes { person := Person.third, number := Number.plural } { person := Person.second, number := Number.plural } = [Morphology.Morph.pref "g"]

The -t that Set B lists for the second person plural is T's, since a plural third-person subject's -es leaves none for the object ((3)).