Root realizations: indices realized in context

import Linglib.Morphology.Realization · namespace Morphology

A realization assigns to an index r and a context c the finite set realize r c of forms that realize r in c. The index is opaque, and the frameworks that separate an item from its form choose it differently: a root of Distributed Morphology, given its form at Vocabulary Insertion; one of Borer's roots, a phonological index whose form its categorial context selects, as grow and growth; a lexeme of Paradigm Function Morphology, realized at a cell; Spencer's lexemic index. An empty set says that r is not licensed in c, and a set of two forms is an overabundant cell. An interpreted realization adds a second contextual map, to readings, which is Marantz's separation of the forms of List 2 from the meanings of List 3.

A homomorphism of realizations merges indices and translates contexts so that realization is preserved. The strict homomorphisms of interpreted realizations translate contexts independently of the index and preserve readings too, so the indices they merge have the same forms and readings in every context, and passing to these profiles, Interpreted.reduce, merges as much as any strict homomorphism can. The disputes over individuation, such as fat roots against sister roots, are mergers at the lax tier, which include forms and readings rather than preserving them.

Main definitions

Morphology.Realization: indices realized in context, with IsLicensed, Realizes, exponents, IsTotal, IsUnivalent and IsCrossCategorial.
Morphology.IsConstantIn, Morphology.IsVariantIn: constancy and variance of a contextual map at an index, which give IsInvariant and IsSuppletive for forms and IsIntrinsic and IsAllosemous for readings.
Morphology.Realization.Hom, Morphology.Realization.Interpreted.Hom, Morphology.Realization.Interpreted.LaxHom: mergers of indices, the strict ones preserving readings.
Morphology.Realization.comp: realization through an intermediate inventory.
Morphology.Realization.Interpreted.reduce: the realization on profiles.

Main statements

Morphology.Realization.isSuppletive_iff: form variance at an index is overabundance in one cell or suppletion across cells.
Morphology.Realization.Interpreted.Hom.profileEq_of_onRoot_eq: indices that a strict homomorphism merges have the same profile.

Implementation notes

Sign-based lexicalism, Construction Morphology and Haspelmath's morph-based comparative root are rival ontologies that the parameters of a realization measure, not instances of it. The interface does not say whether indices are listed or constructed.
A strict homomorphism cannot consult the index when it translates contexts, so categorial information has to sit in the context, which quietly encodes the Categorization Assumption.
Extensional profiles underdetermine individuation. The criteria the literature uses, such as locality of first categorization, are further structure on admissible mergers that studies supply.

References

Harley 2014, On the Identity of Roots formalized
Marantz 1997, No escape from syntax: Don’t try morphological analysis in the privacy of your own lexicon
Embick 2021, The Motivation for Roots in Distributed Morphology formalized
Borer 2013, Structuring Sense: Volume III: Taking Form formalized
Stump 2001, Inflectional Morphology: A Theory of Paradigm Structure
Bonami & Stump 2016, Paradigm Function Morphology formalized
Spencer 2013, Lexical Relatedness: A Paradigm-Based Model
Beard 1995, Lexeme-Morpheme Base Morphology: A General Theory of Inflection and Word Formation
Haspelmath 2025b, Roots and Root Classes in Comparative Grammar formalized
Lohndal 2020, Syntactic Categorization of Roots
Blevins 2016, Word and Paradigm Morphology
Arad 2005, Roots and Patterns: Hebrew Morpho-syntax formalized
Gouskova & Bobaljik 2020, Allomorphy and Vocabulary Insertion
Corbett 2007, Canonical typology, suppletion, and possible words
Stump 2016, Inflectional Paradigms: Content and Form at the Syntax-Morphology Interface formalized

Declarations

IsConstantIn g r says all values of the contextual map g at the index r coincide across all contexts.

def IsConstantIn L86–89

{R : Type u_1} {Ctx : Type u_2} {X : Type u_5} (g : R → Ctx → Finset X) (r : R) :

Prop

IsConstantIn g r = ∀ ⦃c c' : Ctx⦄, ∀ x ∈ g r c, ∀ x' ∈ g r c', x = x'

Used by not_isConstantIn_of_isVariantIn, isConstantIn_iff_not_isVariantIn, isConstantIn_iff_subsingleton, Realization.IsInvariant, Realization.Interpreted.IsIntrinsic

IsVariantIn g r says two distinct values of the contextual map g arise at the index r.

def IsVariantIn L91–94

{R : Type u_1} {Ctx : Type u_2} {X : Type u_5} (g : R → Ctx → Finset X) (r : R) :

Prop

IsVariantIn g r = ∃ (c : Ctx) (c' : Ctx), ∃ x ∈ g r c, ∃ x' ∈ g r c', x ≠ x'

Used by not_isConstantIn_of_isVariantIn, isConstantIn_iff_not_isVariantIn, Realization.IsSuppletive, Realization.Interpreted.IsAllosemous

L96–99

L101–103

L105–111

A root realization realizes an opaque index type in context. The fiber realize r c is empty where r is unlicensed and non-singleton at an overabundant cell.

structure Realization L113–120

(R : Type u_6) (Ctx : Type u_7) (F : Type u_8) :

Type (max (max u_6 u_7) u_8)

realize : R → Ctx → Finset F
realize r c is the set of forms realizing the index r in the context c, computed by Vocabulary Insertion (DM), the paradigm function (PFM) or spellout (nanosyntax).

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Inflection, Morphology/Paradigm/Basic, Morphology/Paradigm/Linkage, Bloomfield1933 and 2 more

r is licensed in c when some realization of it exists there.

def Realization.IsLicensed L126–127

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) (c : Ctx) :

Prop

S.IsLicensed r c = (S.realize r c).Nonempty

Built from

Used by Realization.IsCrossCategorial, Realization.instDecidableIsLicensed, Realization.Hom.isLicensed

Used in Arad2005

f realizes r in some context.

def Realization.Realizes L129–130

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) (f : F) :

Prop

S.Realizes r f = ∃ (c : Ctx), f ∈ S.realize r c

Built from

Used by Realization.exponents, Realization.mem_exponents, Realization.instDecidableRealizes, Realization.Hom.realizes

exponents r is the allomorph set of the root r.

def Realization.exponents L132–133

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) :

Set F

S.exponents r = {f : F | S.Realizes r f}

Built from ,

Used by Realization.mem_exponents, Realization.isInvariant_iff_subsingleton_exponents

L135–136

IsTotal says every index is licensed everywhere, PFM's stratum.

def Realization.IsTotal L138–139

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) :

Prop

S.IsTotal = ∀ (r : R) (c : Ctx), (S.realize r c).Nonempty

Built from

Used by Realization.instDecidableIsTotal, Realization.comp_isTotal

Used in Morphology/Inflection, Morphology/Paradigm/Basic, Morphology/Paradigm/Linkage, Stump2012

IsUnivalent says every cell has at most one form, the stratum of Option-shaped engine outputs.

def Realization.IsUnivalent L141–143

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) :

Prop

S.IsUnivalent = ∀ (r : R) (c : Ctx), (S.realize r c).card ≤ 1

Built from

Used by Realization.instDecidableIsUnivalent

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Inflection, Morphology/Paradigm/Basic, Morphology/Paradigm/Linkage

IsInvariant r says r has one form wherever it is licensed, the classical context-free morpheme as the degenerate case.

def Realization.IsInvariant L145–147

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) :

Prop

S.IsInvariant r = IsConstantIn S.realize r

Built from ,

Used by Realization.not_isInvariant_of_isSuppletive, Realization.isInvariant_iff_subsingleton_exponents, Realization.isClassDetermined_range_const_iff, Realization.instDecidableIsInvariant

Used in Morphology/Inflection, Morphology/Paradigm/Linkage, Bloomfield1933

IsSuppletive r says r has two distinct forms, in contexts that need not differ, as √GO has go and went, the case behind Harley 2014's argument that indices, not forms, individuate. When the forms are competing Vocabulary Items this is suppletive allomorphy, of a root or of an affix alike (Gouskova & Bobaljik 2020); when they are stems it is variance in Corbett 2007's lexical material, which is suppletion in Stump 2016's sense where no inflection class determines it (IsClassDetermined).

def Realization.IsSuppletive L149–156

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) :

Prop

S.IsSuppletive r = IsVariantIn S.realize r

Built from ,

Used by Realization.not_isInvariant_of_isSuppletive, Realization.isSuppletive_iff, Realization.instDecidableIsSuppletive

Used in Morphology/DistributedMorphology/VocabularyInsertion/Basic, Morphology/Inflection, Morphology/Paradigm/Linkage, Bloomfield1933, Stump2006 and 1 more

Form variance at an index decomposes into overabundance or suppletion proper.

theorem Realization.isSuppletive_iff L178–196

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r : R} :

S.IsSuppletive r ↔ S.IsOverabundant r ∨ S.IsProperlySuppletive r

Built from , , ,

L198–200

L202–203

r is cross-categorial when it is licensed in two contexts whose categories k differ, as a category-free root is (Marantz 1997, Arad 2005).

def Realization.IsCrossCategorial L205–208

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {K : Type u_6} (k : Ctx → K) (r : R) :

Prop

S.IsCrossCategorial k r = ∃ (c : Ctx) (c' : Ctx), k c ≠ k c' ∧ S.IsLicensed r c ∧ S.IsLicensed r c'

Built from ,

Used by Realization.instDecidableIsCrossCategorialOfDecidableEq

Used in Arad2005

The pipeline composition S.comp T realizes through an intermediate inventory, the Kleisli composition of Finset over a shared context. Late-insertion architectures factor the grammar's realization as such a composite; PFM's stem-choice-then-blocks cascade is another.

def Realization.comp L299–305

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {G : Type u_6} [DecidableEq G] (S : Realization R Ctx F) (T : Realization F Ctx G) :

Realization R Ctx G

S.comp T = { realize := fun (r : R) (c : Ctx) => (S.realize r c).biUnion fun (f : F) => T.realize f c }

Built from

Used by Realization.comp_isTotal

L307–313

A hom is an index merger that tracks spellout, in which onRoot may merge indices and onCtx translates contexts and may consult the source index. It is the transport tier; individuation disputes are adjudicated with Realization.Interpreted.Hom, whose root-independent context translation blocks re-encoding the source index in the target context.

structure Realization.Hom L319–331

{F : Type u_3} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Realization R₁ C₁ F) (T : Realization R₂ C₂ F) :

Type (max (max (max u_6 u_7) u_8) u_9)

onRoot : R₁ → R₂
onRoot translates indices, and its non-injectivity is individuation coarsening.
onCtx : R₁ → C₁ → C₂
onCtx translates contexts.
realize_eq (r : R₁) (c : C₁) : S.realize r c = T.realize (self.onRoot r) (self.onCtx r c)
Realization is preserved.

Built from

Used by Realization.Hom.id, Realization.Hom.comp, Realization.Hom.isLicensed, Realization.Hom.realizes, Realization.Interpreted.Hom.toRealizationHom

IsIntrinsic r says r has one meaning in every context, the lexicalist degenerate case.

def Realization.Interpreted.IsIntrinsic L379–381

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) (r : R) :

Prop

S.IsIntrinsic r = IsConstantIn S.interp r

Built from ,

Used by Realization.Interpreted.not_isIntrinsic_of_isAllosemous, Realization.Interpreted.instDecidableIsIntrinsicOfFintypeOfDecidableEq

IsAllosemous r says r has two distinct meanings, DM allosemy, the failure of intrinsic meaning.

def Realization.Interpreted.IsAllosemous L383–385

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) (r : R) :

Prop

S.IsAllosemous r = IsVariantIn S.interp r

Built from ,

Used by Realization.Interpreted.not_isIntrinsic_of_isAllosemous, Realization.Interpreted.instDecidableIsAllosemousOfFintypeOfDecidableEq

Used in Morphology/DistributedMorphology/Allosemy, Arad2005

L387–389

L391–393

L395–398

A strict hom, the tier on which individuation disputes are stated, translates contexts independently of the root, so that the target context cannot re-encode the source index, and preserves interpretation alongside spellout.

structure Realization.Interpreted.Hom L404–416

{F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Interpreted R₁ C₁ F M) (T : Interpreted R₂ C₂ F M) :

Type (max (max (max u_6 u_7) u_8) u_9)

onRoot : R₁ → R₂
onRoot translates indices.
onCtx : C₁ → C₂
onCtx translates contexts independently of the root.
realize_eq (r : R₁) (c : C₁) : S.realize r c = T.realize (self.onRoot r) (self.onCtx c)
Realization is preserved.
interp_eq (r : R₁) (c : C₁) : S.interp r c = T.interp (self.onRoot r) (self.onCtx c)
Interpretation is preserved.

Built from

Used by Realization.Interpreted.Hom.toRealizationHom, Realization.Interpreted.Hom.interp_eq_of_onRoot_eq, Realization.Interpreted.Hom.realize_eq_of_onRoot_eq, Realization.Interpreted.Hom.toLaxHom, Realization.Interpreted.reduceHom, Realization.Interpreted.Hom.profileEq_of_onRoot_eq

L418–421

L423–427

L429–433

At the lax tier, a hom includes realization and interpretation rather than matching them. Where a strict Hom merger asserts identity, a lax merger asserts subsumption, so that each source index's forms and readings are among its image's, as when a lexeme's listed properties are among its root's Encyclopedia entry (Arad 2005). Pattern-bound lexemes lax-merge into a total root without ever strict-merging.

structure Realization.Interpreted.LaxHom L435–449

{F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Interpreted R₁ C₁ F M) (T : Interpreted R₂ C₂ F M) :

Type (max (max (max u_6 u_7) u_8) u_9)

onRoot : R₁ → R₂
onRoot translates indices.
onCtx : C₁ → C₂
onCtx translates contexts independently of the root.
realize_sub (r : R₁) (c : C₁) : S.realize r c ⊆ T.realize (self.onRoot r) (self.onCtx c)
Realizations are included.
interp_sub (r : R₁) (c : C₁) : S.interp r c ⊆ T.interp (self.onRoot r) (self.onCtx c)
Interpretations are included.

Built from

Used by Realization.Interpreted.Hom.toLaxHom, Realization.Interpreted.LaxHom.comp

The reduced presentation takes its indices to be realization-and-interpretation profiles. Every system presents its reduction; the strict hom tier is change of presentation, and only the lax tier merges beyond profiles.

def Realization.Interpreted.reduce L486–492

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) :

Interpreted (Quotient S.profileSetoid) Ctx F M

S.reduce = { realize := Quotient.lift S.realize ⋯, interp := Quotient.lift S.interp ⋯ }

Built from ,

Used by Realization.Interpreted.reduceHom

L494–496

Mergers along any strict hom refine profile equality, so reduce merges as much as the strict tier ever can. Mergers beyond profiles, such as the hammer carvings or pattern-bound lexemes into an Arad 2005 root, are necessarily lax.

theorem Realization.Interpreted.Hom.profileEq_of_onRoot_eq L498–506

{R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) {R₂ : Type u_6} {C₂ : Type u_7} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) {r r' : R} (h : φ.onRoot r = φ.onRoot r') :

S.ProfileEq r r'

Built from , ,