Documentation

Linglib.Studies.McGinnis2013

Agree and Fission in Georgian plurals #

[mcginnis-2013]: the interactions among the number suffixes of the Georgian verb follow from one number-agreement feature on T, specified [Group], and from Fission of the fused Tense/Aspect/Mood node during Vocabulary Insertion. T's [Group] probes the subject, then a first- or second-person object clitic, so one argument per clause triggers plural agreement ((5)–(6)); the TAM node is realized by strict scansion, each item discharging its intrinsic features and the residue passing on, so the third-person plural screeve -es leaves no Group for -t (*g-nax-es-t, (3)), -t [#, Group] leaves no # for the default -s [#] (*g-nax-o-s-t, (15), (20)), and -s's TAM restriction is contextual, not discharged ((13)–(14)). The dative first-person plural bears the collective person feature Multispeaker with its Group impoverished ((8)), so gv- marks it and no -t follows ((23)), while gv-nax-e-t (21) has a single Group, the subject's. The person prefixes (9) are ranked by the feature geometry (4): a dependent node brings every node it depends on, so gv- [Multispeaker] ⊃ m- [Speaker] ⊃ g- [Participant], and the geometry supplies the [#] of the revised -t (13c).

Main definitions #

Feature, site: geometry nodes, case, and TAM features; a site as the lower set of the nodes it mentions.
Argument, numberTarget, personTarget: the arguments and the two probes.
prefixes, Screeve.vocabulary: the Vocabularies (9), (10), (13).
personPrefix, suffixes: the person prefix by the Subset Principle and the TAM suffixes by scansion.

Main results #

rows_realized: every row of the pool is grammatical iff the prefix and suffixes are what the analysis inserts.
dependent_more_specific, prefix_ranking: geometric dependence is site inclusion, so the engine ranks (9a) > (9b) > (9c) and (9d) > (9e) > (9f).
t_revised: the geometry gives -t its [#].
sites_lowerSets, screeve_first, number_ranked: every site is a lower set, interpretable features are discharged first, and the number items are ranked by intrinsic then contextual features.
count_group_le_one: the TAM node never carries two Groups.

References #

[S. Béjar, Phi-syntax][bejar-2003]
[S. R. Anderson, On representations in morphology][anderson-1984]
H. Harley and E. Ritter, Person and number in pronouns
A. González Poot and M. McGinnis, Local versus long-distance Fission

Features and arguments #

inductive McGinnis2013.Feature :

Geometry nodes, dative case, and the interpretable TAM features: 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

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.instReprFeature :

Equations

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

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

A site as the geometry reads it: every node at or below those mentioned — a dependent brings what it depends on — with any further feature.

Equations

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

Instances For

structure McGinnis2013.Argument :

An agreeing argument: person, plurality, and dative case.

person : Person
plural : Bool
dat : Bool

Instances For

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance McGinnis2013.instDecidableEqArgument :

DecidableEq Argument

Equations

McGinnis2013.instDecidableEqArgument = McGinnis2013.instDecidableEqArgument.decEq

@[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.personNodes (a : Argument) :

List Phi.Geometry.Node

Georgian activates Speaker but not Addressee: first person is Participant with Speaker — and Multispeaker when plural — second person bare Participant, third person nothing.

Equations

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

Instances For

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

Bool

Group survives on a plural argument unless Impoverishment deletes it: the dative first-person plural ((8)).

Equations

a.hasGroup = (a.plural && !(a.dat && decide (a.person = Person.first)))

Instances For

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

A first- or second-person argument: a clitic, within T's reach.

Equations

a.IsParticipant = (a.person = Person.first ∨ a.person = Person.second)

Instances For

@[instance_reducible]

instance McGinnis2013.instDecidablePredArgumentIsParticipant :

DecidablePred Argument.IsParticipant

Equations

McGinnis2013.instDecidablePredArgumentIsParticipant x✝ = McGinnis2013.instDecidablePredArgumentIsParticipant._aux_1 x✝

Agree #

def McGinnis2013.numberTarget (subj obj : Argument) :

Option Argument

T's [Group] probe: the subject if plural; probing again, a plural participant object clitic; otherwise nothing, and Group deletes ((5)–(7)).

Equations

McGinnis2013.numberTarget subj obj = if subj.hasGroup = true then some subj else if obj.IsParticipant ∧ obj.hasGroup = true then some obj else none

Instances For

def McGinnis2013.personTarget (subj obj : Argument) :

Option Argument

v's [Participant] probe: a participant object first, else a participant subject ((7), (9)).

Equations

McGinnis2013.personTarget subj obj = if obj.IsParticipant then some obj else if subj.IsParticipant then some subj else none

Instances For

def McGinnis2013.numberNodes :

Option Argument → List Phi.Geometry.Node

The Individuation content T copies from its target: Group, and Class for a third-person argument; the bare # node when no argument is plural.

Equations

McGinnis2013.numberNodes (some a) = [Phi.Geometry.Node.individuation, Phi.Geometry.Node.group] ++ if a.person = Person.third then [Phi.Geometry.Node.nounClass] else []
McGinnis2013.numberNodes none = [Phi.Geometry.Node.individuation]

Instances For

def McGinnis2013.prefixNode (subj obj : Argument) :

The person-agreement node on v: the target's person content with its case.

Equations

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

Instances For

inductive McGinnis2013.Screeve :

The two screeves treated: aorist (10) and 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 ⋯

@[instance_reducible]

instance McGinnis2013.instReprScreeve :

Equations

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

def McGinnis2013.instReprScreeve.repr :

Screeve → ℕ → Std.Format

Equations

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

Instances For

def McGinnis2013.Screeve.features :

Screeve → List Feature

The screeve's interpretable features.

Equations

Instances For

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

The fused TAM node: the screeve's features, person agreement with the subject, 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 (9), (9e) without its x- allomorph.

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.aoristScreeve :

List (DistributedMorphology.VocabularyItem Feature String)

The aorist screeve items (10a–c).

Equations

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

Instances For

def McGinnis2013.aoristNumber :

List (DistributedMorphology.VocabularyItem Feature String)

The aorist number items: -t (13c) and the elsewhere.

Equations

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

Instances For

def McGinnis2013.optativeScreeve :

List (DistributedMorphology.VocabularyItem Feature String)

The optative screeve item (13a).

Equations

McGinnis2013.optativeScreeve = [DistributedMorphology.VocabularyItem.ofFeatures [McGinnis2013.Feature.ftam, McGinnis2013.Feature.optative] "o"]

Instances For

def McGinnis2013.optativeNumber :

List (DistributedMorphology.VocabularyItem Feature String)

The optative number items (13b–e): contextual features condition insertion without being discharged.

Equations

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

Instances For

def McGinnis2013.Screeve.vocabulary :

Screeve → List (DistributedMorphology.VocabularyItem Feature String)

A screeve's Vocabulary in scansion order: interpretable features first.

Equations

Instances For

def McGinnis2013.personPrefix (subj obj : Argument) :

Option String

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

Equations

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

Instances For

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

List String

The overt TAM suffixes: strict scansion with local Fission at the fused node, whose own features stand as context to every item.

Equations

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

Instances For

The data pool #

structure McGinnis2013.Row :

A row: the arguments, screeve, and the attested prefix and suffixes.

subj : Argument
obj : Argument
screeve : Screeve
prefix_ : String
suffixes : List String
accepted : Bool

Instances For

def McGinnis2013.instReprRow.repr :

Row → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance McGinnis2013.instReprRow :

Repr Row

Equations

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

def McGinnis2013.Person.ofLabel :

String → Option Person

Equations

McGinnis2013.Person.ofLabel "1" = some Person.first
McGinnis2013.Person.ofLabel "2" = some Person.second
McGinnis2013.Person.ofLabel "3" = some Person.third
McGinnis2013.Person.ofLabel x✝ = none

Instances For

def McGinnis2013.Screeve.ofLabel :

String → Option Screeve

Equations

McGinnis2013.Screeve.ofLabel "aorist" = some McGinnis2013.Screeve.aorist
McGinnis2013.Screeve.ofLabel "optative" = some McGinnis2013.Screeve.optative
McGinnis2013.Screeve.ofLabel x✝ = none

Instances For

def McGinnis2013.Row.ofExample (ex : Data.Examples.LinguisticExample) :

Option Row

Equations

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

Instances For

theorem McGinnis2013.row_ofExample_isSome (ex : Data.Examples.LinguisticExample) :

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

def McGinnis2013.rows :

List Row

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

Equations

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

Instances For

theorem McGinnis2013.rows_realized (r : Row) :

r ∈ rows → (r.accepted = true) = (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 — one Group per clause, no -t after -es, no -s beside -t, no -t for a dative first-person plural.

The geometry's ranking #

theorem McGinnis2013.dependent_more_specific {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: geometric dependence is site inclusion, hence engine ranking (VocabularyItem.le_iff).

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

(9a) ⊃ (9b) ⊃ (9c) and (9d) ⊃ (9e) ⊃ (9f): the prefixes are ranked by the geometry, Multispeaker depending on Speaker on Participant.

theorem McGinnis2013.t_revised :

site [Phi.Geometry.Node.group] [] = [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 is [#, Group].

theorem McGinnis2013.sites_lowerSets (i : DistributedMorphology.VocabularyItem Feature String) :

i ∈ prefixes ++ aoristScreeve ++ aoristNumber ++ optativeScreeve ++ optativeNumber → IsLowerSet ↑(insert ⊥ (List.filterMap (fun (f : Feature) => match f with | Feature.node n => some n | x => none) i.site.focus).toFinset)

The geometry nodes of every site form a lower set with the root.

The ranking of the number items #

theorem McGinnis2013.screeve_first :

(∀ i ∈ aoristScreeve, Feature.aorist ∈ i.site.focus) ∧ (∀ i ∈ aoristNumber, Feature.aorist ∉ i.site.focus) ∧ (∀ i ∈ optativeScreeve, Feature.ftam ∈ i.site.focus) ∧ ∀ i ∈ optativeNumber, Feature.ftam ∉ i.site.focus ∧ Feature.optative ∉ i.site.focus

Interpretable features are discharged first: every screeve item carries one and no number item does.

theorem McGinnis2013.number_ranked :

List.Pairwise (fun (i j : DistributedMorphology.VocabularyItem Feature String) => toLex (j.site.focus.length, j.site.leftCtx.flatten.length) < toLex (i.site.focus.length, i.site.leftCtx.flatten.length)) optativeNumber

Pāṇinian ranking with intrinsic features leading and contextual features deciding ties: the number items descend lexicographically in (intrinsic, contextual) feature count, -t above -s ((20)).

One Group per clause #

theorem McGinnis2013.count_group_personNodes (a : Argument) :

List.count Phi.Geometry.Node.group a.personNodes = 0

theorem McGinnis2013.count_group_numberNodes (t : Option Argument) :

List.count Phi.Geometry.Node.group (numberNodes t) ≤ 1

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

List.count (Feature.node Phi.Geometry.Node.group) (tamNode s subj obj) ≤ 1

T carries at most one Group: plural agreement with one argument ((5), §3.3.1).