Roots in Distributed Morphology

The abstract Root: a syntactic atom individuated by an arbitrary index, with no phonological or semantic content ([Har14b] §2, [Mar97]). It is acategorial — it enters the syntax only by merging with a categorizing head (the Categorization Assumption; the categorizer inventory and RootLicense interface are DM/Categorizer.lean, whose RootIdx parameter this type instantiates) — and receives its form at Vocabulary Insertion (DM/VocabularyInsertion.lean).

This is a different object from the comparative-concept root of Morphology/Root/Basic.lean, which is a contentful morph: a DM Root is not a form but an abstract element realized by forms. Where [Has25b] treats hammer (noun) and hammer (verb) as heterosemous sister roots, DM derives both from one acategorial √ under different categorizers; that rivalry is study content, this file only fixes the object.

structure Morphology.DM.Root : Type

A Root terminal node, individuated by an arbitrary index alone — with deliberately no form or meaning fields, following [Har14b]'s answer to what roots are.

• index : Nat

  The individuating index.

@[implicit_reducible]

instance Morphology.DM.instDecidableEqRoot : DecidableEq Root

Equations

• Morphology.DM.instDecidableEqRoot = Morphology.DM.instDecidableEqRoot.decEq

def Morphology.DM.instDecidableEqRoot.decEq (x✝ x✝¹ : Root) : Decidable (x✝ = x✝¹)

Equations

• Morphology.DM.instDecidableEqRoot.decEq { index := a } { index := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Morphology.DM.instReprRoot.repr : Root → Nat → Std.Format

Equations

• Morphology.DM.instReprRoot.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "index" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.index)).group) " }"

@[implicit_reducible]

instance Morphology.DM.instReprRoot : Repr Root

Equations

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