Distributed Morphology

Distributed Morphology builds words in the syntax and supplies their forms late. The syntax combines abstract morphemes: roots, which have no category, and functional morphemes, bundles of features, among them the categorizers n, v and a with one of which every root combines. Head movement and the operations after syntax gather a root and the heads above it into a complex head, and Vocabulary Insertion realizes its terminals, choosing among Vocabulary Items by the Subset Principle.

This file defines those objects. A complex head ComplexHead R H is a root of type R with the heads of type H adjoined above it, innermost first. Taking R to be Root, an index with no form, follows the view that roots are inserted late like every other morpheme; taking it to be a Morpheme whose exponent is already supplied follows the view that a root brings its phonology into the syntax.

Main definitions

• DistributedMorphology.Root: a root, individuated by an index alone.
• DistributedMorphology.Categorizer: the categorizers n, v and a.
• DistributedMorphology.Morpheme: a terminal at PF, its features with the exponent Vocabulary Insertion substitutes for its variable Q.
• DistributedMorphology.ComplexHead: a root with the heads adjoined above it.
• DistributedMorphology.ComplexHead.word: the complex head after some steps of Merger.
• DistributedMorphology.ComplexHead.surface: the linear order of a complex head.

Main statements

• DistributedMorphology.ComplexHead.surface_eq: the Mirror Principle.

Implementation notes

The operations on complex heads are in their own files: Vocabulary Items and the Subset Principle in VocabularyInsertion/Basic.lean, insertion from the inside out in VocabularyInsertion/InsideOut.lean, the contexts rules read in Neighborhood.lean, the locality of allomorphy and allosemy within words in Locality.lean and across phrases in PhrasalLocality.lean, the configurations in which a Root is categorized and the diagnostics that can tell them apart in RootCategorization.lean, the rules that change terminals before insertion in Impoverishment.lean, Fission.lean, Fusion.lean and Spellout.lean, gender on n in Gender.lean, and contextual meaning in Allosemy.lean.

References

• [HM93]
• [Har14b]
• [Emb15]
• [Bak85]
• [KBC+26]

Roots and categorizers

structure DistributedMorphology.Root : Type

A root is individuated by an arbitrary index alone, with deliberately no form or meaning, and 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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqRoot : DecidableEq Root

Equations

• DistributedMorphology.instDecidableEqRoot = DistributedMorphology.instDecidableEqRoot.decEq

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.instReprRoot : Repr Root

Equations

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

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

Equations

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

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, an open class.

inductive DistributedMorphology.Categorizer : Type

The categorizing heads, which merge with a root that has no category.

• 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

There are exactly three categorizers, unlike the infinitely many roots.

Morphemes

structure DistributedMorphology.Morpheme (F : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A morpheme at PF carries its features, the value of its Q variable (none before Vocabulary Insertion, the exponent after), and the side on which it is linearized.

• feats : List F

  The synsem and diacritic features.

• exp : Option E

  The Q variable is none until an exponent is substituted for it.

• side : Morphology.Morph.Side

  The side of its host the morpheme is linearized on.

@[instance_reducible]

instance DistributedMorphology.instDecidableEqMorpheme {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] : DecidableEq (Morpheme F✝ E✝)

Equations

• DistributedMorphology.instDecidableEqMorpheme = DistributedMorphology.instDecidableEqMorpheme.decEq

def DistributedMorphology.instDecidableEqMorpheme.decEq {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] (x✝ x✝¹ : Morpheme F✝ E✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprMorpheme {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : Repr (Morpheme F✝ E✝)

Equations

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

def DistributedMorphology.instReprMorpheme.repr {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : Morpheme F✝ E✝ → ℕ → Std.Format

Equations

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

def DistributedMorphology.Morpheme.IsRealized {F : Type u_1} {E : Type u_2} (s : Morpheme F E) : Prop

The morpheme has been realized.

Equations

• s.IsRealized = (s.exp.isSome = true)

@[instance_reducible]

instance DistributedMorphology.Morpheme.instDecidableIsRealized {F : Type u_1} {E : Type u_2} (s : Morpheme F E) : Decidable s.IsRealized

Equations

• s.instDecidableIsRealized = DistributedMorphology.Morpheme.instDecidableIsRealized._aux_1 s

def DistributedMorphology.Morpheme.realize {F : Type u_1} {E : Type u_2} (s : Morpheme F E) (e : E) : Morpheme F E

Substitute the exponent for Q.

Equations

• s.realize e = { feats := s.feats, exp := some e, side := s.side }

Complex heads

structure DistributedMorphology.ComplexHead (R : Type u_1) (H : Type u_2) : Type (max u_1 u_2)

A complex head is a root with the heads adjoined above it, innermost first.

• root : R

  The root.

• heads : List H

  The heads above the root, innermost first.

@[instance_reducible]

instance DistributedMorphology.instDecidableEqComplexHead {R✝ : Type u_1} {H✝ : Type u_2} [DecidableEq R✝] [DecidableEq H✝] : DecidableEq (ComplexHead R✝ H✝)

Equations

• DistributedMorphology.instDecidableEqComplexHead = DistributedMorphology.instDecidableEqComplexHead.decEq

def DistributedMorphology.instDecidableEqComplexHead.decEq {R✝ : Type u_1} {H✝ : Type u_2} [DecidableEq R✝] [DecidableEq H✝] (x✝ x✝¹ : ComplexHead R✝ H✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprComplexHead {R✝ : Type u_1} {H✝ : Type u_2} [Repr R✝] [Repr H✝] : Repr (ComplexHead R✝ H✝)

Equations

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

def DistributedMorphology.instReprComplexHead.repr {R✝ : Type u_1} {H✝ : Type u_2} [Repr R✝] [Repr H✝] : ComplexHead R✝ H✝ → ℕ → Std.Format

Equations

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

def DistributedMorphology.ComplexHead.word {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (k : ℕ) : ComplexHead R H

The complex head after k steps of Merger, the root with the first k heads. The remaining heads are realized periphrastically.

Equations

• s.word k = { root := s.root, heads := List.take k s.heads }

theorem DistributedMorphology.ComplexHead.heads_word_isPrefix {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (k : ℕ) : (s.word k).heads <+: s.heads

theorem DistributedMorphology.ComplexHead.mem_word_of_le {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) {k : ℕ} {i j : Fin s.heads.length} (hji : j ≤ i) (hi : ↑i < k) : ↑j < k

Merger skips no head, so a head in the word brings every head below it.

def DistributedMorphology.ComplexHead.toTree {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (side : H → Morphology.Morph.Side) : Morphology.Word.Tree (R ⊕ H)

The word tree, each head attached on the side its exponent takes, innermost first.

Equations

• s.toTree side = Morphology.Word.Tree.attachAll (Sum.inl s.root) (List.map (fun (h : H) => (side h, Sum.inr h)) s.heads)

def DistributedMorphology.ComplexHead.surface {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (side : H → Morphology.Morph.Side) : List (R ⊕ H)

The surface order of root and heads.

Equations

• s.surface side = (s.toTree side).toList

theorem DistributedMorphology.ComplexHead.surface_eq {R : Type u_1} {H : Type u_2} (s : ComplexHead R H) (side : H → Morphology.Morph.Side) : s.surface side = (List.map Sum.inr (List.filter (fun (h : H) => decide (side h = Morphology.Morph.Side.before)) s.heads)).reverse ++ Sum.inl s.root :: List.map Sum.inr (List.filter (fun (h : H) => decide (side h = Morphology.Morph.Side.after)) s.heads)

The Mirror Principle. The surface is the prefixal heads outermost first, the root, and the suffixal heads innermost first, so on each side the surface order outward from the root is the order of merger.