Docs / Morphology / DistributedMorphology / LateInsertion

Late insertion

import Linglib.Morphology.DistributedMorphology.LateInsertion · namespace DistributedMorphology

The syntax hands PF a spell-out domain: the pronounced terminals of a linearized syntactic object, left to right, each read as a feature bundle (SpelloutDomain.ofLinearized). The postsyntactic pipeline then runs on it and Vocabulary Insertion realizes each surviving position in its neighborhood: late insertion, on which no phonological content travels through the syntax. Early insertion is the degenerate case: over the vocabulary whose items each spell out one terminal's own token as its lexically listed form, the empty-module pipeline returns exactly the carrier's pfPhon, so terminals carrying their forms compute what one context-free item per token computes, and contextual allomorphy is precisely what such a vocabulary cannot state.

Main definitions

DistributedMorphology.SpelloutDomain.ofLinearized: the handover.
DistributedMorphology.earlyItems, DistributedMorphology.earlySpellout: one context-free item per token, spelling out its lexically listed form, and the pipeline it drives.

Main results

DistributedMorphology.pf_earlySpellout: the early pipeline realizes each token's listed form.
DistributedMorphology.pfPhon_eq_earlyInsertion: pfPhon is the early-insertion pipeline.

References

Halle & Marantz 1993, Distributed Morphology and the pieces of inflection formalized
Embick & Noyer 2001, Movement Operations after Syntax

Declarations

The spell-out domain of a linearized syntactic object: its pronounced terminals, left to right, each read as a feature bundle.

def SpelloutDomain.ofLinearized L48–52

{Bundle : Type u_1} (feats : Minimalist.LexicalItem.Token → Bundle) (t : Minimalist.LinearizedSyntacticObject) :

SpelloutDomain Bundle

SpelloutDomain.ofLinearized feats t = List.map feats (Minimalist.pfYield t)

Used by pfPhon_eq_earlyInsertion

Used in Akkus2026

Early insertion

The early-insertion vocabulary over the tokens toks: each token its own atomic feature, spelled out as its lexically listed form.

def earlyItems L56–60

(toks : List Minimalist.LexicalItem.Token) :

Morphology.Exponence.RuleSet (VocabularyItem Minimalist.LexicalItem.Token String)

earlyItems toks = List.map (fun (tok : Minimalist.LexicalItem.Token) => VocabularyItem.ofFeatures {tok} tok.item.phonForm) toks

Used by applicable_earlyItems

Early insertion: no postsyntactic modules, each position realizing the Subset Principle's exponent for the early vocabulary.

def earlySpellout L62–66

(toks : List Minimalist.LexicalItem.Token) :

Spellout (Finset Minimalist.LexicalItem.Token) String

The definition is too large to print here; read it in the source.

Used by pf_earlySpellout, pfPhon_eq_earlyInsertion

Used in Akkus2026

L68–80

The early pipeline realizes, at each position, the token's lexically listed form.

theorem pf_earlySpellout L82–95

{toks : List Minimalist.LexicalItem.Token} (hnd : toks.Nodup) :

(earlySpellout toks).pf (List.map (fun (x : Minimalist.LexicalItem.Token) => {x}) toks) = List.map (fun (tok : Minimalist.LexicalItem.Token) => [tok.item.phonForm]) toks

Built from

pfPhon is the early-insertion pipeline: handing the pronounced terminals over as atomic features and inserting each token's lexically listed form returns the carrier's own pronunciation, silent tokens dropped.

theorem pfPhon_eq_earlyInsertion L97–111

(t : Minimalist.LinearizedSyntacticObject) :

Minimalist.pfPhon t = List.filter (fun (x : String) => decide (x ≠ "")) ((earlySpellout (Minimalist.pfYield t)).pf (SpelloutDomain.ofLinearized (fun (x : Minimalist.LexicalItem.Token) => {x}) t)).flatten

Built from ,