Complex heads and Vocabulary Insertion from the inside out

A morpheme at PF is a bundle of features together with a variable Q that Vocabulary Insertion substitutes with a phonological exponent, the features persisting; a root carries its form from the start. The complex head that successive adjunction builds — the M-Word, its terminals the morphemes — is the root with the morphemes above it, innermost first, each linearized on one side, so that linearization respects No Tangling: prefixes outermost first, the root, then suffixes innermost first. Vocabulary Insertion targets morphemes only, once each, and proceeds from the inside out; at each morpheme the context an item sees is the complex head as it then stands, the inner morphemes realized — their features and the morphophonological features of their exponents — and the outer ones still bare. Which morphemes count as context is a locality regime: the concatenated neighbors after null exponents are pruned, or every morpheme by hierarchical distance. What insertion does to a morpheme's features is a second parameter: they persist, or the item's features are rewritten away.

Main definitions

• Morpheme, ComplexHead: the morpheme with its Q variable, and the complex head.
• ComplexHead.order, ComplexHead.exponents: linearization and the surface exponents.
• Locality, Discharge: the two regimes and the two fates of features.
• ComplexHead.contextAt, ComplexHead.insertAt, ComplexHead.insertAll: the context a morpheme presents, insertion at one morpheme, and insertion from the inside out.

Main results

• insertAt_of_isRealized, exp_insertAll_of_eq_some: Uniqueness — a realized morpheme is never realized again.
• feats_insertAll_nondeletion: under non-deletion, features survive insertion.
• exp_insertUpTo_of_le, visible_of_exp_none: inside-out insertion leaves the outer morphemes bare, so outward-looking conditioning sees features only.
• length_heads_insertAll: insertion adds no morpheme.

References

• [D. Embick, The morpheme: A theoretical introduction][embick-2015]
• D. Embick and R. Noyer, Distributed Morphology and the syntax/morphology interface
• J. D. Bobaljik, The ins and outs of contextual allomorphy
• M. Halle, Distributed Morphology: Impoverishment and Fission

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

A morpheme at PF: 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: none until an exponent is substituted for it.

• side : Morphology.Morph.Side

  The side of its host the morpheme is linearized on.

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.instDecidableEqMorpheme {F✝ : Type u_1} {E✝ : Type u_2} [DecidableEq F✝] [DecidableEq E✝] : DecidableEq (Morpheme F✝ E✝)

Equations

• DistributedMorphology.instDecidableEqMorpheme = DistributedMorphology.instDecidableEqMorpheme.decEq

@[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.

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

The complex head: the root, whose form is present from the start, and the morphemes adjoined above it, innermost first.

• root : Morpheme F E

  The root, with its underlying form.

• heads : List (Morpheme F E)

  The morphemes above the root, innermost first.

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

Equations

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

@[instance_reducible]

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

Equations

• DistributedMorphology.instDecidableEqComplexHead = DistributedMorphology.instDecidableEqComplexHead.decEq

@[instance_reducible]

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

Equations

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

def DistributedMorphology.instReprComplexHead.repr {F✝ : Type u_1} {E✝ : Type u_2} [Repr F✝] [Repr E✝] : ComplexHead 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 }

Linearization

def DistributedMorphology.ComplexHead.order {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) : List (Option ℕ)

The positions of the complex head in linear order, respecting No Tangling: prefixal morphemes outermost first, the root (none), suffixal morphemes innermost first.

Equations

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

def DistributedMorphology.ComplexHead.at? {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) : Option ℕ → Option (Morpheme F E)

The morpheme at a position.

Equations

• w.at? none = some w.root
• w.at? (some i) = w.heads[i]?

def DistributedMorphology.ComplexHead.exponents {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) : List E

The surface exponents, in linear order.

Equations

• w.exponents = List.filterMap (fun (p : Option ℕ) => (w.at? p).bind fun (x : DistributedMorphology.Morpheme F E) => x.exp) w.order

Context

inductive DistributedMorphology.ComplexHead.Locality : Type

Which morphemes stand as context to a morpheme undergoing insertion: its concatenated neighbors, null exponents pruned; or every morpheme of the complex head by hierarchical distance, inner and outer.

• concatenation : Locality

  The concatenated neighbors, with null exponents pruned.

• hierarchical : Locality

  Every morpheme, by hierarchical distance.

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instDecidableEqLocality : DecidableEq Locality

Equations

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

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instReprLocality : Repr Locality

Equations

• DistributedMorphology.ComplexHead.instReprLocality = { reprPrec := DistributedMorphology.ComplexHead.instReprLocality.repr }

def DistributedMorphology.ComplexHead.instReprLocality.repr : Locality → ℕ → Std.Format

Equations

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

inductive DistributedMorphology.ComplexHead.Discharge : Type

What insertion does to a morpheme's features: they persist, or the inserted item's features are rewritten away.

• nondeletion : Discharge

  Features survive insertion.

• rewriting : Discharge

  The item's features are deleted on insertion.

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instDecidableEqDischarge : DecidableEq Discharge

Equations

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

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instReprDischarge : Repr Discharge

Equations

• DistributedMorphology.ComplexHead.instReprDischarge = { reprPrec := DistributedMorphology.ComplexHead.instReprDischarge.repr }

def DistributedMorphology.ComplexHead.instReprDischarge.repr : Discharge → ℕ → Std.Format

Equations

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

def DistributedMorphology.ComplexHead.visible {F : Type u_1} {E : Type u_2} (expFeatures : E → List F) (s : Morpheme F E) : List F

The features a morpheme presents as context: its own, and — once realized — the morphophonological features of its exponent.

Equations

• DistributedMorphology.ComplexHead.visible expFeatures s = s.feats ++ (Option.map expFeatures s.exp).getD []

@[simp]

theorem DistributedMorphology.ComplexHead.visible_of_exp_none {F : Type u_1} {E : Type u_2} {expFeatures : E → List F} {s : Morpheme F E} (h : s.exp = none) : visible expFeatures s = s.feats

A bare morpheme presents its features only: nothing of an exponent is visible before insertion.

def DistributedMorphology.ComplexHead.Pruned {F : Type u_1} {E : Type u_2} (isNull : E → Prop) (s : Morpheme F E) : Prop

A realized morpheme whose exponent is null is pruned from concatenation.

Equations

• DistributedMorphology.ComplexHead.Pruned isNull s = ∃ (e : E), s.exp = some e ∧ isNull e

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instDecidablePrunedOfDecidablePred {F : Type u_1} {E : Type u_2} (isNull : E → Prop) [DecidablePred isNull] (s : Morpheme F E) : Decidable (Pruned isNull s)

Equations

• DistributedMorphology.ComplexHead.instDecidablePrunedOfDecidablePred isNull s = match h : s.exp with | none => isFalse ⋯ | some e => decidable_of_iff (isNull e) ⋯

def DistributedMorphology.ComplexHead.concat {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] : List (Option ℕ)

The linear order with pruned morphemes removed.

Equations

• w.concat isNull = List.filter (fun (p : Option ℕ) => decide ¬∃ s ∈ w.at? p, DistributedMorphology.ComplexHead.Pruned isNull s) w.order

def DistributedMorphology.ComplexHead.neighbors {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] (i : ℕ) : Option (Morpheme F E) × Option (Morpheme F E)

The concatenated neighbors of head i: the inner side and the outer side of the position, each the nearest unpruned morpheme, if any.

Equations

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

def DistributedMorphology.ComplexHead.contextAt {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] (loc : Locality) (expFeatures : E → List F) (i : ℕ) : Neighborhood (List F)

The context head i presents to Vocabulary Insertion: its features in focus; inner context on the left, outer on the right, nearest first — under concatenation the unpruned neighbors, under hierarchy every morpheme of the complex head by distance.

Equations

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

Insertion

def DistributedMorphology.ComplexHead.insertAt {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] (vocab : List (VocabularyItem F E)) (loc : Locality) (expFeatures : E → List F) (dis : Discharge) (i : ℕ) : ComplexHead F E

Vocabulary Insertion at head i: the Subset Principle's winner is substituted for Q, once only; under rewriting its features are deleted.

Equations

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

def DistributedMorphology.ComplexHead.insertUpTo {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] (vocab : List (VocabularyItem F E)) (loc : Locality) (expFeatures : E → List F) (dis : Discharge) (n : ℕ) : ComplexHead F E

Insertion at the first n heads, from the inside out.

Equations

• w.insertUpTo isNull vocab loc expFeatures dis n = List.foldl (fun (w : DistributedMorphology.ComplexHead F E) (i : ℕ) => w.insertAt isNull vocab loc expFeatures dis i) w (List.range n)

def DistributedMorphology.ComplexHead.insertAll {F : Type u_1} {E : Type u_2} (w : ComplexHead F E) (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] (vocab : List (VocabularyItem F E)) (loc : Locality) (expFeatures : E → List F) (dis : Discharge) : ComplexHead F E

Vocabulary Insertion from the inside out: every head in turn.

Equations

• w.insertAll isNull vocab loc expFeatures dis = w.insertUpTo isNull vocab loc expFeatures dis w.heads.length

Uniqueness and terminal insertion

@[simp]

theorem DistributedMorphology.ComplexHead.insertUpTo_zero {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} : w.insertUpTo isNull vocab loc expFeatures dis 0 = w

theorem DistributedMorphology.ComplexHead.insertUpTo_succ {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (n : ℕ) : w.insertUpTo isNull vocab loc expFeatures dis (n + 1) = (w.insertUpTo isNull vocab loc expFeatures dis n).insertAt isNull vocab loc expFeatures dis n

@[simp]

theorem DistributedMorphology.ComplexHead.root_insertAt {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (i : ℕ) : (w.insertAt isNull vocab loc expFeatures dis i).root = w.root

@[simp]

theorem DistributedMorphology.ComplexHead.length_heads_insertAt {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (i : ℕ) : (w.insertAt isNull vocab loc expFeatures dis i).heads.length = w.heads.length

theorem DistributedMorphology.ComplexHead.insertAt_of_isRealized {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} {i : ℕ} {s : Morpheme F E} (hs : w.heads[i]? = some s) (h : s.IsRealized) : w.insertAt isNull vocab loc expFeatures dis i = w

A realized morpheme is left alone: insertion applies once.

theorem DistributedMorphology.ComplexHead.getElem?_heads_insertAt_of_ne {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} {i j : ℕ} (h : i ≠ j) : (w.insertAt isNull vocab loc expFeatures dis i).heads[j]? = w.heads[j]?

Insertion at one head touches no other.

theorem DistributedMorphology.ComplexHead.exp_insertAt_of_eq_some {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} {i j : ℕ} {s : Morpheme F E} {e : E} (hs : w.heads[j]? = some s) (he : s.exp = some e) : ∃ (s' : Morpheme F E), (w.insertAt isNull vocab loc expFeatures dis i).heads[j]? = some s' ∧ s'.exp = some e

A realized exponent survives insertion elsewhere and at its own head.

theorem DistributedMorphology.ComplexHead.exp_insertUpTo_of_eq_some {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (n : ℕ) {j : ℕ} {s : Morpheme F E} {e : E} (hs : w.heads[j]? = some s) (he : s.exp = some e) : ∃ (s' : Morpheme F E), (w.insertUpTo isNull vocab loc expFeatures dis n).heads[j]? = some s' ∧ s'.exp = some e

theorem DistributedMorphology.ComplexHead.exp_insertAll_of_eq_some {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} {j : ℕ} {s : Morpheme F E} {e : E} (hs : w.heads[j]? = some s) (he : s.exp = some e) : ∃ (s' : Morpheme F E), (w.insertAll isNull vocab loc expFeatures dis).heads[j]? = some s' ∧ s'.exp = some e

Uniqueness: an exponent, once substituted for Q, is never replaced.

Inside-out insertion

theorem DistributedMorphology.ComplexHead.exp_insertAt_of_lt {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} {i j : ℕ} (hij : i < j) {s : Morpheme F E} (hs : w.heads[j]? = some s) (he : s.exp = none) : ∃ (s' : Morpheme F E), (w.insertAt isNull vocab loc expFeatures dis i).heads[j]? = some s' ∧ s'.exp = none

Insertion at an inner head leaves an outer head bare.

theorem DistributedMorphology.ComplexHead.exp_insertUpTo_of_le {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (n : ℕ) {j : ℕ} (hnj : n ≤ j) {s : Morpheme F E} (hs : w.heads[j]? = some s) (he : s.exp = none) : ∃ (s' : Morpheme F E), (w.insertUpTo isNull vocab loc expFeatures dis n).heads[j]? = some s' ∧ s'.exp = none

Inside-out insertion up to n leaves every head from n on bare: when a head is reached, its outer context carries features only.

Non-deletion

theorem DistributedMorphology.ComplexHead.feats_insertAt_nondeletion {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} (i : ℕ) : List.map (fun (x : Morpheme F E) => x.feats) (w.insertAt isNull vocab loc expFeatures Discharge.nondeletion i).heads = List.map (fun (x : Morpheme F E) => x.feats) w.heads

theorem DistributedMorphology.ComplexHead.feats_insertUpTo_nondeletion {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} (n : ℕ) : List.map (fun (x : Morpheme F E) => x.feats) (w.insertUpTo isNull vocab loc expFeatures Discharge.nondeletion n).heads = List.map (fun (x : Morpheme F E) => x.feats) w.heads

Under non-deletion, features survive inside-out insertion.

theorem DistributedMorphology.ComplexHead.feats_insertAll_nondeletion {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} : List.map (fun (x : Morpheme F E) => x.feats) (w.insertAll isNull vocab loc expFeatures Discharge.nondeletion).heads = List.map (fun (x : Morpheme F E) => x.feats) w.heads

theorem DistributedMorphology.ComplexHead.length_heads_insertUpTo {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} (n : ℕ) : (w.insertUpTo isNull vocab loc expFeatures dis n).heads.length = w.heads.length

@[simp]

theorem DistributedMorphology.ComplexHead.length_heads_insertAll {F : Type u_1} {E : Type u_2} {w : ComplexHead F E} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} {dis : Discharge} : (w.insertAll isNull vocab loc expFeatures dis).heads.length = w.heads.length