The extended nominal projection

The extended nominal projection — the nominal spine √ROOT < n < Poss < Num < D — as an order of heads, with the positions of the nominal domain classified by where they attach. Locality to n is then geometry: a position is within nP exactly when its attachment site is at or below n, which is what [Ada24]'s Gender Locality Hypothesis (gender features on n are valued only within nP) quantifies over. The inalienable/alienable possession contrast is a contrast of attachment sites — Spec,nP versus Spec,PossP ([Ale03]; [Myl16]) — and low versus high number likewise ([Ada24]).

Main definitions

• NominalProjection.Head — the heads of the extended nominal projection, linearly ordered by height
• NominalProjection.Position, Position.attachmentSite, isWithinNP — the positions of the nominal domain and their place on the projection
• PossessionType, NumberPosition — the possession and number contrasts as attachment contrasts
• ExternalFeature — features attached above nP, clausal ones outside the nominal spine altogether (⊤)
• PossessionGenderMechanism — possessee gender vs inherited gender

Main statements

• ExternalFeature.not_withinNP — no external feature attaches within nP

Implementation notes

PossessionType.possessorPosition .inalienable = .specN is a contemporary DM gloss: [Ale03] (and [KA26]'s rendering of it) places the inalienable possessor as the complement of NP rather than Spec,nP. Downstream consumers (Tseltalan possessor extraction in [AP25], Icelandic hafa/eiga in [Myl16]) recover the right empirical predictions either way, but not every formulation carves the contrast at exactly Spec,nP vs Spec,PossP — Michelioudakis et al. collapse both possessor types into Spec,nP (as [KA26] notes), which this substrate does not represent.

References

• A. Alexiadou, Some notes on the structure of alienable and inalienable possessors
• L. J. Adamson, Gender assignment is local
• N. Myler, Building and interpreting possession sentences

The heads

inductive DistributedMorphology.NominalProjection.Head : Type

The heads of the extended nominal projection, in order of height: √ROOT < n < Poss < Num < D ([Ada24]; the Poss layer after [Ale03], [Myl16]).

• root : Head
• n : Head
• poss : Head
• num : Head
• d : Head

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instDecidableEqHead : DecidableEq Head

Equations

• DistributedMorphology.NominalProjection.instDecidableEqHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.NominalProjection.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instReprHead : Repr Head

Equations

• DistributedMorphology.NominalProjection.instReprHead = { reprPrec := DistributedMorphology.NominalProjection.instReprHead.repr }

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instFintypeHead : Fintype Head

Equations

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

def DistributedMorphology.NominalProjection.Head.height : Head → ℕ

The height of a head on the projection.

Equations

• DistributedMorphology.NominalProjection.Head.root.height = 0
• DistributedMorphology.NominalProjection.Head.n.height = 1
• DistributedMorphology.NominalProjection.Head.poss.height = 2
• DistributedMorphology.NominalProjection.Head.num.height = 3
• DistributedMorphology.NominalProjection.Head.d.height = 4

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instLinearOrderHead : LinearOrder Head

Equations

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

Positions and their attachment sites

inductive DistributedMorphology.NominalProjection.Position : Type

Structural positions within and around the nominal phrase:

[DP D [NumP Num [PossP DP Poss [nP DP [n √ROOT n]]]]]

heads of the projection together with the two possessor specifiers.

• root : Position
• nHead : Position
• specN : Position
• poss : Position
• specPoss : Position
• num : Position
• d : Position

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instDecidableEqPosition : DecidableEq Position

Equations

• DistributedMorphology.NominalProjection.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instReprPosition : Repr Position

Equations

• DistributedMorphology.NominalProjection.instReprPosition = { reprPrec := DistributedMorphology.NominalProjection.instReprPosition.repr }

def DistributedMorphology.NominalProjection.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.NominalProjection.instFintypePosition : Fintype Position

Equations

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

def DistributedMorphology.NominalProjection.Position.attachmentSite : Position → Head

Where each position attaches: a specifier attaches at its head's projection.

Equations

• DistributedMorphology.NominalProjection.Position.root.attachmentSite = DistributedMorphology.NominalProjection.Head.root
• DistributedMorphology.NominalProjection.Position.nHead.attachmentSite = DistributedMorphology.NominalProjection.Head.n
• DistributedMorphology.NominalProjection.Position.specN.attachmentSite = DistributedMorphology.NominalProjection.Head.n
• DistributedMorphology.NominalProjection.Position.poss.attachmentSite = DistributedMorphology.NominalProjection.Head.poss
• DistributedMorphology.NominalProjection.Position.specPoss.attachmentSite = DistributedMorphology.NominalProjection.Head.poss
• DistributedMorphology.NominalProjection.Position.num.attachmentSite = DistributedMorphology.NominalProjection.Head.num
• DistributedMorphology.NominalProjection.Position.d.attachmentSite = DistributedMorphology.NominalProjection.Head.d

def DistributedMorphology.NominalProjection.Position.isWithinNP (p : Position) : Bool

Within-nP is geometry: the position attaches at or below n.

Equations

• p.isWithinNP = decide (p.attachmentSite ≤ DistributedMorphology.NominalProjection.Head.n)

def DistributedMorphology.genderLocalityHypothesis (pos : NominalProjection.Position) : Bool

The Gender Locality Hypothesis ([Ada24]): gender features on n are valued only within nP, so a position can condition gender exactly when its attachment site is at or below n.

Equations

• DistributedMorphology.genderLocalityHypothesis pos = pos.isWithinNP

Possession

inductive DistributedMorphology.PossessionType : Type

Two types of possession, distinguished by the possessor's attachment site ([Ada24], following [Myl16]; [Ale03]). The inalienable possessor sits in Spec,nP, licensed by an n bearing the selectional feature {D} (Categorizer.Head.selectsD) and interpreted by a part-whole relation; the alienable possessor sits in Spec,PossP, mediated by a Poss head and often extra morphology (Teop te).

• inalienable : PossessionType
• alienable : PossessionType

@[instance_reducible]

instance DistributedMorphology.instDecidableEqPossessionType : DecidableEq PossessionType

Equations

• DistributedMorphology.instDecidableEqPossessionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.instReprPossessionType.repr : PossessionType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprPossessionType : Repr PossessionType

Equations

• DistributedMorphology.instReprPossessionType = { reprPrec := DistributedMorphology.instReprPossessionType.repr }

@[instance_reducible]

instance DistributedMorphology.instFintypePossessionType : Fintype PossessionType

Equations

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

def DistributedMorphology.PossessionType.possessorPosition : PossessionType → NominalProjection.Position

The possessor's position.

Equations

• DistributedMorphology.PossessionType.inalienable.possessorPosition = DistributedMorphology.NominalProjection.Position.specN
• DistributedMorphology.PossessionType.alienable.possessorPosition = DistributedMorphology.NominalProjection.Position.specPoss

def DistributedMorphology.PossessionType.canAffectGender (pt : PossessionType) : Bool

Whether this possession type can affect gender assignment: the GLH applied to the possessor's attachment site.

Equations

• pt.canAffectGender = DistributedMorphology.genderLocalityHypothesis pt.possessorPosition

Number

inductive DistributedMorphology.NumberPosition : Type

Number features appear in two positions ([Ada24]): low number on n is derivational and can interact with gender (Standard Italian -a plurals, Tunisian Arabic collectives); high number on Num is inflectional and cannot.

• onN : NumberPosition
• onNum : NumberPosition

@[instance_reducible]

instance DistributedMorphology.instDecidableEqNumberPosition : DecidableEq NumberPosition

Equations

• DistributedMorphology.instDecidableEqNumberPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instReprNumberPosition : Repr NumberPosition

Equations

• DistributedMorphology.instReprNumberPosition = { reprPrec := DistributedMorphology.instReprNumberPosition.repr }

def DistributedMorphology.instReprNumberPosition.repr : NumberPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instFintypeNumberPosition : Fintype NumberPosition

Equations

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

def DistributedMorphology.NumberPosition.toPosition : NumberPosition → NominalProjection.Position

The position a number feature occupies.

Equations

• DistributedMorphology.NumberPosition.onN.toPosition = DistributedMorphology.NominalProjection.Position.nHead
• DistributedMorphology.NumberPosition.onNum.toPosition = DistributedMorphology.NominalProjection.Position.num

External features

inductive DistributedMorphology.ExternalFeature : Type

Features attached outside nP, which the GLH bars from conditioning gender ([Ada24]): case and definiteness in the nominal periphery, tense, aspect, and voice on the clausal spine.

• case : ExternalFeature
• definiteness : ExternalFeature
• tense : ExternalFeature
• aspect : ExternalFeature
• voice : ExternalFeature

@[instance_reducible]

instance DistributedMorphology.instDecidableEqExternalFeature : DecidableEq ExternalFeature

Equations

• DistributedMorphology.instDecidableEqExternalFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.instReprExternalFeature.repr : ExternalFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprExternalFeature : Repr ExternalFeature

Equations

• DistributedMorphology.instReprExternalFeature = { reprPrec := DistributedMorphology.instReprExternalFeature.repr }

@[instance_reducible]

instance DistributedMorphology.instFintypeExternalFeature : Fintype ExternalFeature

Equations

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

def DistributedMorphology.ExternalFeature.attachmentSite : ExternalFeature → WithTop NominalProjection.Head

Where an external feature attaches: case and definiteness at D, the clausal features outside the nominal projection altogether.

Equations

• DistributedMorphology.ExternalFeature.case.attachmentSite = some DistributedMorphology.NominalProjection.Head.d
• DistributedMorphology.ExternalFeature.definiteness.attachmentSite = some DistributedMorphology.NominalProjection.Head.d
• DistributedMorphology.ExternalFeature.tense.attachmentSite = ⊤
• DistributedMorphology.ExternalFeature.aspect.attachmentSite = ⊤
• DistributedMorphology.ExternalFeature.voice.attachmentSite = ⊤

theorem DistributedMorphology.ExternalFeature.not_withinNP (f : ExternalFeature) : ¬f.attachmentSite ≤ ↑NominalProjection.Head.n

No external feature attaches within nP.

Possession–gender mechanisms

inductive DistributedMorphology.PossessionGenderMechanism : Type

The two mechanisms by which inalienable possession can affect gender ([Ada24]): under possessee gender the noun's gender is determined by whether it has an iPossessor — the licensing n itself bears the gender feature (Teop, Jarawara) — while under inherited gender the noun's gender is the iPossessor's, an unvalued probe on n valued by Agree (Yanyuwa, Coastal Marind). Both mechanisms place the possessor in Spec,nP, within the GLH's reach.

• possesseeGender : PossessionGenderMechanism
• inheritedGender : PossessionGenderMechanism

@[instance_reducible]

instance DistributedMorphology.instDecidableEqPossessionGenderMechanism : DecidableEq PossessionGenderMechanism

Equations

• DistributedMorphology.instDecidableEqPossessionGenderMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.instReprPossessionGenderMechanism.repr : PossessionGenderMechanism → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprPossessionGenderMechanism : Repr PossessionGenderMechanism

Equations

• DistributedMorphology.instReprPossessionGenderMechanism = { reprPrec := DistributedMorphology.instReprPossessionGenderMechanism.repr }

@[instance_reducible]

instance DistributedMorphology.instFintypePossessionGenderMechanism : Fintype PossessionGenderMechanism

Equations

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

def DistributedMorphology.PossessionGenderMechanism.possessorPosition : PossessionGenderMechanism → NominalProjection.Position

Both mechanisms involve an iPossessor in Spec,nP.

Equations

• DistributedMorphology.PossessionGenderMechanism.possesseeGender.possessorPosition = DistributedMorphology.NominalProjection.Position.specN
• DistributedMorphology.PossessionGenderMechanism.inheritedGender.possessorPosition = DistributedMorphology.NominalProjection.Position.specN