Roots

The Root terminal of Distributed Morphology: List 1's acategorial atom, individuated by an arbitrary index and carrying no form or meaning — form arrives at Vocabulary Insertion, meaning at alloseme selection. Root is a tagged copy of ℕ (Root.equivNat), so the root inventory is unbounded (Infinite Root): List 1 is an open class, in contrast with the closed categorizer inventory (card_categorizer).

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• H. Harley, On the identity of roots

structure DistributedMorphology.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. It receives its form at Vocabulary Insertion. A different object from the comparative-concept root of Morphology/Root/Basic.lean, which is a contentful morph.

• index : ℕ

  The individuating index.

theorem DistributedMorphology.Root.ext_iff {x y : Root} : x = y ↔ x.index = y.index

theorem DistributedMorphology.Root.ext {x y : Root} (index : x.index = y.index) : x = y

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

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqRoot : DecidableEq Root

Equations

• DistributedMorphology.instDecidableEqRoot = DistributedMorphology.instDecidableEqRoot.decEq

def DistributedMorphology.instReprRoot.repr : Root → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprRoot : Repr Root

Equations

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

def DistributedMorphology.Root.equivNat : Root ≃ ℕ

Roots are their indices and nothing more.

Equations

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

instance DistributedMorphology.instInfiniteRoot : Infinite Root

The root inventory is unbounded: List 1 is an open class.