Docs / Morphology / Exponence / Containment / Selection

Containment hierarchies: Elsewhere insertion and Superset spellout

import Linglib.Morphology.Exponence.Containment.Selection · namespace Morphology.Containment

This file defines the realization of a rule set over a containment hierarchy under each reading as the shared core's score selection. Elsewhere insertion selects the applicable rule of greatest threshold, the most specific; Superset spellout selects the matching entry of least span, Minimize Junk. Both realize Elsewhere winners. Elsewhere insertion is the chain instance of feature-decomposition exponence, reading a rule as the initial segment of grades up to its threshold.

Main definitions

realize: Elsewhere insertion.
spellout: Superset spellout.
SpanRule.toDecomposition: a rule as a feature-decomposition rule over initial segments.

Main results

realize_realizes, spellout_realizes: both realize the exponent of an Elsewhere winner.
realize_eq_of_threshold_le: the rule selected at a grade is realized at every lower grade it applies at.
spellout_eq_none_of_le: spellout gaps propagate upward.
spellout_eq_some_of_filter_of_le: the loss of entries extends a form downward only.
pattern_toDecomposition: Elsewhere insertion is decomposition exponence over the chain.

References

Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized
Bubnov 2026, Not all coexpressions are syncretisms: Limiting Nanosyntax formalized
Caha 2009, The Nanosyntax of Case formalized
Dekier 2021, Morphosyntax of specific and non-specific indefinite markers formalized
Halle 1997, Distributed Morphology: Impoverishment and Fission

Elsewhere insertion

Elsewhere insertion realizes at each grade the exponent of the applicable rule of greatest threshold, the most specific, the first listed on ties, and none where no rule applies.

@[reducible, inline] abbrev realize L53–56

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Paradigm n (Option F)

realize v = v.realize SpanRule.threshold

Used by realize_realizes, realize_eq_of_threshold_le, pattern_toDecomposition

Used in Morphology/Exponence/Containment/Contiguity, Bobaljik2012, Graf2019, SmithMoskalEtAl2019

theorem realize_realizes L62–63

{n : ℕ} {F : Type u_1} {g : Fin n} {φ : F} {v : Exponence.RuleSet (SpanRule n F)} (h : realize v g = some φ) :

v.Realizes Exponence.applySet g φ

Built from

The rule selected at a grade is realized at every lower grade its threshold reaches, so Elsewhere insertion plateaus between thresholds.

theorem realize_eq_of_threshold_le L65–70

{n : ℕ} {F : Type u_1} {g g' : Fin n} {v : Exponence.RuleSet (SpanRule n F)} {it : SpanRule n F} (h : v.selectBy SpanRule.threshold g' = some it) (hit : it.threshold ≤ g) (hg : g ≤ g') :

realize v g = realize v g'

Built from

Superset spellout

Superset spellout realizes at each grade the exponent of the matching entry storing the least structure, the first listed on ties, and none where no entry matches.

@[reducible, inline] abbrev spellout L76–79

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SupersetRule n F)) :

Paradigm n (Option F)

spellout v = v.realize fun (e : SupersetRule n F) => OrderDual.toDual e.spans

Used by spellout_realizes, spellout_eq_none_of_le, spellout_eq_of_le_spans, spellout_eq_some_of_filter_of_le

Used in Morphology/Exponence/Containment/Contiguity, Morphology/Nanosyntax/Lexicalization, Morphology/Nanosyntax/TreeSpellout, Bobaljik2012, Bubnov2026 and 1 more

theorem spellout_realizes L85–87

{n : ℕ} {F : Type u_1} {g : Fin n} {φ : F} {v : Exponence.RuleSet (SupersetRule n F)} (h : spellout v g = some φ) :

v.Realizes Exponence.applySet g φ

Built from

Spellout gaps propagate upward, since an entry matching a higher grade matches the lower one too, Dekier 2021's paradigm-gap monotonicity for indefinites.

theorem spellout_eq_none_of_le L89–93

{n : ℕ} {F : Type u_1} {g g' : Fin n} {v : Exponence.RuleSet (SupersetRule n F)} (h : spellout v g = none) (hg : g ≤ g') :

spellout v g' = none

Built from

L95–98

The loss of entries extends a form downward only. If an antihomophonous lexicon spells out a form at a grade and, after losing entries, still spells it out at a higher grade, it spelled it out there before (Bubnov 2026).

theorem spellout_eq_some_of_filter_of_le L100–109

{n : ℕ} {F : Type u_1} {g g' : Fin n} {φ : F} {v : Exponence.RuleSet (SupersetRule n F)} (hv : v.Antihomophonous) {p : SupersetRule n F → Bool} (h : spellout v g = some φ) (h' : spellout (List.filter p v) g' = some φ) (hg : g ≤ g') :

spellout v g' = some φ

Built from

The chain decomposition

Feature-decomposition exponence (Exponence/Decomposition.lean) over the decomposition of each grade into the initial segment below it: a rule specified for the grades up to its threshold applies where its threshold does, and feature counting maximizes the threshold.

A rule as a feature-decomposition rule specified for the grades up to its threshold.

def SpanRule.toDecomposition L119–121

{n : ℕ} {F : Type u_1} (it : SpanRule n F) :

Decomposition.Rule (Fin n) Finset.Iic F

it.toDecomposition = { feats := Finset.Iic it.threshold, exponent := it.exponent }

Used by pattern_toDecomposition

Elsewhere insertion is feature-decomposition exponence over the chain of initial segments.

theorem pattern_toDecomposition L123–130

{n : ℕ} {F : Type u_1} (v : Exponence.RuleSet (SpanRule n F)) :

Decomposition.pattern (List.map SpanRule.toDecomposition v) = realize v

Built from ,