Nominal Phrase Structure (Distributed Morphology)

@cite{alexiadou-2003} @cite{adamson-2024} @cite{myler-2016} @cite{kramer-2015} @cite{kampanarou-alexiadou-2026}

Structural positions within the extended nominal projection, the Gender Locality Hypothesis (GLH), and the possession-type distinction.

These types encode general claims about nominal structure that are independent of any particular language:

• The nominal spine: √ROOT < n < (Num) < (Poss) < D
• The GLH: gender features on n must be valued within nP
• Inalienable vs alienable possession: nP-internal vs PossP-external

The inalienable/alienable structural distinction is canonically @cite{alexiadou-2003} (with earlier proposals in Guéron 1985, Vergnaud & Zubizarreta 1992); subsequent treatments include @cite{myler-2016} and the DM refinement of @cite{adamson-2024}, which adds the GLH. Recent uptake of the same distinction (recoverable from Greek genitive alternation): @cite{kampanarou-alexiadou-2026}.

Caveat on PossessionType.possessorPosition .inalienable = .specN. The original Alexiadou 2003 / @cite{kampanarou-alexiadou-2026} eq. 37a analysis represents the inalienable possessor as the complement of NP (sister of the possessee under a higher NP node), not as Spec,nP. The substrate's .specN is a contemporary DM gloss on this — close enough that downstream consumers (Tseltalan possessor extraction in @cite{aissen-polian-2025}, Icelandic hafa/eiga in @cite{myler-2016}) recover the right empirical predictions, but readers should be aware that not every formulation in the literature carves up the alienable/inalienable contrast at exactly Spec,nP vs Spec,PossP. Field divergence: Michelioudakis et al. 2024 explicitly collapses both possessor types into Spec,nP (cf. @cite{kampanarou-alexiadou-2026} p. 24), which the substrate does not currently represent.

inductive Morphology.DM.NominalPosition : Type

Structural positions within and around the nominal phrase.

@cite{adamson-2024} distinguishes positions by their locality to n, the locus of gender features:

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

Only positions within nP are local enough to condition gender.

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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqNominalPosition : DecidableEq NominalPosition

Equations

• Morphology.DM.instDecidableEqNominalPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.instReprNominalPosition.repr : NominalPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprNominalPosition : Repr NominalPosition

Equations

• Morphology.DM.instReprNominalPosition = { reprPrec := Morphology.DM.instReprNominalPosition.repr }

def Morphology.DM.NominalPosition.isWithinNP : NominalPosition → Bool

Is this position within nP?

nP-internal positions: root, n head, Spec,nP (inalienable possessor). Everything else (Poss, Spec,PossP, Num, D) is outside nP.

Equations

• Morphology.DM.NominalPosition.root.isWithinNP = true
• Morphology.DM.NominalPosition.nHead.isWithinNP = true
• Morphology.DM.NominalPosition.specN.isWithinNP = true
• Morphology.DM.NominalPosition.poss.isWithinNP = false
• Morphology.DM.NominalPosition.specPoss.isWithinNP = false
• Morphology.DM.NominalPosition.num.isWithinNP = false
• Morphology.DM.NominalPosition.d.isWithinNP = false

def Morphology.DM.genderLocalityHypothesis (pos : NominalPosition) : Bool

Gender Locality Hypothesis (GLH):

"Gender features on n must be valued only within nP." (@cite{adamson-2024} (15))

A position can influence gender assignment iff it is nP-internal. Elements introduced at Poss, Num, D, or higher cannot condition gender.

Equations

• Morphology.DM.genderLocalityHypothesis pos = pos.isWithinNP

theorem Morphology.DM.glh_inalienable_possessor : genderLocalityHypothesis NominalPosition.specN = true

theorem Morphology.DM.glh_alienable_possessor : genderLocalityHypothesis NominalPosition.specPoss = false

theorem Morphology.DM.glh_high_number_irrelevant : genderLocalityHypothesis NominalPosition.num = false

theorem Morphology.DM.glh_definiteness_irrelevant : genderLocalityHypothesis NominalPosition.d = false

theorem Morphology.DM.glh_root_and_n_local : genderLocalityHypothesis NominalPosition.root = true ∧ genderLocalityHypothesis NominalPosition.nHead = true

inductive Morphology.DM.PossessionType : Type

Two types of possession, distinguished by structural position (@cite{adamson-2024}, following @cite{myler-2016}).

• Inalienable (iPossession): possessor introduced in Spec,nP. The n head bears a selectional feature {D} (CatHead.selectsD). Semantically introduces a body-part-of / part-whole relation.
• Alienable (aPossession): possessor introduced in Spec,PossP, mediated by a Poss head. Requires additional morphological marking in many languages (e.g., Teop te).

• inalienable : PossessionType
• alienable : PossessionType

@[implicit_reducible]

instance Morphology.DM.instDecidableEqPossessionType : DecidableEq PossessionType

Equations

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

def Morphology.DM.instReprPossessionType.repr : PossessionType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprPossessionType : Repr PossessionType

Equations

• Morphology.DM.instReprPossessionType = { reprPrec := Morphology.DM.instReprPossessionType.repr }

def Morphology.DM.PossessionType.possessorPosition : PossessionType → NominalPosition

Equations

• Morphology.DM.PossessionType.inalienable.possessorPosition = Morphology.DM.NominalPosition.specN
• Morphology.DM.PossessionType.alienable.possessorPosition = Morphology.DM.NominalPosition.specPoss

def Morphology.DM.PossessionType.canAffectGender (pt : PossessionType) : Bool

Can this possession type affect gender assignment? Derived from the GLH and the possessor's structural position.

Equations

• pt.canAffectGender = Morphology.DM.genderLocalityHypothesis pt.possessorPosition

theorem Morphology.DM.inalienable_can_affect_gender : PossessionType.inalienable.canAffectGender = true

theorem Morphology.DM.alienable_cannot_affect_gender : PossessionType.alienable.canAffectGender = false

inductive Morphology.DM.NumberPosition : Type

Number features can appear in two positions (@cite{adamson-2024} §5.1):

• Low number (on n): derivational, can interact with gender. Evidence: Standard Italian -a plurals (masc.sg → fem.pl), Tunisian Arabic collectives (Dali & Mathieu 2021).
• High number (on Num): inflectional, cannot interact with gender.

• onN : NumberPosition
• onNum : NumberPosition

@[implicit_reducible]

instance Morphology.DM.instDecidableEqNumberPosition : DecidableEq NumberPosition

Equations

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

def Morphology.DM.instReprNumberPosition.repr : NumberPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprNumberPosition : Repr NumberPosition

Equations

• Morphology.DM.instReprNumberPosition = { reprPrec := Morphology.DM.instReprNumberPosition.repr }

def Morphology.DM.NumberPosition.toNominalPosition : NumberPosition → NominalPosition

Equations

• Morphology.DM.NumberPosition.onN.toNominalPosition = Morphology.DM.NominalPosition.nHead
• Morphology.DM.NumberPosition.onNum.toNominalPosition = Morphology.DM.NominalPosition.num

theorem Morphology.DM.low_number_can_affect_gender : genderLocalityHypothesis NumberPosition.onN.toNominalPosition = true

theorem Morphology.DM.high_number_cannot_affect_gender : genderLocalityHypothesis NumberPosition.onNum.toNominalPosition = false

inductive Morphology.DM.ExternalFeature : Type

Functional heads outside nP whose features cannot affect gender assignment under the GLH (@cite{adamson-2024} §5.2).

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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqExternalFeature : DecidableEq ExternalFeature

Equations

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

def Morphology.DM.instReprExternalFeature.repr : ExternalFeature → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprExternalFeature : Repr ExternalFeature

Equations

• Morphology.DM.instReprExternalFeature = { reprPrec := Morphology.DM.instReprExternalFeature.repr }

def Morphology.DM.ExternalFeature.toNominalPosition : ExternalFeature → NominalPosition

Map external features to their nearest NominalPosition (lower bound). Clausal features are outside DP entirely; D is the highest nominal position, itself already outside nP.

Equations

• Morphology.DM.ExternalFeature.case.toNominalPosition = Morphology.DM.NominalPosition.d
• Morphology.DM.ExternalFeature.definiteness.toNominalPosition = Morphology.DM.NominalPosition.d
• Morphology.DM.ExternalFeature.tense.toNominalPosition = Morphology.DM.NominalPosition.d
• Morphology.DM.ExternalFeature.aspect.toNominalPosition = Morphology.DM.NominalPosition.d
• Morphology.DM.ExternalFeature.voice.toNominalPosition = Morphology.DM.NominalPosition.d

theorem Morphology.DM.external_features_irrelevant (f : ExternalFeature) : genderLocalityHypothesis f.toNominalPosition = false

inductive Morphology.DM.PossessionGenderMechanism : Type

Two mechanisms by which iPossession can affect gender (@cite{adamson-2024} §§2.3, 3–4):

1. Possessee gender: the noun's gender is determined by WHETHER it has an iPossessor. The n head that introduces an iPossessor bears particular gender features. (Teop, Jarawara)
2. Inherited gender: the noun's gender is determined by the GENDER OF the iPossessor. An unvalued gender probe on n is valued via Probe-Goal agreement with the iPossessor DP. (Yanyuwa, Coastal Marind)

• possesseeGender : PossessionGenderMechanism
• inheritedGender : PossessionGenderMechanism

@[implicit_reducible]

instance Morphology.DM.instDecidableEqPossessionGenderMechanism : DecidableEq PossessionGenderMechanism

Equations

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

def Morphology.DM.instReprPossessionGenderMechanism.repr : PossessionGenderMechanism → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprPossessionGenderMechanism : Repr PossessionGenderMechanism

Equations

• Morphology.DM.instReprPossessionGenderMechanism = { reprPrec := Morphology.DM.instReprPossessionGenderMechanism.repr }

def Morphology.DM.PossessionGenderMechanism.possessorPosition : PossessionGenderMechanism → NominalPosition

Both mechanisms involve an iPossessor in Spec,nP.

Equations

• Morphology.DM.PossessionGenderMechanism.possesseeGender.possessorPosition = Morphology.DM.NominalPosition.specN
• Morphology.DM.PossessionGenderMechanism.inheritedGender.possessorPosition = Morphology.DM.NominalPosition.specN

theorem Morphology.DM.both_mechanisms_glh_consistent : genderLocalityHypothesis PossessionGenderMechanism.possesseeGender.possessorPosition = true ∧ genderLocalityHypothesis PossessionGenderMechanism.inheritedGender.possessorPosition = true

Both mechanisms are consistent with the GLH: in both possessee gender (Teop, Jarawara) and inherited gender (Yanyuwa, Coastal Marind), the gender-affecting element is nP-internal.