Categorization

Word formation is syntactic: a categorizing head n, v, or a merges with an acategorial root — the categorization assumption — and layered derivation is more of the same merger, [v [n √SHELF]] for to shelve beside [n √SHELF] for shelf. Word-internal structure is a nonplanar tree over root and head leaves, the same carrier shape as syntactic and morphological objects elsewhere in the library, so the root's survival across (re)categorization and the structural difference between direct and layered derivation are facts about leaves rather than stipulations.

Main definitions

• Categorizer — the closed inventory n, v, a
• WordStructure — word-internal structure over a head alphabet: Categorizer for the bare theory, Categorizer.Head (Categorizer/Gender.lean) when heads carry φ-content
• categorize, roots, heads, Headed — head merger, the two leaf projections, and outermost headedness

Main statements

• roots_categorize — categorization does not touch root leaves: one root index across categories and layers
• categorize_ne_of_ne, categorize_categorize_ne — distinct heads build distinct structures, and layered derivation differs from direct derivation even when the outermost head agrees
• agentive_voice_is_phase — Voice, not the categorizer, bounds idiomatic interpretation

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• A. Marantz, No escape from syntax
• H. Harley, On the identity of roots
• D. Embick and A. Marantz, Architecture and blocking
• [A. Marantz, Locality domains for contextual allomorphy across the interfaces][marantz-2013]

The categorizer inventory

inductive DistributedMorphology.Categorizer : Type

A categorizing head that merges with an acategorial root to project syntactic structure. The three options correspond to the functional heads n, v, a in Distributed Morphology ([Mar97], [Har14b] §2).

• n : Categorizer
• v : Categorizer
• a : Categorizer

@[instance_reducible]

instance DistributedMorphology.instDecidableEqCategorizer : DecidableEq Categorizer

Equations

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

def DistributedMorphology.instReprCategorizer.repr : Categorizer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprCategorizer : Repr Categorizer

Equations

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

@[instance_reducible]

instance DistributedMorphology.instFintypeCategorizer : Fintype Categorizer

Equations

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

theorem DistributedMorphology.card_categorizer : Fintype.card Categorizer = 3

The categorizer inventory is closed: unlike the open class of roots (Infinite Root), the functional heads are exactly n, v, a.

def DistributedMorphology.Categorizer.toCategory : Categorizer → Minimalist.Cat

The syntactic category of a categorizer.

Equations

• DistributedMorphology.Categorizer.n.toCategory = Minimalist.Cat.N
• DistributedMorphology.Categorizer.v.toCategory = Minimalist.Cat.V
• DistributedMorphology.Categorizer.a.toCategory = Minimalist.Cat.A

Word-internal structure

Distributed Morphology builds words with the same binary structure building as sentences ([HM93]): a categorized root is the configuration [x √], not a kind of object, and re-categorization is merger of a further head. The carrier is a nonplanar tree whose leaves are acategorial roots or categorizing heads and whose internal vertices are bare.

@[reducible, inline]

abbrev DistributedMorphology.WordStructure (H : Type u_1) : Type u_1

Word-internal syntactic structure over head labels H: a nonplanar tree whose leaves are acategorial roots or heads and whose internal vertices are bare.

Equations

• DistributedMorphology.WordStructure H = RoseTree.Nonplanar ((DistributedMorphology.Root ⊕ H) ⊕ Unit)

def DistributedMorphology.ofRoot {H : Type u_1} (r : Root) : WordStructure H

The structure consisting of a bare root.

Equations

• DistributedMorphology.ofRoot r = RoseTree.Nonplanar.leaf (Sum.inl (Sum.inl r))

def DistributedMorphology.ofHead {H : Type u_1} (h : H) : WordStructure H

The structure consisting of a bare head.

Equations

• DistributedMorphology.ofHead h = RoseTree.Nonplanar.leaf (Sum.inl (Sum.inr h))

noncomputable def DistributedMorphology.categorize {H : Type u_1} (h : H) (T : WordStructure H) : WordStructure H

Merge a categorizing head with a structure: the configuration [h T]. Categorization is categorize h (ofRoot r); re-categorization is another categorize on top — to shelve is categorize .v (categorize .n (ofRoot shelf)) — and every further derivation (happi-ness a → n, boy-ish n → a) is simply another instance, with no inventory of re-categorization types to extend.

Equations

• DistributedMorphology.categorize h T = RoseTree.Nonplanar.node (Sum.inr ()) (DistributedMorphology.ofHead h ::ₘ {T})

def DistributedMorphology.roots {H : Type u_1} (T : WordStructure H) : Multiset Root

The root leaves: the List-1 content of a word structure.

Equations

• DistributedMorphology.roots T = Multiset.filterMap (fun (x : (DistributedMorphology.Root ⊕ H) ⊕ Unit) => x.getLeft?.bind Sum.getLeft?) (RoseTree.Nonplanar.leaves T)

def DistributedMorphology.heads {H : Type u_1} (T : WordStructure H) : Multiset H

The head leaves: the functional content of a word structure.

Equations

• DistributedMorphology.heads T = Multiset.filterMap (fun (x : (DistributedMorphology.Root ⊕ H) ⊕ Unit) => x.getLeft?.bind Sum.getRight?) (RoseTree.Nonplanar.leaves T)

@[simp]

theorem DistributedMorphology.roots_ofRoot {H : Type u_1} (r : Root) : roots (ofRoot r) = {r}

@[simp]

theorem DistributedMorphology.roots_ofHead {H : Type u_1} (h : H) : roots (ofHead h) = 0

@[simp]

theorem DistributedMorphology.heads_ofHead {H : Type u_1} (h : H) : heads (ofHead h) = {h}

@[simp]

theorem DistributedMorphology.heads_ofRoot {H : Type u_1} (r : Root) : heads (ofRoot r) = 0

theorem DistributedMorphology.roots_categorize {H : Type u_1} (h : H) (T : WordStructure H) : roots (categorize h T) = roots T

Categorization does not touch root leaves: the same root index survives categorization and re-categorization — √HAMMER is one root across hammer and to hammer ([Har14b] §2, §4) — and with it every piece of root-level lexical content. C-selection is therefore untouched by the categorizer ([Har14b] §3: one-replacement, verb-object idioms, ergative splits), in contrast with l-selection, which varies with the functional structure (Hewett2026).

theorem DistributedMorphology.heads_categorize {H : Type u_1} (h : H) (T : WordStructure H) : heads (categorize h T) = h ::ₘ heads T

Each categorization contributes exactly its head.

theorem DistributedMorphology.numLeaves_categorize {H : Type u_1} (h : H) (T : WordStructure H) : RoseTree.Nonplanar.numLeaves (categorize h T) = RoseTree.Nonplanar.numLeaves T + 1

Each categorization adds one leaf.

inductive DistributedMorphology.Headed {H : Type u_1} : WordStructure H → H → Prop

Outermost headedness: the structure is the head itself, or was built by merging it last.

• ofHead {H : Type u_1} (h : H) : Headed (DistributedMorphology.ofHead h) h
• categorize {H : Type u_1} (h : H) (T : WordStructure H) : Headed (DistributedMorphology.categorize h T) h

theorem DistributedMorphology.categorize_ne_of_ne {H : Type u_1} {h h' : H} (hne : h ≠ h') (T : WordStructure H) : categorize h T ≠ categorize h' T

Same base, different categorizer, different structure: √HAMMER under n (hammer) and under v (to hammer) are distinct objects ([Mar97], [Har14b] §2).

theorem DistributedMorphology.categorize_categorize_ne {H : Type u_1} (h₁ h₂ h₃ : H) (T : WordStructure H) : categorize h₁ (categorize h₂ T) ≠ categorize h₃ T

Layered derivation is structurally distinct from direct derivation even when the outermost head agrees: [v [n √SHELF]] (to shelve) is not [v √SHELF], though both are Headed by v — the ambiguity a bare category label hides ([Har14b] §2, §4).

VoiceP as the idiom boundary

[Har14b] §4: multiply derived words carry idiosyncratic senses above the first categorizer ((36) editor-ial, classifi-eds, national-ize), while the external argument that Voice introduces stays compositional. This is the idiom domain (Spine.IdiomLocal, Locality.lean); the choice of a root's alloseme is bounded separately, by the cyclic categorizers ([marantz-2013]; Spine.RootLocal).

theorem DistributedMorphology.agentive_voice_is_phase : Minimalist.Voice.agentive.IsPhasal

Agentive Voice is a phase head — the boundary above which idiomatic interpretation is unavailable. [Har14b] §4: "Voice is the phase head, not v"; the categorizer inventory here accordingly carries no phasal structure of its own, so the idiom domain extends past n, v, a and closes only at Voice.

theorem DistributedMorphology.voice_introduces_external_arg : Minimalist.Voice.agentive.HasD ∧ Minimalist.Voice.agentive.AssignsTheta

Voice introduces the external argument ([Har14b] §4, following [Kra96]). The categorizer does NOT introduce arguments — complement selection is a root property ([Har14b] §3).