Syntactic Modification via Feature Composition

@cite{alexeyenko-zeijlstra-2025}

Nominal modification as a species of complementation: adjectives and nouns cannot directly merge because neither c-selects the other. Resolution comes either from the adjective lexically carrying [N, uN] (in φ/κ-complete languages like Greek) or from an Attr head that mediates the feature conversion.

Core Claims

1. Modification = complementation: both are driven by c-selection features ([uF] checked under sisterhood with [F]). An adjective [A] and a noun [N] can merge only if one bears the other's uninterpretable categorial feature.

2. Two feature compositions (§5.1):

   • Direct: adjective enters as [N, uN], selects and merges with [N] directly. Available only when pred & attr adjectives have identical φ/κ-specification. Corresponds semantically to predicate modification.
   • Attr-mediated: an Attr head converts [A] → [N, uN] (part of xAP) or [N] → [N, uA] (part of xNP). Required when adjectives lack full φ/κ-specification.

3. Attr status determines linearization (§5.2): the morphophonological realization of Attr (affix / clitic / free word / null) determines whether it must be linearly adjacent to its host, via the Input Correspondence Principle (@cite{ackema-neeleman-2004}).

Types Exported

• AttrStatus — morphophonological status of the attributivizer
• AdjMorphProfile — per-language adjective morphosyntactic profile
• ModificationRoute — direct (no Attr) vs Attr-mediated modification
• morphStatusToAttrStatus — bridge from Core.Lexical.MorphRule.MorphStatus

inductive Minimalism.Modification.AttrStatus : Type

Morphophonological status of the attributivizer (Attr head, §5.2). Determines whether Attr imposes linear adjacency with the adjective.

• affix : AttrStatus
• clitic : AttrStatus
• freeWord : AttrStatus
• null : AttrStatus

instance Minimalism.Modification.instDecidableEqAttrStatus : DecidableEq AttrStatus

Equations

• Minimalism.Modification.instDecidableEqAttrStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.Modification.instBEqAttrStatus.beq : AttrStatus → AttrStatus → Bool

Equations

• Minimalism.Modification.instBEqAttrStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.Modification.instBEqAttrStatus : BEq AttrStatus

Equations

• Minimalism.Modification.instBEqAttrStatus = { beq := Minimalism.Modification.instBEqAttrStatus.beq }

instance Minimalism.Modification.instReprAttrStatus : Repr AttrStatus

Equations

• Minimalism.Modification.instReprAttrStatus = { reprPrec := Minimalism.Modification.instReprAttrStatus.repr }

def Minimalism.Modification.instReprAttrStatus.repr : AttrStatus → Nat → Std.Format

Equations

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

inductive Minimalism.Modification.AdjPosition : Type

Position of attributive adjectives relative to the modified noun.

• prenominal : AdjPosition
• postnominal : AdjPosition
• both : AdjPosition

instance Minimalism.Modification.instDecidableEqAdjPosition : DecidableEq AdjPosition

Equations

• Minimalism.Modification.instDecidableEqAdjPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.Modification.instBEqAdjPosition.beq : AdjPosition → AdjPosition → Bool

Equations

• Minimalism.Modification.instBEqAdjPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.Modification.instBEqAdjPosition : BEq AdjPosition

Equations

• Minimalism.Modification.instBEqAdjPosition = { beq := Minimalism.Modification.instBEqAdjPosition.beq }

def Minimalism.Modification.instReprAdjPosition.repr : AdjPosition → Nat → Std.Format

Equations

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

instance Minimalism.Modification.instReprAdjPosition : Repr AdjPosition

Equations

• Minimalism.Modification.instReprAdjPosition = { reprPrec := Minimalism.Modification.instReprAdjPosition.repr }

structure Minimalism.Modification.AdjMorphProfile : Type

Morphosyntactic profile of adjectives in a language.

The MAG (34) is determined by two independent factors:

• Morphosyntactic (§5.1): agreement identity between predicative and attributive forms, and completeness of that agreement for all φ/κ-features
• Morphophonological (§5.2): status of the attributivizer

• adjPosition : AdjPosition

  Primary position of attributive adjectives relative to N

• apDirection : HeadDirection

  Internal head direction of the AP

• predAttrSameAgreement : Bool

  MAG (34a), clause 1: the agreement marker on attr adjectives is also present on predicative adjectives (pred = attr featurally).

• agreementPhiKappaComplete : Bool

  MAG (34a), clause 2: the agreement marker is specified for ALL φ/κ-features available in the DP. Per fn 17, κ (case) is always a DP feature whether morphologically realized or not.

• attrStatus : AttrStatus

  MAG (34b): morphophonological status of the attributivizer

def Minimalism.Modification.instDecidableEqAdjMorphProfile.decEq (x✝ x✝¹ : AdjMorphProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.Modification.instDecidableEqAdjMorphProfile : DecidableEq AdjMorphProfile

Equations

• Minimalism.Modification.instDecidableEqAdjMorphProfile = Minimalism.Modification.instDecidableEqAdjMorphProfile.decEq

def Minimalism.Modification.instBEqAdjMorphProfile.beq : AdjMorphProfile → AdjMorphProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.Modification.instBEqAdjMorphProfile.beq x✝¹ x✝ = false

instance Minimalism.Modification.instBEqAdjMorphProfile : BEq AdjMorphProfile

Equations

• Minimalism.Modification.instBEqAdjMorphProfile = { beq := Minimalism.Modification.instBEqAdjMorphProfile.beq }

instance Minimalism.Modification.instReprAdjMorphProfile : Repr AdjMorphProfile

Equations

• Minimalism.Modification.instReprAdjMorphProfile = { reprPrec := Minimalism.Modification.instReprAdjMorphProfile.repr }

def Minimalism.Modification.instReprAdjMorphProfile.repr : AdjMorphProfile → Nat → Std.Format

Equations

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

inductive Minimalism.Modification.ModificationRoute : Type

The two routes to nominal modification (§5.1.2 vs §5.1.3).

• direct: adjective lexically carries [N, uN], merges directly with the noun. No Attr head needed. Only available in φ/κ-complete languages (Greek, Russian, Latin, Kalaallisut).
• attrMediated: an Attr functional head mediates the feature conversion. Required when adjectives lack full φ/κ-specification. Attr may be part of the extended adjectival projection (xAP) or the extended nominal projection (xNP).

• direct : ModificationRoute
• attrMediated : ModificationRoute

instance Minimalism.Modification.instDecidableEqModificationRoute : DecidableEq ModificationRoute

Equations

• Minimalism.Modification.instDecidableEqModificationRoute x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.Modification.instBEqModificationRoute : BEq ModificationRoute

Equations

• Minimalism.Modification.instBEqModificationRoute = { beq := Minimalism.Modification.instBEqModificationRoute.beq }

def Minimalism.Modification.instBEqModificationRoute.beq : ModificationRoute → ModificationRoute → Bool

Equations

• Minimalism.Modification.instBEqModificationRoute.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.Modification.instReprModificationRoute : Repr ModificationRoute

Equations

• Minimalism.Modification.instReprModificationRoute = { reprPrec := Minimalism.Modification.instReprModificationRoute.repr }

def Minimalism.Modification.instReprModificationRoute.repr : ModificationRoute → Nat → Std.Format

Equations

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

def Minimalism.Modification.modificationRoute (prof : AdjMorphProfile) : ModificationRoute

Determine the modification route from the adjective morphosyntactic profile. φ/κ-complete languages use direct modification; all others require an Attr head.

Equations

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

theorem Minimalism.Modification.phiKappaComplete_implies_direct (prof : AdjMorphProfile) (hSame : prof.predAttrSameAgreement = true) (hComplete : prof.agreementPhiKappaComplete = true) : modificationRoute prof = ModificationRoute.direct

φ/κ-complete languages use direct modification.

theorem Minimalism.Modification.predNeAttr_implies_attrMediated (prof : AdjMorphProfile) (h : prof.predAttrSameAgreement = false) : modificationRoute prof = ModificationRoute.attrMediated

Languages with pred ≠ attr require Attr.

theorem Minimalism.Modification.incomplete_implies_attrMediated (prof : AdjMorphProfile) (h : prof.agreementPhiKappaComplete = false) : modificationRoute prof = ModificationRoute.attrMediated

Languages with incomplete φ/κ require Attr.

def Minimalism.Modification.morphStatusToAttrStatus : Core.Morphology.MorphStatus → AttrStatus

Map the framework-agnostic MorphStatus (from Zwicky & Pullum's clitic-affix cline) to the MAG's AttrStatus. Both inflectional and derivational affixes impose adjacency per the ICP. Both simple and special clitics are morphophonologically independent.

Equations

• Minimalism.Modification.morphStatusToAttrStatus Core.Morphology.MorphStatus.freeWord = Minimalism.Modification.AttrStatus.freeWord
• Minimalism.Modification.morphStatusToAttrStatus Core.Morphology.MorphStatus.simpleClitic = Minimalism.Modification.AttrStatus.clitic
• Minimalism.Modification.morphStatusToAttrStatus Core.Morphology.MorphStatus.specialClitic = Minimalism.Modification.AttrStatus.clitic
• Minimalism.Modification.morphStatusToAttrStatus Core.Morphology.MorphStatus.inflAffix = Minimalism.Modification.AttrStatus.affix
• Minimalism.Modification.morphStatusToAttrStatus Core.Morphology.MorphStatus.derivAffix = Minimalism.Modification.AttrStatus.affix

theorem Minimalism.Modification.affix_maps_to_affix : morphStatusToAttrStatus Core.Morphology.MorphStatus.inflAffix = AttrStatus.affix

Affixes impose adjacency.

theorem Minimalism.Modification.clitic_maps_to_clitic : morphStatusToAttrStatus Core.Morphology.MorphStatus.simpleClitic = AttrStatus.clitic

Clitics are morphophonologically independent.

theorem Minimalism.Modification.freeWord_maps_to_freeWord : morphStatusToAttrStatus Core.Morphology.MorphStatus.freeWord = AttrStatus.freeWord

Free words map to free words.

inductive Minimalism.Modification.MAGFeatureType : Type

The feature types that MAG condition (a) requires agreement for. φ-features map to Minimalism.PhiFeature, κ-features to CaseVal.

• phi : PhiFeature → MAGFeatureType
• kappa : CaseVal → MAGFeatureType

def Minimalism.Modification.instDecidableEqMAGFeatureType.decEq (x✝ x✝¹ : MAGFeatureType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.Modification.instDecidableEqMAGFeatureType.decEq (Minimalism.Modification.MAGFeatureType.phi a) (Minimalism.Modification.MAGFeatureType.kappa a_1) = isFalse ⋯
• Minimalism.Modification.instDecidableEqMAGFeatureType.decEq (Minimalism.Modification.MAGFeatureType.kappa a) (Minimalism.Modification.MAGFeatureType.phi a_1) = isFalse ⋯

instance Minimalism.Modification.instDecidableEqMAGFeatureType : DecidableEq MAGFeatureType

Equations

• Minimalism.Modification.instDecidableEqMAGFeatureType = Minimalism.Modification.instDecidableEqMAGFeatureType.decEq

def Minimalism.Modification.instReprMAGFeatureType.repr : MAGFeatureType → Nat → Std.Format

Equations

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

instance Minimalism.Modification.instReprMAGFeatureType : Repr MAGFeatureType

Equations

• Minimalism.Modification.instReprMAGFeatureType = { reprPrec := Minimalism.Modification.instReprMAGFeatureType.repr }

structure Minimalism.Modification.AdjAgreementEntry : Type

An adjective agreement entry: which features are morphologically realized on adjectives in each syntactic position.

• predFeatures : List MAGFeatureType

  Features realized on predicative adjectives.

• attrFeatures : List MAGFeatureType

  Features realized on attributive adjectives.

• dpFeatures : List MAGFeatureType

  All φ/κ-features available in the DP of this language.

def Minimalism.Modification.instReprAdjAgreementEntry.repr : AdjAgreementEntry → Nat → Std.Format

Equations

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

instance Minimalism.Modification.instReprAdjAgreementEntry : Repr AdjAgreementEntry

Equations

• Minimalism.Modification.instReprAdjAgreementEntry = { reprPrec := Minimalism.Modification.instReprAdjAgreementEntry.repr }

def Minimalism.Modification.AdjAgreementEntry.sameAgreement (e : AdjAgreementEntry) : Bool

Derive predAttrSameAgreement from an agreement entry: true iff the attr feature list is a subset of the pred features and vice versa (same set). Simplified to list equality for decidability.

Equations

• e.sameAgreement = (e.predFeatures.length == e.attrFeatures.length && e.attrFeatures.all fun (x : Minimalism.Modification.MAGFeatureType) => e.predFeatures.contains x)

def Minimalism.Modification.AdjAgreementEntry.phiKappaComplete (e : AdjAgreementEntry) : Bool

Derive agreementPhiKappaComplete from an agreement entry: true iff every DP feature appears on the attributive adjective.

Equations

• e.phiKappaComplete = e.dpFeatures.all fun (x : Minimalism.Modification.MAGFeatureType) => e.attrFeatures.contains x