Synthetic and analytic realization: Merger over a containment hierarchy

[Bob12]

[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. Because Merger cannot skip intervening heads (part of Marantz's definition; equivalently, successive-cyclic head movement), the merged region is an initial segment of the hierarchy — recorded here as Synthesis.wordTop. Two of the book's generalizations then fall out:

• SSG (Synthesis.syntheticAt_of_le): no morphological superlative without a morphological comparative — synthesis is downward closed. The empirical content lives in the modeling choice (merged region = initial segment); the theorem is its one-line consequence.
• RSG (rsg): root suppletion is limited to synthetic comparatives. Items can only be conditioned by word-internal structure, so a lexeme whose comparative is periphrastic (wordTop = 0) realizes the same root form at every grade (realizeIn_const_of_wordTop_eq_zero) — no *good – more bett.

Main declarations

• Synthesis n — how far up the hierarchy the lexeme's word extends
• realizeIn — realization seeing only word-internal structure
• Synthesis.syntheticAt_of_le (SSG), rsg, isContiguous_realizeIn

structure Morphology.Containment.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. That the merged region is an initial segment encodes [Bob12]'s "Merger cannot skip intervening heads".

• wordTop : Fin n

  The highest head merged into the root's word.

@[implicit_reducible]

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

Equations

• Morphology.Containment.instDecidableEqSynthesis = Morphology.Containment.instDecidableEqSynthesis.decEq

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

def Morphology.Containment.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.Containment.instDecidableSyntheticAt {n : ℕ} (s : Synthesis n) (g : Fin n) : Decidable (s.SyntheticAt g)

Equations

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

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

SSG core ([Bob12] ch. 3): synthesis is downward closed — a synthetic superlative entails a synthetic comparative. No language has long – more long – longest.

def Morphology.Containment.realizeIn {n : ℕ} {F : Type u_1} (s : Synthesis n) (v : List (ExponenceRule n F)) : Pattern 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.Containment.realizeIn s v g = Morphology.Containment.realize v (min g s.wordTop)

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

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

theorem Morphology.Containment.realizeIn_const_of_wordTop_eq_zero {n : ℕ} {F : Type u_1} {s : Synthesis n} {v : List (ExponenceRule 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.Containment.rsg {F : Type u_1} {s : Synthesis 3} {v : List (ExponenceRule 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. Contrapositively: a lexeme showing distinct root forms at two grades must have undergone Merger at least once — its comparative is synthetic. Excludes *good – more bett.