Synthetic and analytic realization: Merger over a containment hierarchy

[Bob12] ch. 3 treats the synthetic/analytic distinction as structural: a grade is realized synthetically when Merger has bundled its heads into the root's complex word, periphrastically otherwise. MergerStep models one application of Merger — adjoin a head to the merged region, skipping no intervening head (part of Marantz's definition; equivalently, successive-cyclic head movement) — and the book's generalizations are theorems about the reachable regions:

• Initial segments (mergerReachable_iff_exists_region): the regions reachable from the bare root are exactly the initial segments of the hierarchy, coordinatized by Synthesis.wordTop.
• SSG (MergerReachable.mem_of_le, Synthesis.syntheticAt_of_le): no morphological superlative without a morphological comparative — merged regions are downward closed in heads, so synthesis is downward closed in grades. No language has long – more long – longest.
• RSG (min_lt_wordTop_of_realizeIn_ne, specialized as rsg): root suppletion is limited to synthetic comparatives. Items can only be conditioned by word-internal structure (realizeIn), so distinct root forms at two grades force Merger past their lower grade — no *good – more bett.

The merged region also induces a two-block domain partition of the grades (Synthesis.domainPartition) — [Bob12]'s structural adjacency as one source of Morphology/DM/DomainLocality.lean's domain-relativized contiguity, alongside the accessibility-domain refinements of [Mos15a] and [SMX+19].

Main declarations

• MergerStep, MergerReachable — Merger as successive-cyclic head bundling; the reachable merged regions
• Synthesis n — how far up the hierarchy the lexeme's word extends
• realizeIn — realization seeing only word-internal structure
• MergerReachable.mem_of_le, Synthesis.syntheticAt_of_le (SSG), min_lt_wordTop_of_realizeIn_ne (RSG), isContiguous_realizeIn, Synthesis.domainPartition

Merger as successive-cyclic head bundling

def Morphology.DM.MergerStep {n : ℕ} [NeZero n] (R S : Finset (Fin n)) : Prop

One application of Merger: adjoin head h to the merged region R. The side condition that every head strictly between the root and h is already merged is [Bob12]'s "Merger cannot skip intervening heads" (part of Marantz's definition of Morphological Merger; equivalently, successive-cyclic head movement).

Equations

• Morphology.DM.MergerStep R S = ∃ (h : Fin n), 0 < h ∧ h ∉ R ∧ (∀ (k : Fin n), 0 < k → k < h → k ∈ R) ∧ S = insert h R

def Morphology.DM.MergerReachable {n : ℕ} [NeZero n] (R : Finset (Fin n)) : Prop

The merged regions reachable from the bare root (empty region) by successive applications of Merger.

Equations

• Morphology.DM.MergerReachable R = Relation.ReflTransGen Morphology.DM.MergerStep ∅ R

theorem Morphology.DM.mergerReachable_Ioc {n : ℕ} [NeZero n] (t : Fin n) : MergerReachable (Finset.Ioc 0 t)

theorem Morphology.DM.mergerReachable_iff {n : ℕ} [NeZero n] {R : Finset (Fin n)} : MergerReachable R ↔ ∃ (t : Fin n), R = Finset.Ioc 0 t

The regions reachable by successive Merger are exactly the initial segments of the hierarchy: the no-skipping condition forces every head below a merged head to be merged.

theorem Morphology.DM.MergerReachable.mem_of_le {n : ℕ} [NeZero n] {R : Finset (Fin n)} (hR : MergerReachable R) {h k : Fin n} (hk0 : 0 < k) (hkh : k ≤ h) (hh : h ∈ R) : k ∈ R

SSG core ([Bob12] ch. 3): merged regions are downward closed in heads — if the superlative head has merged, so has the comparative head below it.

The synthetic extent

structure Morphology.DM.Synthesis (n : ℕ) : Type

The synthetic extent of a lexeme's paradigm: heads 1..wordTop are realized word-internally with the root (Merger applied); grades above wordTop are periphrastic. wordTop coordinatizes the merged region: by mergerReachable_iff_exists_region, the regions successive-cyclic Merger can build are exactly those of this form.

• wordTop : Fin n

  The highest head merged into the root's word.

def Morphology.DM.instDecidableEqSynthesis.decEq {n✝ : ℕ} (x✝ x✝¹ : Synthesis n✝) : Decidable (x✝ = x✝¹)

Equations

• Morphology.DM.instDecidableEqSynthesis.decEq { wordTop := a } { wordTop := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.DM.instDecidableEqSynthesis {n✝ : ℕ} : DecidableEq (Synthesis n✝)

Equations

• Morphology.DM.instDecidableEqSynthesis = Morphology.DM.instDecidableEqSynthesis.decEq

def Morphology.DM.instReprSynthesis.repr {n✝ : ℕ} : Synthesis n✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprSynthesis {n✝ : ℕ} : Repr (Synthesis n✝)

Equations

• Morphology.DM.instReprSynthesis = { reprPrec := Morphology.DM.instReprSynthesis.repr }

def Morphology.DM.Synthesis.region {n : ℕ} [NeZero n] (s : Synthesis n) : Finset (Fin n)

The merged region of the lexeme's word: heads 1..wordTop.

Equations

• s.region = Finset.Ioc 0 s.wordTop

theorem Morphology.DM.mergerReachable_iff_exists_region {n : ℕ} [NeZero n] {R : Finset (Fin n)} : MergerReachable R ↔ ∃ (s : Synthesis n), R = s.region

Merged regions and synthetic extents are in coordinatizing correspondence: a region is Merger-reachable iff it is s.region for some Synthesis s.

theorem Morphology.DM.Synthesis.mergerReachable_region {n : ℕ} [NeZero n] (s : Synthesis n) : MergerReachable s.region

def Morphology.DM.Synthesis.SyntheticAt {n : ℕ} (s : Synthesis n) (g : Fin n) : Prop

Grade g is realized synthetically: all its heads are word-internal.

Equations

• s.SyntheticAt g = (g ≤ s.wordTop)

@[implicit_reducible]

instance Morphology.DM.instDecidableSyntheticAt {n : ℕ} (s : Synthesis n) (g : Fin n) : Decidable (s.SyntheticAt g)

Equations

• Morphology.DM.instDecidableSyntheticAt s g = Morphology.DM.instDecidableSyntheticAt._aux_1 s g

theorem Morphology.DM.Synthesis.syntheticAt_iff_region {n : ℕ} [NeZero n] {s : Synthesis n} {g : Fin n} : s.SyntheticAt g ↔ Finset.Ioc 0 g ⊆ s.region

Syntheticity is containment of the grade's heads in the merged region.

theorem Morphology.DM.Synthesis.syntheticAt_of_le {n : ℕ} {s : Synthesis n} {g g' : Fin n} (h : s.SyntheticAt g) (h' : g' ≤ g) : s.SyntheticAt g'

SSG ([Bob12] ch. 3): synthesis is downward closed — a synthetic superlative entails a synthetic comparative. The grade-level shadow of MergerReachable.mem_of_le.

Word-internal realization

def Morphology.DM.realizeIn {n : ℕ} {F : Type u_1} (s : Synthesis n) (v : List (Containment.SpanRule n F)) : Paradigm n (Option F)

Realization restricted to word-internal structure: at grade g, rules see only the merged region — suppletion cannot be conditioned by periphrastic material outside the word ([Bob12]'s locality condition (90) applied through Merger). Models the comparative-embedding periphrasis type (Greek, the book's (107a–b)); the positive-embedding type (Russian, (107c–d)) needs a per-grade embedding choice rather than a single wordTop.

Equations

• Morphology.DM.realizeIn s v g = Morphology.Containment.realize v (min g s.wordTop)

theorem Morphology.DM.realizeIn_eq_realize_of_le {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (Containment.SpanRule n F)} {g : Fin n} (h : g ≤ s.wordTop) : realizeIn s v g = Containment.realize v g

At a synthetic grade, word-internal realization is realization.

theorem Morphology.DM.realizeIn_eq_realize_wordTop_of_le {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (Containment.SpanRule n F)} {g : Fin n} (h : s.wordTop ≤ g) : realizeIn s v g = Containment.realize v s.wordTop

At a periphrastic grade, the root word realizes as at wordTop — the highest grade whose structure is word-internal.

theorem Morphology.DM.isContiguous_realizeIn {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (Containment.SpanRule n F)} (hAH : Containment.Antihomophonous v) : IsContiguous (realizeIn s v)

Word-internal realization is still contiguous: realizeIn is realize precomposed with the monotone regrading min · wordTop.

theorem Morphology.DM.realizeIn_const_of_wordTop_eq_zero {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (Containment.SpanRule n F)} (h : ↑s.wordTop = 0) (g g' : Fin n) : realizeIn s v g = realizeIn s v g'

A lexeme with no Merger at all (wordTop = 0, fully periphrastic paradigm) realizes the same root form at every grade.

theorem Morphology.DM.min_lt_wordTop_of_realizeIn_ne {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (Containment.SpanRule n F)} {g g' : Fin n} (h : realizeIn s v g ≠ realizeIn s v g') : min g g' < s.wordTop

RSG, general form ([Bob12] ch. 3): distinct root forms at two grades force Merger past their lower grade — root suppletion at a grade requires that grade's word to be synthetic. Contrapositively: above wordTop the word realizes constantly ( realizeIn_eq_realize_wordTop_of_le).

theorem Morphology.DM.rsg {F : Type u_1} {s : Synthesis 3} {v : List (Containment.SpanRule 3 F)} {g g' : Fin 3} (h : realizeIn s v g ≠ realizeIn s v g') : s.SyntheticAt 1

RSG ([Bob12] ch. 3): root suppletion is limited to synthetic comparatives — a lexeme showing distinct root forms at two grades has undergone Merger at least once, so its comparative is synthetic. Excludes *good – more bett.

The induced domain partition

def Morphology.DM.Synthesis.domainPartition {n : ℕ} (s : Synthesis n) : DomainLocality.DomainPartition n Bool

The two-block domain partition induced by Merger: word-internal grades vs periphrastic ones — [Bob12]'s structural adjacency as a source of domain partitions for Morphology/DM/DomainLocality.lean.

Equations

• s.domainPartition g = decide (s.SyntheticAt g)

theorem Morphology.DM.Synthesis.sameDomain_domainPartition_iff {n : ℕ} {s : Synthesis n} {i j : Fin n} : DomainLocality.SameDomain s.domainPartition i j ↔ (s.SyntheticAt i ↔ s.SyntheticAt j)