Vocabulary Insertion from the inside out

Vocabulary Insertion targets the morphemes of a complex head, once each, from the inside out. At each morpheme the context an item sees is the complex head as it then stands: the inner morphemes realized, with their features and the morphophonological features of their exponents, and the outer ones still bare. Which morphemes count as context is a locality regime, either 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 insertion rewrites the morpheme as its exponent and they are gone. The root is a morpheme whose exponent is present from the start, and insertion targets the heads above it.

Main definitions

• DistributedMorphology.ComplexHead.order, DistributedMorphology.ComplexHead.exponents: the positions of a complex head of morphemes in linear order, and its surface exponents.
• DistributedMorphology.ComplexHead.Locality, DistributedMorphology.ComplexHead.Discharge: the two regimes of context and the two fates of features.
• DistributedMorphology.ComplexHead.contextAt, DistributedMorphology.ComplexHead.insertAt, DistributedMorphology.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.
• visible_insertUpTo_rewriting: under rewriting, a realized morpheme keeps no features, so inward-looking conditioning sees exponents only.
• 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.
• nth_contextAt_hierarchical, nth_contextAt_hierarchical_root: under hierarchy, head j stands at offset j - i from head i and the root at -(i + 1).

References

• [Emb15]
• [EN07]
• [Bob00]
• [Hal97a]

Linearization

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

The positions of the complex head in linear order respect No Tangling, with prefixal morphemes outermost first, then the root (none), then 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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

The context of a morpheme undergoing insertion is either 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 ⋯

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

Equations

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

@[instance_reducible]

instance DistributedMorphology.ComplexHead.instReprLocality : Repr Locality

Equations

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

inductive DistributedMorphology.ComplexHead.Discharge : Type

Insertion either leaves a morpheme's features in place or rewrites the morpheme as its exponent, deleting them.

• nondeletion : Discharge

  Features survive insertion.

• rewriting : Discharge

  The morpheme'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

A morpheme presents as context its own features 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, since 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme F E)) (isNull : E → Prop) [DecidablePred isNull] (i : ℕ) : Option (Morpheme F E) × Option (Morpheme F E)

The concatenated neighbors of head i are the nearest unpruned morphemes on its inner and outer sides, 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 (Morpheme F E) (Morpheme F E)) (isNull : E → Prop) [DecidablePred isNull] (loc : Locality) (expFeatures : E → List F) (i : ℕ) : Neighborhood (List F)

Head i presents its features in focus to Vocabulary Insertion, with inner context on the left and outer on the right, nearest first. Under concatenation the context is the unpruned neighbors, under hierarchy the neighborhood of head i in the complex head read from the root outward.

Equations

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

theorem DistributedMorphology.ComplexHead.nth_contextAt_hierarchical {F : Type u_1} {E : Type u_2} (w : ComplexHead (Morpheme F E) (Morpheme F E)) (isNull : E → Prop) [DecidablePred isNull] {expFeatures : E → List F} {i j : ℕ} (hi : i ≤ w.heads.length) (hj : j ≠ i) : (w.contextAt isNull Locality.hierarchical expFeatures i).nth (↑j - ↑i) = (List.map (visible expFeatures) w.heads).getD j []

Under hierarchy, context is by distance, head j standing at offset j - i from head i.

theorem DistributedMorphology.ComplexHead.nth_contextAt_hierarchical_root {F : Type u_1} {E : Type u_2} (w : ComplexHead (Morpheme F E) (Morpheme F E)) (isNull : E → Prop) [DecidablePred isNull] {expFeatures : E → List F} {i : ℕ} (hi : i ≤ w.heads.length) : (w.contextAt isNull Locality.hierarchical expFeatures i).nth (-(↑i + 1)) = visible expFeatures w.root

Under hierarchy, the root stands at offset -(i + 1) from head i.

Insertion

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

Vocabulary Insertion at head i substitutes the Subset Principle's winner for Q, once only; under rewriting it deletes the morpheme's features.

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 (Morpheme F E) (Morpheme F E)) (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] (vocab : List (VocabularyItem F E)) (loc : Locality) (expFeatures : E → List F) (dis : Discharge) (n : ℕ) : ComplexHead (Morpheme F E) (Morpheme F E)

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

Equations

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

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

Vocabulary Insertion from the inside out reaches 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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

Insertion applies once, leaving a realized morpheme alone.

theorem DistributedMorphology.ComplexHead.getElem?_heads_insertAt_of_ne {F : Type u_1} {E : Type u_2} {w : ComplexHead (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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, so 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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

Rewriting

theorem DistributedMorphology.ComplexHead.feats_insertAt_rewriting {F : Type u_1} {E : Type u_2} {w : ComplexHead (Morpheme F E) (Morpheme F E)} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} (h : ∀ s ∈ w.heads, s.IsRealized → s.feats = []) (i : ℕ) (s : Morpheme F E) : s ∈ (w.insertAt isNull vocab loc expFeatures Discharge.rewriting i).heads → s.IsRealized → s.feats = []

Under rewriting, insertion leaves no features on the morpheme it realizes.

theorem DistributedMorphology.ComplexHead.feats_insertUpTo_rewriting {F : Type u_1} {E : Type u_2} {w : ComplexHead (Morpheme F E) (Morpheme F E)} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} (hw : ∀ s ∈ w.heads, s.exp = none) (n : ℕ) (s : Morpheme F E) : s ∈ (w.insertUpTo isNull vocab loc expFeatures Discharge.rewriting n).heads → s.IsRealized → s.feats = []

theorem DistributedMorphology.ComplexHead.visible_insertUpTo_rewriting {F : Type u_1} {E : Type u_2} {w : ComplexHead (Morpheme F E) (Morpheme F E)} (isNull : E → Prop) [DecidablePred isNull] [DecidableEq F] {vocab : List (VocabularyItem F E)} {loc : Locality} {expFeatures : E → List F} (hw : ∀ s ∈ w.heads, s.exp = none) (n : ℕ) {s : Morpheme F E} (hs : s ∈ (w.insertUpTo isNull vocab loc expFeatures Discharge.rewriting n).heads) {e : E} (he : s.exp = some e) : visible expFeatures s = expFeatures e

Under rewriting, inside-out insertion from bare morphemes replaces each morpheme it realizes by its exponent, so an inner morpheme presents its exponent's features alone.

theorem DistributedMorphology.ComplexHead.length_heads_insertUpTo {F : Type u_1} {E : Type u_2} {w : ComplexHead (Morpheme F E) (Morpheme 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 (Morpheme F E) (Morpheme 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