Containment hierarchies: realization patterns and contiguity

[Bob12] [Cah09] [Gra19]

A containment hierarchy is a graded sequence of morphosyntactic structures, each properly containing the last: degree (positive ⊂ comparative ⊂ superlative, [Bob12]), case (NOM ⊂ ACC ⊂ GEN ⊂ DAT, [Cah09]), path roles ([Pan11]). A Pattern n F records which form occupies each grade's cell, and the cross-linguistic *ABA generalization says a form never recurs across a distinct intervening form: each form's fiber is order-convex (IsContiguous). [Gra19] reconstructs *ABA across these domains as feasible monotonicity: the form assignment is monotone with respect to some linear order on the output forms (his def. (6); the base hierarchy is what is fixed). Over a linear hierarchy, that is equivalent to the assignment being the kernel of a monotone score (FeasiblyMonotone) — isContiguous_iff_feasiblyMonotone, stated here as the general theorem behind Graf's instance-by-instance verification, independently of any insertion mechanism.

Main declarations

• Pattern n F — assignment of forms to the n grades of a hierarchy
• IsContiguous — no ABA configuration: fibers are convex
• FeasiblyMonotone, isContiguous_iff_feasiblyMonotone — [Gra19]'s monotonicity reconstruction of *ABA
• IsContiguous.comp_monotone, isContiguous_comp_left — composition API

Theory-laden derivations of contiguity (vocabulary insertion under the Elsewhere Condition) live in Morphology/Containment/Vocabulary.lean; the n = 3 degree and n = 4 case specializations in Morphology/DegreeContainment.lean and Morphology/Case/Allomorphy.lean.

@[reducible, inline]

abbrev Morphology.Containment.Pattern (n : ℕ) (F : Type u_2) : Type u_2

A realization pattern over an n-grade containment hierarchy: the form occupying each grade's cell.

Equations

• Morphology.Containment.Pattern n F = (Fin n → F)

def Morphology.Containment.IsContiguous {n : ℕ} {F : Type u_1} (p : Pattern n F) : Prop

A pattern is contiguous when no form recurs across a distinct intervening form: if the cells at i ≤ k agree, every cell between them agrees too, so each form's fiber is an interval of grades. ABA (![a, b, a]) violates this; AAA, ABB, ABC — and AAB — satisfy it. (*AAB is excluded by vocabulary-level conditions, not by contiguity; see Morphology/Containment/Vocabulary.lean.)

Equations

• Morphology.Containment.IsContiguous p = ∀ ⦃i j k : Fin n⦄, i ≤ j → j ≤ k → p i = p k → p i = p j

@[implicit_reducible]

instance Morphology.Containment.instDecidableIsContiguousOfDecidableEq {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Pattern n F) : Decidable (IsContiguous p)

Equations

• Morphology.Containment.instDecidableIsContiguousOfDecidableEq p = Morphology.Containment.instDecidableIsContiguousOfDecidableEq._aux_1 p

theorem Morphology.Containment.IsContiguous.comp_monotone {n : ℕ} {F : Type u_1} {m : ℕ} {p : Pattern n F} (hp : IsContiguous p) {f : Fin m → Fin n} (hf : Monotone f) : IsContiguous (p ∘ f)

Precomposition with a monotone regrading preserves contiguity.

theorem Morphology.Containment.isContiguous_comp_left {n : ℕ} {F : Type u_1} {β : Type u_2} [PartialOrder β] {g : Fin n → β} (hg : Monotone g) {h : β → F} (hh : Set.InjOn h (Set.range g)) : IsContiguous (h ∘ g)

A pattern that factors as a monotone score followed by a map injective on the score's range is contiguous.

Graf's monotonicity reconstruction

[Gra19] recasts the *ABA generalization — across adjectival gradation, person-pronoun syncretism, case syncretism, and noun stem allomorphy — as feasible monotonicity of the form assignment from a fixed base hierarchy ([BS18] is the feature-combinatoric counterpart, deriving which cell arrangements exclude ABA without stipulating containment). The kernel formulation below is this file's gloss: forms are bins, so feasible monotonicity over a linear hierarchy is the existence of a monotone score with the pattern's kernel. The prefix-image score i ↦ #{forms among cells 0..i} is monotone and has the same kernel as a contiguous pattern, and conversely any pattern sharing its kernel with a monotone score has convex fibers. (Graf's case hierarchies are partial orders going beyond this linear setting, and his PCC/GCC treatment is a different object — monotone maps into the fixed two-element truth-value algebra, i.e. upper sets; see Studies/Graf2019.lean.)

def Morphology.Containment.FeasiblyMonotone {n : ℕ} {F : Type u_1} (p : Pattern n F) : Prop

Feasible monotonicity ([Gra19] def. (6)), in monotone-score form: some monotone score identifies exactly the cells the pattern identifies. Equivalent to Graf's literal statement — monotone with respect to some linear order on the output forms — over a finite hierarchy, since forms are bins and only the kernel matters.

Equations

• Morphology.Containment.FeasiblyMonotone p = ∃ (g : Fin n → ℕ), Monotone g ∧ ∀ (i j : Fin n), p i = p j ↔ g i = g j

theorem Morphology.Containment.isContiguous_iff_feasiblyMonotone {n : ℕ} {F : Type u_1} (p : Pattern n F) : IsContiguous p ↔ FeasiblyMonotone p

*[Gra19]'s monotonicity reconstruction of ABA: a pattern is contiguous iff it is feasibly monotonic. Forward direction via the prefix-image score; backward direction is the sandwich argument that makes monotone kernels convex.